我正在使用 UPPAAL 4.1.24 对一个由 1 个主进程和 3 个观察者进程组成的简单系统进行建模。主进程使用由观察者进程收听的广播频道。我已启用Options -> Diagnostic Trace -> Some.
现在，每次我通过验证程序的查询检查属性时，我都可以看到跟踪并在 Simulator 选项卡下的 Trace 框中重放它。但是，它仅适用于得到满足的属性。如果不满足查询给定的属性，则不会更新跟踪，并且我看不到该“未满足”属性的跟踪。
任何想法？
问问题
72 次