This post continues the quest to get Java developers using Alloy, a tool that, in the right
hands, is a fantastic way to explore software and hardware designs. Today we will explore a
*state machine*. I ran into a state machine problem at a customer and used Alloy to debug it
before I committed it to Java code. This blog is because it could be useful to share this experience.
It probably would help if you read the previous post about Alloy.

## About State Machines

A finite-state machine (FSM) is a *mathematical model* of a computation. It is an abstract machine
that can be in exactly one of a finite number of *states* at any given time. The FSM can change from
one state to another in response to some external *event*. The change from one state to another is
called a *transition*. An FSM is defined by its initial state, and a table that specifies
the conditions for the transitions.

## A Flip-Flop

Probably the simplest FSM is a *flip flop*. A flip flop is a circuit that reverses its output when
the clock goes from low to high. The state of the flip-flop is either ON or OFF.The edge of
the clock is the *event*, let’s call it CLOCK. To make the problem a tad more interesting we also
add a RESET event that always forces the state to OFF.

```
open util/ordering[Transition]
enum Event { CLOCK, RESET }
enum State { ON, OFF }
```

## Transitions

We now can define the table that constraints the transitions. In Alloy, such a table is called a
*relation*. It consists of a set of tuples. For the flip flop we need the following columns in
this table:

`state`

– The state the row applies to`event`

– The event`next`

– The next state

We define this table in a function in Alloy:

```
fun transitions : State -> Event -> State {
ON -> CLOCK -> OFF
+ OFF -> CLOCK -> ON
+ ON -> RESET -> OFF
+ OFF -> RESET -> OFF
}
```

Or as a table:

```
┌────┬──────┬────┐
│OFF⁰│CLOCK⁰│ON⁰ │
│ ├──────┼────┤
│ │RESET⁰│OFF⁰│
├────┼──────┼────┤
│ON⁰ │CLOCK⁰│OFF⁰│
│ ├──────┼────┤
│ │RESET⁰│OFF⁰│
└────┴──────┴────┘
```

## Verification

Now we get to the interesting part! Clearly, a flip flop changes over *time*. How do we explore this time aspect?
In Alloy, we can explore time aspects by creating a *trace*. A trace is basically a table (relation) where each
row represents a moment in time. In generally, each row represents a *step* and rows before other rows were earlier in
time. Each step is generally an atomic step in a (concurrent) algorithm.

So let’s define the data for the trace.

```
sig Transition {
before : State,
occurs : Event
}
```

Notice that at the start we made Trace `sig`

objects *ordered*. That is, there is a *first* and *last* Trace
as well as that all Trace atoms have a `next`

and `prev`

. As an aside, this ordering is internally maintained
as a table:

```
┌───────────┬───────────┐
│Transition⁰│Transition¹│
├───────────┼───────────┤
│Transition¹│Transition²│
├───────────┼───────────┤
│Transition²│Transition³│
├───────────┼───────────┤
│Transition³│Transition⁴│
├───────────┼───────────┤
│Transition⁴│Transition⁵│
├───────────┼───────────┤
│Transition⁵│Transition⁶│
├───────────┼───────────┤
│Transition⁶│Transition⁷│
├───────────┼───────────┤
│Transition⁷│Transition⁸│
├───────────┼───────────┤
│Transition⁸│Transition⁹│
└───────────┴───────────┘
```

## Magic

The hardest part to get now is that Alloy is a bit like a quantum computer, it looks like it has the superposition of *all*
possible values. We can ask Alloy for example how one of the possible trace table looks like without any constraints
defined on it:

```
run random {} for 10
```

```
┌───────────────┬──────┬──────┐
│this/Transition│before│occurs│
├───────────────┼──────┼──────┤
│Transition⁰ │ON⁰ │RESET⁰│
├───────────────┼──────┼──────┤
│Transition¹ │OFF⁰ │RESET⁰│
├───────────────┼──────┼──────┤
│Transition² │OFF⁰ │RESET⁰│
├───────────────┼──────┼──────┤
│Transition³ │OFF⁰ │RESET⁰│
├───────────────┼──────┼──────┤
│Transition⁴ │OFF⁰ │RESET⁰│
├───────────────┼──────┼──────┤
│Transition⁵ │OFF⁰ │CLOCK⁰│
├───────────────┼──────┼──────┤
│Transition⁶ │OFF⁰ │RESET⁰│
├───────────────┼──────┼──────┤
│Transition⁷ │ON⁰ │RESET⁰│
├───────────────┼──────┼──────┤
│Transition⁸ │OFF⁰ │RESET⁰│
├───────────────┼──────┼──────┤
│Transition⁹ │OFF⁰ │RESET⁰│
└───────────────┴──────┴──────┘
```

This just one of the 4096 possible trace tables. (#state * #event)^10. This clearly is a tiny example, the state table that inspired this blog had 14 states, 7 events, and I tried 40 steps. The number of state tables is about as high as the number of particles in the universe: 10^80.

Our task is therefore not to create specific tables (all possible tables already exist in Alloy’s model), our task
is instead to *carve out* the tables that should **not** be part of our solution.

In this case, we’re only interested in traces where each step to the next Trace is constrained by the `transitions`

we
defined earlier.

In Alloy we can define such a constraint in a *predicate*. If we then ask for an *instance* of the model where that
predicate is true, we should see a trace that nicely reverses the flip-flop state at each CLOCK and properly handles
RESET events.

Translating this to Alloy requires us to constrain the changes between 2 subsequent trace rows. Let’s call the first
trace row `t`

and the next row `t'`

. This is a common practice in mathematics and formal models.

Using `t`

and `t'`

we can limit the allowed transitions of the state from `t`

to `t'`

. I.e. we want the `state`

in
the next row to be constrained by the `transitions`

table.

```
pred trace {
all t : Transition-last, t' : t.next {
t'.before = transitions[t.before][t.occurs]
}
}
```

We can now ask Alloy for an instance:

```
run trace for 10
```

```
┌───────────────┬──────┬──────┐
│this/Transition│before│occurs│
├───────────────┼──────┼──────┤
│Transition⁰ │OFF⁰ │CLOCK⁰│
├───────────────┼──────┼──────┤
│Transition¹ │ON⁰ │CLOCK⁰│
├───────────────┼──────┼──────┤
│Transition² │OFF⁰ │RESET⁰│
├───────────────┼──────┼──────┤
│Transition³ │OFF⁰ │CLOCK⁰│
├───────────────┼──────┼──────┤
│Transition⁴ │ON⁰ │CLOCK⁰│
├───────────────┼──────┼──────┤
│Transition⁵ │OFF⁰ │CLOCK⁰│
├───────────────┼──────┼──────┤
│Transition⁶ │ON⁰ │CLOCK⁰│
├───────────────┼──────┼──────┤
│Transition⁷ │OFF⁰ │CLOCK⁰│
├───────────────┼──────┼──────┤
│Transition⁸ │ON⁰ │CLOCK⁰│
├───────────────┼──────┼──────┤
│Transition⁹ │OFF⁰ │CLOCK⁰│
└───────────────┴──────┴──────┘
```

In this case the first state is `OFF`

. Are there also solutions where the first state is `ON`

? We can ask
Alloy for such a solution the following way:

```
run firstOn {
trace
first.before = ON
} for 10
```

And this works fine:

```
┌───────────────┬──────┬──────┐
│this/Transition│before│occurs│
├───────────────┼──────┼──────┤
│Transition⁰ │ON⁰ │CLOCK⁰│
├───────────────┼──────┼──────┤
│Transition¹ │OFF⁰ │CLOCK⁰│
├───────────────┼──────┼──────┤
│Transition² │ON⁰ │CLOCK⁰│
├───────────────┼──────┼──────┤
│Transition³ │OFF⁰ │CLOCK⁰│
├───────────────┼──────┼──────┤
│Transition⁴ │ON⁰ │CLOCK⁰│
├───────────────┼──────┼──────┤
│Transition⁵ │OFF⁰ │CLOCK⁰│
├───────────────┼──────┼──────┤
│Transition⁶ │ON⁰ │CLOCK⁰│
├───────────────┼──────┼──────┤
│Transition⁷ │OFF⁰ │CLOCK⁰│
├───────────────┼──────┼──────┤
│Transition⁸ │ON⁰ │CLOCK⁰│
├───────────────┼──────┼──────┤
│Transition⁹ │OFF⁰ │CLOCK⁰│
└───────────────┴──────┴──────┘
```

## Querying

Since we have a trace now we can ask for specific instances. Note that so far we’ve seen instances of the model but that was only a minute part of the possible instances. For example, could we have a trace where the state would always be OFF?

```
run AlwaysOff {
trace
first.before = OFF
all t : Transition | t.before = OFF
} for 10 expect 1
```

An instance of this is:

```
┌───────────────┬──────┬──────┐
│this/Transition│before│occurs│
├───────────────┼──────┼──────┤
│Transition⁰ │OFF⁰ │RESET⁰│
├───────────────┼──────┼──────┤
│Transition¹ │OFF⁰ │RESET⁰│
├───────────────┼──────┼──────┤
│Transition² │OFF⁰ │RESET⁰│
├───────────────┼──────┼──────┤
│Transition³ │OFF⁰ │RESET⁰│
├───────────────┼──────┼──────┤
│Transition⁴ │OFF⁰ │RESET⁰│
├───────────────┼──────┼──────┤
│Transition⁵ │OFF⁰ │RESET⁰│
├───────────────┼──────┼──────┤
│Transition⁶ │OFF⁰ │RESET⁰│
├───────────────┼──────┼──────┤
│Transition⁷ │OFF⁰ │RESET⁰│
├───────────────┼──────┼──────┤
│Transition⁸ │OFF⁰ │RESET⁰│
├───────────────┼──────┼──────┤
│Transition⁹ │OFF⁰ │CLOCK⁰│
└───────────────┴──────┴──────┘
```

Could we also get the reverse, a trace with only ON?

```
run AlwaysOn {
trace
first.before = ON
all t : Transition | t.before = ON
} for 10 expect 0
```

And this indeed does not provide us with an instance.

## Conclusion

Alloy is an odd beast in the software development tooling landscape since it has no counterpart, it
is genuinly something new. It is excellent in stating quite exactly what you mean. It is perfect that
it than often shows you did not understand the problem yet. Clearly for state machines it is
an impressive tool. However, what I find most is that I use it to *explore* software designs. Alloy
is a bit like editor that allows you to play with the *essence* of a system.

Ah well, let me know if you this was interesting for you. I could write up the actual larger state machine I developed (and found quite a few errors in the transitions table with using Alloy).

Peter Kriens (@pkriens)