他の充足性判定例 (CWB-NC の利用 )

のように勝利集合を求める演算は，最大不動点計算(ν)に帰着され，最大不動点はψを充 足するモデルM の最大の部分モデルM⁰⁰を求めていることに相当する．

min X = [-]ff \/ <->X

ここで[-]ffは全てのアクションがまったく実行できない状況を表し，この状態に到達

するか可能性を再帰的にXは定義している．minは最小不動点演算に関係している[2](詳 しくは付録A.2.4参照)．

deadlockになるかどうかを判定することにより，nilに遷移するかどうか，すなわち性質

Spec0を充足するかどうかを判定する．以下はcan_deadlockを”dead.mu”というファイ ルから読み，プロセス(Sys_ok,Sys_ng)が仕様(Spec0)を充足するかどうかを，判定した ログである．CWB-NCを用いた充足性判定の例は，付録A.3章を参照のこと．

¶ ³

*プロパティ(nil遷移付き)と掛け合わせてdeadlockしないか(nil遷移がないか）

* を見る方法

*以下のようにnilに遷移するのをみつけます load dead.mu

cwb-nc> search Prod_ok can_deadlock States explored: 4

No state found satisfying can_deadlock.

cwb-nc> search Prod_ng can_deadlock State found satisfying can_deadlock.

Path to state contains 1 states, invoking simulator.

1: Prod_ng

*cwb-nc-sim>

µ ´

Spec0をSys_okは充足し，Sys_ngは充足しないことがわかる．

3.4 ∇ ^{演算の導入}

LTSに対してψⁿ_αi→βjを充足するような動作を強要する演算∇ψⁿ

αi→βj を導入する．

3.4.1 ∇

ψⁿ_α

i→βj に対応するLTS(LTS_ψⁿ

αi→βj とする)において，

以下順序制約ψⁿ_α

i→βjに対応する∇演算∇ψ_αi→βjⁿ を以下のように定義する．

∇ψ_αi→βjⁿ :P roc×int×Act×int×Act×int7→P roc

• 任意のLTSに対して,COM(LTS,LTS1’ψⁿ

αi→βj)によって定義されるLTS’を得る

• LTS’において初期プロセスs0から到達可能なLTSの部分モデルLTS”を得る 到達可能な部分LTSを得るための演算は，以下に示すCP re演算を用いる．

CP re₁(X) ={s ∈S₁|∃t ∈E(s), t∈X}

CP re₁(X)が単調な関数であるので，Tarskiの不動点定理[28] より，最大不動点，最小 不動点が存在し，適切な初期集合X₀を選択して，CP re₁(X)を繰り返し適用して，収束 先を求めることにより，不動点を手続き的に計算できることが，不動点理論より知られて いる．

W in₁ =νX.(R∩CP re₁(X))

ここでRとはN Gでない状態の集合S− {N G}である．最大不動点の場合は，X₀ =S

としてCP re₁(X)を繰り返し適用し，収束する状態の集合が最大不動点F IX である．

X₀ =S

X₁ =R∩CP re₁(X₀)

· · · =· · ·

X_n =R∩CP re₁(X_n−1)

· · · =· · ·

F IX =lim_N(X_n), X_n =X_n−1 最大不動点が，到達可能な部分LTSのプロセスの集合になる.

∇ψ_αi→βjⁿ (P)は順序制約ψ_αⁿ

i→βjに従い，P を起点とするLTSの中でψ_αⁿ

i→βjに矛盾する遷 移を抑制する意味を持つ．

例えば，プロセスP T₁ ^def= a·b·0, P T₂ ^def= c·d·0の並列結合に対して制約∇ψ_bk→dk¹ を挿 入するとする．

最初に，P T₁|P T₂は以下のLTSを構成している，

¶ ³

LTS7:

Proc={s0=a.b.0|c.d.0, s1=b.0|c.d.0, s3=0|c.d.0, s6=0|d.0, s8=0|0, s2=a.b.0|d.0, s5=a.b.0|0, s4=b.0|d.0, s7=b.0|0}

Act={a,b,c,d}

-a-> = {(s0,s1),(s2,s4),(s5,s7)}

-b-> = {(s1,s3),(s4,s6),(s7,s8)}

-c-> = {(s0,s2),(s1,s4),(s3,s6)}

-d-> = {(s2,s5),(s4,s7),(s6,s8)}

µ ´

∇ψ¹_bk→dk のLTSからNG状態及びNGへの遷移を削除すると以下のLTS8を得る

¶ ³

LTS8:

Proc = {P0,P1}

Act = {b,d}

-b->{(P0,P1)},-d->{(P1,P0)}

µ ´

ここでLTS8のb,dをb, dに置き換え M⁰ =∂_b,d(s0|P0)[b|b/b, d|d/d]

を計算し，s0’=s0|P0, s1’=s1|P0,s2’=s2|0,s3’=s3|P1,s4’=s4|P0, s6’=s6|P1,s8’=s8|P0， とすると結果は，以下のようになる

¶ ³

Proc={s0’,s1’,s2’,s3’,s4’,s6’,s8’}

Act={a,b,c,d}

-a-> = {(s0’,s1’),(s2’,s4’)}

-b-> = {(s1’,s3’),(s4’,s6’)}

-c-> = {(s0’,s2’),(s1’,s4’),(s3’,s6’)}

-d-> = {(s6’,s8’)}

µ ´

即ちもとのLTSに比べて遷移が制限されたLTSが得られた．

3.4.2 ∇

OW:

∇ψⁿ

OW:αi→βj

演算は同様にψⁿ

OW:αi→βj

に対応する順序制約挿入演算である．