The abstract state data type. This type must be immutable. The state type that encodes the abstract state. The abstract state should model all the features we need from the real state, the system under test. We should leave out all details that aren't needed for specifying our pre- and postconditions. The state type must be called State and be immutable.

The command generator. Given an abstract state, the generator should return a command that is allowed to run in that state. Note that it is still neccessary to define preconditions on the commands if there are any. The generator is just giving a hint of which commands that are suitable for a given state, the preconditions will still be checked before a command runs. Sometimes you maybe want to adjust the distribution of your command generator according to the state, or do other calculations based on the state.

initialState should reset the system under test to a well defined initial state, and return the abstract version of that state.

Abstract commands are defined as subtypes of the traits Command or SetCommand. Each command must have a run method and a method that returns the new abstract state, as it should look after the command has been run. A command can also define a precondition that states how the current abstract state must look if the command should be allowed to run. Finally, we can also define a postcondition which verifies that the system under test is in a correct state after the command exectution.

A command that binds its result for later use