Skip to content

Lecture 8.1: Modeling Processes

So far we have been mostly concerned with specifying, implementing, and reasoning about computations in the form of functions with a set of inputs and an output. Last week, we introduced the notion of mutable state, but, to keep our programs easier to read, we wanted to keep mutability localized to functions. The input-output model of computation doesn't fit all systems we encounter or build. More often than not, software systems are more than just black-boxes that only take some data as input to process it into some output and stop running. Many systems are designed to run an indefinite amount of time and communicate with users or other systems. We will look at how to model these kinds of systems.

State machines

Consider a lamp with a toggle switch. It has two states: on or off. If the lamp is off, we can toggle the switch to turn it on. If the lamp is on, we can toggle the switch to turn it off. The following diagram illustrates this system.

stateDiagram-v2
    direction LR
    OFF --> ON : toggle
    ON --> OFF : toggle

We immediately see the two ingredients: we have states (OFF, ON) and we have an action/input (toggle) that triggers transitions between these states. In our case the action models the act of interacting with the toggle switch of the lamp. A state machine is a mathematical model of a system that consists of a set of states, a set of inputs, an initial state, and a transition function that describes how the system transitions from one state to another in response to an input or an action.

We can formalize the notion of a state machine in OCaml as follows:

module type StateMachine = sig
  type state
  type input
  val init : state
  val step : state -> input -> state
end;;

Since we are modeling transitions using a function that takes a state and an input action as an argument and returns a single state, our state machines are deterministic: for a given combination of a state and an action there is always only one possible next state.

Our lamp can thus be modeled as the following state machine:

module Lamp : StateMachine = struct
  type state = On | Off
  type input = Toggle

  let init = Off

  let step s Toggle = 
    match s with 
    | Off -> On
    | On -> Off
end;;

For a more interesting example of an interactive system, let's look at a vending machine, which allows the user to insert coins and, once enough change has been inserted, allows the user to dispense a candy bar. We're experiencing budget costs, so our vending machine only offers a single type of item and only accepts 50c coins. On the upside for our customers, we have an unlimited number of items. The machine also doesn't allow to enter more than $1.00 before the "vend" button is pressed. We'll upgrade soon.

stateDiagram-v2
    0INSERTED : $0.00 INSERTED
    50INSERTED : $0.50 INSERTED
    100INSERTED : $1.00 INSERTED
    0INSERTED --> 50INSERTED : insert50c
    50INSERTED --> 100INSERTED : insert50c
    100INSERTED --> 0INSERTED : vend

A straightforward OCaml implementation of this vending machine could look like this:

module SimpleVendingMachine : StateMachine = struct
  type state = 
    | Cents0
    | Cents50
    | Cents100

  type input = InsertCoin | Vend

  let init = Cents0

  let insert_coin state = 
    match state with 
    | Cents0 -> Cents50
    | Cents50 -> Cents100
    | Cents100 -> failwith "can't insert more coins"

  let can_vend state =
    match state with 
    | Cents100 -> true
    | _ -> false

  let step state input = 
    match input with 
    | InsertCoin -> insert_coin state
    | Vend when can_vend state -> Cents0
    | Vend -> failwith "not enough money"
end;;

These two examples have one thing in common: they only have a finite number of states. This is not always the case. For example, we can imagine a vending machine that keeps track of the amount of money inserted so far, and allows the user to insert any amount of money (in 50c increments) before pressing the "vend" button. In this case, we have an infinite number of states (the amount of money inserted so far). Drawing a full diagram for this system is not possible, but here's a partial diagram that illustrates the idea:

stateDiagram-v2
    classDef empty stroke:none, fill:white, height:20px;
    0INSERTED : $0.00 INSERTED
    50INSERTED : $0.50 INSERTED
    100INSERTED : $1.00 INSERTED
    150INSERTED : $1.50 INSERTED
    REST : ...
    0INSERTED --> 50INSERTED : insert50c
    50INSERTED --> 100INSERTED : insert50c
    100INSERTED --> 0INSERTED : vend
    100INSERTED --> 150INSERTED : insert50c
    150INSERTED --> 50INSERTED : vend
    150INSERTED --> REST:::empty : insert50c

Here's the OCaml implementation of this vending machine:

module VendingMachine : StateMachine = struct
  type state = float
  type input = InsertCoin | Vend

  let init = 0.0

  let step state input = 
    match input with 
    | InsertCoin -> state +. 0.50
    | Vend when state >= 1.00 -> state -. 1.00
    | Vend -> failwith "not enough money"
end;;

Note, that we could also simply keep count of the number of coins inserted so far instead of the total amount of money, which would also give us an infinite number of states. The choice of how to model the states is up to us and depends on what details we want to reason about.

A mathematical notation

While it is certainly advantageous to be able to write down the behaviour of these systems as OCaml modules (we can run them and test them), it is often more convenient to specify the behaviour of these systems in a more concise way. The diagrams we drew above are one way to do this, but they can become unwieldy for systems with many states and transitions. More realistic system models might have an infinite number of states, which makes them impossible to capture using diagrams.

The notation we will use here is called a process algebra. It has a few simple elements which we will combine with mathematical notation to be able to specify interesting systems.

There are five basic forms of expressions in this language:

  • P, Q, OFF, TIMER(n), ..., represents a state of the system, which we will call a process. The name of the process is just a label that we can use to refer to it. We can also use parameters to refer to processes that take arguments, e.g., TIMER(n) represents a process that takes a parameter n.
  • 0 represents a process that has no behavior, i.e., it represents a state with no outgoing transitions
  • a.P represents a process that can perform action a and then behave like process P
  • P + Q represents a process that can behave like either process P or process Q
  • P if C represents a process that behaves like process P if condition C holds, and has no behavior otherwise

For example, a clock that ticks every second and runs forever can be specified as follows. Observe how we model the passage of time using a "tick" action.

CLOCK := tick.CLOCK

The above corresponds to this diagram:

stateDiagram-v2
    CLOCK --> CLOCK : tick

We will also use "parameters" which are simply process names that take arguments. For example, a timer that counts down from 10 seconds and then sounds an alarm can be specified as follows. As a convention, we designate an initial state using the name INIT.

INIT := TIMER(10)
TIMER(n) := tick.TIMER(n - 1) if n > 0
TIMER(1) := tick.ALARM
ALARM := off.0

In OCaml, the above would correspond to the following implementation:

module Timer : StateMachine = struct
  type state = Timer of int | Alarm | Done
  type input = Tick | Off

  let init = 10

  let timer ticks input =
    match input with 
    | Tick when ticks > 1 -> Timer (ticks - 1)
    | Tick when ticks = 1 -> Alarm

  let step state input = 
    match state with 
    | Alarm when input = Off -> Done
    | Timer n -> timer n input
    | _ -> failwith "invalid input"
end;;

Let us revisit our examples from before and see how we can specify them using this process algebra.

Lamp

OFF := toggle.ON
ON := toggle.OFF

A Simple Vending Machine

INIT := 0INSERTED
0INSERTED := insert50c.50INSERTED
50INSERTED := insert50c.100INSERTED
100INSERTED := vend.0INSERTED

Alternatively, we can use state parameters to specify the same machine.

INIT := INSERTED(0.00)
INSERTED(0.00) := insert50c.INSERTED(0.50)
INSERTED(0.50) := insert50c.INSERTED(1.00)
INSERTED(1.00) := vend.INSERTED(0.00)

A more complex vending machine

INIT := INSERTED(0.00)
INSERTED(x) := insert50c.INSERTED(x + 0.50)
INSERTED(x) := vend.INSERTED(x - 1.00) if x >= 1.00

A machine that tracks both the amount of money inserted and the number of items available

INIT := MACHINE(0.00, 10)
MACHINE(money, items) := 
    insert10c.MACHINE(money + 0.10, items)
  + insert25c.MACHINE(money + 0.25, items)
  + insert50c.MACHINE(money + 0.50, items)
  + vend.MACHINE(money - 1.00, items - 1) if money >= 1.00 and items >= 1

Here is the OCaml implementation of this machine:

module MoneyItemVendingMachine : StateMachine = struct
  type state = { money: float; items: int }
  type input = Insert10c | Insert25c | Insert50c | Vend

  let init = { money = 0.0; items = 10 }

  let step state input =
    match input with 
    | Insert10c -> { state with money = state.money +. 0.10 }
    | Insert25c -> { state with money = state.money +. 0.25 }
    | Insert50c -> { state with money = state.money +. 0.50 }
    | Vend when state.money >= 1.00 && state.items >= 1 -> 
        { money = state.money -. 1.00; items = state.items - 1 }
    | Vend when state.money < 1.00 -> failwith "not enough money"
    | Vend when state.items < 1 -> failwith "no items left"
end;;

Bonus: A calculator

(Currently, the calculator example in the 8.1.ml is a little different: it allows to complete the previous operation by pressing an operator button instead of the "equals" button.)

CALCULATOR(acc, op) := 
    button0.CALCULATOR(acc * 10 , op)
  + button1.CALCULATOR(acc * 10 + 1, op)
  + button2.CALCULATOR(acc * 10 + 2, op)
  + button3.CALCULATOR(acc * 10 + 3, op)
  + button4.CALCULATOR(acc * 10 + 4, op)
  + button5.CALCULATOR(acc * 10 + 5, op)
  + button6.CALCULATOR(acc * 10 + 6, op)
  + button7.CALCULATOR(acc * 10 + 7, op)
  + button8.CALCULATOR(acc * 10 + 8, op)
  + button9.CALCULATOR(acc * 10 + 9, op)
  + clear.CALCULATOR(0, None)

CALCULATOR(acc, None) :=
  + plus.CALCULATOR(0, Plus(acc))
  + minus.CALCULATOR(0, Minus(acc))
  + times.CALCULATOR(0, Times(acc))
  + divide.CALCULATOR(0, Divide(acc))

CALCULATOR(acc, Plus(x)) := equals.CALCULATOR(x + acc, None)
CALCULATOR(acc, Minus(x)) := equals.CALCULATOR(x - acc, None)
CALCULATOR(acc, Times(x)) := equals.CALCULATOR(x * acc, None)
CALCULATOR(acc, Divide(x)) := equals.CALCULATOR(x / acc, None) if acc != 0

For the full OCaml code, see 8.1.ml.