model-checking - NuSMV で kripke の構造を作成するには?

Question

NuSMV で Kripke の構造を作成し、いくつかのプロパティを確認する必要があります。

誰か助けて？構造とプロパティ (LTL、CTL、および CTL*) は写真にあります。

ここに構造とプロパティがあります：

http://cl.ly/image/1x0b1v3E0P0D/Screen%20Shot%202014-10-16%20at%2016.52.34.png

Answer 1

Kripke Structure 用の、よりシンプルで一見信頼性の高い NuSMV コードを見つけました。私の質問に答えてくれたdejvuthに感謝します。コードは次のとおりです。

     MODULE main
     VAR
        state : {s0,s1,s2,s3,s4};
     ASSIGN
        init(state) := s0;
        next(state):=
             case
                 state = s0 : {s1,s2};
                 state = s1 : {s1,s2};
                 state = s2 : {s1,s2,s3};
                 state = s3 : {s1,s4};
                 state = s4 : {s4};
             esac;
     DEFINE
        p := state = s1 | state = s2 | state = s3 | state = s4;
        q := state = s1 | state = s2;
        r := state = s3;
     SPEC
       EG p;
     SPEC
       AG p;
     SPEC
       EF (AG p);