0

我在 UPPAAL 4.1 版本中构建了这个模板。我们可以在图 1 中看到，存在代理可以执行反射处理的单一路径，但是当我编写给定属性时

E<> 不是（MonitorAgent.ReflexProcessing）

验证者满意。

它不应该满足，因为在 ReflexProcessing 完成的地方存在一条路径。请添加您的建议。在此处输入图像描述

4

0 回答 0