-
Notifications
You must be signed in to change notification settings - Fork 205
/
Copy pathComposition.tla
142 lines (114 loc) · 4 KB
/
Composition.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
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
---------------------------- MODULE Composition ----------------------------
(**************************************************************************)
(* Background reading: Conjoining Specifications by Abadi and Lamport *)
(* https://lamport.azurewebsites.net/pubs/abadi-conjoining.pdf *)
(**************************************************************************)
EXTENDS Integers, Sequences
Nodes == 1..3 \* Fixed to 1..3 here but should be a constant.
(* COMPONENT Spec A (Computation) *)
------ MODULE A --------
VARIABLES x, \* Private to this component.
active \* Shared with component spec B.
vars == <<x,active>>
Type ==
/\ x \in 0..10
/\ active \in [ Nodes -> BOOLEAN ]
Init ==
/\ x = 0
/\ active \in [ Nodes -> BOOLEAN ]
Next ==
\* Not all nodes are inactive.
/\ \E i \in DOMAIN active : active[i] = TRUE
\* Mimic some computation.
/\ x' \in 1..10
\* Computation changed the activation of 0 to N nodes.
/\ active' \in [ Nodes -> BOOLEAN ]
==================================
(* COMPONENT Spec B (Safra's termination detection) *)
------------ MODULE B ------------
VARIABLES active, \* Shared with component A.
inactive \* Shared with component C.
vars == <<inactive, active>>
Type ==
/\ inactive \subseteq Nodes
/\ active \in [ Nodes -> BOOLEAN ]
Init ==
/\ inactive = {}
/\ active \in [ Nodes -> BOOLEAN ]
Next ==
\* Since this high-level composition abstracts away communication,
\* we could abstract termination detection into a single step:
\* /\ \A i \in DOMAIN active : active[i] = FALSE
\* /\ inactive' = Nodes
\* However, we want to model the possible interleavings of the
\* A and B spec.
/\ \E i \in DOMAIN active:
active[i] = FALSE /\ i \notin inactive
/\ inactive' = inactive \cup {
CHOOSE i \in DOMAIN active:
active[i] = FALSE /\ i \notin inactive
}
/\ UNCHANGED active
==================================
(* COMPONENT Spec C (orderly/graceful shutdown) *)
------------ MODULE C ------------
VARIABLES inactive \* Shared with component spec B.
vars == <<inactive>>
Type ==
/\ inactive \subseteq Nodes
Init ==
/\ inactive \subseteq Nodes
IOExit == TRUE \* Shutdown via sys.exit
Next ==
/\ inactive = Nodes
/\ UNCHANGED inactive
/\ IOExit
==================================
-----------------------------------------------------------------------------
(* Component specification. *)
VARIABLES x, active, inactive
vars ==
<<inactive, x, active>>
A == INSTANCE A
B == INSTANCE B
C == INSTANCE C
TypeOK ==
/\ A!Type
/\ B!Type
/\ C!Type
Init ==
/\ A!Init
/\ B!Init
/\ C!Init
\* PlusPy will most certainly not be able to evaluate this
\* Next formula. Might have to introduce an auxiliary variable
\* that represents the phase/stage of composed system.
Next ==
\/ /\ ENABLED A!Next
/\ [A!Next]_vars
/\ UNCHANGED <<inactive>>
\/ /\ ENABLED B!Next
/\ [B!Next]_vars
/\ UNCHANGED <<x>>
\/ /\ [C!Next]_vars
/\ UNCHANGED <<x, active>>
Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
THEOREM Spec => []TypeOK
(* The system eventually converges to shutdown. This, however, does
*not* hold because component spec A could keep computing forever. *)
AlwaysShutdown ==
<>[][C!Next]_vars
(* Unless all nodes are inactive at startup, some computation will occur. *)
ComputationIfSomeActive ==
[n \in Nodes |-> FALSE] # active => <>[](x \in 1..10)
THEOREM Spec => ComputationIfSomeActive
(* Iff - from some point onward - all nodes will become
inactive, the composed system will eventually shutdown. *)
ShutdownIfNoComputation ==
<>[][~ A!Next]_vars => <>[][C!Next]_vars
THEOREM Spec => ShutdownIfNoComputation
=============================================================================
\* Modification History
\* Last modified Mon Jun 15 17:37:21 PDT 2020 by markus
\* Last modified Fri Jun 12 16:30:19 PDT 2020 by Markus Kuppe
\* Created Fri Jun 12 10:30:09 PDT 2020 by Leslie Lamport