UPPAAL中的多个同步

Question

如何在UPPAAL中对多个同步进行建模？例如:状态更改会在不同的模板中同时触发另外两个状态更改。在synchronization字段中，我只能设置一个通道(sync1！或者同步！)。我如何组合sync1！还有sync2！？

谢谢

Answer 1

最简单的方法是将表示状态更改的边一分为二，并在中间引入一个提交的位置。从源位置到提交位置的第一条边应该包含从原始边开始的所有内容，但第二次同步除外。从提交位置到目标位置的第二条边应该包含第二次同步。

提交位置是为了帮助模拟这种行为而引入的虚拟位置。当一个自动机进入一个承诺的位置时，它必须立即离开它，不能有任何时间流逝，也不能与任何其他自动机交错。这还意味着，除非可以根据规则保留提交的位置，否则不会输入该位置。