Property-Based Testing

Property tests assert an invariant over every generated input, not one path.

The runner

runProperty(arb, predicate) generates values, feeds each to the predicate, fails on first false. Import from @mantaq/pbt.

• fc is fast-check’s full API. @mantaq/pbt adds: anyDuration, anySmallDuration, anyPayload, anyName, anyActorSnapshot.
• MANTAQ_SEED env var overrides the fixed default seed. Default numRuns: 100.

Deadline-exactness invariant

Machine in submitting schedules submittingDone after timeoutMs. VirtualClock.advance(ms) is synchronous, fires timers, drains queue.

import { Actor, VirtualClock } from "@mantaq/core";
import { fc, runProperty } from "@mantaq/pbt";

runProperty(
  fc.tuple(fc.integer({ min: 0, max: 1000 }), fc.integer({ min: 0, max: 1000 })),
  ([timeoutMs, advanceMs]) => {
    const clock = new VirtualClock();
    const actor = new Actor({
      clock,
      inputs: [],
      internal: [submittingDone],
      states: [basicInfo, shippingAddress, payment, submitting, success],
      initial: submitting,
      setup: (m) => {
        m.on(submitting, submittingDone, () => ({ state: success }));
        m.effect(submitting, {
          name: "startSubmitTimeout",
          fn: ({ signal, clock: c, emit }) => {
            c.setTimeout(timeoutMs, () => emit(submittingDone.create()), { signal });
          },
        });
      },
    });
    clock.advance(advanceMs);
    const inSuccess = actor.snapshot().path[0] === "success";
    return advanceMs >= timeoutMs ? inSuccess : !inSuccess;
  },
);

internal: [submittingDone] marks it machine-internal so external sends cannot fake the deadline.

Back-navigation invariant

From any pre-payment step, mashing back never reaches a final state.

runProperty(fc.integer({ min: 0, max: 10 }), (presses) => {
  const clock = new VirtualClock();
  const actor = new Actor({
    inputs: [back, submitBasicInfo, submitShipping],
    states: [basicInfo, shippingAddress, payment, success, error],
    initial: basicInfo,
    setup: (m) => {
      m.on(basicInfo, submitBasicInfo, () => ({ state: shippingAddress }));
      m.on(shippingAddress, back, () => ({ state: basicInfo }));
      m.on(shippingAddress, submitShipping, () => ({ state: payment }));
      m.on(payment, back, () => ({ state: shippingAddress }));
    },
  });

  for (let i = 0; i < presses; i++) {
    const current = actor.snapshot().path[0];
    actor.send(back.create());
    if (actor.snapshot().path[0] === "payment") return false;
    if (current === "basicInfo" && actor.snapshot().path[0] !== "basicInfo") return false;
  }
  return actor.snapshot().done !== true;
});

Seeding and CI

• Default seed is fixed. CI runs are deterministic, failures reproducible.
• Set MANTAQ_SEED=<n> to explore new input regions or replay a counterexample.