I‘ve posted 3 specifications of the echo algorithms to the models repository. They are meant to play with Alloy6.
Here the idea of the algorithm:
The echo algorithm constructs a spanning tree in a connected undirected graph. We consider the nodes of the graph as agents. An agent has a unique id. It can send messages to its neighbors. The nodes cooperate by the following protocol to construct the tree, see e.g. Chap. 4.3 in: Wan Fokkik Distributed algorithms: an intuitive approach, MIT Press, 2018.
One of the nodes is chosen at random to begin the protocol. This the initiator. The other nodes are called participants. The initiator will end up being the root of the spannung tree. It initiates the protocol by sending its own id to each neighbor.
Each participant checks its inbox and, if not empty, takes some message from it. If the participant has not yet marked a parent node, the id in this message becomes its parent and it sends its own id to each neighbor except its parent.
When a participant has received messages from each of its neighbors, it sends its id to its parent.
Finally, when the initiator has received an echo from each neighbor, the relation parent of pairs of nodes constructed in the course of the message exchange forms a spanning tree of the graph with the initiator as the root.
I‘ve made 3 specifications of the algorithm
echo,md, echo.thm specifying graphs with a dedicated initiator
echo_reif.md, echo_reif.thm the same graphs with enhanced visualisation in the Alloy Analyzer
echo_var.md, echo_var.thm using graphs without a dedicated initiator letting the model finder choose one.
Hi
thanks for this interesting contribution! I just looked quickly at the first model and I have a few questions/remarks:
I would parenthsize the quantification range in all u: Node - n.neighbors + fp | u.inbox' = u.inbox to be sure that the parser doesn’t recognize Node - (n.neighbors + fp).
The initiate pred calls init, and init is also called in the first state of the trans fact: is this normal?
It seems to me you could state a simpler SpanningTree property as: always (INode.color = Green implies (tree[~parent] and rootedAt[~parent, INode])) (or always (INode.color = Green implies eventually (tree[~parent] and rootedAt[~parent, INode]))?
Your first point. I changed all u: Node - n.neighbors + fp | u.inbox' = u.inbox
to all u: (Node - n.neighbors) + fp | unchanged[u.inbox]
That’s in branch patch1.
Your second point.
An alternative approach would be
fact trans {
initiate
after always {
some n, msg: Node | forward[n, msg] or
some n: Node | echo[n] or
stutter
}
}
because the first step has to be initiate. But rather for didactic reasons I thought I would use the scheme (1) define the initial state and (2) then specify with an always all possible state transitions.
Do you think the other approach is better, or is there even another possibility?
In the variant specification echo_var.md I had to perform the initiate as explicit first step, because I let the model finder choose the initial node.
Your third point. I agree: your formula is much simpler!
I changed this in branch patch2.
First, let me just say I think this is an excellent example for Alloy 6, as correctness of the protocol is checked at once for all arbitrary network configuration up to the defined scope.
I think you can keep the initiate (without the init predicate call) as a “normal” event inside the always (without the after). If I understood correctly the protocol, without any guard that would mean that initiate could occur more than once, but subsequent occurrences would be indistinguishable from stuttering and would not affect the correctness of the protocol. Also, before initiate occurs the other events cannot occur because of the respective guards.
But if you really want initiate to occur only once you have to somehow memorize that it already occurred. For example, you could add a var sig Initiated in INode {} that records whether INode has already initiated (initially empty), and add guard no Initiated and effect some Initiated' to event initiate.