0

我在 UPPAAL 模型检查工具中创建了一些自动机，它们之间有一个对话框。当其中一个发生错误时，必须重置另一个。我不能将所有节点的返回边都放到起始节点，因为我不能为所有可能的错误设置警卫。有没有办法用一个函数或类似的东西来重置自动机？我们可以不通过边去不同的节点吗？我的意思是直接从一个节点跳转到初始节点而不使用边缘。谢谢你！

4

1 回答 1

0

不。

最接近的解决方案是将自动机的状态编码到变量中，然后边变成对这些变量有保护的循环，然后可以用另一个循环边重置这些变量。

于 2018-06-28T07:34:00.810 回答