A.2.3 囚人の割り当て - Model Base

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

---

( a ) 安全な割り当てを表現する述語safe を完成させ、安全な割り当てとそうでない割り当ての両方の例を生成せよ

 -- 二人の囚人が異なるギャングのメンバーであった場合、
 -- その二人が同じ監房に入ることはない
 pred safe () {
   all disj i1,i2 : Inmate |
   let G1 = members.i1, G2 = members.i2 |
   {
     -- 二人はギャングのメンバーである
     some G1 and some G2
     -- 二人は同じギャングのメンバーでない
     G1 not = G2
     }
   =>
   no ( i1.room & i2.room )
   }
 
 fact{
   #Inmate > 1
   } 
 
 pred show () {
   safe
   }
 
 run show

複数のギャングに所属する場合も考慮する。

( b ) ギャングメンバーは同じギャングのメンバーとだけ監房を共有できる、という新たな述語happyを書け

 -- ギャングメンバーは同じギャングメンバーとだけ監房を共有できる
 pred happy{
   all c: Cell | 
   some members.(room.c) => all disj i1,i2: room.c | members.i1 = members.i2
   } 
   

安全な割り当ては必ずしも幸せな割り当てではない。アサーションとそれを検査するコマンドを書き、反例を見つけ、なぜそうではないのかを説明せよ。

 check c {
   safe => happy
   }

ギャングでない囚人がいるから。

( c ) 安全性が幸せを含意することを保証するような制約をファクトとして追加せよ。

 fact{
   Inmate in univ.members
   }    

ギャング専用の刑務所とすれば、反例がなくなる。