Introduction to State Machine Properties

Finite state machines

Finite state machines (FSM) are, informally speaking, an abstraction describing specific stateful programs. The program can be in only one of the multiple known states at a time (such as a traffic light being red, yellow, or green). Transitions from one state to another are based on specific inputs or events. Within each state, the program may behave differently.

Why use state machine properties

Let’s imagine a program that should take special measures, like forbidding some actions or enabling new features, depending on whether network connectivity is good, bad, or entirely unavailable. Testing such a program with stateful properties while keeping them deterministic would create a large number of possible cases. If there are six possible events and three possible states, we get at least eighteen possible combinations of calls versus states. We would have to do quite a bit of filtering in preconditions to hope to cover all kinds of transitions.

To help with this, PropEr provides finite state machine properties, which allow us to specifically model state machines. State names and transitions are made into first-class citizens, which allow us to adequately explore their expected transitions in a less cumbersome manner than would be required with regular stateful properties or example tests.

Finite-state properties are specifically helpful when users interact with the system while perceiving multiple states instead of knowing that the system has an internal state machine. To put it another way, state machine properties are for when the model itself is a state machine, instead of the system. If there are no specific, discernible states for the user, and therefore no specific, discernible states for the model, then regular stateful properties are more appropriate.