Model Base
A.4.2 状態機械の模倣関係
最終更新：
modelbase
更新日2011-10-23
[ Alloy Analyzer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題 解答例 ]
( h ) トレースを定義した状態機械のAlloy モデルを作成し、状態機械の例と関連するトレース集合をいくつか生成してみよ
モデル化の方針
まず、遷移ラベルと状態は以下のように定義する。
sig A{}
abstract sig State{}
この設問で考えさせられたのはトレースの表現であった。 設問内の定義によれば状態機械のトレースとは、
初期状態からはじまる遷移ラベルからなる有限列
ということである。 これを算出するには、状態機械がたどった遷移の履歴(これを経路と呼びたい)、 から遷移ラベルを抽出すればよい。
いま状態機械の遷移の表現を
A -> State -> State
とするなら、状態機械の経路の表現は、遷移の発生順序を表す
Int -> A -> State -> State
といったものになり、そのトレースは経路の左側の2項を抽出した
Int -> A
とすればよい、と最初は考えた。
しかしながら、後の問いで状態機械が出力するトレース集合を比較することになるのだが、 そのために状態機械の経路の集合を枚挙する必要にせまられる。 上記では経路の表現(Int -> A -> State -> State) は集合であるので、経路の集合、すなわち 集合の集合を枚挙する必要が生じるのだが、一方でAlloy語は集合の集合(2階の論理)が 記述できず、最初の考え方によるモデリングは手詰まりとなってしまった。
考えてみれば、Alloyで行う検査は有界モデル検査であり、考察対象とするトーレスも有限列である。 なので検査の範囲を、たとえば状態機械の遷移が3回発生した経路(これをサイズ3の経路と呼びたい) までを検証対象とする、割り切ったモデルを作ることにする。
そうなれば、サイズ1の経路を、
A -> State -> State
と表現し、サイズ2の経路を、
A -> State -> State -> A -> State -> State
と表現し、サイズ3の経路を、
A -> State -> State -> A -> State -> State -> A -> State -> State
と表現することにしたうえで経路の枚挙を考えれば、 それは集合の集合で表すことを避け、単に上記の3つの集合で表すことができる。
確かに、この方針でモデル化を進めることはできたのだが、次に関係のアリティ数が障害となった。
Alloy語の言語仕様として関係のアリティ数は有限であるが、その上限値は明記されていない。
だがツールの実装上どこかにリミットが引かれているはずで、実際にアリティ9で作成したモデルは
CNFへコンパイルする段階でエラーが発生した。(Alloyのバージョンは4.1.10)
Generating CNF... A type error has occurred: Translation capacity exceeded. In this scope, universe contains 28 atoms and relations of arity 9 cannot be represented. Visit http://alloy.mit.edu/ for advice on refactoring.
そこで経路の表現のアリティ数を減らすため、遷移を表すsig
abstract sig Tran{ tran: A -> State -> State }{ one tran }
を導入し、サイズ3の経路をアリティ3の関係にした。
Tran -> Tran -> Tran
状態機械、経路、トレースのモデル化
上記の方針をふまえて、状態機械をモデル化する。
以下では、状態機械関連のsig以外に、一連の設問に必要なsigを予め定義している。 具体的には、模倣関係の設問に備えて状態機械を2種類(FSM1,FSM2)定義し、 模倣関係をモデル化するための sig Relation を定義した。
sig A{}
abstract sig State{}
abstract sig Tran{ tran: A -> State -> State }{ one tran }
abstract sig FSM{
S : some State,
S0: some S,
sigma: set Tran,
}{
srcState[sigma] in S
dstState[sigma] in S
}
lone sig Relation{ relation: State -> State }
fun alphabet[ts: set Tran]: set A{ ts.tran.univ.univ }
fun srcState[ts: set Tran]: set State{ univ.(ts.tran).univ }
fun dstState[ts: set Tran]: set State{ univ.(univ.(ts.tran)) }
sig S1,S2 extends State{}
sig FSM1 extends FSM{}{ S in S1 }
sig FSM2 extends FSM{}{ S in S2 }
sig Transition extends Tran{}
まず、サイズ#nの指定のトレースが指定の状態機械のトレースとなるかどうかを 以下のような述語tran#nでモデル化する。
pred tran1[m: FSM, t1: Tran]{
t1 in m.sigma
srcState[t1] in m.S0
}
pred tran2[m: FSM, t1,t2: Tran]{
tran1[m,t1]
t2 in m.sigma
dstState[t1] = srcState[t2]
}
pred tran3[m: FSM, t1,t2,t3: Tran]{
tran2[m,t1,t2]
t3 in m.sigma
dstState[t2] = srcState[t3]
}
次に述語tran#nを利用して、サイズ#nの経路の集合を以下のような関数path#nでモデル化する。
fun path1[m: FSM]: set Tran{
{t1: Tran | tran1[m,t1]}
}
fun path2[m: FSM]: Tran->Tran{
{t1,t2: Tran | tran2[m,t1,t2]}
}
fun path3[m: FSM]: Tran->Tran->Tran{
{t1,t2,t3: Tran | tran3[m,t1,t2,t3]}
}
最後にpath#nを利用して、サイズ#nのトレースの集合を以下のような関数trace#nでモデル化する。
fun trace1[m: FSM]: set A{
{a1: A |{
a1 in alphabet[path1[m]]
}}
}
fun trace2[m: FSM]: A->A{
{a1,a2: A |{
a1 in trace1[m]
a2 in alphabet[univ.(path2[m])]
}}
}
fun trace3[m: FSM]: A->A->A{
{a1,a2,a3: A |{
a1->a2 in trace2[m]
a3 in alphabet[univ.(univ.(path3[m]))]
}}
}
ついでに、ビジュアライザで遷移Tと経路P#n(#nはサイズ)を観察するための関数も用意した。
--ビジュアライザ観察用
fun T: State->A->State{
{s: State, a: A, s': State | a->s->s' in FSM.sigma.tran}
}
fun P1: State->Int->A->State{
some path1[FSM] =>
{s: State, i: Int, a: A, s': State | {
i=0
a->s->s' in path1[FSM].tran
}}
else { s:none, i:none, a:none , s':none | none not = univ}
}
fun P2: State->Int->A->State{
some path2[FSM] =>
{s: State, i: Int, a: A, s': State | {
(i=0 and a->s->s' in path2[FSM].univ.tran) or
(i=1 and a->s->s' in (univ.(path2[FSM])).tran)
}}
else { s:none, i:none, a:none , s':none | none not = univ}
}
fun P3: State->Int->A->State{
some path3[FSM] =>
{s: State, i: Int, a: A, s': State | {
(i=0 and a->s->s' in path3[FSM].univ.univ.tran) or
(i=1 and a->s->s' in (univ.(path3[FSM]).univ).tran) or
(i=2 and a->s->s' in (univ.(univ.(path3[FSM]))).tran)
}}
else { s:none, i:none, a:none , s':none | none not = univ}
}
トレース集合の例
A.4.2で状態機械の定義を変更したので、設問A.4.1に出てきた状態機械の例を 改めてモデリングし直す。
pred deterministic[m: FSM]{
one m.S0
all a: A, s: m.S | lone s.(a.(m.sigma.tran))
}
pred nonDeterministic[m: FSM]{
not deterministic[m]
}
pred unreachable[m: FSM]{
some s: m.S0, s': m.S | not reachableFrom[m, s, s']
}
pred reachable[m: FSM]{
not unreachable[m]
}
pred reachableFrom[m: FSM, s, s': State]{
s' in s.*(univ.(m.sigma.tran))
}
pred connected[m: FSM]{
all s1,s2: m.S | reachableFrom[m, s1, s2]
}
pred deadLock[m: FSM]{
some s0: m.S0, s: m.S |{
reachableFrom[m, s0, s]
no s.(univ.(m.sigma.tran))
}
}
pred liveLock[m: FSM]{
some s0: FSM.S0, hauntS1: m.S |
some disj hauntS2, neglectedS: m.S |{
-- 状態neglectedSは、常に到達可能な状態であるにもかかわらず
reachableFrom[m, hauntS1, neglectedS]
-- 状態neglectedSに決して到達しないような無限長の遷移列が存在する
reachableFrom[m, s0, hauntS1] and loop[m, m.S-neglectedS, hauntS1, hauntS2]
}
}
-- 状態集合ssに含まれる状態のみ、かつs1とs2を含む遷移の循環がある
pred loop[m: FSM, ss: set State, s1,s2: State]{
s1 = s2
=>{
s1 in ss
s1->s1 in univ.(m.sigma.tran)
}
else{
reachableFrom[m, ss, s1, s2]
reachableFrom[m, ss, s2, s1]
}
}
-- 状態集合ssに含まれる状態のみで、sからs'へ遷移可能
pred reachableFrom[m: FSM, ss: set State, s, s': State]{
s' in s.*( (ss<:(univ.(m.sigma.tran))):>ss )
}
いくつかの状態機械でトレース集合を生成する。
pred env_A_2_h{
no Relation
one FSM
#(alphabet[FSM.sigma]) > 1
# FSM.S > 2
# FSM.sigma > 2
}
run A_2_h_a{
env_A_2_h
all m: FSM | deterministic[m]
}for 3 but 18 Tran
run A_2_h_b{
env_A_2_h
all m: FSM | nonDeterministic[m]
}for 3 but 18 Tran
run A_2_h_c{
env_A_2_h
all m: FSM | unreachable[m]
}for 3 but 18 Tran
run A_2_h_d{
env_A_2_h
all m: FSM | reachable[m]
}for 3 but 18 Tran
run A_2_h_e{
env_A_2_h
all m: FSM | connected[m]
}for 3 but 18 Tran
run A_2_h_f{
env_A_2_h
all m: FSM | deadLock[m]
}for 3 but 18 Tran
run A_2_h_g{
env_A_2_h
all m: FSM | liveLock[m]
}for 3 but 18 Tran
$P1,$P2,$P3 などを観察すればどのようなトレース集合が生成されたかわかるが、 Evalutorで trace#n[FSM] (#nは1,2,3)などを入力してトレース集合を表示させたほうが 簡単に結果を確認できる。
なお、ビジュアライザで見やすくするためのテーマファイル(4.2.thm)をこのページにアップした。
● 決定性機械
● 非決定性機械
● 非到達な状態のある機械
● 非到達な状態のない機械
● 強連結な機械
● デッドロックのある機械
● ライブロックのある機械
( i ) 模倣の概念を追加し、模倣によって関連付けられる状態機械の組の例をいくつか生成せよ
模倣概念のモデル化
設問で紹介されている模倣関係と双模倣関係の定義を、Alloy語に翻訳してみる。
pred simulation[r: State->State, m1,m2: FSM]{
--m1 の状態からm2 の状態への関係r
r.univ = m1.S and univ.r = m2.S
all s1,s1': m1.S, s2: m2.S, a: A |{
{
--r によってm1 の状態s1 がm2 の状態s2 に関係付けられ、
s1->s2 in r
--m1?に状態s1 からs1'へのラベル付き遷移a があるとき、
a->s1->s1' in m1.sigma.tran
}=>
some s2': m2.S |{
--m2 においてもr によってs1'から関係付けられたs2'が常に存在し、
s1'->s2' in r
--s2 からs2'へラベル付き遷移a が存在する
a->s2->s2' in m2.sigma.tran
}
}
--s1 がm1 の初期状態であるとき、
all s1: m1.S0 |
--m2 の初期状態s2 が常に存在して、s1 とs2 がr によって関係付けられる
some s2: m2.S0 | s1->s2 in r
}
pred bisimulation[r: State->State, m1,m2: FSM]{
--~r もm2 のm1 に対する模倣関係であるとき、関係r は双模倣関係という
simulation[r, m1,m2]and simulation[~r, m2,m1]
}
pred simulation[m1,m2: FSM]{
some Relation
simulation[Relation.relation, m1, m2]
}
pred bisimulation[m1,m2: FSM]{
some Relation
bisimulation[Relation.relation, m1, m2]
}
模倣によって関連付けられる状態機械の組の例
次に模倣関係にある状態機械の組(FSM1,FSM2)を表示させてみる。 状態機械は、非到達な状態のない決定性機械に限定する。
pred env_A_2_i{
one FSM1
one FSM2
all m: FSM | deterministic[m]
all m: FSM | reachable[m]
}
--ビジュアライザ観察用
fun R: State->State{ Relation.relation }
run A_2_i_s{
env_A_2_i
simulation[FSM1, FSM2]
}for 3 but exactly 2 A, 3 S1, 3 S2, 36 Tran
run A_2_i_b{
env_A_2_i
bisimulation[FSM1, FSM2]
}for 3 but exactly 2 A, 3 S1, 3 S2, 36 Tran
●模倣の例
↑遷移がない場合は模倣関係が成立してしまう。
●双模倣の例
↑遷移がない場合は双模倣関係が成立してしまう。
( j ) 2 つの機械が模倣の関係にあるとき、その2 つは必ず同じトレースの集合を持つだろうか？ Alloy を使ってこの仮説を検査せよ。双模倣についてはどうか
トレース集合が同じか否かを判定する述語を用意する。
pred sameTrace1[m1,m2: FSM]{
trace1[m1] = trace1[m2]
}
pred sameTrace2[m1,m2: FSM]{
sameTrace1[m1,m2]
trace2[m1] = trace2[m2]
}
pred sameTrace3[m1,m2: FSM]{
sameTrace2[m1,m2]
trace3[m1] = trace3[m2]
}
述語sameTrace3 はサイズ3までの経路について、２つの状態機械のトレース集合が一致するかどうか判定する。
● 仮説１：模倣の関係にある２つの状態機械は同じトレース集合をもつ
仮説１を検査してみる。
この仮説については反例が出ることを予想しているので、
時短のため探索範囲を狭めることに(状態数や遷移数を少なめに設定)する。
check A_2_j_s{
all m1: FSM1, m2: FSM2 |{
{
simulation[m1, m2]
}
=> sameTrace3[m1,m2]
}
}for 1 but exactly 1 Relation, exactly 2 A, exactly 1 FSM1, exactly 1 FSM2,
exactly 2 S1, exactly 2 S2, exactly 4 Transition
以下のような反例が出た。
状態機械を限定(遷移有り、デッドロックなし、決定性、到達可能) してみたら、どうなるだろうか。
pred condFSM[m: FSM]{
some m.sigma
!deadLock[m]
deterministic[m]
reachable[m]
}
check A_2_j_s{
all m1: FSM1, m2: FSM2 |{
{
condFSM[m1] and condFSM[m2]
simulation[m1, m2]
}
=> sameTrace3[m1,m2]
}
}for 1 but exactly 1 Relation, exactly 2 A, exactly 1 FSM1, exactly 1 FSM2,
exactly 2 S1, exactly 2 S2, exactly 4 Transition
以下のような反例が出た。
● 仮説２：双模倣は同じトレース集合を持つ
仮説２を検査してみる。
check A_2_j_b{
all disj m1,m2: FSM |{
bisimulation[m1, m2]
=> sameTrace3[m1,m2]
}
}for 1 but exactly 1 Relation,//...検索範囲の設定
この仮説については反例が出ないことを予想しているので、
3状態、2ラベルの範囲全探索できるよう、遷移のインスタンスを36(=2ラベルx3状態x3状態x2機械)にする。
}for 1 but exactly 1 Relation, exactly 2 A, exactly 1 FSM1, exactly 1 FSM2,
exactly 3 S1, exactly 3 S2, exactly 36 Transition
しかしながら、この探索範囲は広すぎるようで結果を得ることができなかった。
次に、 ２つの状態機械をどちらもFSM1のインスタンスにすることで状態数を半減させ、
遷移のインスタンスも半減させるアプローチをした。
}for 1 but exactly 1 Relation, exactly 2 A, exactly 2 FSM1, 0 FSM2,
exactly 3 S1, 0 S2, exactly 18 Transition
しかしながら、これも結果を得ることができなかった。 (SATを変えて試したがだめだった。)
そこで、以下のように遷移を固定のインスタンスにすることを試みた。
check A_2_j_b{
all disj m1,m2: FSM |{
bisimulation[m1, m2]
=> sameTrace3[m1,m2]
}
}for 1 but exactly 1 Relation, 0 FSM1, 0 FSM2, exactly 2 FSMX,
0 A, 0 S1, 0 S2, exactly 3 SX, 0 Transition
one sig A0,A1 extends A{}
abstract sig SX extends State{}
one sig SX1,SX2,SX3 extends SX{}
sig FSMX extends FSM{}{ S in SX }
abstract sig Tran_A0 extends Tran{}{ alphabet[this]in A0 }
abstract sig Tran_A0_SX1 extends Tran_A0{}{ srcState[this]in SX1 }
abstract sig Tran_A0_SX2 extends Tran_A0{}{ srcState[this]in SX2 }
abstract sig Tran_A0_SX3 extends Tran_A0{}{ srcState[this]in SX3 }
one sig Tran_A0_SX1_SX1 extends Tran_A0_SX1{}{ dstState[this] in SX1 }
one sig Tran_A0_SX1_SX2 extends Tran_A0_SX1{}{ dstState[this] in SX2 }
one sig Tran_A0_SX1_SX3 extends Tran_A0_SX1{}{ dstState[this] in SX3 }
one sig Tran_A0_SX2_SX1 extends Tran_A0_SX2{}{ dstState[this] in SX1 }
one sig Tran_A0_SX2_SX2 extends Tran_A0_SX2{}{ dstState[this] in SX2 }
one sig Tran_A0_SX2_SX3 extends Tran_A0_SX2{}{ dstState[this] in SX3 }
one sig Tran_A0_SX3_SX1 extends Tran_A0_SX3{}{ dstState[this] in SX1 }
one sig Tran_A0_SX3_SX2 extends Tran_A0_SX3{}{ dstState[this] in SX2 }
one sig Tran_A0_SX3_SX3 extends Tran_A0_SX3{}{ dstState[this] in SX3 }
abstract sig Tran_A1 extends Tran{}{ alphabet[this]in A1 }
abstract sig Tran_A1_SX1 extends Tran_A1{}{ srcState[this]in SX1 }
abstract sig Tran_A1_SX2 extends Tran_A1{}{ srcState[this]in SX2 }
abstract sig Tran_A1_SX3 extends Tran_A1{}{ srcState[this]in SX3 }
one sig Tran_A1_SX1_SX1 extends Tran_A1_SX1{}{ dstState[this] in SX1 }
one sig Tran_A1_SX1_SX2 extends Tran_A1_SX1{}{ dstState[this] in SX2 }
one sig Tran_A1_SX1_SX3 extends Tran_A1_SX1{}{ dstState[this] in SX3 }
one sig Tran_A1_SX2_SX1 extends Tran_A1_SX2{}{ dstState[this] in SX1 }
one sig Tran_A1_SX2_SX2 extends Tran_A1_SX2{}{ dstState[this] in SX2 }
one sig Tran_A1_SX2_SX3 extends Tran_A1_SX2{}{ dstState[this] in SX3 }
one sig Tran_A1_SX3_SX1 extends Tran_A1_SX3{}{ dstState[this] in SX1 }
one sig Tran_A1_SX3_SX2 extends Tran_A1_SX3{}{ dstState[this] in SX2 }
one sig Tran_A1_SX3_SX3 extends Tran_A1_SX3{}{ dstState[this] in SX3 }
このアプローチでは探索を完了することができ、結果は以下のように、反例が出なかった。
ラベル2、状態数3、経路のサイズが3以内の規模では、双模倣関係にある状態機械のトレース集合は一致する。
Executing "Check A_2_j_b for 1 but exactly 1 Relation, 0 FSM1, 0 FSM2, exactly 2 FSMX, 0 A, 0 S1, 0 S2, exactly 3 SX, 0 Transition" Solver=minisat(jni) Bitwidth=4 MaxSeq=1 SkolemDepth=1 Symmetry=20 33175 vars. 403 primary vars. 110388 clauses. 7531ms. No counterexample found. Assertion may be valid. 392875ms.
この問題の解答を考えるほとんどの時間は、模倣性やトレース集合のモデルを検討することよりも、
解析器の制約を回避するためにAlloy語表現の工夫を試行錯誤することに費やした。
現在の解析器で実務的な問題に取り組むのは、モデラーにかなりのスキルを要求される気がする。
