Model-Based Testing for Stateful Systems

Relevant source files

The following files were used as context for generating this wiki page:

• packages/fast-check/src/arbitrary/commands.ts
• packages/fast-check/src/check/model/ModelRunner.ts
• examples/004-stateMachine/musicPlayer/main.spec.ts
• examples/004-stateMachine/musicPlayer/model-based/MusicPlayerModel.ts
• packages/fast-check/test/unit/check/model/commands/CommandWrapper.spec.ts
• website/blog/2023-05-21-whats-new-in-fast-check-3-9-0/index.md

Model-based testing in fast-check is a powerful feature for verifying the correctness of stateful systems. It involves creating a simplified software model of the system under test and defining a series of commands that can be executed against both the model and the real system. fast-check then generates sequences of these commands, executing them and comparing the state of the real system to the state of the model. This approach is highly effective at finding bugs in complex state transitions and interactions.

The core idea is to check if the real system's behavior consistently matches the model's expected behavior across a vast number of generated scenarios. When a discrepancy is found, fast-check automatically shrinks the sequence of commands to the minimal failing case, making debugging significantly easier.

Core Concepts

Model-based testing in fast-check is built upon three main pillars: the Model, the Commands, and the Command Arbitrary.

The Model

The model is a simplified representation of the system under test. It should capture the state and the logic of state transitions but can omit implementation details not relevant to the properties being tested. It is typically implemented as a class.

For instance, a model for a music player would track properties like isPlaying and volume.

// examples/004-stateMachine/musicPlayer/model-based/MusicPlayerModel.ts:10-14
export class MusicPlayerModel {
  isPlaying = false;
  volume = 50;
  // ...
}

Sources: examples/004-stateMachine/musicPlayer/model-based/MusicPlayerModel.ts:10-14

Commands

Commands represent the actions that can be performed on the system. Each command must be defined to operate on both the model and the real system. fast-check provides Command<Model, Real> and AsyncCommand<Model, Real> interfaces for synchronous and asynchronous operations, respectively.

A command has two primary methods:

• check(model: Readonly<Model>): boolean: A precondition that determines if the command can be executed in the current state of the model.
• run(model: Model, real: Real): void | Promise<void>: The execution logic. This method performs the action on the real system, updates the model's state, and asserts that the real system's state matches the model's new state.

The following diagram illustrates the structure of a command.

This diagram shows the Command interface and example implementations.
Sources: packages/fast-check/src/arbitrary/commands.ts:28-44, examples/004-stateMachine/musicPlayer/model-based/MusicPlayerModel.ts:16-30, 48-64

The Command Arbitrary (fc.commands)

The fc.commands arbitrary is responsible for generating sequences of executable commands. It takes an array of arbitraries, where each arbitrary produces a specific type of command. It also accepts constraints like maxCommands to limit the length of the generated sequences.

// examples/004-stateMachine/musicPlayer/main.spec.ts:16-23
const allCommands = [
  fc.constant(new PlayCommand()),
  fc.constant(new StopCommand()),
  fc.record({
    v: fc.integer({ min: 0, max: 100 }),
  }).map((r) => new VolumeCommand(r.v)),
];

const commandsArb = fc.commands(allCommands, { maxCommands: 10 });

In this example, fc.commands will generate arrays of PlayCommand, StopCommand, and VolumeCommand instances.
Sources: packages/fast-check/src/arbitrary/commands.ts:119-143, examples/004-stateMachine/musicPlayer/main.spec.ts:16-23

Execution Flow

The execution of a model-based test is managed by a runner function, which orchestrates the generation and execution of command sequences.

The Model Runner (fc.modelRun)

The fc.modelRun function is the engine that drives the testing process. It is used within an fc.assert property. It takes a setup function that initializes the model and the real system, and an arbitrary that generates command sequences (typically fc.commands).

For each generated sequence, fc.modelRun iterates through the commands and performs the following steps for each one:

1. Precondition Check: It calls command.check(model) to verify if the command can run in the current model state. If not, the command is skipped.
2. Execution: If the precondition passes, it calls command.run(model, real). This method updates both the model and the real system.
3. Post-condition Assertion: Inside run, assertions are made to ensure the state of the real system is consistent with the model.

Sources: packages/fast-check/src/check/model/ModelRunner.ts:23-57

Sequence Diagram of a Test Run

The following diagram shows the interaction between the test runner, the model, and the real system during a single test run.

This diagram illustrates the check and run phases for a single command within a sequence.
Sources: packages/fast-check/src/check/model/ModelRunner.ts:45-53

Key Interfaces and Classes

Command<Model, Real> Interface

This is the central interface for defining synchronous commands.

Method	Description
check(m: Readonly<Model>): boolean	A precondition to check if the command can be executed against the current model state.
run(m: Model, r: Real): void	Executes the command on the model and the real system, and asserts for consistency.
toString(): string	Provides a string representation of the command, used for reporting failures.

Sources: packages/fast-check/src/arbitrary/commands.ts:28-44

CommandWrapper Class

Internally, fast-check wraps each command instance in a CommandWrapper. This wrapper adds metadata and functionality, such as:

• Tracking Execution: A hasRan flag to know if the command's run method has been executed.
• Cloning: A clone() method that allows fast-check to re-create command sequences during the shrinking process. If the underlying command has a [cloneMethod], it will be used; otherwise, the same command reference is kept.
• String Representation: It delegates toString to the underlying command.

The CommandWrapper ensures that the state of each command in a sequence is properly managed throughout the testing and shrinking phases.
Sources: packages/fast-check/src/arbitrary/commands.ts:57-117, packages/fast-check/test/unit/check/model/commands/CommandWrapper.spec.ts:10-101

Practical Example: Music Player

Let's look at a concrete implementation using the MusicPlayer example.

Defining the Model

The model class holds the state variables.

// examples/004-stateMachine/musicPlayer/model-based/MusicPlayerModel.ts:10-14
export class MusicPlayerModel {
  isPlaying = false;
  volume = 50;
  // ...
}

Sources: examples/004-stateMachine/musicPlayer/model-based/MusicPlayerModel.ts:10-14

Implementing Commands

Here is an example of the PlayCommand. The check method ensures we only play if the player is currently stopped. The run method calls play() on the real object, updates the model's isPlaying state, and then asserts that the real player's state matches.

// examples/004-stateMachine/musicPlayer/model-based/MusicPlayerModel.ts:16-30
class PlayCommand implements fc.Command<MusicPlayerModel, MusicPlayer> {
  check = (m: Readonly<MusicPlayerModel>) => !m.isPlaying;
  run = (m: MusicPlayerModel, r: MusicPlayer) => {
    r.play();
    m.isPlaying = true;
    expect(r.isPlaying).toBe(true);
  };
  toString = () => `play`;
}

Sources: examples/004-stateMachine/musicPlayer/model-based/MusicPlayerModel.ts:16-30

Setting up the Property Test

The test is defined using fc.assert and fc.modelRun. The setup function provides initial instances of the model and the real system for each test run.

// examples/004-stateMachine/musicPlayer/main.spec.ts:25-32
it('should run the same way as the model', () => {
  fc.assert(
    fc.property(commandsArb, (cmds) => {
      const s = () => ({ model: new MusicPlayerModel(), real: new MusicPlayer() });
      fc.modelRun(s, cmds);
    })
  );
});

Sources: examples/004-stateMachine/musicPlayer/main.spec.ts:25-32

Asynchronous Model Testing

For systems with asynchronous operations, fast-check provides AsyncCommand<Model, Real> and scheduledModelRun.

• AsyncCommand: Similar to Command, but its run method can return a Promise.
• scheduledModelRun: A specialized runner for asynchronous commands that integrates with fc.scheduler to test for race conditions. A bug was fixed in this runner to prevent potential infinite loops where the model would wait endlessly for tasks that failed to schedule.

Sources: packages/fast-check/src/arbitrary/commands.ts:46-55, packages/fast-check/src/check/model/ModelRunner.ts:65-102, website/blog/2023-05-21-whats-new-in-fast-check-3-9-0/index.md

Conclusion

Model-based testing with fast-check offers a structured and automated way to find bugs in stateful applications. By abstracting the system's behavior into a model and a set of commands, developers can leverage property-based testing to explore a vast state space of interactions that would be impractical to cover with traditional unit tests. The automatic shrinking of failing test cases further solidifies its role as an efficient tool for building robust and reliable software.