Modelling a state machine in Electrum (towards Alloy 6)

[grayswandyr]

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.

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:

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.

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.

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.

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:

enum Event { Send, Compute, Skip }

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

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

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

3. give a name to the set of event instances:

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

4. 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).

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

Hope this helps!

[keithb_b]

That’s great, thanks!

This idiom looks like what I was trying to grope my way towards. I struggle, though, to write the event reification functions for my case where the event involves a higher arity predicate. If I have

pred Vehicle::unlockAZone[z: Zone]{
    this.unlocked' = this.unlocked + {z}
    this.locked'   = this.locked   - {z}
    this.zonesOtherThanUnchanged[z]
}

how do I write the function? This:

fun _unlock: Command -> Vehicle -> Zone {
    Unlock -> {z : Zone | {v: Vehicle | v.unlockAZone[z]}}
} 

doesn’t typecheck because {v: Vehicle | v.unlockAZone[z]} is not “a formula expression”, and

fun _unlock[c: Command, v:Vehicle]: Zone {
    Unlock -> {z : Zone | v.unlockAZone[z]}
}

doesn’t typecheck because "…the body must be a relation with arity 1. So the body’s type cannot be: {this/Command->this/Zone} "

[grayswandyr]

Indeed, {v: Vehicle | v.unlockAZone[z]} defines a set (defined by “comprehension” or “intension”). You want:

fun _unlock: Command -> Vehicle -> Zone {
    Unlock -> {z : Zone, v: Vehicle | v.unlockAZone[z]}
} 

[keithb_b]

Right! I was using the wrong metal model there. I was thinking about how to capture the “arguments”, not how to build the relation. It’s an interesting shift to have a language where the intentional and extensional definitions of a function have equal status. I don’t think even Prolog does that.

Which reminds me, there’s a result that I’ve been searching for and can’t find, I wonder if you’ve seen anything like it…

What grounds do we have for considering that there are intentional and extensional definitions of the same one function? Eg, what grounds do we have for thinking of

λx.x²

and

{ 0 → 0 
+ 1 → 1
+ 2 → 4
+ 3 → 9
…}

as the same thing?

[grayswandyr]

@keithb_b

It’s an interesting shift to have a language where the intentional and extensional definitions of a function have equal status. I don’t think even Prolog does that.

I may misunderstand your statement but, in a strictly formal sense, I’d say Alloy only has intensional definitions as atoms are not part of the user language. Even when you write one sig A, A is not technically an atom, it’s a singleton set containing a 1-tuple made of one atom (call it A$1 for instance).

@keithb_b

What grounds do we have for considering that there are intentional and extensional definitions of the same one function? Eg, what grounds do we have for thinking of
[snip]
as the same thing?

As a matter of fact, they’re not the same thing. The former is a finite syntactic object while the latter is an loosely-defined (because of ...) infinite set (which happens to be the graph of the former under a certain semantics and given some hypotheses). This is off-topic here, but this is typically addressed in a course on computability theory or on lambda calculus.

[keithb_b]

They are not the same thing, and they do belong to different formalisms. And yet people are very happy to talk about them as being the “same” function. I’ve not seen any discussion anywhere of why that’s reasonable. But as you say, off topic for here.

I’ve implemented the event reification in my model, many thanks for pointing out that idiom. This looks really good:

But next comes this:

which I find very confusing. How is the model able to get to the final state where all zones are unlocked without any further Commands? Have I underconstrained the model somehow, to let the vars change without a Command? Or, maybe I’ve misunderstood what this reification achieves.

The model is below. Further feedback welcome.

abstract sig Location{}

abstract sig Zone{
    locations: disj some Location
}

abstract sig Vehicle{
  //structural relations
    ,locations: some Location

    ,zones: some Zone
    ,locationsInZone: zones one -> some locations

  //state
    ,var locked:   disj set zones
    ,var unlocked: disj set zones
}{
  //facts about derived relations
    all z: zones | z.locations = locationsInZone[z]
  //facts about state
    zones = locked + unlocked
}

one sig DriverFront extends Location{}
one sig PassengerFront extends Location{}
one sig PassengerSide extends Location{}
one sig Rear extends Location{}

one sig People extends Zone{}
abstract sig Cargo extends Zone{}
one sig RearCargo extends Cargo{}
one sig OtherCargo extends Cargo{}

sig Transit extends Vehicle {
}{
   zones = 
         People 
       + RearCargo 
       + OtherCargo

   locations = 
         Rear
       + PassengerSide
       + DriverFront
       + PassengerFront

   locationsInZone = 
         People     -> DriverFront
       + People     -> PassengerFront
       + RearCargo  -> Rear
       + OtherCargo -> PassengerSide
}

//observations
pred Vehicle::zoneLocked[z: Zone]{
    z in this.locked
}

pred Vehicle::zoneUnchanged[z: Zone]{
    {z} & this.locked   = {z} & this.locked'
    {z} & this.unlocked = {z} & this.unlocked'
}

pred Vehicle::zonesOtherThanUnchanged[z: Zone]{
    all z: this.zones - z | this.zoneUnchanged[z]
}

//actions
pred Vehicle::unlockAZone[z: Zone]{
    this.unlocked' = this.unlocked + {z}
    this.locked'   = this.locked   - {z}
    this.zonesOtherThanUnchanged[z]
}

pred Vehicle::lockAZone[z: Zone]{
    this.locked'   = this.locked   + {z}
    this.unlocked' = this.unlocked - {z}
    this.zonesOtherThanUnchanged[z]
}

pred skip{
    all v: Vehicle |
        all z: v.zones |
            v.zoneUnchanged[z]
}

//event reification

enum Command {Unlock, Lock, Skip}
fun _unlock: Command -> Vehicle -> Zone {
    Unlock -> {v: Vehicle, z: Zone| v.unlockAZone[z]}
}

fun _lock: Command -> Vehicle -> Zone {
    Lock -> {v: Vehicle, z: Zone| v.lockAZone[z]}
}

fun _skip: Command {
    {c : Skip | skip}
}

fun commands: set Command {
    (_unlock + _lock).Zone.Vehicle + _skip
}
    
//demonstration    
pred trace{
    //initally -- it would be nice to have a (yes, redundant!) keyword for this
    all v:Vehicle |
        all z: v.zones | v.zoneLocked[z]
    always
           skip
        or one v: Vehicle |
               one z: Zone |
                      v.unlockAZone[z]
                   or v.lockAZone[z]
    eventually
        all v:Vehicle | 
            all z: v.zones | not v.zoneLocked[z]
}

run {trace} for exactly 1 Transit, 6 Time

[alcino]

Hi,

Could the problem be the lack of parenthesis here (always has stronger precedence than or)?

@keithb_b

    always
           skip
        or one v: Vehicle |
               one z: Zone |
                      v.unlockAZone[z]
                   or v.lockAZone[z]

Best,
Alcino

[keithb_b]

That’s it! Many thanks.

[grayswandyr]

FTR we made all unary logical operators bind stronger than binary logical ones This way it’s easy to remember and it corresponds to standard practice in other formalisms.

(Regarding the remark on the “same” functions: they’re not the same thing because the graph is the graph of plenty of different algorithms. Consider sorting functions: they all have the same graph but insertion sort and heap sort do differ.)

EDIT: more precise wording.

[grayswandyr]

A couple of comments/questions:

• Is there a reason for writing z between braces (on several lines)?
• To me, the trace part can most of the time be a fact, leaving the eventually ... constraint as a goal for run.
• Concerning the initial conditions, you can just put them in a pred or fact called init, which makes it clear what they stand for.
• Usually, I avoid one quantification in the definition of a trace because it’s often over-constraining. The weaker some may allow for more behaviors, in principle. Then, even with some, it will often happen that there won’t be more of them. Why? Not because of one over-constraining but because of frame conditions. I think its better because frame conditions represent a “real” phenomenon (an event leaves some thing unchanged) while one is something you enforce. (For this particular model, there may be a good reason for your choice, I’m just pointing this out as a general hint.)

[steve.freeman]

Q. Does

,var locked:   disj set zones
,var unlocked: disj set zones

mean that the two sets are disjoint from each other?

[steve.freeman]

Dumb question. I see where the commands are defined, but not where they’re used. How are they bound in?

[alcino]

No, I believe that using disj in a declaration, such as

sig A {}
sig B { r : disj set A }

forces that an atom of A will never appear associated with two different atoms of B via relation r. It is the same as having no disj and add constraint

fact {
  all a : A | lone r.a
}

or the equivalent

fact {
	all disj b1, b2 : B | no b1.r & b2.r
}

In the above example it would mean that the same zone will never appear in the locked relation of two different vehicles (likewise for unlocked) at the same time.

Best,
Alcino

[grayswandyr]

Caution! Such constraints hold in every state (see the language ref):

When more than one variable is declared at once, the keyword disj
appearing on the left indicates that the declared variables are mutually
disjoint in every state (that is, the relations they denote have empty
intersections in every state). In the declarations of fields (within
signatures), the disj keyword may appear also on the right, for
example:

sig S { var f: disj e }

This constrains the field values of distinct members of the signature to
be disjoint in every state. In this case, it is equivalent to the
constraint

always all a, b: S | a != b implies no a.f & b.f

which can be written more succinctly (using the disj keyword in a
different role) as

always all disj a, b: S | disj [a.f, b.f]

[keithb_b]

@alcino

In the above example it would mean that the same zone will never appear in the locked relation of two different vehicles (likewise for unlocked ) at the same time.

If you mean my example, that’s not my intent. I write:

abstract sig Vehicle{
…
    ,zones: some Zone
…

  //state
    ,var locked:   disj set zones
    ,var unlocked: disj set zones
}{
…
  //facts about state
    zones = locked + unlocked
}

with the intent that each of the zones on a given Vehicle are exactly one of locked or unlocked at any given time. Note that locked and unlocked of a Vehicle are subsets of that vehicle’s zones and not of Zone. Does that not do what I think it does?

At this point the model doesn’t deal correctly with multiple vehicles, although all vans of the same model have the same arrangement of doors. I do need to extend the model to cope with multiple vehicles.

I found that I couldn’t say ,var part locked, unlocked: zones, hence the sig fact that zones = locked + unlocked. I ended up preferring the two-line declaration to the one-line declaration ,var disj locked, unlocked: zones of the two sets but I don’t recall why.

[keithb_b]

@grayswandyr

• Is there a reason for writing z between braces (on several lines)?

Do you mean, eg, why v.unlockAZone[z] and not z.v.unlockAZone? The latter reads very unnaturally to me. I suppose that “aZone.onAVehicle.isUnlocked” would be fine, if there’s a reason to avoid the [] syntax for joins. Is there?

• To me, the trace part can most of the time be a fact, leaving the eventually ... constraint as a goal for run .

I’ll try that and see how it looks to me.

• Usually, I avoid one quantification in the definition of a trace because it’s often over-constraining. … I think its better because frame conditions represent a “real” phenomenon (an event leaves some thing unchanged) while one is something you enforce. (For this particular model, there may be a good reason for your choice, I’m just pointing this out as a general hint.)

Right. In this case the one is a real constraint: the vehicle operator can only press one button on the remote control at a time.

[alcino]

@keithb_b

with the intent that each of the zones on a given Vehicle are exactly one of locked or unlocked at any given time. Note that locked and unlocked of a Vehicle are subsets of that vehicle’s zones and not of Zone . Does that not do what I think it does?

It’s not clear to me what was your intent: do you want locked and unlocked to always be disjoint for a given vehicle? If that is the case, your declaration does not ensure that. A quick check reveals a counter-example:

check {
  always all v : Vehicle | no v.locked & v.unlocked
}

@keithb_b

I ended up preferring the two-line declaration to the one-line declaration ,var disj locked, unlocked: zones of the two sets but I don’t recall why.

Those two options are not the same. Actually var disj locked, unlocked : set zones would indeed ensure that locked and unlocked are always disjoint for a given vehicle, while var locked : disj set zones, var unlocked : disj set zones ensures that the same zone is never locked (nor unlocked) in two different vehicles.

Best,
Alcino

[keithb_b]

@steve.freeman

Dumb question. I see where the commands are defined, but not where they’re used. How are they bound in?

My understanding is that the

fun commands: set Command {
    (_unlock + _lock).Zone.Vehicle + _skip
}

does the wiring up, so that if, eg, v.unlockAZone[z] is true then the

fun _unlock: Command -> Vehicle -> Zone {
    Unlock -> {v: Vehicle, z: Zone| v.unlockAZone[z]}
}

says that there has to be a suitable tuple with an Unlock in it.

[steve.freeman]

So, to reinforce, the disj declaration for locked and unlocked means that they can’t both contain a given location, so we know this ensures that their union has all the zones exactly once.

[grayswandyr]

@keithb_b

Do you mean, eg, why v.unlockAZone[z] and not z.v.unlockAZone ? The latter reads very unnaturally to me. I suppose that “aZone.onAVehicle.isUnlocked” would be fine, if there’s a reason to avoid the [] syntax for joins. Is there?

No, I meant you sometimes write {z} instead of plain z.

@keithb_b

Right. In this case the one is a real constraint: the vehicle operator can only press one button on the remote control at a time.

Hmmm. I think some would do in this case because frame conditions ensure that you can’t do any of the three events at the same time. Apart from relaxing assumptions (which is always good), it would (in general) allow you to detect that some events have the same effect in some cases (because they would happen at the same time) or you forgot some frame conditions.