StateMachine

Rasuvaeff\PropertyTesting\StateMachine\StateMachine

Class — Source

Drives a CommandSequence against a fresh system under test for stateful / model-based testing.

Call it from a property body with the generated sequence and a factory that builds a fresh system per run:

#[Property]
public function stackMatchesModel(CommandSequence $sequence): void
{
    StateMachine::check($sequence, static fn(): Stack => new Stack());
}

For each command it re-checks Command::preCondition() against the running model and skips the command if it no longer holds — shrinking may have dropped an earlier step that a later precondition depended on, so a replayed sequence stays sound without the arbitrary re-validating every candidate. A passing precondition runs the command, asserts Command::postCondition() (throwing PostconditionViolation on failure), then advances the model.

Methods

check()

static check(StateMachine\CommandSequence $sequence, Closure $system): void