Added Leslie's Spanning Tree Excercise

README.md

@@ -76,6 +76,7 @@ Do you have your own case study that you like to share with the community? Send
 | 62 | Misra Reachability Algorithm | <a href="https://github.com/tlaplus/Examples/tree/master/specifications/MisraReachability">Misra Reachability Algorithm</a> | Leslie Lamport | &#10004;  | &#10004; | Int, Seq, FiniteSets, TLC, TLAPS, NaturalsInduction | 
 | 63 | Loop Invariance | <a href="https://github.com/tlaplus/Examples/tree/master/specifications/LoopInvariance">Loop Invariance</a> | Leslie Lamport | &#10004;  | &#10004; | Int, Seq, FiniteSets, TLC, TLAPS, SequenceTheorems, NaturalsInduction | 
 | 64 | Teaching Concurrency | <a href="https://github.com/tlaplus/Examples/tree/master/specifications/TeachingConcurrency">Teaching Concurrency</a> | Leslie Lamport | &#10004;  | &#10004; | Int, TLAPS | 
+| 64 | Spanning Tree | <a href="https://github.com/tlaplus/Examples/tree/master/specifications/SpanningTree">Spanning Tree</a> | Leslie Lamport |  | &#10004; | Int, FiniteSets, TLC, Randomization | 
 
 
 ## License

specifications/SpanningTree/README.txt

@@ -0,0 +1,34 @@
+TLA+ Exercises for your first steps to winning a Turing award.
+
+Leslie Lamport
+last modified on Mon 17 June 2019 at  5:09:56 PST by lamport
+
+------------------------------------------------------------------------
+The specification SpanTree contains a spec that's an abstract,
+non-distributed version of the algorithm in the paper "An Assertional
+Correctness Proof of a Distributed Program", available here:
+
+   http://lamport.azurewebsites.net/pubs/pubs.html#dist
+
+The SpanTree spec bears the same relation to the algorithm in that
+paper as the Voting spec bears to the Paxos consensus spec.  Your
+problem is to write the TLA+ spec of the distributed algorithm and use
+TLC to check that it implements the SpanTree spec.  
+
+The SpanTree spec contains a liveness condition as well as the kind of
+safety condition you've seen in the lectures and in the three Paxos
+specs.  If you can figure out how to express the appropriate liveness
+condition for the distributed algorithm, then you can be quite sure
+that your algorithm is correct if TLC shows that it implements the
+SpanTree spec for a large enough model.  Otherwise, you will have to
+write a safety spec of the distributed algorithm and modify the
+SpanTree spec to remove its liveness condition.  You should then check
+that TLC finds any error that you introduce in your spec.  (A spec
+that allows no behaviors implements any safety spec.)
+
+Remember to first test your spec on really tiny networks.
+
+
+
+
+

specifications/SpanningTree/SpanTree.tla

@@ -0,0 +1,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 algorith 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

specifications/SpanningTree/SpanTree.toolbox/.project

@@ -0,0 +1,24 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+	<name>SpanTree</name>
+	<comment></comment>
+	<projects>
+	</projects>
+	<buildSpec>
+		<buildCommand>
+			<name>toolbox.builder.TLAParserBuilder</name>
+			<arguments>
+			</arguments>
+		</buildCommand>
+	</buildSpec>
+	<natures>
+		<nature>toolbox.natures.TLANature</nature>
+	</natures>
+	<linkedResources>
+		<link>
+			<name>SpanTree.tla</name>
+			<type>1</type>
+			<locationURI>PARENT-1-PROJECT_LOC/SpanTree.tla</locationURI>
+		</link>
+	</linkedResources>
+</projectDescription>

specifications/SpanningTree/SpanTree.toolbox/.settings/org.lamport.tla.toolbox.prefs

@@ -0,0 +1,2 @@
+ProjectRootFile=PARENT-1-PROJECT_LOC/SpanTree.tla
+eclipse.preferences.version=1

specifications/SpanningTree/SpanTree.toolbox/SpanTree___Model_1.launch

@@ -0,0 +1,35 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
+    <stringAttribute key="configurationName" value="Model_1"/>
+    <intAttribute key="distributedFPSetCount" value="0"/>
+    <stringAttribute key="distributedNetworkInterface" value="100.64.12.255"/>
+    <intAttribute key="distributedNodesCount" value="1"/>
+    <stringAttribute key="distributedTLC" value="off"/>
+    <intAttribute key="fpIndex" value="0"/>
+    <intAttribute key="maxHeapSize" value="25"/>
+    <stringAttribute key="modelBehaviorInit" value=""/>
+    <stringAttribute key="modelBehaviorNext" value=""/>
+    <stringAttribute key="modelBehaviorSpec" value="Spec"/>
+    <intAttribute key="modelBehaviorSpecType" value="1"/>
+    <stringAttribute key="modelBehaviorVars" value="mom, dist"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="false"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1TypeOK"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="1Safety"/>
+        <listEntry value="1Liveness"/>
+    </listAttribute>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="Edges;;{{n1, n2}, {n1, n3}, {n2, n3}, {n2, n4}, {n3, n4}, {n3, n5}, {n4, n5}};0;0"/>
+        <listEntry value="MaxCardinality;;6;0;0"/>
+        <listEntry value="Nodes;;{n1, n2, n3, n4, n5};1;0"/>
+        <listEntry value="Root;;n1;0;0"/>
+    </listAttribute>
+    <intAttribute key="numberOfWorkers" value="2"/>
+    <stringAttribute key="result.mail.address" value=""/>
+    <stringAttribute key="specName" value="SpanTree"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+</launchConfiguration>