Laying Out State Machine Properties

The layout

State machine properties are very similar to regular stateful properties, conceptually speaking. They share the same three major components:

• A model, which represents what the system should do at a high level.
• A generator for commands, which represent the execution flow of the program.
• An actual system, which is validated against our model.

Since FSM properties are really a specialization of stateful properties, the differences are subtle.