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

---

注：你的问题的其余部分我也不清楚，所以请仍存在一些悬而未决的部分只需编辑你的问题，并澄清一点。