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

---

注：你的問題的其餘部分我也不清楚，所以請仍存在一些懸而未決的部分只需編輯你的問題，並澄清一點。