glyde/testing

A harness for driving a sans-IO state machine, and for running every ordering of a set of inputs against an invariant.

It drives any machine of the shape state plus input gives a new state and a list of outputs, which is glyde’s three and any of yours built the same way.

let gw = fn(shard, input) {
  let gateway.Step(shard:, outputs:) = gateway.step(shard, input)
  #(shard, outputs)
}

let inputs = [zombie_beat, peer_close, late_resumed]
assert testing.every_ordering(gw, shard, inputs, fn(run) {
    list.count(run.outputs, is_open) <= 1
  })
  == testing.Held

Hold time still across a permutation run: a machine that reads a clock out of its own state sees timestamped inputs out of time order otherwise.

Types

A timer waiting to fire, at an absolute time on the clock.

pub type Armed(input, timer) {
  Armed(timer: timer, at_ms: Int, fires: input)
}

Constructors

  • Armed(timer: timer, at_ms: Int, fires: input)

The time, the state, what the machine has emitted, and the timers it is waiting on. Time moves only when you move it, and never backwards.

Timers is passed to feed and advance rather than stored here: a record holding a closure cannot be compared against a literal.

pub type Clock(state, input, output, timer) {
  Clock(
    now_ms: Int,
    state: state,
    outputs: List(output),
    armed: List(Armed(input, timer)),
  )
}

Constructors

  • Clock(
      now_ms: Int,
      state: state,
      outputs: List(output),
      armed: List(Armed(input, timer)),
    )

    Arguments

    outputs

    Everything emitted since the clock was made, or since flush.

    armed

    Waiting timers, soonest first. Two due at the same instant fire in the order they were armed.

A state machine this harness can drive: one input, a new state and whatever it emitted on the way. Timer wiring is a separate Timers, and classifying an output is an argument to notes and without_notes.

pub type Machine(state, input, output) =
  fn(state, input) -> #(state, List(output))

One distinct result, and every ordering that produced it.

pub type Outcome(input, observation) {
  Outcome(observed: observation, orderings: List(List(input)))
}

Constructors

  • Outcome(observed: observation, orderings: List(List(input)))

Where a machine ended up and everything it emitted getting there.

pub type Run(state, output) {
  Run(state: state, outputs: List(output))
}

Constructors

  • Run(state: state, outputs: List(output))

advance gave up: fired timers went off and still_due were due before the deadline, which is a machine re-arming a zero delay.

The clock is the one the firing stopped on, so time has not reached the deadline and nothing armed is in the past.

pub type Stall(state, input, output, timer) {
  Stalled(
    clock: Clock(state, input, output, timer),
    fired: Int,
    still_due: Int,
  )
}

Constructors

  • Stalled(
      clock: Clock(state, input, output, timer),
      fired: Int,
      still_due: Int,
    )

What one output does to the timer table. One or the other: a single output arms a timer or cancels one, and there is no way to say both.

pub type TimerEffect(input, timer) {
  Arms(timer: timer, in_ms: Int, fires: input)
  Cancels(timer: timer)
}

Constructors

  • Arms(timer: timer, in_ms: Int, fires: input)

    A timer the machine asked for, and the input that firing it delivers.

  • Cancels(timer: timer)

How a test wants the machine’s timer outputs recognised.

Without this a test writes Fired(Reconnect, Stamp(1)) by hand, and a guessed stamp is dropped as stale while the test asserts the silence.

let timers =
  testing.Timers(effect: fn(output) {
    case output {
      gateway.ArmTimer(timer:, in_ms:, stamp:) ->
        Some(testing.Arms(
          timer:,
          in_ms:,
          fires: gateway.Fired(timer, stamp),
        ))
      gateway.CancelTimer(timer) -> Some(testing.Cancels(timer))
      _ -> None
    }
  })
pub type Timers(input, output, timer) {
  Timers(
    effect: fn(output) -> option.Option(TimerEffect(input, timer)),
  )
}

Constructors

  • Timers(
      effect: fn(output) -> option.Option(TimerEffect(input, timer)),
    )

    Arguments

    effect

    What this output does to the timer table, if it touches it at all.

Why both runners refuse a set of inputs, rather than hang on it.

pub type TooMany {
  TooManyToPermute(inputs: Int)
}

Constructors

  • TooManyToPermute(inputs: Int)

    n! orderings of this many inputs is not a test, it is a hang.

What every ordering of a set of inputs did to an invariant.

pub type Verdict(state, input, output) {
  Held
  Broke(
    ordering: List(input),
    broke_after: List(input),
    run: Run(state, output),
  )
  Refused(TooMany)
}

Constructors

  • Held

    Every ordering satisfied it.

  • Broke(
      ordering: List(input),
      broke_after: List(input),
      run: Run(state, output),
    )

    One did not, and here it is.

    Arguments

    ordering

    The full ordering. Hand it back to drive to reproduce.

    broke_after

    The shortest prefix of ordering that already broke the invariant. Empty means the starting state was already failing.

    run

    The run of broke_after.

  • Refused(TooMany)

    Past max_permuted, so nothing ran.

Values

pub fn advance(
  machine: fn(state, input) -> #(state, List(output)),
  timers: Timers(input, output, timer),
  clock: Clock(state, input, output, timer),
  by_ms: Int,
) -> Result(
  Clock(state, input, output, timer),
  Stall(state, input, output, timer),
)

Move time forward, firing every timer that comes due, soonest first.

A timer armed while advancing and still due before the new time fires in the same call, as a real event loop does. by_ms below zero is zero.

Error(Stalled(..)) once max_firings have gone off with more still due, which is a machine re-arming a zero delay.

pub fn advance_to_next(
  machine: fn(state, input) -> #(state, List(output)),
  timers: Timers(input, output, timer),
  clock: Clock(state, input, output, timer),
) -> Result(
  Clock(state, input, output, timer),
  Stall(state, input, output, timer),
)

Move time to the soonest armed deadline and fire it, along with anything else due at that instant. No change when nothing is armed.

pub fn armed_at(
  clock: Clock(state, input, output, timer),
  timer: timer,
) -> option.Option(Int)

When timer is next due, as an absolute time on this clock.

pub fn clock(state: state) -> Clock(state, input, output, timer)

A clock at zero holding state, with nothing armed.

pub fn drive(
  machine: fn(state, input) -> #(state, List(output)),
  state: state,
  inputs: List(input),
) -> Run(state, output)

Fold the inputs through the machine, keeping every output in the order it came out.

pub fn every_ordering(
  machine: fn(state, input) -> #(state, List(output)),
  state: state,
  inputs: List(input),
  invariant: fn(Run(state, output)) -> Bool,
) -> Verdict(state, input, output)

Run every ordering of inputs from state, checking invariant on the starting state and after every input.

It must be a safety property. A liveness one is false at the start, so every ordering comes back Broke(broke_after: []).

The shortest break is reported, and among equals the earliest ordering.

pub fn feed(
  machine: fn(state, input) -> #(state, List(output)),
  timers: Timers(input, output, timer),
  clock: Clock(state, input, output, timer),
  input: input,
) -> Clock(state, input, output, timer)

Deliver one input at the current time, then apply whatever its outputs said about timers.

pub fn feed_all(
  machine: fn(state, input) -> #(state, List(output)),
  timers: Timers(input, output, timer),
  clock: Clock(state, input, output, timer),
  inputs: List(input),
) -> Clock(state, input, output, timer)

Deliver several inputs at the current time, in order.

pub fn final_state(run: Run(state, output)) -> state

The projection for “did every ordering land in the same state”.

pub fn flush(
  clock: Clock(state, input, output, timer),
) -> Clock(state, input, output, timer)

Forget the outputs so far, so the next assertion covers only what the next inputs produce. Time, state and armed timers are untouched.

pub const max_firings: Int

Timers one advance fires before it gives up. Our choice: far above any real chain of deadlines, far below a hang.

pub const max_permuted: Int

The most inputs the runners below will permute. Eight is 40 320 orderings and nine is nine times that, so eight is our choice.

pub fn no_timers() -> Timers(input, output, timer)

For a machine that arms nothing. The clock then only tracks time.

pub fn notes(
  is_note: fn(output) -> Bool,
  outputs: List(output),
) -> List(output)

Keep only the diagnostics. Asserting that a stale timer was recognised and dropped says more than asserting that nothing happened.

pub fn orderings(items: List(a)) -> List(List(a))

Every ordering of items: the identity first, then by the position each item held. The order is part of this module’s contract.

n items give n! orderings, and unlike the runners this refuses nothing.

pub fn outcomes(
  machine: fn(state, input) -> #(state, List(output)),
  state: state,
  inputs: List(input),
  observe: fn(Run(state, output)) -> observation,
) -> Result(List(Outcome(input, observation)), TooMany)

Run every ordering of inputs and group them by what observe makes of each run.

One group means every ordering converged, which is the question an invariant cannot answer: you have to have thought of a failure to assert against it.

Groups come out in first-seen order and orderings within a group in enumeration order. Grouping is by == on the observation.

pub fn without_notes(
  is_note: fn(output) -> Bool,
  outputs: List(output),
) -> List(output)

Drop the diagnostics, so a table row asserts the protocol effects and nothing else.

is_note is True for outputs that are diagnostics and never protocol-significant. fn(_) { False } for a machine that emits none.

Search Document