ctl - NuSMV 实时 CTL

Question

我正在使用 NuSMV，并且正在尝试编写实时 CTL 属性。
我想知道是否有办法从状态设置步骤，例如：
((s.state = on) ABG (0..5 s.state = off))

读作：if (s.state=on) is true，从此状态和其他 5 个步骤的属性(s.state= off) is true。
我试图写这样的东西，但它不起作用。你能帮助我吗？

否则，是否可以从不是第一个状态开始检查相同的属性？

Answer 1

问题。写if (s.state=on) is true，从这个状态和其他 5 个步骤的属性(s.state= off) is true.

CTL。

CTLSPEC AG ((s.state = on) -> 
            ((AX s.state = off) &
             (AX AX s.state = off) &
             (AX AX AX s.state = off) &
             (AX AX AX AX s.state = off) &
             (AX AX AX AX AX s.state = off)
           ));

使用此公式，您可以测试每次命中s.state = on条件s.state = off是否在当前状态之后的至少5 个状态中都为真，而不管您的路径选择如何。

初始AG确保此属性必须在执行路径上的任何位置保持，而不仅仅是在初始状态。

实时 CTL。

来自nusmv 邮件列表：

((s.state = on) ABG (1..5 s.state = off))

---

注意： 我不清楚你的其余问题，所以如果仍有一些未回答的部分，请编辑你的问题并澄清一下。