[Japanese Version]Deadlock Detection for Dining Philosophers Problem in Alloy

dining_philosophers_ja.als

-- This can be executed by alloy4.2-rc.jar on http://alloy.mit.edu/community/node/1039
-- This version supports unicode identifiers.
open util/ordering[システム状態]

sig 哲学者 {
	disj 左フォーク, 右フォーク: one フォーク,
	左, 右: one 哲学者
}
sig フォーク { 
	disj 左, 右: one 哲学者
}
fact 哲学者とフォークが交互に並んでいる{
	#哲学者 = #フォーク
	-- 哲学者の両隣にはフォークがある。
	(all p: 哲学者 | p.左 = p.左フォーク.左 and p.右 = p.右フォーク.右 )
	-- フォークの両隣には哲学者がいる。
	(all f: フォーク | f = f.左.右フォーク and f = f.右.左フォーク)
}

fact テーブルは一つ{
	-- 左(右)の推移的閉包は哲学者全体を含む
	(all p: 哲学者 | 哲学者 in p.^右 and 哲学者 in p.^左)
	-- 左.左フォーク(右.右フォーク)の推移的閉包はフォーク全体を含む
	(all f: フォーク | フォーク in f.^( 左.左フォーク ) and フォーク in f.^( 右.右フォーク ))
}

-- Global システム状態
sig システム状態 {
     -- フォークの保持者は高々一人(lone:least or equal to one)
	保持者: フォーク -> lone 哲学者
}{
	-- フォークは自分の両脇の哲学者からしか保持されない
	all f:フォーク | 保持者[f] in f.(左+右)
}
-- フォークの為の述語
pred 利用可能 ( s: システム状態, f: フォーク ) {
	no s.保持者 [ f ]
}

-- 哲学者の為の述語
pred 食べている ( s: システム状態, p: 哲学者 ) {
	p  = s.保持者[p.右フォーク] and p =  s.保持者[p.左フォーク]
}

-- アルゴリズム
-- 状態sで哲学者pが動作をした次の状態がs'である。
pred 左フォークを取る ( s: システム状態, s': システム状態, p: 哲学者 ) {
	-- sではpの左のフォークは利用可能いていて、s'ではpの左のフォークはpが保持している
	-- (述語に引数を適用する場合には[]を使う)
	利用可能[s,p.左フォーク] and s'.保持者[p.左フォーク] = p
	-- それ以外のフォークは保持者が変化していない
	and (all f: (フォーク - p.左フォーク) | s.保持者[f] = s'.保持者[f])
}
pred 右フォークを取る ( s: システム状態, s': システム状態, p: 哲学者 ) {
	利用可能[s,p.左フォーク] and s'.保持者[p.右フォーク] = p
	and (all f: (フォーク - p.右フォーク) | s.保持者[f] = s'.保持者[f])
}
pred 両フォークを手放す(s:システム状態, s':システム状態, p:哲学者){
	食べている[s,p] and (利用可能[s',p.右フォーク] and 利用可能[s',p.左フォーク])	
	and (all f: (フォーク - (p.左フォーク + p.右フォーク)) | s.保持者[f] = s'.保持者[f])
}

-- 初期状態の述語
pred 誰も持っていない ( s: システム状態 ) {
	all f: フォーク | 利用可能 [ s, f ]
}
-- 状態上の全順序に与える制約
fact 状態遷移の制約 {
	-- firstは誰も持っていないを満たす
	誰も持っていない [ first ] 
	-- 最後の状態以外の状態sは
	-- 誰かが動作できる状態ならsの次の状態next[s]は誰かが動いた後の状態であり、
	-- かつ、そう出なければ、何も変わっていない(デッドロックが続いている)
	all s: システム状態 - last
		| 誰かが動作できる[s] => 誰かが動作[s,next[s]] else s.保持者 = next[s].保持者
} 
-- 状態sで、誰かが動いた状態がs'である。
pred 誰かが動作 ( s: システム状態, s': システム状態 ) {
	some p: 哲学者 | 左フォークを取る [ s, s', p ] or 右フォークを取る [ s, s', p ] or 両フォークを手放す[s,s',p] 
}
-- 状態sで誰かが動作できる。
pred 誰かが動作できる(s:システム状態){
	some p: 哲学者 | 
		利用可能[s,p.左フォーク] or 利用可能[s,p.右フォーク] or 食べている[s,p]
}

pred デッドロックが存在する実行{
	some s:システム状態 | not 誰かが動作できる[s] 
				and all s': s.^next | not 誰かが動作できる[s'] -- s以降のs'はずっとデッドロック
				and all s'': s.^prev | 誰かが動作できる[s''] -- s以前はずっと誰かが動ける
}
-- デッドロックが存在する実行を見つけてくれ、というコマンド。
-- 3フォーク、3人の哲学者、実行の長さは20ステップ
run デッドロックが存在する実行 for exactly 3 フォーク, 3 哲学者,  10 システム状態