Search⌘ K

How State Machine Properties Run

Explore how PropEr runs state machine properties by generating sequences of commands in an abstract phase and applying them to the real system in a testing phase. Understand the use of initial states, preconditions, postconditions, and state transitions to validate system behavior. This lesson helps you grasp the mechanisms behind testing finite state machines effectively.

We'll cover the following...

Abstract phase

PropEr divides the execution of a finite state machine test into two phases, one abstract and one real. The abstract phase is used to create a test scenario using the model and command generation callbacks to build out the sequence of calls that will later be applied to the system.

A graphical representation might look like this:

The two big conceptual ...