NuSMV Realtime CTL

Question

NuSMVを使用しています。リアルタイムCTLプロパティを書き込もうとしています。この状態から、他5プロパティ(s.state= off) is trueの手順については、if (s.state=on) is true：として読み込まれ
((s.state = on) ABG (0..5 s.state = off))

：
私は次のように、状態からのステップを設定する方法があるかどうかを知りたいです。
私はこのようなことを書こうとしましたが、うまくいきません。手伝って頂けますか？

それ以外の場合は、最初でない状態から同じプロパティを確認できますか？

Answer 1

質問。この状態から、および他の5ため書き込みif (s.state=on) is trueは、プロパティ(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) 
      )); 

は、あなたは毎回あなたは関係なく、あなたのパスの選択の、現在の1以下の少なくとも5の状態のためにtrueになりますs.state = on条件s.state = offを打つことは事実であるかどうかをテストします。

最初のAGは、このプロパティが初期状態だけでなく実行パスのどこかに保持されていることを保証します。

リアルタイムCTL。 nusmvメーリングリストから

：

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

---

注：あなたの質問の残りの部分はので、いくつかの未解決の部分だけ編集がまだあるしてください場合は、私には明らかではないが、あなたの質問と少し明確にする。