Model Base
A.3.6 外科医のグローブ
最終更新：
modelbase
更新日2011-09-03
[ Alloy Analyzer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題 解答例 ]
設問
ある外科医が3 人の患者を手術しなければ ならないが、2 組のグローブしかない。二次汚染はあってはならない。つまり、外科 医はどの患者の血と接触してもならないし、どの患者も他の患者の血と接触しては ならない。外科医は手術に両手を使う。この外科医はどうすべきか？ この問題をAlloy で表現し、解析器を使って解を見つけよ。
モデル化の方針
求められているのは "外科医はどうすべきか？" なので、"外科医がすること"のイベント列を提示すればよい。
書籍の2.4 や6.1.3で紹介されているように、util/ordering ライブラリモジュールを用いて
全順序関係となる○○列の存在を宣言する。この問では、特定の目標へ到達するためのイベント発生系列を発見したい。
したがって、初期状態から目標の状態へ移りゆく過程を状態の全順序関係として、下記のような fact traces で定義する。
状態の順序がわかれば、状態とイベントの紐付けをしておくことで、容易にイベント発生系列を観察できる。
ちなみに、下記のfirst, next, last はutil/orderingライブラリで定義されている関数である。 (ツールで、File -> Sample Models -> util -> ordering.als と選択すれば、ライブラリモジュールの記述を見ることができる)
fact traces {
// 初期状態となる状態が存在する
init [first]
// 遷移を満たす状態が存在する
all s: S | let s’ = next [s] |
e1 [s, s'] or e2 [s, s'] or ... or e#N[s, s']
// 目標となる状態が存在する
goal[last]
}
上記のfactを検査するために以下の記述を"作り込む"ことが、この問題を解くための具体的なモデル化作業となる。
("作り込む"の様子は、どんどん複雑になっていくというよりも、無駄なものが無くなりどんどん単純になっていく感じだ)
-
状態空間Sの記述
上記パターンのSにあたるsigの記述
-
不変条件の記述
状態空間Sに関するfactの記述
-
初期状態が満たす条件initの記述
上記パターンのinitにあたるpredの記述
-
目標となる状が満たす条件goalの記述
上記パターンのgoalにあたるpredの記述
-
遷移の記述
上記パターンのe1～e#Nにあたるpredの記述
具体的には遷移の事前状態と事後状態の記述
モデル化
【状態空間 sig DoctorState などの記述】
設問で課された制約が表現できるように、状態空間を形成するための情報を考える。
モデル化の中心的な作業は問題を解くに必要十分な状態空間を考察することであり、
これは1度で書き上げるのではなく、他の記述を考える過程で推敲されていく。
以下の情報で状態空間を形成する sig DoctorState を定義することにした。
- 外科医の手の状況
- 感染したグローブの表面
- 手術が済んだ患者
ポイントは"外科医の手"であり、グローブがどのように手にはめられるているかの表現である。
この問題の解はグローブの重ね着が要点であり、これを表現できるようにした。
予め解の見通しがあるなら、解に必要な情報が表現できる程度の簡素な状態空間の設計ができるのだが、
普通は先行きが見えないから、現実世界に近い状態空間の描写を目指してしまう。
しかし表現が具体的であるほど、状態空間が巨大化して解析が困難になる。逆に抽象的すぎると解が得られない。
この辺の模索で試行錯誤することが、モデル化作業の核心部分かもしれない。
【不変条件 fact inv の記述】
DoctorState や Glove のsigに現れるフィールドの限量指定や、run{} のパラメータに exactly キーワードで
要素数を指定していることで、いくつかの不変条件を定義することができる。
不変条件 fact inv は、そのようにして定義できないものを記述した。
不変条件を記述する際の注意点として、起きてはならない事柄を網羅的に記述して、不変条件の記述で
正確な状態空間を定義する必要がないことが言える。
たとえば、DoctorState の"外科医の手の状況"で同一のグローブを2重にはめている状況は起こりえない(※)ので、
不変条件でそのような状況を排除する記述を書いてしまいたくなる。同様に、起きるはずが無いことをもれなく
不変条件に書き足したくなり、だがどれだけの制約を定義すればよいのかわからくなる。
しかし、これらは遷移の条件記述(事後条件、事前条件)で明言することが可能で(実際、※はグローブをはめる遷移の
事前条件として記述)、そのように遷移と関連した条件として網羅意するほうが問題を解くに必要十分な状態空間の精度におさめられる。
【初期状態が満たす条件 pred init の記述】
初期状態は sig DoctorState の初期のインスタンスを宣言する述語で記述するので、
DoctorStateが決まれば、おのずと何を宣言すれば良いかに気づく。
むしろ、初期状態として何を宣言するかの予想が pred init の記述作業より前にあり、それが DoctorState 設計の判断材料となっている。
【目標となる状態が満たす条件 pred goal の記述】
目標となる状態では、制限(起きてほしくないこと)でなく、目標(起きてほしいこと)を書けばよい。
初期状態同様、目標状態として何を宣言するかの予想が、DoctorState の設計の判断材料となる。
【遷移 pred e の記述】
イベントeを契機にして起動する状態遷移の事前条件と事後条件を(イベント名と同じような名前の)predで記述する。
事前条件はイベントeを受理できる DoctorState のインスタンスdが満たすべき条件の記述となる。
事後条件はイベントeによって遷移する先の DoctorState のインスタンスd'が満たすべき条件の記述となる。
一般に事後条件は事前の状態dを用いて(dとの差で)記述される。
注意すべき点は、事後の状況と事前の状況に変化が無い場合も、"変化が無い"旨を明言することである。
自然言語で書かれた仕様書では、"何も書かないこと"が"変化が無いこと"を示す暗黙の了解が成立することも多いが、
Alloyなどのツールでは明言されないことは"どのように変化してもかまわない"と解析器に解釈されるので、注意が必要である。
モデルの記述
open util/ordering[DoctorState]
--------------------------------------------------
--状態空間の記述
--------------------------------------------------
sig Patient{}
abstract sig Surface{}
sig GloveSurface extends Surface{}
sig Glove{
disj inside, outside: one GloveSurface,
glove: inside->one outside
}
sig DoctorState{
--外科医の手の状況: 内側のグローブの表面 -> 外側のグローブの裏面
hand: Surface->Surface,
--感染したグローブの表面
infected: set Surface,
--手術が済んだ患者
ope: set Patient,
--次の状態に遷移する際の操作
e: lone Event,
}
--関係 hand の端点
one sig Bottom, Top extends Surface{}
--------------------------------------------------
--不変条件の記述
--------------------------------------------------
fact inv {
// 異なるグローブではグローブの表面も異なる
all disj g1,g2: Glove | no (g1.inside+g1.outside) & (g2.inside+g2.outside)
}
--------------------------------------------------
--初期状態の記述
--------------------------------------------------
pred init[d: DoctorState]{
d.hand = Bottom->Top
no d.infected
no d.ope
}
--------------------------------------------------
--目標となる状態の記述
--------------------------------------------------
pred goal[d: DoctorState]{
Patient in d.ope
no d.e
}
--------------------------------------------------
-- 遷移の記述
--------------------------------------------------
abstract sig Event{}
one sig
Do_Operation, --手術する
Wear_Glove, --グローブをはめる
Wear_Glove_Reversly, --グローブを裏返してはめる
Remove_Glove --グローブを脱ぐ
extends Event{}
pred Do_Operation[d,d': DoctorState]{
d.e = Do_Operation
----------------------
--事前条件
----------------------
// グローブをはめている
wearing_some_glove[d]
// 一番外側のグローブの表面は感染してない
not infected[most_outside[d.hand], d]
----------------------
--事後条件
----------------------
--手の状況
keep_hand[d, d']
--感染状況
// 一番外側のグローブの表面は感染する
increase_infected[most_outside[d.hand], d, d']
--手術の状況
// 手術した患者が増える
increase_ope[d,d']
}
pred Wear_Glove[d,d': DoctorState]{
d.e = Wear_Glove
some g: Glove | wear_glove[g, d, d', g.inside, g.outside]
}
pred Wear_Glove_Reversly[d,d': DoctorState]{
d.e = Wear_Glove_Reversly
some g: Glove |{
// グローブgのどちらかの面が感染している(つまらないインスタンスを排除)
infected[g.inside, d]or infected[g.outside, d]
wear_glove[g, d, d', g.outside, g.inside]
}
}
pred wear_glove[g: Glove, d,d': DoctorState, is, os: GloveSurface]{
----------------------
--事前条件
----------------------
// グローブgは現在手にはめていないグローブ
not wearing[g, d]
// 現在素手ならば、グローブgの内側は感染してない
not wearing_some_glove[d]=> not infected[is, d]
----------------------
--事後条件
----------------------
--手の状況
// グローブgの表面が最も外側の面になる
increase_glove[d, d', is, os]
--感染状況
// 現在の最も外側の面が感染しているか、グローブgの内側が感染しているなら、感染するグローブの面が増える
(infected[most_outside[d.hand], d] or infected[is, d])
=> increase_infected[most_outside[d.hand]+is, d, d']
else keep_infected[d,d']
--手術の状況
keep_ope[d,d']
}
pred Remove_Glove[d,d': DoctorState]{
d.e = Remove_Glove
----------------------
--事前条件
----------------------
// グローブをはめている
wearing_some_glove[d]
----------------------
--事後条件
----------------------
--手の状況
// はめているグローブが減る
decrease_glove[d, d']
--感染状況
keep_infected[d,d']
--手術の状況
keep_ope[d,d']
}
--------------------------------------------------
-- イベント列の存在
--------------------------------------------------
fact traces{
--初期状態
init[first]
--状態遷移
all d: DoctorState - last | let d' = next[d]|{
Do_Operation[d,d']
or Wear_Glove[d,d']
or Wear_Glove_Reversly[d,d']
or Remove_Glove[d,d']
}
--目標状態
goal[last]
}
----------------------
--補助述語、補助関数
----------------------
fun most_outside[r: Surface->Surface]: Surface{ r.Top }
pred wearing_some_glove[d: DoctorState]{
Bottom->Top not in d.hand
}
pred wearing[g: Glove, d: DoctorState]{
let sfs = (d.hand).univ+univ.(d.hand) |
(g.inside + g.outside) in sfs
}
pred infected[sfs: set Surface, d: DoctorState]{
sfs in d.infected
}
pred increase_infected[sfs: set Surface, d,d': DoctorState]{
d'.infected = d.infected + sfs
}
pred increase_glove[d,d': DoctorState, is, os:GloveSurface]{
d'.hand = (d.hand ++ (most_outside[d.hand]->is)) + os->Top
}
pred decrease_glove[d,d': DoctorState]{
one mo': Surface, g: Glove |{
mo'->g.inside + g.outside->Top in d.hand
d'.hand = ((d.hand):>(univ.(d.hand)-Top)) ++ mo'->Top
}
}
pred increase_ope[d,d': DoctorState]{
one d'.ope - d.ope
}
pred keep_ope[d,d': DoctorState]{ d.ope = d'.ope }
pred keep_infected[d,d': DoctorState]{ d.infected = d'.infected }
pred keep_hand[d,d': DoctorState]{ d.hand = d'.hand }
run {}for 3 but exactly 3 Patient, exactly 2 Glove, exactly 4 GloveSurface, 8 DoctorState
解析器を使って解をみつける
ビジュアライザよりもツリー表示で見たほうが結果を確認しやすい。
DoctorStateの要素はfirstからlastの順番で表示されるので、各要素の field e を観察すれば、
イベント系列を確認できる。
- Wear_Glove グローブをはめる
- Do_Operation 手術する
- Remove_Glove グローブを脱ぐ
- Weare_Glove 別のグローブをはめる
- Do_Operation 手術する
- Weare_Glove_Reversly 別のグローブを裏返しにしてはめる
- Do_Operation 手術する
