# 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:** 18\
**Page:** 2

<div class="post-metadata">

**Author:** ![steve.freeman](https://avatars.discourse-cdn.com/v4/letter/s/2acd7d/32.png) [@steve.freeman](https://alloytools.discourse.group/u/steve.freeman)\
**Post date:** [September 15, 2020, 9:12am UTC](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88/21 "2020-09-15T09:12:51Z")

</div>

Damn, that’s subtle. The `commands` function introduces new instances of the Command sig into the “environment”, which have to be matched.  
And the name of the function and the leading underbars are just conventions that have no significance.

---

<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 15, 2020, 9:16am UTC](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88/22 "2020-09-15T09:16:50Z")

</div>

I’m not sure to understand what’s meant by “wiring up” here.

You don’t need the “commands” function to make the model work. You need it to be able to easily say which commands should be displayed in the Visualizer. Indeed, in Alloy, every function without parameters yields a set that can be themed in the Visualizer.

Here, “commands” returns the set of commands that are “fired”: the Visualizer evaluates it in every state. This way, you can theme your visualization by (1) saying you don’t want to display _all_ commands (`sig Command: Show = Off`) but (2) only those that are fired in the current state (`set $commands: Show = On`).

Notice this is plain Alloy, but I’ll admit it’s subtle at first. And yes, underscores are only a convention.

---

<div class="post-metadata">

**Author:** ![keithb\_b](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/keithb_b/32/7_2.png) [@keithb\_b](https://alloytools.discourse.group/u/keithb_b)\
**Post date:** [September 15, 2020, 9:22am UTC](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88/23 "2020-09-15T09:22:52Z")

</div>

That’s my understanding. The revelatory thing here is that a `fun` isn’t a delayed expression (there’s a `let` form for that), it’s a set of tuples of a certain shape. A `fun` seems to be more concrete than a `sig`.

---

<div class="post-metadata">

**Author:** ![keithb\_b](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/keithb_b/32/7_2.png) [@keithb\_b](https://alloytools.discourse.group/u/keithb_b)\
**Post date:** [September 15, 2020, 9:33am UTC](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88/24 "2020-09-15T09:33:03Z")

</div>

> [@grayswandyr](#):
>
> You don’t need the “commands” function to make the model work. You need it to be able to easily say which commands should be displayed in the Visualizer.

That’s what I mean by wiring up. The model worked as well as ever it did without the `Command`s.

---

<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 15, 2020, 9:44am UTC](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88/25 "2020-09-15T09:44:00Z")

</div>

> [@steve.freeman](#):
>
> The `commands` function introduces new instances of the Command sig into the “environment”, which have to be matched.

> [@keithb\_b](#):
>
> The revelatory thing here is that a `fun` isn’t a delayed expression (there’s a `let` form for that), it’s a set of tuples of a certain shape. A `fun` seems to be more concrete than a `sig` .

A `fun` is simply an expression with a name and, possibly, parameters. Similarly a `pred` is simply a _constraint_ with a name and, possibly, parameters. So to speak, both are parametrized shortcuts.

A `sig` represents a set (of atoms). But if you think of `fun`s without parameters, it also represents a set. Therefore, as the Visualizer knows how to theme _sets_, it can theme `sig`s as muchs as parameter-less `fun`s.

Also, as Electrum instances are traces (= sequences of states), the value of any set (except those known to be constant) may change in every state.

Now, in the Visualizer, you don’t want to represent the set of all possible commands, in general. You _only_ want to represent the set of commands that happen in a given state that you’re currently displaying. Which is what `commands` yields.

---

<div class="post-metadata">

**Author:** ![keithb\_b](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/keithb_b/32/7_2.png) [@keithb\_b](https://alloytools.discourse.group/u/keithb_b)\
**Post date:** [September 15, 2020, 10:02am UTC](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88/26 "2020-09-15T10:02:57Z")

</div>

> [@alcino](#):
>
> do you want `locked` and `unlocked` to always be disjoint for a given vehicle?

Yes.

> [@](#):
>
> If that is the case, your declaration does not ensure that.

No, I see that now, although the predicates do seem to. And the reason I think that is that I’ve never seen an instance where the rule doesn’t hold.

So, while this:

> [@](#):
>
> ```
> check {
> always all v : Vehicle | no v.locked & v.unlocked
> }
> 
> ```

can create a counter-example, if I include it in the trace the run is fine. Which is interesting.

However, my misunderstanding about the use of `disj` is the reason that models with multiple vehicles don’t work, so thanks for explaining that.

---

<div class="post-metadata">

**Author:** ![keithb\_b](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/keithb_b/32/7_2.png) [@keithb\_b](https://alloytools.discourse.group/u/keithb_b)\
**Post date:** [September 15, 2020, 10:09am UTC](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88/27 "2020-09-15T10:09:35Z")

</div>

> [@grayswandyr](#):
>
> A `fun` is simply an expression with a name and, possibly, parameters.

Yes, but given the way they behave, it doesn’t seem to be _delayed_, hanging around unevaluated, waiting to be instantiated as a stack frame or activation record in the way that a function in a functional language or a procedure in a procedural language are.

---

<div class="post-metadata">

**Author:** ![steve.freeman](https://avatars.discourse-cdn.com/v4/letter/s/2acd7d/32.png) [@steve.freeman](https://alloytools.discourse.group/u/steve.freeman)\
**Post date:** [September 15, 2020, 10:24am UTC](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88/28 "2020-09-15T10:24:02Z")

</div>

> [@grayswandyr](#):
>
> Now, in the Visualizer, you don’t want to represent the set of all possible commands, in general. You _only_ want to represent the set of commands that happen in a given state that you’re currently displaying. Which is what `commands` yields.

This is the head-banging bit for us old-school coders.

My next thought is that, in our world, repeated patterns like this are often a hint of missing features.

---

<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 15, 2020, 10:40am UTC](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88/29 "2020-09-15T10:40:13Z")

</div>

> [@steve.freeman](#):
>
> This is the head-banging bit for us old-school coders.

Well I think it’s pretty normal. As you said, this is subtle. I should add however that Daniel’s book, even if on Alloy 4 only, is very helpful to understand a lot of this. There is also some work coming for Alloy 6/Electrum.

> [@steve.freeman](#):
>
> My next thought is that, in our world, repeated patterns like this are often a hint of missing features.

Absolutely.  
We had a prototype for this for a former version of Electrum but it was too limited and a bit bogus. More importantly, we decided to retain the freedom and “declarativeness” of Alloy on purpose, when we submitted Electrum.

We will propose an extension for state machine modelling in the future and it will, in particular, handle these patterns automatically.

---

<div class="post-metadata">

**Author:** ![steve.freeman](https://avatars.discourse-cdn.com/v4/letter/s/2acd7d/32.png) [@steve.freeman](https://alloytools.discourse.group/u/steve.freeman)\
**Post date:** [September 15, 2020, 11:26am UTC](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88/30 "2020-09-15T11:26:13Z")

</div>

Here’s my new version of the cards problem. It seems to be getting more compact, which is nice.

I used the guard clause in `cancel` to make sure I have the right cards, rather than filtering up front (counterintuitive to me). In principle, I could have just passed in the target card to cancel, but I wanted the visualiser to show me its replacement as well. I might change my mind on this.

```
enum Status { unissued, issued, cancelled }

sig Card {
  var status : Status 
}
sig Customer { 
  var cards: disj some Card 
}

// ---- events ----
pred cancel[toCancel, replacement: Card] {
	toCancel in Customer.cards
  replacement in status.unissued

  let customer = cards.toCancel {
    status' = (status ++ toCancel->cancelled) ++ replacement->issued
    cards' = cards - customer->toCancel + customer->replacement
  }
}

pred skip {
  status' = status
  cards' = cards
}

// ---- reification ----
enum Event { Cancel, Skip }
fun _cancel : Event -> Card -> Card {
  Cancel -> { card, replacement: Card | cancel[card, replacement] }
}
fun _skip : Event { 
  {event : Skip | skip} 
}
fun events : set Event {
  _cancel.Card.Card + _skip
}

// ---- behaviours ----
pred init {
  no status.cancelled
  #status.unissued > 1
  all customer: Customer | some customer.cards
  status.issued = Customer.cards 
}

fact traces {
  init
  always (skip or some toCancel, replacement: Card | cancel[toCancel, replacement])
}

pred example { eventually no status.unissued }

assert card_lifecycle {
  always all card : Card | card.status' = card.status or card.status' = card.status.next
}

check card_lifecycle for 6 but exactly 2 Customer, 4 steps

run { example } for 6 but exactly 2 Customer, 4 steps
```

---

<div class="post-metadata">

**Author:** ![steve.freeman](https://avatars.discourse-cdn.com/v4/letter/s/2acd7d/32.png) [@steve.freeman](https://alloytools.discourse.group/u/steve.freeman)\
**Post date:** [September 15, 2020, 11:31am UTC](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88/31 "2020-09-15T11:31:11Z")

</div>

and it turns out that fun and pred do not share a namespace, so can name both `cancel`, which reads better in the visualiser. Is your experience that this causes problems?

---

<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 15, 2020, 11:34am UTC](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88/32 "2020-09-15T11:34:55Z")

</div>

I hid this fact because I feared it would be even more mind-boggling 😃  
I seem to recall I had one issue some time but I haven’t kept a record so I’m not sure. As far as I’m concerned, I use the same name.

---

<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 15, 2020, 11:58am UTC](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88/33 "2020-09-15T11:58:19Z")

</div>

Looks good to me.

Remark: ` cards' = cards - customer->toCancel + customer->replacement` could be simplified as:  
` cards' = cards ++ customer->replacement`.

---

<div class="post-metadata">

**Author:** ![steve.freeman](https://avatars.discourse-cdn.com/v4/letter/s/2acd7d/32.png) [@steve.freeman](https://alloytools.discourse.group/u/steve.freeman)\
**Post date:** [September 15, 2020, 12:24pm UTC](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88/34 "2020-09-15T12:24:11Z")

</div>

> [@grayswandyr](#):
>
> Remark: ` cards' = cards - customer->toCancel + customer->replacement` could be simplified as:  
> ` cards' = cards ++ customer->replacement` .

except that `cards` is one customer to many cards, whereas `status` is one card to one status.

---

<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 15, 2020, 12:58pm UTC](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88/35 "2020-09-15T12:58:32Z")

</div>

Oops, right, you cancel one card but keep the others, of course.

---

<div class="post-metadata">

**Author:** ![keithb\_b](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/keithb_b/32/7_2.png) [@keithb\_b](https://alloytools.discourse.group/u/keithb_b)\
**Post date:** [September 15, 2020, 3:52pm UTC](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88/36 "2020-09-15T15:52:16Z")

</div>

Ah, ok, that’s an interesting tip.

As to `{z}`, that’s because I haven’t full internalised that Alloy doesn’t have atoms, only singleton sets.

---

<div class="post-metadata">

**Author:** ![ilkane](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/ilkane/32/124_2.png) [@ilkane](https://alloytools.discourse.group/u/ilkane)\
**Post date:** [March 8, 2022, 10:01am UTC](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88/37 "2022-03-08T10:01:43Z")

</div>

> [@steve.freeman](#):
>
> ```auto
> enum Status { unissued, issued, cancelled }
> 
> sig Card {
> var status : Status 
> }
> sig Customer { 
> var cards: disj some Card 
> }
> 
> // ---- events ----
> pred cancel[toCancel, replacement: Card] {
> toCancel in Customer.cards
> replacement in status.unissued
> 
> let customer = cards.toCancel {
> status' = (status ++ toCancel->cancelled) ++ replacement->issued
> cards' = cards - customer->toCancel + customer->replacement
> }
> }
> 
> pred skip {
> status' = status
> cards' = cards
> }
> 
> // ---- reification ----
> enum Event { Cancel, Skip }
> fun _cancel : Event -> Card -> Card {
> Cancel -> { card, replacement: Card | cancel[card, replacement] }
> }
> fun _skip : Event { 
> {event : Skip | skip} 
> }
> fun events : set Event {
> _cancel.Card.Card + _skip
> }
> 
> // ---- behaviours ----
> pred init {
> no status.cancelled
> #status.unissued > 1
> all customer: Customer | some customer.cards
> status.issued = Customer.cards 
> }
> 
> fact traces {
> init
> always (skip or some toCancel, replacement: Card | cancel[toCancel, replacement])
> }
> 
> pred example { eventually no status.unissued }
> 
> assert card_lifecycle {
> always all card : Card | card.status' = card.status or card.status' = card.status.next
> }
> 
> check card_lifecycle for 6 but exactly 2 Customer, 4 steps
> 
> run { example } for 6 but exactly 2 Customer, 4 steps
> 
> ```

This is a great example,  
in the text mode one can see the used event and the arguments.  
…  
skolem $\_cancel={Cancel$0-\>Card$2-\>Card$3}  
skolem $\_skip={}  
skolem $events={Cancel$0}  
But, when I run this model with kodkod, these skolems aren’t available there.  
Any idea why?  
The kodkod output is the same with Alloy Analyzer text output, but the skolems \_cancel and \_skip are missing.

---

<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:** [March 8, 2022, 10:30am UTC](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88/38 "2022-03-08T10:30:17Z")

</div>

This is because `pred`icates and `fun`ctions do not exist at the Kodkod level. When the compilation to Kodkod happens, all calls to predicates and functions are unfolded away.

(PS: in `traces`, you could even have written `always some events` instead of `always (skip or some toCancel, replacement: Card | cancel[toCancel, replacement])`).

[Previous page](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88.md?page=1)