-
Notifications
You must be signed in to change notification settings - Fork 200
/
SpanTree.tla
168 lines (158 loc) · 10.6 KB
/
SpanTree.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
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
------------------------------ MODULE SpanTree ------------------------------
(***************************************************************************)
(* This is an algorithm to compute a spanning tree of an undirected graph *)
(* with a given root. Look up "spanning tree" on the Web to see what that *)
(* means. You may find pages for finding spanning trees of graphs with *)
(* weighted edges. The algorithm here effectively assumes each edge has *)
(* weight 1. *)
(* *)
(* A rooted tree is usually described by a set of nodes with a *)
(* parent/child relation, where the root is the oldest ancestor of all *)
(* other nodes. The algorithm computes this relation as a function `mom' *)
(* where mom[n] equals the parent of node n, except that if n is the root *)
(* then mom[n] = n. If the graph is not connected, then the rooted tree *)
(* does not contain nodes of the graph that have no path to the root. *)
(* Such nodes n will have mom[n]=n. *)
(* *)
(* A simple algorithm to compute the rooted spanning tree computes a *)
(* function dist where dist[n] is the distance of node n from the root. *)
(* Initially, dist[n] equals 0 if n is the root and otherwise equals *)
(* infinity. The algorithm repeatedly performs the following action. It *)
(* chooses an arbitrary node n that has a neighbor m such that dist[n] > *)
(* dist[m]+1, and it sets dist[n] to dist[m]+1. *)
(* *)
(* For simplicity, we assume that we're also given a number MaxCardinality *)
(* that's greater than or equal to the number of nodes, and we use *)
(* MaxCardinality instead of infinity. For a reason to be given below, we *)
(* also modify the algorithm as follows. For a node n with dist[n] > *)
(* dist[m}+1, instead of setting dist[n] to dist[m]+1 the algorithm sets *)
(* it to an arbitrary number d such that dist[n] > d >= dist[m} + 1. *)
(***************************************************************************)
EXTENDS Integers, FiniteSets
(***************************************************************************)
(* We represent the graph by a set of Nodes of nodes and a set Edges of *)
(* edges. We assume that there are no edges from a node to itself and *)
(* there is at most one edge joining any two nodes. We represent an edge *)
(* joining nodes m and n by the set {m, n}. We let Root be the root node. *)
(***************************************************************************)
CONSTANTS Nodes, Edges, Root, MaxCardinality
(***************************************************************************)
(* This assumption asserts mathematically what we are assuming about the *)
(* constants. *)
(***************************************************************************)
ASSUME /\ Root \in Nodes
/\ \A e \in Edges : (e \subseteq Nodes) /\ (Cardinality(e) = 2)
/\ MaxCardinality \in Nat
/\ MaxCardinality >= Cardinality(Nodes)
(***************************************************************************)
(* This defines Nbrs(n) to be the set of neighbors of node n in the *)
(* graph--that is, the set of nodes joined by an edge to n. *)
(***************************************************************************)
Nbrs(n) == {m \in Nodes : {m, n} \in Edges}
(***************************************************************************)
(* The spec is a straightforward TLA+ spec of the algorithm described *)
(* above. *)
(***************************************************************************)
VARIABLES mom, dist
vars == <<mom, dist>>
TypeOK == /\ mom \in [Nodes -> Nodes]
/\ dist \in [Nodes -> Nat]
Init == /\ mom = [n \in Nodes |-> n]
/\ dist = [n \in Nodes |-> IF n = Root THEN 0 ELSE MaxCardinality]
Next == \E n \in Nodes :
\E m \in Nbrs(n) :
/\ dist[m] < 1 + dist[n]
/\ \E d \in (dist[m]+1) .. (dist[n] - 1) :
/\ dist' = [dist EXCEPT ![n] = d]
/\ mom' = [mom EXCEPT ![n] = m]
Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
(************************************************************************)
(* The formula WF_vars(Next) asserts that a behavior must not stop if *)
(* it's possible to take a Next step. Thus, the algorithm must either *)
(* terminate (because Next equals FALSE for all values of dist' and *)
(* mom') or else it continues taking Next steps forever. Don't worry *)
(* about it if you haven't learned how to express liveness in TLA+. *)
(************************************************************************)
-----------------------------------------------------------------------------
(***************************************************************************)
(* A direct mathematical definition of exactly what the function mom *)
(* should be is somewhat complicated and cannot be efficiently evaluated *)
(* by TLC. Here is the definition of a postcondition (a condition to be *)
(* satisfied when the algorithm terminates) that implies that mom has the *)
(* correct value. *)
(***************************************************************************)
PostCondition ==
\A n \in Nodes :
\/ /\ n = Root
/\ dist[n] = 0
/\ mom[n] = n
\/ /\ dist[n] = MaxCardinality
/\ mom[n] = n
/\ \A m \in Nbrs(n) : dist[m] = MaxCardinality
\/ /\ dist[n] \in 1..(MaxCardinality-1)
/\ mom[n] \in Nbrs(n)
/\ dist[n] = dist[mom[n]] + 1
(***************************************************************************)
(* ENABLED Next is the TLA+ formula that is true of a state iff (if and *)
(* only if) there is a step satisfying Next starting in the state. Thus, *)
(* ~ ENABLED Next asserts that the algorithm has terminated. The safety *)
(* property that algorithm should satisfy, that it's always true that if *)
(* the algorithm has terminated then PostCondition is true, is asserted by *)
(* this formula. *)
(***************************************************************************)
Safety == []((~ ENABLED Next) => PostCondition)
(***************************************************************************)
(* This formula asserts the liveness condition that the algorithm *)
(* eventually terminates *)
(***************************************************************************)
Liveness == <>(~ ENABLED Next)
-----------------------------------------------------------------------------
(***************************************************************************)
(* These properties of the spec can be checked with the model that should *)
(* have come with this file. That model has TLC check the algorithm *)
(* satisfies properties Safety and Liveness for a single simple graph with *)
(* 6 nodes. You should clone that model and change it to try a few *)
(* different graphs. However, this is tedious. There are two better ways *)
(* to have TLC check the spec. The best is to try it on all graphs with a *)
(* given number of nodes. The spec with root file SpanTreeTest does this. *)
(* It can very quickly check all graphs with 4 nodes. It takes about 25 *)
(* minutes on my laptop to check all graphs with 5 nodes. TLC will *)
(* probably run out of space after running for a long time if I tried it *)
(* for all graphs with 6 nodes. The spec SpanTreeRandom tests the *)
(* algorithm for a randomly chosen graph with a given set of nodes. This *)
(* allows you easily to repeatedly check different graphs. *)
(* *)
(* As a problem, you can now specify an algorithm that is a distributed *)
(* implementation of this algorithm. We can view the algorithm in the *)
(* current module as one in which a node n sets its value of dist[n] by *)
(* directly reading the values of dist[m] from all its neighbors m. Your *)
(* problem is to write an algorithm in which nodes learn the values of *)
(* dist[m] from a neighbor m by receiving messages sent by m. The root r *)
(* sends an initial message informing its neighbors that dist[r] = 0. *)
(* Subsequently, each node n sends a message containing dist[n] to all its *)
(* neighbors whenever its value of dist[n] changes. *)
(* *)
(* Your algorithm should have variables mom and dist that implement the *)
(* variables of the same name in the current algorithm. (Hence, it should *)
(* implement the current algorithm with a trivial refinement mapping *)
(* assigning to every variable and constant the variable or constant of *)
(* the same name.) You can use TLC to check that your algorithm does *)
(* indeed implement the algorithm in the current module. *)
(* *)
(* You may not know how to write a suitable liveness condition for your *)
(* algorithm. (To find out how, you would have to look through the *)
(* available TLA+ documentation.) In that case, just write a safety *)
(* specification of the form Init /\ [][Next]_vars and modify formula Spec *)
(* of the current module by comment out the /\ WF_vars(Next) conjunction *)
(* so it too becomes a safey spec. *)
(* *)
(* *)
(* When writing your algorithm, you should realize why the Next action in *)
(* the current module doesn't just set dist[n] to dist[m] + 1 rather than *)
(* allowing it to be set to any value in (dist[m]+1) .. (dist[n]-1) . If *)
(* you don't see why, use TLC to find out for you. *)
(***************************************************************************)
=============================================================================
\* Modification History
\* Last modified Mon Jun 17 05:52:09 PDT 2019 by lamport
\* Created Fri Jun 14 03:07:58 PDT 2019 by lamport