# AlloyTools/models/algorithms/echo

**URL:** <https://alloytools.discourse.group/t/alloytools-models-algorithms-echo/223>\
**Category:** models\
**Created:** [February 13, 2022, 8:33am UTC](https://alloytools.discourse.group/t/alloytools-models-algorithms-echo/223 "2022-02-13T08:33:40Z")\
**Posts on this page:** 6\
**Page:** 1

<div class="post-metadata">

**Author:** ![esb-dev](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/esb-dev/32/63_2.png) [@esb-dev](https://alloytools.discourse.group/u/esb-dev)\
**Post date:** [February 13, 2022, 8:33am UTC](https://alloytools.discourse.group/t/alloytools-models-algorithms-echo/223/1 "2022-02-13T08:33:40Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![peter.kriens](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/peter.kriens/32/3_2.png) [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\
**Post date:** [February 13, 2022, 3:58pm UTC](https://alloytools.discourse.group/t/alloytools-models-algorithms-echo/223/2 "2022-02-13T15:58:14Z")

</div>

You can find the models here: [models/algorithms/echo at master · AlloyTools/models · GitHub](https://github.com/AlloyTools/models/tree/master/algorithms/echo)

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [February 21, 2022, 9:59am UTC](https://alloytools.discourse.group/t/alloytools-models-algorithms-echo/223/3 "2022-02-21T09:59:56Z")

</div>

Hi  
thanks for this interesting contribution! I just looked quickly at the first model and I have a few questions/remarks:

1. 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)`.
2. The `initiate` pred calls `init`, and `init` is also called in the first state of the `trans` fact: is this normal?
3. 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]))`?

---

<div class="post-metadata">

**Author:** ![esb-dev](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/esb-dev/32/63_2.png) [@esb-dev](https://alloytools.discourse.group/u/esb-dev)\
**Post date:** [February 21, 2022, 12:33pm UTC](https://alloytools.discourse.group/t/alloytools-models-algorithms-echo/223/4 "2022-02-21T12:33:49Z")

</div>

Hi David,

I will look at your suggestions as soon as I am back from skiing in the Alpes.

---

<div class="post-metadata">

**Author:** ![esb-dev](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/esb-dev/32/63_2.png) [@esb-dev](https://alloytools.discourse.group/u/esb-dev)\
**Post date:** [March 3, 2022, 2:26pm UTC](https://alloytools.discourse.group/t/alloytools-models-algorithms-echo/223/5 "2022-03-03T14:26:11Z")

</div>

Hi David,

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

```auto
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`.

---

<div class="post-metadata">

**Author:** ![alcino](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/alcino/32/25_2.png) [@alcino](https://alloytools.discourse.group/u/alcino)\
**Post date:** [March 8, 2022, 9:33am UTC](https://alloytools.discourse.group/t/alloytools-models-algorithms-echo/223/6 "2022-03-08T09:33:51Z")

</div>

Hi,

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.

> [@esb-dev](#):
>
> Your second point.  
> An alternative approach would be
> 
> ```auto
> 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?

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`.

Best,  
Alcino