Model-Based Testing

/**
 * Generate arrays of commands for model-based testing
 * @param commandArbs - Array of arbitraries generating commands
 * @param constraints - Size and depth constraints
 * @returns Arbitrary generating command sequences
 */
function commands<Model, Real, CheckAsync>(
  commandArbs: Arbitrary<AsyncCommand<Model, Real, CheckAsync>>[],
  constraints?: CommandsContraints
): Arbitrary<Iterable<AsyncCommand<Model, Real, CheckAsync>>>;

interface CommandsContraints {
  maxCommands?: number;
  size?: SizeForArbitrary;
  disableReplayLog?: boolean;
}

/**
 * Run synchronous commands over a model and real system
 * @param s - Setup function returning initial model and real system
 * @param cmds - Iterable of commands to execute
 * @throws If model and real behaviors diverge
 */
function modelRun<Model, Real, InitialModel>(
  s: ModelRunSetup<InitialModel, Real>,
  cmds: Iterable<Command<Model, Real>>
): void;

/**
 * Run asynchronous commands over a model and real system
 * @param s - Setup function (sync or async) returning initial state
 * @param cmds - Iterable of async commands to execute
 * @returns Promise that resolves if consistent, rejects on inconsistency
 */
function asyncModelRun<Model, Real, CheckAsync, InitialModel>(
  s: ModelRunSetup<InitialModel, Real> | ModelRunAsyncSetup<InitialModel, Real>,
  cmds: Iterable<AsyncCommand<Model, Real, CheckAsync>>
): Promise<void>;

/**
 * Run scheduled asynchronous commands with a scheduler
 * @param scheduler - Scheduler controlling async execution order
 * @param s - Setup function returning initial state
 * @param cmds - Iterable of async commands to execute
 * @returns Promise that resolves if consistent, rejects on inconsistency
 */
function scheduledModelRun<Model, Real, CheckAsync, InitialModel>(
  scheduler: Scheduler,
  s: ModelRunSetup<InitialModel, Real> | ModelRunAsyncSetup<InitialModel, Real>,
  cmds: Iterable<AsyncCommand<Model, Real, CheckAsync>>
): Promise<void>;

type ModelRunSetup<Model, Real> = () => { model: Model; real: Real };

type ModelRunAsyncSetup<Model, Real> = () => Promise<{ model: Model; real: Real }>;

/**
 * Base interface for all commands
 */
interface ICommand<Model, Real, RunResult, CheckAsync extends boolean> {
  /**
   * Check if command can run in current model state (precondition)
   * @param m - Current model state
   * @returns true if command can run
   */
  check(m: Readonly<Model>): boolean;

  /**
   * Execute command on real system
   * @param m - Current model state
   * @param r - Real system
   * @returns Command result (sync or async based on CheckAsync)
   */
  run(m: Model, r: Real): CheckAsync extends true ? Promise<RunResult> : RunResult;
}

/**
 * Synchronous command interface
 */
interface Command<Model, Real> extends ICommand<Model, Real, void, false> {
  check(m: Readonly<Model>): boolean;
  run(m: Model, r: Real): void;
}

/**
 * Asynchronous command interface
 */
interface AsyncCommand<Model, Real, CheckAsync extends boolean> extends ICommand<Model, Real, void, CheckAsync> {
  check(m: Readonly<Model>): CheckAsync extends true ? Promise<boolean> | boolean : boolean;
  run(m: Model, r: Real): CheckAsync extends true ? Promise<void> : void;
}

import {
  commands,
  asyncModelRun,
  property,
  assert,
  integer,
  Arbitrary,
  AsyncCommand,
  constant,
} from 'fast-check';

// Real system: simple counter
class Counter {
  private value = 0;

  increment(): void {
    this.value++;
  }

  decrement(): void {
    this.value--;
  }

  getValue(): number {
    return this.value;
  }
}

// Model: number representing counter value
type Model = { count: number };
type Real = Counter;

// Command: Increment
class IncrementCommand implements AsyncCommand<Model, Real, false> {
  check(m: Readonly<Model>): boolean {
    return true; // Always allowed
  }

  run(m: Model, r: Real): void {
    m.count++;
    r.increment();
    // Verify consistency
    if (r.getValue() !== m.count) {
      throw new Error(`Inconsistency: model=${m.count}, real=${r.getValue()}`);
    }
  }

  toString(): string {
    return 'Increment';
  }
}

// Command: Decrement
class DecrementCommand implements AsyncCommand<Model, Real, false> {
  check(m: Readonly<Model>): boolean {
    return m.count > 0; // Only allow if count is positive
  }

  run(m: Model, r: Real): void {
    m.count--;
    r.decrement();
    // Verify consistency
    if (r.getValue() !== m.count) {
      throw new Error(`Inconsistency: model=${m.count}, real=${r.getValue()}`);
    }
  }

  toString(): string {
    return 'Decrement';
  }
}

// Command: Check value
class CheckValueCommand implements AsyncCommand<Model, Real, false> {
  constructor(private expectedValue: number) {}

  check(m: Readonly<Model>): boolean {
    return m.count === this.expectedValue;
  }

  run(m: Model, r: Real): void {
    if (r.getValue() !== this.expectedValue) {
      throw new Error(`Expected ${this.expectedValue}, got ${r.getValue()}`);
    }
  }

  toString(): string {
    return `CheckValue(${this.expectedValue})`;
  }
}

// Create command arbitraries
const allCommands = [
  constant(new IncrementCommand()),
  constant(new DecrementCommand()),
  integer({ min: 0, max: 10 }).map((n) => new CheckValueCommand(n)),
];

// Test the counter
assert(
  property(commands(allCommands, { maxCommands: 100 }), async (cmds) => {
    const setup = () => ({
      model: { count: 0 },
      real: new Counter(),
    });
    await asyncModelRun(setup, cmds);
  })
);

import { scheduler, scheduledModelRun, commands, property, assert, constant } from 'fast-check';

assert(
  property(
    scheduler(),
    commands(asyncCommandArbs, { maxCommands: 10 }),
    async (s, cmds) => {
      await scheduledModelRun(s, setup, cmds);
    }
  )
);

class AddItemCommand implements AsyncCommand<Model, Real, false> {
  constructor(private item: Item) {}

  check(m: Readonly<Model>): boolean {
    return m.items.length < 100;
  }

  async run(m: Model, r: Real): Promise<void> {
    m.items.push(this.item);
    await r.addItem(this.item);
    // Verify
    const realItems = await r.getItems();
    assert.deepEqual(realItems, m.items);
  }

  toString(): string {
    return `AddItem(${JSON.stringify(this.item)})`;
  }
}

// Generate commands with random items
const addItemArb: Arbitrary<AddItemCommand> = record({
  id: uuid(),
  name: string(),
}).map((item) => new AddItemCommand(item));

type SizeForArbitrary =
  | 'xsmall'
  | 'small'
  | 'medium'
  | 'large'
  | 'xlarge'
  | '='
  | number
  | { min?: number; max?: number };