Model Base

A.4.1 状態機械の定義

最終更新：2011年09月04日 23:53

modelbase

- view

管理者のみ編集可

更新日2011-09-04
[ Alloy Analyzer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題解答例 ]

状態機械は、1 つ以上の初期状態と、各状態から次状態への遷移についての関係を持つ。状態機械のAlloy モデルを構築し、制約を追加して解析器に解かせ、以下の様々な状態機械の例を生成せよ。

Wiki Pedia の有限オートマトンで紹介されている数学モデルの表現を参考にして、この問が設定する状態機械を記述してみる。

状態機械は単純であり、定義の構成要素は以下の３つのみとなる。

<S,s0,δ>

S は有限であって空でない状態の集合
s0 はSの要素でもある初期状態の集合
σ は状態遷移関数 σ: S→P(S) 　ただしP()は冪集合
(イベントの集合Σは要素が１つなので、σ: S×Σ→P(S) を σ: S→P(S)　とした)

これをAlloy語に翻訳する。

 some sig S{}
 one sig FSM{
   S0 : some S, 
   sigma: S -> S,
   }

ビジュアライザで観察しやすいように以下の関数を用意し、さらにThemeを編集して、sigmaの Show as arcs を off にしておく。

 --ビジュアライザ観察用
 fun r: S->S{ FSM.sigma }

以下、状態機械の図は、典型的なものだけスナップショットを撮った。

( a ) 決定性機械：各状態に対して次状態は高々1 つしかない

 pred A_4_1_a{
   all s: S | deterministic[s]
   }
 
 pred deterministic[s: S]{ lone s.(FSM.sigma) }
 
 run A_4_1_a

( b ) 非決定性機械：次状態が複数あるような状態が存在しうる

 pred A_4_1_b{
   not A_4_1_a
   }
   
 run A_4_1_b

( c ) 非到達な状態のある機械

 pred A_4_1_c{
   some s0: FSM.S0, s: S | not reachableFrom[s0,s]
   }
 
 pred reachableFrom[s, s': S]{ s' in s.*(FSM.sigma) }
 
 run A_4_1_c

( d ) 非到達な状態のない機械

 pred A_4_1_d{
   not A_4_1_c
   }
 
 run A_4_1_d

( e ) 強連結な機械：すべての状態が他の状態から到達可能である

 pred A_4_1_e{
   all s1,s2: S | reachableFrom[s1,s2]
   }
 
 run A_4_1_e

( f ) デッドロックのある機械：到達可能で次状態がないような状態のある機械

 pred A_4_1_f{
   some s0: FSM.S0, s: S |{
     reachableFrom[s0,s]
     no s.(FSM.sigma)
     }
   }
   
 run A_4_1_f

( g ) ライブロックのある機械：常に到達可能な状態であるにもかかわらず、その状態に決して到達しないような無限長の遷移列が存在する機械

 pred A_4_1_g{
   some s0: FSM.S0, hauntS1: S |
     some disj hauntS2, neglectedS: S |{
       -- 状態neglectedSは、常に到達可能な状態であるにもかかわらず
       reachableFrom[hauntS1, neglectedS]
       -- 状態neglectedSに決して到達しないような無限長の遷移列が存在する
       reachableFrom[s0, hauntS1] and loop[S-neglectedS, hauntS1, hauntS2]
       }
   }
 
 -- 状態集合ssに含まれない状態のみ、かつs1とs2を含む遷移の循環がある
 pred loop[ss: set S, s1,s2: S]{
   s1 = s2 
   =>{
     s1 in ss
     s1->s1 in FSM.sigma
     }
   else{
     reachableFrom[ss, s1, s2]
     reachableFrom[ss, s2, s1]
     }  
   }
 
 -- 状態集合ssに含まれない状態のみで、sからs'へ遷移可能
 pred reachableFrom[ss: set S, s, s': S]{
   s' in s.*( (ss<:FSM.sigma):>ss ) 
   }
 
 run A_4_1_g

S1で自己遷移を繰り返し続ければライブロックとなる。

S1とS2を反復し続ければライブロックとなる。

ついでに、

ライブロックのある機械は、非決定性機械である

ことを示しておく(証明にはならない)。

 check { A_4_1_g => A_4_1_b } for 8

探索に10秒以上かかるので、要素数8が辛抱の限界か、、、

Executing "Check check$8 for 8"
  Solver=minisat(jni) Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20
  5185 vars. 112 primary vars. 9176 clauses. 375ms.
  No counterexample found. Assertion may be valid. 11484ms.

反例は見つからないので、8状態以下の範囲では正しいと言える。