Finite State Machines

The dirty secret of formal methods is that the only way we know to scale it up is to use state machines. So we might as well learn how to write state machines in TLA+!

Note

I want to write a formal introduction, but in the meantime, here’s a good introduction to state machines.

A Simple State Machine

I have a lamp in my bedroom that’s controlled by both a lamp switch and an wall switch. Both switches have to be on in order for the lamp to be one. The state machine looks like this:

A few things to notice:

• The transitions are nondeterministic. From \(BothOff\), I can either flip the wall switch or the lamp switch.

• There’s no transitions between \(BothOff\) and \(On\), I have to flip the switches one at a time.

• For the same reason, there’s no way to get between \(WallOff\) and \(LampOff\).

In PlusCal, we can model a state machine by placing await statements inside an either-or block. If the await is false the branch is blocked off, but the other branches are still available, preserving nondeterminism.

---- MODULE state_machine ----

(*--algorithm lamp
variable state = "BothOff";
process StateMachine = "SM"
begin
  Action:
    either \* this is the state machine
        await state = "BothOff";
        state := "WallOff";
      or
        await state = "BothOff";
        state := "LampOff";
    or
        await state = "LampOff";
        state := "BothOff";
      or
        await state = "LampOff";
        state := "On";
    or
        await state = "WallOff";
        state := "BothOff";
      or
        await state = "WallOff";
        state := "On";
    or
        await state = "On";
        state := "LampOff";
      or
        await state = "On";
        state := "WallOff";
    end either;
    goto Action;
end process;
end algorithm; *)
====

9 states / 4 distinct spec

Now that’s a bit long, as we need one transition per state machine. We could simplify this with a macro:

macro transition(from, to) begin
  await state = from;
  state := to;
end macro;

Or even

macro transition(from, set_to) begin
  await state = from;
  with to \in set_to begin
    state := to;
  end with;
end macro;

In my opinion, things look a little cleaner if we just do it all in TLA+.

---- MODULE state_machine ----
VARIABLE state

Trans(a, b) ==
  /\ state = a
  /\ state' = b

Init == state = "BothOff"

Next == 
  \/ Trans("BothOff", "WallOff")
  \/ Trans("BothOff", "LampOff")
  \/ Trans("WallOff", "On")
  \/ Trans("WallOff", "BothOff")
  \/ Trans("LampOff", "BothOff")
  \/ Trans("LampOff", "On")
  \/ Trans("On", "WallOff")
  \/ Trans("On", "LampOff")
  \/ Trans("error", "fetching")

Spec == Init /\ [][Next]_state
====

9 states / 4 distinct spec

For this reason I’m going to stick with TLA+ going forward. You can still do state machines in PlusCal, it’s just that more complicated stuff is messier.

Hierarchical State Machines

What’s better than a state machine? A nested state machine.

Also known as Harel Statecharts, hierarchical state machines allow states inside of other states. If state P’ is inside of state P, then P’ can take any transitions that P can take. A simple example is the UI of a web app. You can log on or off, and when logged in you start in a homepage and can move to any secondary page. To make things interesting we’ll say one of the secondary pages also as subpages.

Note

There’s a few different flavors of HSM. For this one, I’m following three restrictions:

1. Transitions can start from any state, but must end in a “leaf” state. You can’t be in LoggedIn or Reports, you have to be in Main or Report1.

2. A state can’t have two different parent states.

3. No state cycles.

To model the hierarchical states, I want to be able to write Trans("LoggedIn", "Logout") and have that include every state of the app: Main, Settings, Report1, and Report2. So we need an In(state1, state2) that’s recursive. Then Trans becomes

Trans(from, to) ==
  /\ In(state, from) \* Recursive!
  /\ state' = to

To represent the state hierarchy, we can go either top-down (a function from states to the set of child states) or bottom-up (a function from states to their parent states). Each has relative tradeoffs:

1. Top-down: Function domain guaranteed to be all states. Can accidentally give two states the same child.

2. Bottom-up: Impossible for a state to have two parents. Worse ergonomics on checking In, as not all states will be in the function’s domain. Harder to check if a state doesn’t have children.

Ah heck, let’s implement both and check they’re equivalent.

---- MODULE reports ----
EXTENDS TLC \* For @@
VARIABLE state

States == {
  "LogOut", 
  "LogIn", "Main", "Settings", 
    "Reports", "Report1", "Report2"
}

TopDown == [LogIn |-> {"Main", "Settings", "Reports"}, 
              Reports |-> {"Report1", "Report2"}] @@ [s \in States |-> {}]
              \* @@ is function left-merge        ^^

BottomUp == [Report1 |-> "Reports", Report2 |-> "Reports",
           Reports |-> "LogIn", Main |-> "LogIn", Settings |-> "LogIn"]

\* For TopDown we need to make sure that there are no double-parents
ASSUME \A s1, s2 \in States: s1 # s2 => TopDown[s1] \cap TopDown[s2] = {}

RECURSIVE InTD(_, _)
InTD(s, p) ==
  \/ s = p
  \/ \E c \in TopDown[p]:
    InTD(s, c)

RECURSIVE InBU(_, _)
InBU(s, p) ==
  \/ s = p
  \/ \E c \in DOMAIN BottomUp:
      /\ p = BottomUp[c]
      /\ InBU(s, c)

\* Check the two are identical
ASSUME \A s, s2 \in States: InTD(s, s2) <=> InBU(s, s2)

Trans(from, to) ==
  /\ InTD(state, from)
  /\ state' = to

Init == state = "LogOut"

Next ==
  \/ Trans("LogOut", "Main")
  \/ Trans("Main", "Settings")
  \/ Trans("Settings", "Main")
  \/ Trans("LogIn", "LogOut")
  \/ Trans("LogIn", "Report1")
  \/ Trans("Report1", "Report2")
  \/ Trans("Report2", "Report1")
  \/ Trans("Reports", "Main")

Spec == Init /\ [][Next]_state
AlwaysInLeaf == TopDown[state] = {}
====

16 states / 5 distinct spec