Skip to content

Lecture 8.1: State Machines

Last week, we presented a view of stateful programming through mutability: the ability for the program to create and modify references. While (of course) very useful, there are some limitations that make it not always the best choice.

Suppose we are building the control logic for a simple vending machine. When the user inserts a coin, the vending machine should show the amount of money in the machine; then, when the user makes a selection, it should vend the item and subtract that item's amount from the balance. If we use mutable state, it could look like this: 

let money : float ref = ref 0.0
let items : (float * string * string) list ref = ref [
    (1.0, "A1", "Chocolate");
    (0.5, "B7", "Gum");
    (0.75, "C2", "Licorice");
]

(* Internal *)
let vend (s : string) = ...

let insert_coin (c : float) : unit = ...
let choose (choice : string) : unit = ...
When the user inserts a coin, we call insert_coin with the coin's amount. When the user makes a choice via choose, if the amount of money is appropriate for the item, we modify the state variables accordingly and call vend.

The issue with the above setup is that our state variables are global, mutable pieces of state. Programming with global state is very dangerous, because any function can do anything to the state. In particular, suppose we also have a function 

let print_coins () = ...
that displays the amount of money to the screen. This function just has type unit -> unit, which makes no guarantees about what state variables it's touching and not touching; thus, we need to fully understand the code to make sure it doesn't modify items!

As we have said earlier in this class, there are two ways to make programs correct: test/verify them to ensure correctness; and make it hard to write incorrect programs. While one could do testing to make sure print_coins doesn't modify items, what if we could make sure, by design, that this never can happen in the first place? The way we can do this is to write our vending machine in a manner that doesn't use mutability. If we don't use mutability in the first place, we can't make it go wrong!

Instead of using mutability for state, we will use a state machine. A state machine is a function which keeps state not through state variables, but instead by explicitly passing around a state variable. Let's change our vending machine to use a state machine. We will keep items simple for now, but it should be clear how to extend it. First, we define our state: 

type vend_state = {
    money : float;
    (* For now: assume each item costs 1.0 and there is only one type of item. *)
    num_items : int; 
}
Then, for the state machine to be useful, it also needs a type of inputs --- the way in which the user interacts with the state machine --- along with a type of outputs, which specifies how the state machine communicates back to the user.

type vend_input = | InsertCoin of float | PressVend
type vend_output = {
    money_display : float;
    items_display : int;
    should_vend : bool
}

Finally, we can implement the state machine logic. Given a type of states s, inputs i and outputs o, a state machine (for our purposes) is simply a function of type s -> i -> s * o: 

let vending_machine (s : vend_state) (i : vend_input) : vend_state * vend_output = 
    match i with 
    | InsertCoin x -> 
        let new_money = s.money +. x in 
        let s' = {s with money = new_money} in 
        let o = {money_display = s'.money; items_display = s'.num_items; should_vend = false} in 
        (s', o)
    | PressVend -> 
        if s.money >= 1.0 then 
            (* This has a bug. We will fix it later. *)
            let s' = {money = s.money -. 1.0; num_items = s.num_items - 1} in 
            let o = {money_display = s'.money; items_display = s'.num_items; should_vend = true} in 
            (s', o)
        else 
            (* Can't vend; don't change state *)
            let s' = s in 
            let o = {money_display = s'.money; items_display = s'.num_items; should_vend = false} in 
            (s', o)

A huge advantage over state machines, rather than functions over mutable state, is that they are more easily testable. Since the state machine is just a pure function, we can easily run it over and over again on different states without worrying about whether our functions mutate any globally defined references.

In particular, we can use something similar to PBT. We can randomly test the state machine via feeding it random inputs, and seeing what happpens over time. To do this, let's first create a generator for random inputs: 

let gen_coin () : float = 
    match Random.int 3 with
    | 0 -> 0.25
    | 1 -> 0.50
    | _ -> 0.75

let gen_input () : vend_input = 
    if Random.bool () then 
        let c = gen_coin () in 
        InsertCoin c
    else 
        PressVend

Next, let's define a type for traces, which specify complete histories of the machine executing: 

type trace = (vend_state * vend_input * vend_output * vend_state) list
Each element of the trace is a four-tuple (s, i, o, s'), which represents s transitioning under input i to outputs o and s'. For the trace to make sense, we will ensure that if (s1, i, o, s2) is directly before (s3, i, o, s4), then s2 = s3. Now, let's generate a trace given a list of inputs:

let rec run_vending_machine (current : vend_state) (is : vend_input list) : trace = 
    match is with 
    | [] -> []
    | i :: is' -> 
       let (s', o) = vending_machine current i in 
       let rest = run_vending_machine s' is' in 
       (current, i, o, s') :: rest

To actually run the vending machine, we need an initial state: 

let init_vend_state = {
    money = 0.0;
    num_items = 10;
}

Let's now look at a few traces.

utop # run_vending_machine init_vend_state [InsertCoin 0.25; InsertCoin 0.25; InsertCoin 0.5; PressVend];;
- : trace =
[({money = 0.; num_items = 10}, InsertCoin 0.25,
  {money_display = 0.25; items_display = 10; should_vend = false},
  {money = 0.25; num_items = 10});
 ({money = 0.25; num_items = 10}, InsertCoin 0.25,
  {money_display = 0.5; items_display = 10; should_vend = false},
  {money = 0.5; num_items = 10});
 ({money = 0.5; num_items = 10}, InsertCoin 0.5,
  {money_display = 1.; items_display = 10; should_vend = false},
  {money = 1.; num_items = 10});
 ({money = 1.; num_items = 10}, PressVend,
  {money_display = 0.; items_display = 9; should_vend = true},
  {money = 0.; num_items = 9})]

top # run_vending_machine init_vend_state [InsertCoin 1.0; PressVend; PressVend];;
- : trace =
[({money = 0.; num_items = 10}, InsertCoin 1.,
  {money_display = 1.; items_display = 10; should_vend = false},
  {money = 1.; num_items = 10});
 ({money = 1.; num_items = 10}, PressVend,
  {money_display = 0.; items_display = 9; should_vend = true},
  {money = 0.; num_items = 9});
 ({money = 0.; num_items = 9}, PressVend,
  {money_display = 0.; items_display = 9; should_vend = false},
  {money = 0.; num_items = 9})]

Trace Properties

Now that we have everything set up, we can perform some tests. The way we will specify properties about state machines are called trace properties, or safety properties. These are given by functions p : trace -> bool, which states whether a trace is a "good" or "safe" one. Given one of these functions, the property we are looking to check is whether p holds on all traces that can be generated by the state machine:

\[ \forall is : \texttt{input list}, p (\texttt{run_vend_machine}(\texttt{init_vend_state}, is)). \]

Encoded into OCaml, what we are doing is as follows: 

let gen_trace n = 
    let is = List.init (Random.int n) (fun _ -> gen_input ()) in 
    run_vending_machine init_vend_state is

let rec forall gen prop n = 
    if n <= 0 then None else 
        let x = gen () in 
        if prop x then forall gen prop (n - 1) else Some x

let machine_pbt (p : trace -> bool) n = forall (fun _ -> gen_trace n) p 50

Now, let's test this on a particular trace property. For example, let's check that we can never reach a trace where the final state has a negative number of items: 

let last (xs : 'a list) : 'a option =
    if List.is_empty xs then None 
        else Some (List.nth xs (List.length xs - 1))

let num_items_ok (p : trace -> bool) = 
    fun tr -> 
        match last tr with 
        | None -> true
        | Some (_, _, _, s) -> s.num_items >= 0

It turns out that this trace property is actually false, because we didn't make this check in our state machine. Thus, it was possible to vend more items than were actually present in the machine. Let's fix it: 

let vending_machine (s : vend_state) (i : vend_input) : vend_state * vend_output = 
    match i with 
    | InsertCoin x -> 
        let new_money = s.money +. x in 
        let s' = {s with money = new_money} in 
        let o = {money_display = s'.money; items_display = s'.num_items; should_vend = false} in 
        (s', o)
    | PressVend -> 
        if s.money >= 1.0 && s.num_items > 0 then  (* Fixed the conditional to make sure there is an item *)
            let s' = {money = s.money -. 1.0; num_items = s.num_items - 1} in 
            let o = {money_display = s'.money; items_display = s'.num_items; should_vend = true} in 
            (s', o)
        else 
            (* Can't vend; don't change state *)
            let s' = s in 
            let o = {money_display = s'.money; items_display = s'.num_items; should_vend = false} in
            (s', o)

Extending our Example

Try adding:

  • Multiple different kinds of items, with different prices;
  • The ability to buy multiple things at once;
  • An input for restocking the machine;
  • A "coin return" functionality, which returns the balance of the machine as a new output;
  • An ability to save the state to a file, and restore that state;

Try modeling:

  • If an item is vended, the user must have deposited enough money for it;
  • If an item is vended, the user must have asked to vend it;
  • That if one saves and restores a state, we don't change the state.

As an additional challenge, one can show that :

  • The order in which we insert multiple coins does not affect the state of the machine.