Skip to content

Lecture 8.2: Reasoning about processes

Previously, we introduced a process algebra and defined several state machines. Today we will talk about how to talk about how to reason about them and how to check them using PBT.

Reasoning about processes

What is the purpose of modeling processes using pure functions or process algebras? One reason is that it allows us to reason about the behavior of these systems.

Recall our simple vending machine from last class which tracks both items and money

INIT := MACHINE(0.00, 10)
MACHINE(money, 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

We can use this model to verify certain properties about our vending machine, for instance:

  • Our vending machine should never allow us to vend an item if we haven't inserted enough money.
  • Our vending machine should never allow for us to have a negative number of items.

Let's formalize this model in OCaml:

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

(* Note that we are implementing a StateMachine signature, but will leave this *)
(* implicit today (similar to what we did in 6.1) *)
module MoneyItemVendingMachine (* : StateMachine *) = struct
  type state = { money: float; items: int }
  type input = Insert25c | Insert50c | Vend

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

  let step state input =
    match input with 
    | 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"
    | _ -> failwith "invalid state"
end;;

What can we test? How should we go about testing this code? What additional state or code would we need to handle in our PBT infrastructure?

At a high level, we will need two things:

  • a way to capture the state of the process over time, given a sequence of inputs.
  • a way to handle failwith exceptions.

Traces

Traces are history of the actions that a process has performed and, optionally, the states the process has visited. For example, the trace of a timer ticking down from 3 seconds, sounding an alarm after the last tick and then being turned off could be represented as follows:

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

But the sequence of actions / inputs that are performed will simply be:

tick, tick, tick, off

Alternatively, you could draw the diagram

stateDiagram-v2
  direction LR
  TIMER(3) --> TIMER(2) : tick
  TIMER(2) --> TIMER(1) : tick
  TIMER(1) --> ALARM    : tick 
  ALARM    --> 0        : off

Now, we would like to collect a trace. Last lecture, we saw several state machine modules that modeled a vending machine. We specified it via three types:

  • a type of inputs, which is how we interact with the state machine;
  • a type of state, which holds the internal state of the machine;
  • a resulting output state that actions transitioned us to.

These will make up our traces: a list of three-tuples, where each tuple holds the current state, an input, and a new state.

We can write collect traces for any state machine adhering to the StateMachine signature:

module MachineTrace (M : StateMachine) = struct
  type trace = (M.state * M.input * M.state) list

  let run_machine (inputs : M.input list) : trace option = 
    let rec go state inputs = 
       match inputs with 
       | [] -> []
       | i :: inputs' -> 
          let state' = M.step state i in 
          (state, i, state') :: go state' inputs'
    in 

    try 
      (* Your first try-catch block in OCaml *)
      Some (go M.init inputs)
    with Failure _ -> None
end;;

module MkTrace = MachineTrace(MoneyItemVendingMachine)

By generating inputs for MoneyItemVendingMachine, we can observe possible traces and check properties, which specifies whether a trace that the machine emits is a "good" one or not.

open MoneyItemVendingMachine

let gen_input () : input =
  match Random.int 3 with
  | 0 -> Insert25c
  | 1 -> Insert50c
  | 2 -> Vend
  | _ -> failwith "invalid integer"

let gen_trace n () : Trace.trace option = 
  let is = List.init (Random.int n) (fun _ -> gen_input ()) in 
  Trace.run_machine is

Property checking with Traces

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:

\[\exists M : \texttt{MachineTrace(VendingMachine)}, \forall is : \texttt{input list}, \texttt{M.run machine}(is) = \texttt{Some } tr \Rightarrow p(tr). \]

Let's test one of our original trace properties stated above. For example, let's check that we can never reach a trace where the final state has a negative number of items:

\[ \forall is : \texttt{(state * input * state) list}, \forall (s, i, s') : is, \texttt{items}(s') \ge 0 \]

Formalizing this in OCaml, we can state and test this property:

let num_items_ok (tr : Trace.trace) : bool = 
  List.for_all (fun (s, i, s') -> s'.items >= 0) tr

let rec forall ?(n : int = 1000) (gen : unit -> 'a) (prop : 'a -> bool) =
  if n <= 0 then None else
    let x = gen () in
    if prop x then forall ~n:(n - 1) gen prop else Some x

let _ =
  forall (gen_trace 20) (fun tr_opt -> match tr_opt with
  | None -> true
  | Some a -> num_items_ok a)