04: MODULE main
05: VAR
06:     -- プロセス1の状態
07:     p1_state : {idle, waiting, critical};
08:     -- プロセス2の状態
09:     p2_state : {idle, waiting, critical};
10:     -- リソースの所有者
11:     res1_owner : {none, p1, p2};
12:     res2_owner : {none, p1, p2};
13: 
14: ASSIGN
15:     init(p1_state) := idle;
16:     init(p2_state) := idle;
17:     init(res1_owner) := none;
18:     init(res2_owner) := none;
19: 
20:     -- p1の遷移：res1を持ってからres2を狙う
21:     next(p1_state) :=
22:         case
23:             p1_state = idle : waiting;
24:             p1_state = waiting & res1_owner=p1 & res2_owner=p1 : critical;
25:             p1_state = critical : idle;
26:             TRUE : p1_state;
27:         esac;
28: 
29:     -- p2の遷移：res2を持ってからres1を狙う（デッドロックの種）
30:     next(p2_state) :=
31:         case
32:             p2_state = idle : waiting;
33:             p2_state = waiting & res2_owner=p2 & res1_owner=p2 : critical;
34:             p2_state = critical : idle;
35:             TRUE : p2_state;
36:         esac;
37: 
38:     -- リソース1の所有権
39:     next(res1_owner) :=
40:         case
41:             res1_owner = none & p1_state = waiting : p1;
42:             res1_owner = none & p2_state = waiting : p2;
43:             p1_state = critical & next(p1_state) = idle : none;
44:             p2_state = critical & next(p2_state) = idle : none;
45:             TRUE : res1_owner;
46:         esac;
47: 
48:     -- リソース2の管理（省略：res1と同様の論理）
49:     next(res2_owner) :=
50:         case
51:             res2_owner = none & p2_state = waiting : p2;
52:             res2_owner = none & p1_state = waiting : p1;
53:             p2_state = critical & next(p2_state) = idle : none;
54:             p1_state = critical & next(p1_state) = idle : none;
55:             TRUE : res2_owner;
56:         esac;
57: 
58: -- CTLSPEC: next() を使わない記述
59: -- 1. 特定の「デッドロック状態」を直接否定する
60: -- 「p1がres1を持ちながらres2を待ち，かつp2がres2を持ちながらres1を待つ」という状態は絶対起きない，と仮定する
61: CTLSPEC
62:     AG !(p1_state = waiting & res1_owner = p1 & 
63:          p2_state = waiting & res2_owner = p2)
64: 
65: -- 2. 「いつかは必ず critical セクションに入れる」という性質（活性）をチェックする
66: -- デッドロックが起きるなら，この式は FALSE になる
67: CTLSPEC
68:     AG (p1_state = waiting -> AF p1_state = critical)
