---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/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] = @ \union {[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] \union {[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 55, 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] \union {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 70, 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 \union {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) \union {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