NuSMVで非決定性状態マシン

非決定性の状態遷移があると実装には落とせないので、非決定性の有無は設計検証の対象になる。しかし、要求仕様の段階では非決定性のままで検証したいこともある。たとえば、ランダムな振る舞いをする外部デバイス等を環境モデルに取り込む場合などである。

ASSIGN
  next (s) :=
    case
       T_S1 : Sl;
       T_S2 : S2;
       T_S3 : S3;
       !inS & next(inS) : S1; -- start state
       TRUE : s;
    esac;


この状態マシンで、T_S1とT_S2が同時に真になった場合、NuSMVはcase式の最初の分岐しか使わないのでS2への遷移がおこなわれなくなる。そこで

ASSIGN
  next (s) :=
    case

       T_S1 & T_S2 : {S1, S2};
       T_S1 : Sl;
       T_S2 : S2;
       T_S3 : S3;
       !inS & next(inS) : S1; -- start state
       TRUE : s;
    esac;

の様にモデル化すれば良い。しかし、この方法は、非決定性遷移の数が少なければ良いが、増えてくると組合せ的に遷移条件数も増えるてしまう欠点がある。そこで、非決定性遷移が多い場合は、ASSIGN文ではなくTRANS文を使用する。TRANS文は論理式なので評価順と言うものが無い。


TRANS
(
(T_S1 & next(inS1)) |
(T_S3 & next(inS3)) |
(T_S2 & next(inS2)) |
(!T_S1 & !T_S2 & !T_S3 & next(s)=s)
)


TRANS
(
!inS & next(inS) -> next(s)=S1 -- start state
)

設計検証ではASSIGN文、要求検証ではTRANS文が使いやすい。