NuSMV を使用しており、リアルタイム CTL プロパティを書き込もうとしています。
次のように、状態からステップを設定する方法があるかどうかを知りたいです。
((s.state = on) ABG (0..5 s.state = off))
として読み取られます: if (s.state=on) is true、この状態から、および他の 5 つのステップでは、プロパティ(s.state= off) is true.
このようなことを書き込もうとしましたが、うまくいきません。手伝って頂けますか？
そうでなければ、最初ではない状態から同じプロパティをチェックすることは可能ですか?