Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
[Japanese Version]Deadlock Detection for Dining Philosophers Problem in Alloy
-- 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 システム状態
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.