01: MODULE main
02: VAR
03:     p0_state : {idle, choosing, waiting, cs, exit};
04:     p1_state : {idle, choosing, waiting, cs, exit};
05:     p0_num : 0..3;
06:     p1_num : 0..3;
07: 
08: ASSIGN
09: -- 初期状態
10: init(p0_state) := idle;
11: init(p1_state) := idle;
12: init(p0_num) := 0;
13: init(p1_num) := 0;
14: 
15: -- P0 の状態遷移
16: next(p0_state) := case
17:     -- idle -> choosing
18:     p0_state = idle : choosing;
19:     -- choosing -> waiting
20:     p0_state = choosing : waiting;
21:     -- waiting -> cs
22:     -- 自分の番号が小さいと入れる
23:     p0_state = waiting & (p1_num = 0 | p0_num < p1_num) : cs;
24:     -- cs -> exit
25:     p0_state = cs : exit;
26:     -- exit -> idle
27:     p0_state = exit : idle;
28:     TRUE : p0_state;
29: esac;
30: 
31: -- P1 の状態遷移
32: next(p1_state) := case
33:     p1_state = idle : choosing;
34:     p1_state = choosing : waiting;
35:     p1_state = waiting & (p0_num = 0 | p1_num < p0_num) : cs;
36:     p1_state = cs : exit;
37:     p1_state = exit : idle;
38:     TRUE : p1_state;
39: esac;
40: 
41: -- ticket番号管理
42: next(p0_num) := case
43:     p0_state = choosing : max(p0_num, p1_num) + 1;
44:     p0_state = exit : 0;
45:     TRUE : p0_num;
46: esac;
47: 
48: next(p1_num) := case
49:     p1_state = choosing : max(p0_num, p1_num) + 1;
50:     p1_state = exit : 0;
51:     TRUE : p1_num;
52: esac;
53: 
54: -- 性質検証
55: --  相互排他:
56: --  同時に cs に入らない
57: SPEC AG !(p0_state = cs & p1_state = cs)
58: --  到達可能性:
59: --  P0 はいつか cs に入れる
60: SPEC AG (p0_state = waiting -> AF p0_state = cs)
61: --  P1 も同様
62: SPEC AG (p1_state = waiting -> AF p1_state = cs)
