Statestep Tutorial

Finite State Machines, Violations

Though Statestep is a flexible tool and can be used in other ways, it was originally designed to help model finite state machine (FSM) behaviour in a simple and systematic way. To see an example of a finite state machine model, open "harelsWatch.s2" from the "samples" directory. This is a relatively simple model of a digital watch.

First, open the Rules window and you'll see a list of events to which the watch must react. For example, the first two events correspond to the pressing and releasing of one of the four buttons (button "a") on the watch.

Click the event b_pressed and open the first rule (_1). This shows the response to pressing button "b" when both of the alarms are beeping. In this case, regardless of the values of all the other variables, both of the alarm variables change their values to quiet-enabled. Also, the light comes on and an additional variable used just to keep track of whether button "b" is pressed changes appropriately. The '=' symbols mean that all of the other variables keep their existing values.

Event b_pressed rule _1

Using finite state machine terminology, the rule is understood in this way: At any time, the state of the digital watch is defined by the values of all the variables, for example, Chime is disabled, Light is off, etc. This rule defines a set of transitions between states: it maps every state in which Alarm1 is beeping and Alarm2 is beeping to another state in which both of the alarms are quiet-enabled, Light is on, B is pressed and the values of the other variables are whatever they were in the first state.

This way of representing finite state machines has some unique advantages. For a discussion of how it compares to other finite state machine notations, see (for example) the user guide to the specification technique which is available on the Statestep website.

Typically, not many variables will change value in a rule. If you look at rules for some of the other events, you will find some in which there is no response, that is, rules where the second row of the table is filled with '=' symbols. The digital watch model is explicitly complete, that is, for each event, rules are defined for every possible state, even where there is no response. This means that, when no coverage errors are reported for an event, we can be sure we've considered what should happen in every possible state.

As with our earlier decision table example, the possible states (combinations) are defined by constraints. Open the constraint table for the digital watch. It's relatively sparse, reflecting a certain simplicity in the model, but it's not empty. Note, for example, that the light is on if and only if button "b" is pressed. (We might arguably have omitted variable B from the model, relying on the value of Light as a way of remembering whether the button was currently pressed or not.)

What if a rule causes a transition from a state which is allowed by the constraints to one which is forbidden? In such a case, a violation is reported. To see this, change the new value for the variable Light from on to =. Now, for any state in which the light is off to begin with, the rule defines a transition to a state in which it is still off but B is pressed - violating constraints in the constraint table. If you click on Violations it will tell you which ones (in this case, either of two constraints in the constraint table is a sufficient explanation on its own; one is chosen arbitrarily).

Violating rule

You might be wondering what happens if the new value of Light is undefined or non-deterministic. Double-click on the table cell to change the '=' to '*' ("don't care"). Double-click again to clear the cell. In both cases, no violation is reported. In effect, the tool reports only definite violations: if you allow a choice that means a violation is possible but can be avoided, no error is reported. If your model is non-deterministic then it's important to be aware of this.

Next: Using Formulas for Constraints