私は単純な kripke 構造を持っています。ここには 3 つの状態があり、次の遷移があります。
s1 --> s2
s2 --> s1
s1 --> s3
s3 --> s3
s1 は唯一の初期状態です。ループ s1 から s2 を一定量以上 (たとえば 2 回) 繰り返したくありません。他のトランジション システムでは、トランジションにガードを追加できます。
Q1: Kripke 構造はトランジションにガードを付けることができますか?
Q2: はいの場合、NuSmv でモデル化するにはどうすればよいですか?
ありがとう