Lecture 31: State Machines🔗

1 Purpose🔗

Discuss state machines.

2 What is a State Machine?🔗

Throughout this class, we have reasoned about state in two different ways: internally, using set! and mutable structs; and externally, through explict passing of state (e.g., in our concurrency primitives such as on-receive, which takes state as input and returns state as output). these two state representations have differing tradeoffs. while internal state via mutability is useful for imperative programming, it is not as useful for reasoning: for example, code within LSL cannot easily replay/rewind state that has been mutated. On the other hand, explicit state can be passed around, duplicated, and otherwise manipulated without running into issues. Indeed, start-debug/start-gui from our concurrency module could not easily be encoded if it did not know ahead of time what the state of each process was, which is easy to know with explicit state.

Thus, to reason about stateful programs, we often use state machines: programs which input and return state. Let’s look at an example state machine, adapted from our lecture on Record:

(define-contract FGInput (OneOf (Constant 'call-f)                                 (Constant 'call-g)))

(define-contract FGOutput String)

(define-contract FGState (OneOf (Constant 'any-next)                                 (Constant 'f-next)                                 (Constant 'g-next)                                 (Constant 'invalid)))

(: fg-transition (-> FGState FGInput (Tuple FGState FGOutput)))

(define (fg-transition st i)   (cond [(equal? i 'call-f)          (cond [(or (equal? st 'any-next) (equal? st 'f-next)) (list 'g-next "ok")]                [else                                           (list 'invalid "error")])]         [(equal? i 'call-g)          (cond [(or (equal? st 'any-next) (equal? st 'g-next)) (list 'f-next "ok")]                [else                                           (list 'invalid "error")])]))

(define fg-init 'any-next)

There are many variants of state machines, but the ones we will consider today will have a type of inputs, a type of outputs a type of states, and a transition function from states and input to states and output. For fg-transition, the inputs are the calls to either f or g, the states indicate which function may be called next, and the outputs are messages indicating whether the call succeeded.

The purpose of fg-transition is to enforce that we cannot call f or g twice in a row; instead, all calls to them must be interleaved. In our lecture on Record, we simply made use of this fact, but we did not verify it was true. While this property may be easy to see for fg-transition, similar properties are much harder to see for more complex state machines!

3 Verifying Trace Properties🔗

Thus, instead, we will use LSL to verify via random testing that this property actually holds. We will do so by considering traces for fg-transition. Intuitively, a trace is a sequence of states and I/O events that are connected by the transition function:

s_\mathsf{0} \xrightarrow{i_1} (s_1, o_1) \xrightarrow{i_2} (s_2, o_2) \xrightarrow{i_3} \dots \xrightarrow{i_n} (s_n, o_n)

where s_0 is the initial state, and for each j>0, (s_j, o_j) = \mathsf{tr}(s_{j-1}, i_j) where \mathsf{tr} is the transition function.

A trace is either an end, which just contains a final state, or a step, which contains the current state, next input, next output, and future trace after applying that input. Traces are parameterized by an arbitrary type of states S and inputs I so that we can reuse their definitions for other state machines.

We then define make-trace to take three arguments: the transition function, the current state, and the list of inputs. If the inputs are empty, we are done, so return make-end with the current state; otherwise, we use the transition function to step the current state and new input, and recursively call make-trace on the result.

Now that we have a way to create traces, we can now define properties of the state machine in terms of trace properties: functions from traces to Booleans. A trace property is valid if it holds for every trace generated by the state machine from the initial state.

What is the suitable trace property for fg-transition? Suppose we have a trace \tau of fg-transition. Then we want to enforce that, if \tau does not output "error", that no two consecutive function calls in \tau are equal. Thus, we first define a function that computes, given a trace, whether the trace has two consecutive equal inputs:

(: has-consecutive-equal-calls (-> (Trace FGState FGInput FGOutput) Boolean))

(define (has-consecutive-equal-calls trace)   (cond ([end? trace] #f)         ([step? trace]          (or (has-consecutive-equal-calls (step-future trace))              (cond [(step? (step-future trace))                     (let* [(i1 (step-input trace))                            (i2 (step-input (step-future trace)))]                       (equal? i1 i2))]                    [else #f])))))

4 Comparing State Machines🔗

Note that, when defining fg-transition-prop, we checked whether it errored not by comparing its state to 'invalid, but by checking if "error" had been output. We make this choice because the states are meant to be internal to the state machine, while the inputs and outputs are externally visible. Indeed, fg-transition-prop is designed to make no reference to the internal state; thus, the internal state could change representation without modifying the trace property.

For example, let’s consider a different representation of the state:

(define-contract FGState2 Integer)

(: fg-transition-2 (-> FGState2 FGInput (Tuple FGState2 FGOutput)))

(define (fg-transition-2 st i)   (cond [(equal? i 'call-f)          (cond [(or (equal? st 0) (equal? st 1)) (list 2 "ok")]                [else                                           (list -1 "error")])]         [(equal? i 'call-g)          (cond [(or (equal? st 0) (equal? st 2)) (list 1 "ok")]                [else                                           (list -2 "error")])]))

(define fg-init-2 0)

This representation is harder to read, but does the same job: 0 corresponds to 'any_next, 1 corresponds to 'f_next, 2 corresponds to 'g_next, and any negative number corresponds to 'invalid. Now, to verify that fg-transition-2 is also correct, we could rerun fg-transition-prop on this new transition function; however, we can do better. Instead, we can test for the equivalence of the two state machines, where by "equivalence", we mean "generate identical visible behavior". This will automatically imply that fg-transition-2 is correct with respect to fg-transition-prop, since fg-transition-prop only talks about externally visible outputs. We can define equivalence by using trace-outputs:

(: fg-equivalence (-> (List FGInput) True))

(define (fg-equivalence inputs)   (let [(trace1 (make-trace fg-transition fg-init inputs))         (trace2 (make-trace fg-transition-2 fg-init-2 inputs))]     (equal? (trace-outputs trace1) (trace-outputs trace2))))

(check-contract fg-equivalence)

Since the two state machines generate the same outputs given the same inputs, their behavior is identical; thus, any property expressed in terms of their external behavior must be equally valid between the two machines.

5 Example: HW10🔗

In HW10, we defined processes a, b, and c that were tested to have certain behaviors. Now that we have a general notion of state machine, we can see that each process’s on-receive function is itself a state machine. Indeed, let’s take a look at the reference solution for on-receive for c (adapted to be in our general format for state machines):

(define-struct packet [from msg])

(define-contract Packet (Struct packet [                                         (OneOf (Constant "a")                                                (Constant "b")                                                (Constant "c"))                                         (OneOf (Constant "hello")                                                (Constant "goodbye")                                                (Constant "got it"))]))

(define-contract CInput Packet)

(define-contract COutput (List Packet))

(define-contract CState Natural)

(: c-receive-soln (-> CState CInput (Tuple CState COutput)))

(define (c-receive-soln st pkt)   (cond [(>= st 4) (list st (list))]         [(and (equal? (packet-from pkt) "b")               (equal? (packet-msg pkt) "hello"))          (list (add1 st) (list (make-packet "a" "got it")))]         [else (list st (list))]))

The only change from the actual solution is that we use Tuple to pair the state and output together (rather than Action), and use a custom Packet struct, rather than ReceivePacket/SendPacket in order to aid testing.

Now, let’s verify that this solution satisfies the specification from the homework: whenever process "c" receives message "hello" from process "b", it should send message "got it" to process "a", unless it has already received 4 "hello" messages from process "b", in which case it should do nothing.

(define (has-four-b-messages inputs)   (>= (length (filter (lambda (pkt)                          (and (equal? "b" (packet-from pkt))                               (equal? "hello" (packet-msg pkt)))) inputs))       4))

(: final-state (All (S I O) (-> (Trace S I O) S)))

(define (final-state trace)   (cond [(end? trace) (end-final-state trace)]         [(step? trace) (final-state (step-future trace))]))

(: c-receive-prop (-> (List CInput) True))

(define (c-receive-prop inputs)   (let* [(trace (make-trace c-receive-soln 0 inputs))          (res   (c-receive-soln (final-state trace) (make-packet "b" "hello")))          (out   (second res))]       (if (not (has-four-b-messages inputs))         (equal? out (list (make-packet "a" "got it")))         (equal? out (list)))))

(check-contract c-receive-prop)

Additionally, let’s verify that our version of c-receive is equivalent to another student’s, randomly selected from the homework:

(: c-receive-student (-> CState CInput (Tuple CState COutput)))

(define (c-receive-student st pkt)  (if (and (equal? (packet-msg pkt) "hello") (equal? (packet-from pkt) "b")           (< st 4))     (list (+ st 1) (list (make-packet "a" "got it")))     (list st '())))

(: c-receive-equivalence (-> (List CInput) True))

(define (c-receive-equivalence inputs)   (let [(trace1 (make-trace c-receive-student 0 inputs))         (trace2 (make-trace c-receive-soln    0 inputs))]     (equal? (trace-outputs trace1) (trace-outputs trace2))))

(check-contract c-receive-equivalence)