201 lines
8.3 KiB
Plaintext
201 lines
8.3 KiB
Plaintext
(* 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 |