uppaal - UPPAAL 中的多重同步

Question

如何在 UPPAAL 中模拟多个同步？例如：状态变化在不同的模板中同时触发另外两个状态变化。在同步领域，我只能放一个通道（sync1！或sync！）。我怎样才能结合sync1！和同步2！?

谢谢

Answer 1

最简单的方法是将表示状态变化的边分成两部分，并在中间引入一个已提交的位置。从源位置到提交位置的第一个边应该包含原始边的所有内容，除了第二个同步。从提交位置到目标位置的第二条边应该包含第二次同步。

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