03: MODULE main
04: VAR
05:     -- リソースの空き状況 (TRUE = 空き, FALSE = 使用中)
06:     res1 : boolean;
07:     res2 : boolean;
08:     
09:     -- 各プロセスの状態
10:     p1 : process worker(1, res1, res2);
11:     p2 : process worker(2, res1, res2);
12: 
13: ASSIGN
14:     init(res1) := TRUE;
15:     init(res2) := TRUE;
16: 
17: -- デッドロックを検出するためのスペック
18: -- 「常に，どこかのプロセスが次に進める状態であること」をチェック
19: CTLSPEC
20:     AG EX TRUE
21: 
22: MODULE worker(id, r1, r2)
23: VAR
24:     state : {idle, want1, want2, critical};
25: 
26: ASSIGN
27:     init(state) := idle;
28:     next(state) := 
29:         case
30:             state = idle : {idle, want1};
31:             -- リソース1を確保しようとする
32:             state = want1 & r1 : want2;
33:             -- リソース2を確保しようとする (ここでデッドロックの可能性)
34:             state = want2 & r2 : critical;
35:             state = critical : idle;
36:             TRUE : state;
37:         esac;
38: 
39:     next(r1) :=
40:         case
41:             state = want1 & r1 : FALSE; -- 確保
42:             state = critical : TRUE;    -- 解放
43:             TRUE : r1;
44:         esac;
45: 
46:     next(r2) :=
47:         case
48:             state = want2 & r2 : FALSE; -- 確保
49:             state = critical : TRUE;    -- 解放
50:             TRUE : r2;
51:         esac;
