Type Alias: CtlCounterExample

CtlCounterExample = { kind: "finite_path"; trace: number[]; } | { cycle: number[]; kind: "lasso"; prefix: number[]; }

Defined in: src/types/temporal.ts:137

A counterexample witness for a failing CTL formula.

Remarks

A union discriminated by kind:

finite_path — trace is a sequence of state IDs s₀ → s₁ → … → sₖ showing how the formula fails starting at s₀.
lasso — a finite prefix followed by an infinitely repeating cycle, demonstrating persistent failure (used for EG/AG violations).

if (result.counterexample?.kind === 'lasso') {
  console.log(result.counterexample.prefix, result.counterexample.cycle);
}