03: MODULE main
04: 
05: VAR
06:     state : {OFF, HIGH, SCANNING, LOCKED};     -- 状態
07:     event : {on, off, scan, reset, lock, end}; -- 入力イベント
08: 
09: ASSIGN
10:     init(state) := OFF; -- 初期状態
11: 
12:     next(state) := case -- 状態遷移
13:         state = OFF & event = on : HIGH;          -- OFF
14:         state = OFF : OFF;
15:         state = HIGH & event = scan : SCANNING;   -- HIGH
16:         state = HIGH & event = off : OFF;
17:         state = HIGH & event = reset : HIGH;
18:         state = HIGH : HIGH;
19:         state = SCANNING & event = lock : LOCKED; -- SCANNING
20:         state = SCANNING & event = end : HIGH;
21:         state = SCANNING & event = off : OFF;
22:         state = SCANNING & event = reset : HIGH;
23:         state = SCANNING : SCANNING;
24:         state = LOCKED & event = scan : SCANNING; -- LOCKE
25:         state = LOCKED & event = reset : HIGH;
26:         state = LOCKED & event = off : OFF;
27:         state = LOCKED : LOCKED;
28:         TRUE : state;
29:     esac;
30: 
31: FAIRNESS (state != SCANNING) | (event = lock) | (event = end)
32: 
33: -- Safety Property
34: SPEC AG !(state = OFF & state = LOCKED)
35: 
36: -- Liveness Property
37: SPEC AG (state = SCANNING ->
38:     AF (state = LOCKED |
39:         state = HIGH |
40:         state = OFF))
41: 
42: -- Deadlock Freedom
43: SPEC AG EX TRUE
44: 
45: -- Always possible to turn off
46: SPEC AG EF (state = OFF)
