# Modelling a state machine in Electrum (towards Alloy 6)

**URL:** <https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88>\
**Category:** Alloy 6\
**Created:** [September 11, 2020, 2:38pm UTC](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88 "2020-09-11T14:38:49Z")\
**Posts on this page:** 1\
**Showing post:** 1

<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:** [September 11, 2020, 2:38pm UTC](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88/1 "2020-09-11T14:38:49Z")

</div>

In this post, I describe the approach we (the Electrum team) follow to devise most of our models of state machines, protocols, etc. This is also to illustrate Electrum now that our [release candidate is ready](https://alloytools.discourse.group/t/new-electrum-release-candidate-towards-alloy-6/87).

Most of this approach is _not new_ as it is based upon work by Leslie Lamport in TLA+ and Daniel Jackson in Alloy. Our main addition is a convenient way to combine a form of modelling that is as expressive as the Alloy “events-as-predicates” idiom and as visualization-friendly as the “events-as-signatures” idiom. We dub it the “event reification” idiom (for want of a better name!).

Let’s consider the leader election protocol studied in Sect. 6.1 of Daniel’s book. Our version is a bit modified to make it more user-friendly, but the overall algorithm is the same. I will not enter into details but focus on the general pattern. Notice however that in this version, only one node does something at a time, for clarity (_interleaving_).

# Structure

First, we describe the system structure. We have nodes with mutable inboxes and outboxes:

```auto
open util/ordering[Id]

sig Node {
	id : one Id,
	succ : one Node,
	var inbox : set Id,
	var outbox : set Id
}

sig Id {}

```

(some additional facts are needed to specify that nodes form a ring…).

# Events

3 events are introduced as predicates. They may have:

- a guard saying when the event is allowed to happen
- an effect on some or all of the state variables (var sigs and fields)
- a frame condition saying what _does not change_.

One of the events (called `skip`) does nothing. One of the reasons it is useful to consider it is that, foe some models, the execution of other events may stop. In that case, the execution trace would be _finite_. However, as Electrum only considers _infinite_ traces, such traces would not be considered by Electrum and we could miss meaningful behaviors. With the `skip` event, such finite traces can “become” infinite by performing `skip` on the last state forever.

```auto
pred send [n : Node] {
	some i : n.outbox {
		// transmit message
		...
	}
	// frame condition
	all m : Node - n.succ | m.inbox' = m.inbox
	all m : Node - n | m.outbox' = m.outbox
}

pred compute [n : Node] { ... }

pred skip {
	inbox' = inbox
	outbox' = outbox
}

```

# Behaviors

We now specify the shape of behaviors. Remark the `some`: in principle, several events may happen at the same time, but due to frame conditions, they will have the same effect and will therefore be indistinguishable.

```auto
fact behaviour {
	// initial conditions
	no inbox
	...
	// execution
	always (skip or some n : Node | send[n] or compute[n])
}

```

# Run

You may now run the Analyzer to look for an instance where some node is elected. Mind the `steps` keyword that replaces `Time` in Alloy and previous versions of Electrum. We ask for traces with as much as 6 steps, including the last step which loops back to a former state or itself.

```auto
pred example { eventually some elected } 
run example for 3 but exactly 3 Node, 6 steps

```

# Event Reification

Until now, we have followed the “events-as-predicates” idiom. For this reason, we can walk along the trace returned by the Analyzer but we must _guess_ which event happened (in each state) as event names aren’t displayed.

Here comes _event reification_!

1. add an enum with as many tags as there are events:

```auto
enum Event { Send, Compute, Skip }

```

1. add _functions_ for every such tag its possible parameter values (use the same name with an underscore in front of it, for instance):

```auto
fun _send : Event -> Node {
	Send -> { n : Node | send[n] }
}

fun _compute : Event -> Node {
	Compute -> { n : Node | compute[n] }
}
fun _skip : Event {
	{ e : Skip | skip }
}

```

1. give a name to the set of event _instances_:

```auto
fun events : set Event {
	(_send + _compute).Node + _skip
}

```

1. Now open the Visualizer and change the theme to your taste. In particular, to see which event(s) happen at a time, do the following:
  - sig Event: Show = Off
  - set $events: Show = On, Show as labels = Off

This way, you will see which events happen as well as their parameters (like `$_send: Node0` in the picture below).

 ![image](https://global.discourse-cdn.com/free1/uploads/alloytools/original/1X/a2527f17b2648ada1359423707ecffec636b4acd.png)

As explained above, several indistinguishable events may be displayed in a given state.

Hope this helps!

---

_[View the full topic](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88)._