Skip to content

Instantly share code, notes, and snippets.

@lemmy
Created August 3, 2020 19:43
Show Gist options
  • Save lemmy/fe3bc8b8bce34114a584452190253a9b to your computer and use it in GitHub Desktop.
Save lemmy/fe3bc8b8bce34114a584452190253a9b to your computer and use it in GitHub Desktop.
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 (PCal = d21f99706781a9eecbdc2ab93a3c7d7e)
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 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] \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 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 (TLA # 4de58148791b78177655a347267e50c7)
(***************************************************************************)
(* 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)
=============================================================================
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment