Command.php

<?php

declare(strict_types=1);

namespace Rasuvaeff\PropertyTesting\StateMachine;

/**
 * A single operation in a stateful / model-based test.
 *
 * A command bundles the four responsibilities of model-based testing:
 * whether it may run in a given model state ({@see preCondition()}), how the
 * model evolves ({@see nextState()}), how the real system executes it
 * ({@see run()}), and how the observed result is checked against the model
 * ({@see postCondition()}). Sequences of commands are generated by
 * {@see \Rasuvaeff\PropertyTesting\Gen::commands()} and driven by
 * {@see StateMachine::check()}.
 *
 * The model is an immutable value threaded through the sequence: {@see nextState()}
 * must return the new model rather than mutate the given one, so the runner and
 * the generator can replay it deterministically. {@see preCondition()},
 * {@see nextState()} and {@see postCondition()} must be pure — only {@see run()}
 * touches the system under test.
 *
 * @api
 */
interface Command extends \Stringable
{
    /**
     * May this command run in the given (pre-state) model? Gates both generation
     * and, during replay, whether the runner executes or skips the command.
     */
    public function preCondition(mixed $model): bool;

    /**
     * The model's expected state after this command. Pure; returns the new model
     * and never touches the system under test.
     */
    public function nextState(mixed $model): mixed;

    /**
     * Execute this command against the system under test and return the observed
     * result for {@see postCondition()} to check. The pre-state model is provided
     * for commands whose action depends on it.
     */
    public function run(mixed $model, mixed $system): mixed;

    /**
     * Verify the observed result against the pre-state model. Return false (or
     * throw) to falsify the property.
     */
    public function postCondition(mixed $model, mixed $result): bool;
}