Skip to content

Commit 7db9bdf

Browse files
lemmylemmy
committed
Compose Compute, Detect Termination (EWD998), and Shutdown.
1 parent 98bcd4f commit 7db9bdf

File tree

1 file changed

+117
-65
lines changed

1 file changed

+117
-65
lines changed

‎specifications/composition/Composition.tla‎

Lines changed: 117 additions & 65 deletions
Original file line numberDiff line numberDiff line change
@@ -2,89 +2,141 @@
22
(**************************************************************************)
33
(* Background reading: Conjoining Specifications by Abadi and Lamport *)
44
(* https://lamport.azurewebsites.net/pubs/abadi-conjoining.pdf *)
5-
(* *)
6-
(* Spec A and B are two components that together are composed into a *)
7-
(* larger system. It's toy example in the sense that minimize *)
8-
(* interaction of A and B to behaviors where first A takes its steps *)
9-
(* followed by B. Variable y in A and B represents the control wire *)
10-
(* that A and B use to synchronize. *)
11-
(* Variable z has been added to make the example more interesting--it *)
12-
(* only appears in spec A but *not* B. *)
13-
(* *)
145
(**************************************************************************)
15-
EXTENDS Naturals, Sequences
16-
17-
(* COMPONENT Spec A *)
18-
------------ MODULE A ------------
19-
VARIABLES x, \* Abstract/very high-level representation of the overall computation.
20-
\* Think of it as some computation going on. At a certain state
21-
\* of the computation, the composed system transitions into the
22-
\* next phase.
23-
z \* z is the variable that is only going to be present in spec A.
24-
varsA == <<x, z>>
25-
26-
InitA ==
6+
EXTENDS Integers, Sequences
7+
8+
Nodes == 1..3 \* Fixed to 1..3 here but should be a constant.
9+
10+
(* COMPONENT Spec A (Computation) *)
11+
------ MODULE A --------
12+
VARIABLES x, \* Private to this component.
13+
active \* Shared with component spec B.
14+
vars == <<x,active>>
15+
16+
Type ==
17+
/\ x \in 0..10
18+
/\ active \in [ Nodes -> BOOLEAN ]
19+
20+
Init ==
2721
/\ x = 0
28-
/\ z = TRUE
29-
30-
NextA ==
31-
/\ x < 6
32-
/\ x' = x + 1
33-
/\ z' = ~ z
22+
/\ active \in [ Nodes -> BOOLEAN ]
23+
24+
Next ==
25+
\* Not all nodes are inactive.
26+
/\ \E i \in DOMAIN active : active[i] = TRUE
27+
\* Mimic some computation.
28+
/\ x' \in 1..10
29+
\* Computation changed the activation of 0 to N nodes.
30+
/\ active' \in [ Nodes -> BOOLEAN ]
3431

3532
==================================
3633

37-
(* COMPONENT Spec B *)
38-
VARIABLES x
39-
varsB == <<x>>
34+
(* COMPONENT Spec B (Safra's termination detection) *)
35+
------------ MODULE B ------------
36+
VARIABLES active, \* Shared with component A.
37+
inactive \* Shared with component C.
38+
vars == <<inactive, active>>
4039

41-
\* ++Observation: This is most likely not the original Init predicate of a
42-
\* standalone B component, unless perhaps we consider spec A
43-
\* the environment of spec B. In this particular example,
44-
\* InitB is superfluouos anyway. However, if one would want
45-
\* to prove something about spec B, we probably need an init
46-
\* predicate (=> Conjoining Specifications).
47-
InitB ==
48-
/\ x \in Nat \* Spec B may starts with x being any natural number,
49-
\* which is where A left off.
40+
Type ==
41+
/\ inactive \subseteq Nodes
42+
/\ active \in [ Nodes -> BOOLEAN ]
5043

51-
NextB ==
52-
/\ x < 10
53-
/\ x' = x + 1
44+
Init ==
45+
/\ inactive = {}
46+
/\ active \in [ Nodes -> BOOLEAN ]
47+
48+
Next ==
49+
\* Since this high-level composition abstracts away communication,
50+
\* we could abstract termination detection into a single step:
51+
\* /\ \A i \in DOMAIN active : active[i] = FALSE
52+
\* /\ inactive' = Nodes
53+
\* However, we want to model the possible interleavings of the
54+
\* A and B spec.
55+
/\ \E i \in DOMAIN active:
56+
active[i] = FALSE /\ i \notin inactive
57+
/\ inactive' = inactive \cup {
58+
CHOOSE i \in DOMAIN active:
59+
active[i] = FALSE /\ i \notin inactive
60+
}
61+
/\ UNCHANGED active
62+
63+
==================================
5464

55-
-----------------------------------------------------------------------------
65+
(* COMPONENT Spec C (orderly/graceful shutdown) *)
66+
------------ MODULE C ------------
67+
VARIABLES inactive \* Shared with component spec B.
68+
vars == <<inactive>>
5669

57-
(* This *extends* component spec B to defines what happens to the variables
58-
in spec A, which are not defined in B, when B takes a step. *)
59-
VARIABLES restOfTheUniverse
70+
Type ==
71+
/\ inactive \subseteq Nodes
6072

61-
\* Note that TLC doesn't complain about restOfTheUniverse
62-
\* not appearing in InitB.
63-
OpenNextB ==
64-
/\ NextB
65-
/\ UNCHANGED <<restOfTheUniverse>>
73+
Init ==
74+
/\ inactive \subseteq Nodes
6675

76+
IOExit == TRUE \* Shutdown via sys.exit
77+
78+
Next ==
79+
/\ inactive = Nodes
80+
/\ UNCHANGED inactive
81+
/\ IOExit
82+
==================================
83+
84+
-----------------------------------------------------------------------------
85+
86+
(* Component specification. *)
87+
VARIABLES x, active, inactive
6788
vars ==
68-
<<x,restOfTheUniverse>>
89+
<<inactive, x, active>>
90+
91+
A == INSTANCE A
92+
B == INSTANCE B
93+
C == INSTANCE C
94+
95+
TypeOK ==
96+
/\ A!Type
97+
/\ B!Type
98+
/\ C!Type
99+
100+
Init ==
101+
/\ A!Init
102+
/\ B!Init
103+
/\ C!Init
104+
105+
\* PlusPy will most certainly not be able to evaluate this
106+
\* Next formula. Might have to introduce an auxiliary variable
107+
\* that represents the phase/stage of composed system.
108+
Next ==
109+
\/ /\ ENABLED A!Next
110+
/\ [A!Next]_vars
111+
/\ UNCHANGED <<inactive>>
112+
\/ /\ ENABLED B!Next
113+
/\ [B!Next]_vars
114+
/\ UNCHANGED <<x>>
115+
\/ /\ [C!Next]_vars
116+
/\ UNCHANGED <<x, active>>
117+
118+
Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
69119

70-
(* Composition of A and B (A /\ B) *)
71-
(* Down here we know about the internals *)
72-
(* of spec A and B (whitebox component). *)
120+
THEOREM Spec => []TypeOK
73121

74-
INSTANCE A WITH z <- restOfTheUniverse
122+
(* The system eventually converges to shutdown. This, however, does
123+
*not* hold because component spec A could keep computing forever. *)
124+
AlwaysShutdown ==
125+
<>[][C!Next]_vars
75126

76-
Spec == InitA /\ InitB /\ [][ IF ENABLED NextA THEN [NextA]_vars
77-
ELSE [OpenNextB]_vars
78-
]_vars
127+
(* Unless all nodes are inactive at startup, some computation will occur. *)
128+
ComputationIfSomeActive ==
129+
[n \in Nodes |-> FALSE] # active => <>[](x \in 1..10)
130+
THEOREM Spec => ComputationIfSomeActive
79131

80-
Inv == x \in 0..10
81-
THEOREM Spec => Inv
132+
(* Iff - from some point onward - all nodes will become
133+
inactive, the composed system will eventually shutdown. *)
134+
ShutdownIfNoComputation ==
135+
<>[][~ A!Next]_vars => <>[][C!Next]_vars
136+
THEOREM Spec => ShutdownIfNoComputation
82137

83-
\* Not a theorem due to no fairness constraint.
84-
Live ==
85-
<>[](x = 10)
86138
=============================================================================
87139
\* Modification History
88-
\* Last modified Fri Jun 12 17:34:09 PDT 2020 by markus
140+
\* Last modified Mon Jun 15 17:37:21 PDT 2020 by markus
89141
\* Last modified Fri Jun 12 16:30:19 PDT 2020 by Markus Kuppe
90142
\* Created Fri Jun 12 10:30:09 PDT 2020 by Leslie Lamport

0 commit comments

Comments
 (0)