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))

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