NuSMVで階層化状態マシン

NuSMVはSPINよりもモデル化の自由度が大きくUML等で出てくる階層化状態マシンをAND状態も含めてモデル化することができる。

まず、与えられた階層化状態マシンについて二つの集合を作成する。

Τ : root stateの集合、トップ状態とAND状態の子供
Α : atomic stateの集合とAND状態

ある状態 s について v(s)は直近の親を表すとする。Tは　v(s) = s ∈ T となるような集合。

Tの要素はNuSMVの列挙型変数とする。そして、列挙型の要素 b は、

a ∈ T の時に、v(b) ∈ a　となるようなb


によって構成される。

この状態図の場合


VAR

  M: {P, Q};

  R: {UI, U2, V};

  S: {Sl, S2, S3};

となる。

次に、以下の様な、その状態にいる時真になる様なマクロを定義する。全ての状態Bについて、

inB := TRUE;          Bはルート状態

inB := inA;           BはAND状態Aの子供

inB := inA & (A = B); BはΑの要素で、Bの親はTの要素

inB := inB1 | inB2 | . . . | inBk; BはOR状態でB1, B2,.., Bkはその子供、そしてBはTの要素ではない

上の状態図では

DEFINE
inM := TRUE;
inP := inM & (M = P);
inQ := inM & (M = Q);
inR := inQ;
inS := inQ;
inU := inU1 | inU2;
inU1 := inR & (R = U1);
inU2 := inR & (R = U2);
inV := inR & (R = V);
inS1 := inS & (S = S1);
inS2 := inS & (S = S2);
inS3 := inS & (S = S3);

そして遷移条件は、たとえばSの場合は

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

の様になる。ここでT_SxはSx状態への遷移条件である。MとRについても同様のASSIGN文を定義することでAND状態を含んだ階層化状態マシンのNuSMVモデルを作ることができる。