-
Notifications
You must be signed in to change notification settings - Fork 0
/
Door.tla
58 lines (48 loc) · 1.67 KB
/
Door.tla
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
-------------------------------- MODULE Door --------------------------------
VARIABLES
now,
limit,
time,
running,
open, \* Represents whether the door is open (TRUE) or not (closed, FALSE)
openPending, \* Represents whether the door is waiting to be opened
closePending \* Represents whther the door is waiting to be closed
vars == << open, openPending, closePending >>
INSTANCE Timer WITH InitialLimit <- 3
TypeInvariant == /\ open \in BOOLEAN
/\ openPending \in BOOLEAN
/\ closePending \in BOOLEAN
/\ (~openPending \/ ~closePending)
----
Init == /\ open \in BOOLEAN
/\ openPending = FALSE
/\ closePending = FALSE
StepOnSignal == /\ ~open
/\ openPending' = TRUE
/\ UNCHANGED << open, closePending >>
StepOffSignal == /\ open
/\ Start
/\ UNCHANGED << open, openPending >>
PrepareClose == /\ Timeout
/\ closePending' = TRUE
/\ UNCHANGED << open, openPending >>
Open == /\ openPending
/\ openPending' = FALSE
/\ open' = TRUE
/\ UNCHANGED << closePending >>
Close == /\ closePending
/\ closePending' = FALSE
/\ open' = FALSE
/\ UNCHANGED << openPending >>
Next == \/ StepOnSignal
\/ StepOffSignal
\/ Open
\/ PrepareClose
\/ Close
Spec == Init /\ [][Next]_vars /\ WF_vars(Open) /\ WF_vars(Close)
----
THEOREM Spec => []TypeInvariant
=============================================================================
\* Modification History
\* Last modified Sat Aug 20 20:09:54 ART 2016 by juampi
\* Created Fri Jul 15 08:31:18 ART 2016 by juampi