Facilities for testing stateful systems using state machines.

Allows defining specially annotated state machines that can be used as the
basis for generating test verification programs to validate stateful
specifications.

Test verification programs are defined as a sequence of transitions that
conform to a state machine.

API OVERVIEW

  The goal for state machine testing is to define the following:

   - A 'model' state machine (using [[defstatem]]). The model state machine
     defines the expected state machine behavior.
   - A interpreter function (adapter between [[defstatem]] and an
     implementation). This function reads model state transitions and performs the
     appropriate behavior in an implementation.

  The most important functions you need to understand are:

   - [[defstatem]] for defining state machines.
   - [[cmd-seq]] for generating symbolic test programs from a state machine.
   - [[run-cmds]] for executing a symbolic test program against code that
                  needs to be verified. This is to compare the state machine
                  behavior to a real implementation.

  There are some useful helper functions that aid in building & debugging
  state machines:

   - [[check!]] run some sanity checks against the state machine definition.
   - [[run-cmds-debug]] is a verbose printout version of [[run-cmds]].
   - [[select-by-frequency]] allows you to skew how [[cmd-seq]] generates commands.
   - [[print-failed-runs!]] prints commands if a particular [[run-cmds]] call fails.