test.tla

(* Example taken from https://github.com/tlaplus/Examples/blob/master/specifications/echo/Echo.tla *)
-------------------------------- MODULE Echo --------------------------------
(***************************************************************************)
(* The Echo algorithm for constructing a spanning tree in an undirected *)
(* graph starting from a single initiator, as a PlusCal algorithm. *)
(***************************************************************************)
EXTENDS Naturals, FiniteSets, Relation, TLC
CONSTANTS Node, \* set of nodes
 initiator, \* single initiator, will be the root of the tree
 R \* neighborhood relation, represented as a Boolean function over nodes 
ASSUME /\ initiator \in Node
 /\ R \in [Node \X Node -> BOOLEAN]
 \* No edge from a node to itself (self-loops).
 /\ IsIrreflexive(R, Node)
 \* Undirected graph (there exists an edge from b 
 \* to a if there exists an edge from a to b).
 /\ IsSymmetric(R, Node)
 \* There exists a spanning tree consisting of *all* nodes.
 \* (no forest of spanning trees). 
 /\ IsConnected(R, Node)
NoNode == CHOOSE x : x \notin Node
neighbors(n) == { m \in Node : R[m,n] }
(**
--algorithm Echo {
 variable inbox = [n \in Node |-> {}]; \* model communication between nodes
 define { \* sending and receiving messages
 \* network obtained from net when p sends message of kind knd to q
 send(net, p, q, knd) == [net EXCEPT ![q] = @ \cup {[kind |-> knd, sndr |-> p]}]
 \* network obtained from net when p receives a message
 receive(net, p, msg) == [net EXCEPT ![p] = @ \ {msg}]
 \* network obtained from net when p send message of kind knd to all nodes in dest
 multicast(net, p, dest, knd) ==
 [m \in Node |-> IF m \in dest THEN net[m] \cup {[kind |-> knd, sndr |-> p]}
 ELSE net[m]]
 }
 process (node \in Node) 
 variables parent = NoNode,
 children = {},
 rcvd = 0,
 nbrs = neighbors(self); {
 n0: if (self = initiator) {
 \* initiator sends first message to all its neighbors
 inbox := multicast(inbox, self, nbrs, "m")
 };
 n1: while (rcvd < Cardinality(nbrs)) {
 \* receive some message from a neighbor
 with (msg \in inbox[self],
 net = receive(inbox, self, msg)) {
 rcvd := rcvd+1;
 if (self # initiator /\ rcvd = 1) {
 assert(msg.kind = "m"); \* the first received message is always of type "m"
 \* note the sender as the node's parent and send an "m" message to all remaining neighbors
 parent := msg.sndr;
 inbox := multicast(net, self, nbrs \ {msg.sndr}, "m")
 }
 else {
 \* subsequent messages are counted but don't give rise to another message
 inbox := net
 };
 if (msg.kind = "c") { children := children \cup {msg.sndr} }
 } \* end with
 }; \* end while
 n2: if (self # initiator) {
 \* when non-initiator has received messages from all neighbors, acknowledge
 \* child relationship to the parent
 assert(parent \in nbrs);
 inbox := send(inbox, self, parent, "c")
 }
 } \* end process
}
**)
\* BEGIN TRANSLATION
VARIABLES inbox, pc
(* define statement *)
send(net, p, q, knd) == [net EXCEPT ![q] = @ \cup {[kind |-> knd, sndr |-> p]}]
receive(net, p, msg) == [net EXCEPT ![p] = @ \ {msg}]
multicast(net, p, dest, knd) ==
 [m \in Node |-> IF m \in dest THEN net[m] \cup {[kind |-> knd, sndr |-> p]}
 ELSE net[m]]
VARIABLES parent, children, rcvd, nbrs
vars == << inbox, pc, parent, children, rcvd, nbrs>>
ProcSet == (Node)
Init == (* Global variables *)
 /\ inbox = [n \in Node |-> {}]
 (* Process node *)
 /\ parent = [self \in Node |-> NoNode]
 /\ children = [self \in Node |-> {}]
 /\ rcvd = [self \in Node |-> 0]
 /\ nbrs = [self \in Node |-> neighbors(self)]
 /\ pc = [self \in ProcSet |-> "n0"]
n0(self) == /\ pc[self] = "n0"
 /\ IF self = initiator
 THEN /\ inbox' = multicast(inbox, self, nbrs[self], "m")
 ELSE /\ TRUE
 /\ inbox' = inbox
 /\ pc' = [pc EXCEPT ![self] = "n1"]
 /\ UNCHANGED << parent, children, rcvd, nbrs>>
n1(self) == /\ pc[self] = "n1"
 /\ IF rcvd[self] < Cardinality(nbrs[self])
 THEN /\ \E msg \in inbox[self]:
 LET net == receive(inbox, self, msg) IN
 /\ rcvd' = [rcvd EXCEPT ![self] = rcvd[self]+1]
 /\ IF self # initiator /\ rcvd'[self] = 1
 THEN /\ Assert((msg.kind = "m"), 
 "Failure of assertion at line 50, column 16.")
 /\ parent' = [parent EXCEPT ![self] = msg.sndr]
 /\ inbox' = multicast(net, self, nbrs[self] \ {msg.sndr}, "m")
 ELSE /\ inbox' = net
 /\ UNCHANGED parent
 /\ IF msg.kind = "c"
 THEN /\ children' = [children EXCEPT ![self] = children[self] \cup {msg.sndr}]
 ELSE /\ TRUE
 /\ UNCHANGED children
 /\ pc' = [pc EXCEPT ![self] = "n1"]
 ELSE /\ pc' = [pc EXCEPT ![self] = "n2"]
 /\ UNCHANGED << inbox, parent, children, rcvd>>
 /\ nbrs' = nbrs
n2(self) == /\ pc[self] = "n2"
 /\ IF self # initiator
 THEN /\ Assert((parent[self] \in nbrs[self]), 
 "Failure of assertion at line 65, column 10.")
 /\ inbox' = send(inbox, self, parent[self], "c")
 ELSE /\ TRUE
 /\ inbox' = inbox
 /\ pc' = [pc EXCEPT ![self] = "Done"]
 /\ UNCHANGED << parent, children, rcvd, nbrs>>
node(self) == n0(self) \/ n1(self) \/ n2(self)
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
 /\ UNCHANGED vars
Next == (\E self \in Node: node(self))
 \/ Terminating
Spec == Init /\ [][Next]_vars
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* END TRANSLATION
(***************************************************************************)
(* Correctness properties. *)
(***************************************************************************)
TypeOK ==
 /\ parent \in [Node -> (Node \cup {NoNode})]
 /\ children \in [Node -> SUBSET Node]
 /\ rcvd \in [Node -> Nat]
 /\ nbrs \in [Node -> SUBSET Node]
 /\ \A n \in Node : nbrs[n] = neighbors(n) /\ rcvd[n] <= Cardinality(nbrs[n])
 /\ inbox \in [Node -> SUBSET [kind : {"m","c"}, sndr : Node]]
 /\ \A n \in Node : \A msg \in inbox[n] : msg.sndr \in nbrs[n]
(* The initiator never has a parent *)
InitiatorNoParent == parent[initiator] = NoNode
(* If a node has a parent, it is a neighbor node *)
ParentIsNeighbor == \A n \in Node : parent[n] \in neighbors(n) \cup {NoNode}
(* A node n is a child of node m only if m is the parent of n.
 At the end of the computation, this is "if and only if". *)
ParentChild == \A m,n \in Node :
 /\ n \in children[m] => m = parent[n]
 /\ m = parent[n] /\ pc[m] = "Done" => n \in children[m]
(* Compute the ancestor relation *)
IsParent == [m,n \in Node |-> n = parent[m]]
IsAncestor == TransitiveClosure(IsParent, Node)
(* At the end of the computation, the initiator is an ancestor of every other node
 and the ancestor relation is acyclic.
 Beware: evaluating this property over any but tiny graphs is costly.
*)
AncestorProperties ==
 (\A n \in Node : pc[n] = "Done")
 => LET anc == IsAncestor
 IN /\ \A n \in Node \ {initiator} : anc[n, initiator]
 /\ IsIrreflexive(anc, Node)
=============================================================================
\* Modification History
\* Last modified Wed Jun 17 09:23:17 PDT 2020 by markus
\* Last modified Sun Jun 14 17:11:39 CEST 2020 by merz
\* Created Tue Apr 26 09:42:23 CEST 2016 by merz