02: MODULE main
03: VAR
04:     -- プロセス状態
05:     p0_state : {idle, choosing, waiting, cs};
06:     p1_state : {idle, choosing, waiting, cs};
07: 
08:     -- ticket番号
09:     p0_num : integer;
10:     p1_num : integer;
11: 
12:     -- choosing flag
13:     p0_choosing : boolean;
14:     p1_choosing : boolean;
15: 
16:     -- scheduler
17:     running : {p0, p1};
18: 
19: ASSIGN
20:     -- 初期状態
21:     init(p0_state) := idle;
22:     init(p1_state) := idle;
23:     init(p0_num) := 0;
24:     init(p1_num) := 0;
25:     init(p0_choosing) := FALSE;
26:     init(p1_choosing) := FALSE;
27:     init(running) := p0;
28:     -- scheduler
29:     next(running) := {p0, p1};
30: 
31:     -- p0 choosing flag
32:     next(p0_choosing) := case
33:         running = p0 & p0_state = idle : TRUE;
34:         running = p0 & p0_state = choosing : FALSE;
35:         TRUE : p0_choosing;
36:     esac;
37: 
38:     -- p1 choosing flag
39:     next(p1_choosing) := case
40:         running = p1 & p1_state = idle : TRUE;
41:         running = p1 & p1_state = choosing : FALSE;
42:         TRUE : p1_choosing;
43:     esac;
44: 
45:     -- p0 ticket
46:     next(p0_num) := case
47:         running = p0 & p0_state = choosing : max(p0_num, p1_num) + 1;
48:         running = p0 & p0_state = cs : 0;
49:         TRUE : p0_num;
50:     esac;
51: 
52:     -- p1 ticket
53:     next(p1_num) := case
54:         running = p1 & p1_state = choosing : max(p0_num, p1_num) + 1;
55:         running = p1 & p1_state = cs : 0;
56:         TRUE : p1_num;
57:     esac;
58: 
59:     -- p0 state transition
60:     next(p0_state) := case
61:         running = p0 & p0_state = idle : choosing;
62:         running = p0 & p0_state = choosing : waiting;
63:         running = p0 & p0_state = waiting & (p1_num = 0 | p0_num < p1_num | (p0_num = p1_num & 0 < 1)) : cs;
64:         running = p0 & p0_state = cs : idle;
65:         TRUE : p0_state;
66:     esac;
67: 
68:     -- p1 state transition
69:     next(p1_state) := case
70:         running = p1 & p1_state = idle : choosing;
71:         running = p1 & p1_state = choosing : waiting;
72:         running = p1 & p1_state = waiting & (p0_num = 0 | p1_num < p0_num | (p1_num = p0_num & 1 < 0)) : cs;
73:         running = p1 & p1_state = cs : idle;
74:         TRUE : p1_state;
75:     esac;
76: 
77: -- FAIRNESS
78: FAIRNESS running = p0
79: FAIRNESS running = p1
80: 
81: -- SAFETY
82: INVARSPEC !(p0_state = cs & p1_state = cs)
83: 
84: -- LIVENESS : nuXmv の infinite-state モデルでは CTL の一部手法が使えない．LTLを使う．
85: SPEC AG (p0_state = waiting -> AF p0_state = cs)
86: SPEC AG (p1_state = waiting -> AF p1_state = cs)
