state/verify

import "github.com/stablekernel/crucible/state/verify"

Package verify checks behavioral properties of a Quenched Crucible state machine and returns, for every property it decides, a witness: the concrete event sequence that proves or refutes the claim.

Overview

Where github.com/stablekernel/crucible/state/analysis reports structural defects (unreachable states, dead transitions, nondeterminism) as a flat catalog, verify answers questions a caller poses about reachability, safety, liveness, configuration invariants, bounded simulation, scenario coverage, and covering-suite generation. It is the property-checking layer that sits on top of the analysis graph primitives rather than a second copy of them.

Structural model and fidelity guarantee

Every check in this package reasons over a guard-agnostic structural model of the machine’s state space. The model is built from the machine’s public IR — the same representation a JSON-loaded machine produces — so no instance is cast and no guard or action is evaluated at check time.

Guard-agnostic means: the model assumes guards pass. A guard can only ever prune a transition at run time, never add one, so the structural model is a superset of any real machine’s execution space. As a result:

A state the model calls reachable is reachable in some run (the witness fires events that drive an instance there when guards cooperate).
An unreachable verdict means the model finds no structural path, which means no guard assignment can make it reachable in any run.

The model’s reachability verdict is cross-checked against the [analysis] package’s authoritative [analysis.KindUnreachableState] pass: verify consumes that proven set rather than re-deriving it, so both packages agree on which states are reachable and the two layers are consistent by construction.

The property checks

Verify takes a [state.Machine] and a tail of functional Option values that select which properties to check. Each decided property becomes a Finding. With no options, Verify checks reachability of every declared state.

Reachable restricts the reachability check to named target states. With no Reachable option, Verify checks every declared state.

ReachAvoiding adds a conditional-reachability check — “reach X along some run that never passes through Y”. The search prunes every configuration whose active states intersect the avoid-set, honoring hierarchy: a configuration is “in Y” when any active leaf, enclosing ancestor, or initial-descent member is Y, so avoiding a region leaf, a superstate, or a sibling initial-descent state each forbids the whole configuration it belongs to. A satisfiable finding carries the witnessing event sequence; an unsatisfiable one carries the zero Witness.

AlwaysEventually adds a liveness check — from every reachable configuration, the target is always eventually reachable (the CTL eventuality AG EF target). The check is answered by reverse reachability from the target: a reachable configuration from which the target can never be reached is a counterexample. A holding verdict (Reachable true) carries the zero Witness; a failing one carries the route to the nearest stuck configuration — a target-free terminal or a node in a target-free cycle — from which the target can never be reached.

CheckInvariant adds configuration invariants — predicates over the active-state configuration that must hold in every reachable configuration. Build invariants with MutualExclusion, Implies, or NeverActive. The exploration models the full set of co-active leaves over the configuration-product space, so orthogonal parallel regions advancing independently are modeled faithfully. A violation carries the shortest route to the nearest configuration that breaks the predicate; its Witness.Target names that configuration as a ’|‘-joined list of active leaves.

SimulateBounded adds bounded exhaustive simulation — it enumerates the machine’s event sequences up to a depth bound over the same configuration-product space, evaluates a caller-supplied Oracle at every reached configuration, and reports the shortest trace whose configuration the oracle rejects. A violation is real and replayable; a clean run is a bounded guarantee only (see Caveats below).

Coverage adds structural-coverage analysis — it replays a set of scenarios (each an ordered event sequence) over the configuration-product explorer and reports which reachable states and transitions they exercise against the reachable universe. The full breakdown is read with Result.Coverage; the accompanying Finding’s Reachable field is true exactly when nothing is left uncovered. An event that names no enabled transition from the current configuration is a clean no-op, mirroring a kernel Fire of an unhandled event.

Covering-suite generation

Alongside the property checkers, CoveringSuite is a producer: it generates a set of typed event sequences that together exercise every reachable state and transition, walking the same configuration-product explorer greedily until nothing reachable is left uncovered. Feeding its output back into Coverage reports 100% coverage of the reachable universe — that round-trip is the suite’s guarantee. The suite is deterministic and stable across runs; it is a covering suite, not a provably minimal one (the generator favors a small, deterministic result over minimum cardinality). MaxScenarioLength caps each scenario’s event count, splitting coverage across more, shorter sequences.

Witnesses and conformance cross-check

A witness is an [analysis.Path] whose Events are the event sequence a driver fires to drive an instance from the initial configuration to the target. For reachability and conditional reachability, the witness proves the property: a test suite can replay it through the conformance harness and confirm the instance lands in the target state. For liveness and invariant violations, the witness is a counterexample: replaying it drives an instance into the stuck or violating configuration, making the defect tangible and drivable.

This cross-check discipline is the package’s reproducibility contract: every non-trivial witness produced by verify has been confirmed replayable by the package’s own conformance cross-check tests, tying the static claim to the kernel’s executable semantics.

Caveats

Guard-agnostic analysis is a structural over-approximation. The model is deliberately wider than any guarded execution, so it can only prove that a property holds structurally or that a structural path exists — it cannot account for guard predicates narrowing the real run space. In practice:

A reachable verdict means “reachable if the guards cooperate”. If a guard in the real machine always blocks the path, the state is structurally but not practically reachable; that is a modeling concern, not a verify defect.
An unreachable verdict is exact: no run can reach the state regardless of guard values.

Bounded simulation is NOT a proof of absence. A holding SimulateBounded verdict (“no violation within the bound”) guarantees only that the oracle held across every configuration reachable in at most the given number of events. A violation may still exist in a longer trace. A violation it does report is real and replayable. For an exact, unbounded verdict over fixed structural predicates, use CheckInvariant instead.

Configuration invariants and all other checks are configuration-level — predicates over the set of active states. Context-value or symbolic reasoning (predicates over the runtime context type C, guard expressions, or data-flow properties) is a separate capability not provided by this package.

Usage

result := verify.Verify(machine,
    verify.Reachable("shipped"),
    verify.AlwaysEventually("delivered"),
    verify.CheckInvariant(verify.MutualExclusion("held", "paid")),
    verify.SimulateBounded("never-shipped", 5, myOracle),
    verify.Coverage([]string{"pay", "ship"}),
)
for _, f := range result.Findings {
    fmt.Println(f.Kind, f.State, f.Reachable)
}

Verify never returns nil and never panics: a machine whose IR cannot be read yields an empty result rather than an error, honoring the kernel’s no-panic contract for read-only inspection.

The package imports only [state], the analysis package, and the standard library, preserving the kernel’s stdlib-only dependency stance. The API is designed to grow additively: new property checks arrive as new Option constructors and new FindingKind values without changing the signatures callers already depend on.

Index

func CoveringSuite[S comparable, E comparable, C any](m *state.Machine[S, E, C], opts …SuiteOption) [][]E
type CoverageReport
type Finding
type FindingKind
type Invariant
type Option
type Oracle
type Result
type SuiteOption
- func MaxScenarioLength(n int) SuiteOption
type Witness

func CoveringSuite

func CoveringSuite[S comparable, E comparable, C any](m *state.Machine[S, E, C], opts ...SuiteOption) [][]E

CoveringSuite generates a covering suite for a Quenched machine: a set of typed event sequences that together exercise every reachable state and every reachable transition. Feed the suite to Coverage and the report shows full coverage of the reachable universe — that round-trip is the suite’s guarantee.

The suite is built by a greedy walk of the same configuration-product explorer the other checks use: scenarios are grown from the initial configuration, each extended to pick up not-yet-covered transitions, until none remain uncovered. It is a covering suite, not a provably minimal one: the generator favors a small, deterministic suite over a minimum-cardinality one, which is a harder optimization it does not attempt.

The result is deterministic and stable across runs. A single-state machine, or any machine whose initial configuration has no outgoing transition, yields a single empty scenario — the initial configuration is covered with nothing to fire. A machine with no initial state yields an empty suite. Unreachable states and the transitions out of them are ignored: the suite covers the reachable space only, exactly the universe Coverage measures against.

Options tune the walk: MaxScenarioLength caps each scenario’s event count, splitting coverage across more, shorter scenarios. Options are additive — new tuning arrives as new constructors without changing this signature.

Example

ExampleCoveringSuite generates a covering suite — a set of event sequences that together exercise every reachable state and transition — and confirms it by feeding it straight back into Coverage, which reports full coverage. The suite is the seed for a conformance test set built from the machine’s structure alone.

package main

import (
  "fmt"

  "github.com/stablekernel/crucible/state"
  "github.com/stablekernel/crucible/state/verify"
)

func main() {
  m := state.Forge[string, string, any]("order").
    State("open").
    Transition("open").On("pay").GoTo("paid").
    Transition("open").On("abandon").GoTo("canceled").
    State("paid").
    Transition("paid").On("ship").GoTo("shipped").
    State("canceled").Final().
    State("shipped").Final().
    Initial("open").
    Quench()

  suite := verify.CoveringSuite(m)
  rep, _ := verify.Verify(m, verify.Coverage(suite...)).Coverage()
  fmt.Printf("suite: %v\n", suite)
  fmt.Printf("covers states: %.0f%%, transitions: %.0f%%\n",
    rep.StateCoverage()*100, rep.TransitionCoverage()*100)

}

Output

suite: [[pay ship] [abandon]]
covers states: 100%, transitions: 100%

type CoverageReport

CoverageReport is the structural-coverage breakdown a Coverage pass produces: which reachable states and transitions a scenario set exercises, the universe it is measured against, and the concrete uncovered remainder. Read it from a Result with Result.Coverage. The zero report describes a machine with an empty universe — 100%-covered by convention, since there is nothing to cover.

type CoverageReport struct {
    // CoveredStates are the reachable states the scenarios entered, sorted.
    CoveredStates []string
    // UncoveredStates are the reachable states no scenario entered, sorted — the
    // state gap a scenario set leaves.
    UncoveredStates []string
    // CoveredTransitions are the reachable transitions the scenarios fired, each
    // rendered "from -on-> to", sorted.
    CoveredTransitions []string
    // UncoveredTransitions are the reachable transitions no scenario fired, each
    // rendered "from -on-> to", sorted — the transition gap a scenario set leaves.
    UncoveredTransitions []string
}

func (CoverageReport) StateCoverage

func (c CoverageReport) StateCoverage() float64

StateCoverage returns the fraction of reachable states the scenarios entered, in the range [0,1]. A machine with no reachable states is fully covered (1) by convention, since there is nothing left to cover.

func (CoverageReport) String

func (c CoverageReport) String() string

String renders the coverage breakdown as two labeled lines — states and transitions — each with its covered/total count, percentage, and the uncovered remainder, so a report is human-readable and diffable.

func (CoverageReport) TransitionCoverage

func (c CoverageReport) TransitionCoverage() float64

TransitionCoverage returns the fraction of reachable transitions the scenarios fired, in the range [0,1]. A machine with no reachable transitions is fully covered (1) by convention.

type Finding

Finding is one decided property about one state. Kind names the property, State names the subject, and Reachable carries the reachability verdict. When the property holds with supporting evidence, Witness is the route that proves it; an unreachable state carries the zero Witness.

type Finding struct {
    // Kind is the property this finding decides.
    Kind FindingKind
    // State is the state the finding concerns.
    State string
    // Reachable is the property verdict for the state. For reachability and
    // conditional-reachability kinds it is true when the (possibly constrained)
    // target is reachable. For [KindLiveness] it is true when the target is always
    // eventually reachable from every reachable configuration — so a true verdict
    // is the desirable one and a false verdict carries a counterexample.
    Reachable bool
    // Witness is the supporting route. For reachability and conditional
    // reachability it is the proving event sequence when the property holds, and
    // the zero Witness when it does not. For [KindLiveness] the witness is inverted:
    // a holding verdict carries the zero Witness, while a failing verdict carries
    // the route to the stuck configuration from which the target can never be
    // reached, whose Target names that configuration.
    Witness Witness
    // contains filtered or unexported fields
}

type FindingKind

FindingKind names the property a Finding decides. New kinds are added as new property checks land; a consumer should treat an unrecognized kind as informational rather than failing on it.

type FindingKind string

The property kinds verify can decide. V1 ships reachability; later additions extend this set without changing existing values.

const (
    // KindReachability is the verdict on whether a declared state can be entered
    // in some run of the machine, starting from the initial state. It is exact:
    // reachability is computed guard-agnostically, and a guard can only ever prune
    // an edge at run time, never add one, so a state reachable here is reachable in
    // some run and an unreachable verdict holds in every run.
    KindReachability FindingKind = "reachability"

    // KindConditionalReachability is the verdict on whether a target state can be
    // reached along some run that never passes through any state in a declared
    // avoid-set — the "reach X without entering Y" safety/reachability property. It
    // is exact in the same sense as KindReachability: the constrained search is
    // guard-agnostic, and a guard can only ever prune an edge at run time, never
    // add one, so a clean route found here exists in some run and an unsatisfiable
    // verdict (every route crosses the avoid-set) holds in every run. A satisfiable
    // finding carries the witnessing event sequence; an unsatisfiable one carries
    // the zero Witness.
    KindConditionalReachability FindingKind = "conditional_reachability"

    // KindLiveness is the verdict on whether a target state is always eventually
    // reachable: from every reachable configuration, can the target still be
    // reached? It is the CTL eventuality AG EF target. It is exact in the same
    // sense as KindReachability: the reverse-reachability computation is
    // guard-agnostic, and a guard can only ever prune an edge at run time, never
    // add one, so a configuration from which the structural graph offers no route
    // to the target has no run to it in any instance, and a holding verdict holds
    // in every run. A holding finding (Reachable true) carries the zero Witness; a
    // failing one carries a counterexample witness: the route to a reachable
    // configuration — a target-free terminal or cycle — from which the target can
    // never be reached.
    KindLiveness FindingKind = "liveness"

    // KindInvariant is the verdict on whether a configuration invariant — a
    // predicate over the active-state configuration, such as mutual exclusion,
    // implication, or never-active — holds in every reachable configuration. It is
    // exact in the same guard-agnostic sense as KindReachability: the
    // configuration-product exploration is guard-agnostic, and a guard can only ever
    // prune an edge at run time, never add one, so a configuration reachable
    // structurally is reachable in some run and a holding verdict holds in every run.
    // A holding finding (Reachable true) carries the zero Witness; a failing one
    // carries a counterexample witness: the shortest route to a reachable
    // configuration that violates the predicate, whose Target names that
    // configuration.
    KindInvariant FindingKind = "invariant"

    // KindBoundedViolation is the verdict of a bounded exhaustive simulation: a
    // caller-supplied oracle was evaluated at every configuration reachable within a
    // depth bound, and either held throughout (Reachable true, zero Witness) or was
    // rejected by some reachable configuration (Reachable false), in which case the
    // Witness is the shortest trace — the event sequence that drives the machine
    // into the rejected configuration, whose Target names it. Unlike the other
    // kinds it is NOT exact: a holding verdict means only that the oracle held
    // across the configurations reachable within the bound, never that it holds in
    // every run. A violation, by contrast, is real: the reported trace is replayable
    // and the oracle genuinely fails at the reached configuration.
    KindBoundedViolation FindingKind = "bounded_violation"

    // KindCoverage is the verdict of a structural-coverage analysis: a set of
    // scenarios (event sequences) was replayed over the configuration-product
    // explorer and the states and transitions they exercised were measured against
    // the reachable universe. Its Reachable field is true when the scenario set
    // leaves no reachable state and no reachable transition uncovered (full
    // coverage), false otherwise. The full breakdown — covered and uncovered states
    // and transitions with their fractions — is read with [Result.Coverage] rather
    // than from a Witness, since coverage concerns a whole universe rather than a
    // single configuration. It is guard-agnostic like the other kinds: the universe
    // is the structural reachable space, so an uncovered element is a real gap a
    // scenario set leaves unexercised.
    KindCoverage FindingKind = "coverage"
)

type Invariant

Invariant is a named predicate over a reachable configuration’s active-state set. Construct one with MutualExclusion, Implies, or NeverActive and pass it to CheckInvariant. Its Invariant.Label is the stable identity a Result indexes the resulting Finding by.

type Invariant struct {
    // contains filtered or unexported fields
}

func Implies

func Implies(antecedent, consequent string) Invariant

Implies builds the invariant “whenever antecedent is active, consequent is active too” — the co-presence/implication property. It is violated by a reachable configuration in which antecedent is active and consequent is not.

func MutualExclusion

func MutualExclusion(a, b string) Invariant

MutualExclusion builds the invariant “states a and b are never simultaneously active in any reachable configuration”. It is violated by a reachable configuration whose active set contains both a and b — for example two leaves of orthogonal parallel regions that advance independently. The order of a and b does not affect the verdict; the label is canonicalized so MutualExclusion(a,b) and MutualExclusion(b,a) share an identity.

func NeverActive

func NeverActive(s string) Invariant

NeverActive builds the invariant “state s is never active in any reachable configuration”. It holds when s is unreachable or otherwise never enters any reachable configuration’s active set, and is violated by the first reachable configuration that activates s.

func (Invariant) Label

func (inv Invariant) Label() string

Label returns the invariant’s stable identity — the key a Result.Invariant lookup uses and the name a report prints. Two invariants built from the same constructor and arguments share a label.

type Option

Option configures a Verify pass. Options compose left to right; with no options Verify checks reachability of every declared state. The option set is designed to grow additively: new property checks arrive as new Option constructors without changing the Verify signature.

type Option func(*config)

func AlwaysEventually

func AlwaysEventually(target string) Option

AlwaysEventually adds a liveness check: from every reachable configuration, is the target state still eventually reachable? This is the CTL eventuality AG EF target — the property “no matter where a run has gone, it can always still make progress to target”. The pass adds one Finding of KindLiveness for target.

The finding holds (its Reachable field is true, with the zero Witness) when every reachable configuration retains some run that reaches target. It fails (Reachable false) when some reachable configuration can never reach target — a configuration parked in a target-free terminal or a target-free cycle. A failing finding carries a counterexample witness: the shortest event sequence from the initial state to that stuck configuration, whose Target names the stuck state. Replaying the witness drives an instance into the trap.

Liveness is exact in the same guard-agnostic sense as reachability: a guard can only ever prune an edge at run time, never add one, so a configuration from which the structural graph offers no route to target has no run to target in any instance, and a holding verdict means every reachable configuration keeps a structural route to target. A target that is not a declared state yields no finding. Repeated AlwaysEventually calls each add their own check.

Example

ExampleAlwaysEventually checks a liveness property: from every reachable configuration, can the order still eventually reach “delivered”? Here a parcel can be marked “lost”, a terminal that delivered can never follow — so the property fails and the counterexample names the stuck configuration.

package main

import (
  "fmt"

  "github.com/stablekernel/crucible/state"
  "github.com/stablekernel/crucible/state/verify"
)

func main() {
  m := state.Forge[string, string, any]("parcel").
    State("shipped").
    Transition("shipped").On("arrive").GoTo("delivered").
    Transition("shipped").On("misroute").GoTo("lost").
    State("lost").Final(). // a terminal from which delivered is unreachable
    State("delivered").Final().
    Initial("shipped").
    Quench()

  result := verify.Verify(m, verify.AlwaysEventually("delivered"))
  f, _ := result.Liveness("delivered")
  fmt.Printf("always delivered: %t; stuck at %q via %v\n",
    f.Reachable, f.Witness.Target, f.Witness.Events())

}

Output

always delivered: false; stuck at "lost" via [misroute]

func CheckInvariant

func CheckInvariant(inv Invariant, more ...Invariant) Option

CheckInvariant adds one or more configuration invariants to the pass: predicates over the active-state configuration that must hold in every reachable configuration. Build invariants with MutualExclusion, Implies, or NeverActive. The pass adds one Finding of KindInvariant per invariant, keyed by the invariant’s Invariant.Label.

A finding holds (its Reachable field is true, with the zero Witness) when the predicate is satisfied by every reachable configuration. It fails (Reachable false) when some reachable configuration violates the predicate; the finding then carries a counterexample witness: the shortest event sequence from the initial state to the nearest violating configuration, whose Target names that configuration (a ’|‘-joined list of its active leaves). Replaying the witness drives an instance into the violating configuration.

Predicates are over the active configuration of states only — pure structural IR, with no runtime context or guard values consulted. Invariant checking is exact in the same guard-agnostic sense as reachability: a guard can only ever prune an edge at run time, never add one, so a configuration reachable structurally is reachable in some run, a structural violation is a real reachable violation, and a holding verdict means every reachable configuration satisfies the predicate. Repeated CheckInvariant calls each add their invariants.

Example

ExampleCheckInvariant checks a configuration invariant: that a parcel is never both “held” and “delivered” at once. The two regions of a parallel state can advance independently, so the configuration where both are active is reachable, the invariant is violated, and the counterexample names that configuration.

package main

import (
  "fmt"

  "github.com/stablekernel/crucible/state"
  "github.com/stablekernel/crucible/state/verify"
)

func main() {
  m := state.Forge[string, string, any]("parcel").
    State("created").
    Transition("created").On("dispatch").GoTo("transit").
    SuperState("transit").
    Region("Custody").Initial("held").
    SubState("held").On("release").GoTo("delivered").
    SubState("delivered").Final().
    EndRegion().
    Region("Billing").Initial("unpaid").
    SubState("unpaid").On("pay").GoTo("paid").
    SubState("paid").Final().
    EndRegion().
    EndSuperState().
    Initial("created").
    Quench()

  inv := verify.MutualExclusion("held", "paid")
  result := verify.Verify(m, verify.CheckInvariant(inv))
  f, _ := result.Invariant(inv.Label())
  fmt.Printf("%s holds: %t; violated at %q via %v\n",
    inv.Label(), f.Reachable, f.Witness.Target, f.Witness.Events())

}

Output

mutex(held,paid) holds: false; violated at "held|paid" via [dispatch pay]

func Coverage

func Coverage[E comparable](scenarios ...[]E) Option

Coverage adds a structural-coverage analysis: replay a set of scenarios — each an ordered event sequence — over the machine and report which reachable states and transitions they exercise, against the universe of reachable states and transitions the explorer enumerates. The pass adds a single Finding of KindCoverage; read the breakdown with Result.Coverage.

Each scenario is replayed over the same guard-agnostic configuration-product explorer the other property checks reason over, so the coverage metric is consistent with verify’s model: an event drives the configuration along the same structural edge the explorer follows, the states entered are the active configurations the run visits, and the transitions fired are the structural edges it traverses. An event that names no enabled transition from the current configuration is a clean no-op — it advances nothing and is neither an error nor counted — exactly as a kernel Fire of an unhandled event is ignored.

The universe a scenario set is measured against is the reachable universe: the reachable states (every state active in some reachable configuration) and the reachable transitions (every structural edge fired between reachable configurations). An empty scenario set is valid and yields 0% coverage with the full universe reported uncovered.

Coverage is exact in the same guard-agnostic sense as the other checks: a guard can only ever prune an edge at run time, never add one, so a state or transition the explorer marks reachable is reachable in some run, and the uncovered set is a real structural gap a scenario set leaves unexercised. Repeated Coverage calls union their scenarios.

Example

ExampleCoverage measures which states and transitions a scenario set exercises against the reachable universe, so a CI gate can flag the structural gap a test suite leaves. Here a single happy-path scenario covers the shipping line but leaves the cancellation branch unexercised.

package main

import (
  "fmt"

  "github.com/stablekernel/crucible/state"
  "github.com/stablekernel/crucible/state/verify"
)

func main() {
  m := state.Forge[string, string, any]("order").
    State("open").
    Transition("open").On("pay").GoTo("paid").
    Transition("open").On("abandon").GoTo("canceled").
    State("paid").
    Transition("paid").On("ship").GoTo("shipped").
    State("canceled").Final().
    State("shipped").Final().
    Initial("open").
    Quench()

  result := verify.Verify(m, verify.Coverage([]string{"pay", "ship"}))
  rep, _ := result.Coverage()
  fmt.Printf("state coverage: %.0f%%\n", rep.StateCoverage()*100)
  fmt.Printf("uncovered states: %v\n", rep.UncoveredStates)
  fmt.Printf("uncovered transitions: %v\n", rep.UncoveredTransitions)

}

Output

state coverage: 75%
uncovered states: [canceled]
uncovered transitions: [open -abandon-> canceled]

func ReachAvoiding

func ReachAvoiding(target string, avoid ...string) Option

ReachAvoiding adds a conditional-reachability check: is target reachable along some run that never passes through any state in avoid? The pass adds one Finding of KindConditionalReachability for target, carrying the witnessing event sequence when a clean route exists, or marked unsatisfiable (no witness) when every route to target must cross an avoided state.

Avoid membership honors hierarchy: a run “passes through” an avoid state when that state is active in any configuration the run visits — as the entered state itself, as an enclosing ancestor, or as an initial-descent member of a composite or parallel configuration. Avoiding a region leaf, a superstate, or a sibling initial-descent state therefore each forbids the whole configuration it belongs to.

An empty avoid set makes this plain reachability. A target that is not a declared state yields no finding. Repeated ReachAvoiding calls each add their own check; the avoid set of a single call is unioned across that call’s arguments.

Example

ExampleReachAvoiding checks a safety property: can the order reach “shipped” along a run that never passes through “canceled”? The clean route exists, and its witness is the event sequence that proves it without ever canceling.

package main

import (
  "fmt"

  "github.com/stablekernel/crucible/state"
  "github.com/stablekernel/crucible/state/verify"
)

func main() {
  m := state.Forge[string, string, any]("order").
    State("open").
    Transition("open").On("pay").GoTo("paid").
    Transition("open").On("abandon").GoTo("canceled").
    State("paid").
    Transition("paid").On("ship").GoTo("shipped").
    State("canceled").Final().
    State("shipped").Final().
    Initial("open").
    Quench()

  result := verify.Verify(m, verify.ReachAvoiding("shipped", "canceled"))
  f, _ := result.ConditionalReach("shipped")
  fmt.Printf("shipped without canceling: %t via %v\n", f.Reachable, f.Witness.Events())

}

Output

shipped without canceling: true via [pay ship]

func Reachable

func Reachable(states ...string) Option

Reachable restricts the reachability check to the named target states. Repeated Reachable calls union their targets. A requested name that is not a declared state simply yields no finding (verify reports on declared states only). With no Reachable option, Verify checks every declared state.

Example

ExampleReachable restricts the pass to named target states.

package main

import (
  "fmt"

  "github.com/stablekernel/crucible/state"
  "github.com/stablekernel/crucible/state/verify"
)

func main() {
  m := state.Forge[string, string, any]("toggle").
    State("off").
    Transition("off").On("flip").GoTo("on").
    State("on").
    Transition("on").On("flip").GoTo("off").
    Initial("off").
    Quench()

  result := verify.Verify(m, verify.Reachable("on"))
  fmt.Printf("%d finding(s): on reachable=%t\n", len(result.Findings), result.CanReach("on"))

}

Output

1 finding(s): on reachable=true

func SimulateBounded

func SimulateBounded(label string, depth int, oracle Oracle) Option

SimulateBounded adds a bounded exhaustive simulation: enumerate the machine’s event sequences (traces) up to depth events deep, evaluate the Oracle at every reached configuration, and report the shortest trace whose configuration the oracle rejects. The pass adds one Finding of KindBoundedViolation keyed by label.

The oracle receives the full active configuration — active leaves plus enclosing ancestors — and returns whether the property HOLDS there (true acceptable, false a violation). The search reuses the configuration-product explorer, so a parallel machine’s orthogonal regions advance independently and the oracle sees true co-active leaf sets. The initial configuration is evaluated at depth 0; a depth of 0 therefore checks only the initial configuration, and a negative depth is treated as 0.

The finding holds (its Reachable field is true, with the zero Witness) when the oracle accepts every configuration reachable within the bound. It fails (Reachable false) when some reachable configuration is rejected; the finding then carries the shortest violating trace — the breadth-first-minimal event sequence to that configuration, whose Target names it (a ’|‘-joined list of its active leaves). Replaying the trace drives an instance into the rejected configuration, where the oracle genuinely fails.

Bounded simulation is a bounded guarantee, not a proof: “no violation within the bound” means only that the oracle held across every configuration reachable in at most depth events. A violation may still exist in a longer trace. For an exact, unbounded verdict over the fixed structural predicates, use CheckInvariant. A violation reported here, however, is real and replayable. Repeated SimulateBounded calls each add their own check.

Example

ExampleSimulateBounded explores every trace up to a depth bound and reports the shortest one whose reached configuration a caller-supplied oracle rejects. Here the oracle flags any configuration where the order is “shipped”, so the bounded search returns the shortest trace that drives the machine there.

package main

import (
  "fmt"

  "github.com/stablekernel/crucible/state"
  "github.com/stablekernel/crucible/state/verify"
)

func main() {
  m := state.Forge[string, string, any]("order").
    State("open").
    Transition("open").On("pay").GoTo("paid").
    State("paid").
    Transition("paid").On("ship").GoTo("shipped").
    State("shipped").Final().
    Initial("open").
    Quench()

  // The oracle holds (true) until the order is shipped.
  oracle := func(active map[string]bool) bool { return !active["shipped"] }
  result := verify.Verify(m, verify.SimulateBounded("never-shipped", 5, oracle))
  f, _ := result.BoundedSim("never-shipped")
  fmt.Printf("held within bound: %t; violation at %q via %v\n",
    f.Reachable, f.Witness.Target, f.Witness.Events())

}

Output

held within bound: false; violation at "shipped" via [pay ship]

type Oracle

Oracle is a caller-supplied predicate over a reached configuration’s active-state set, evaluated by SimulateBounded at every configuration the bounded search reaches. It receives the full active configuration — every active leaf plus every enclosing ancestor that must be active for it, the same set the invariant predicates see — and reports whether the property HOLDS there: return true when the configuration is acceptable, false to flag it as a violation.

An Oracle must be a pure function of its argument: bounded simulation evaluates it many times across the reachable space and reuses the verdict, so a side-effecting or nondeterministic oracle breaks the determinism guarantee.

type Oracle func(active map[string]bool) bool

type Result

Result is the outcome of a Verify pass: one Finding per decided property, in a deterministic order. The zero Result carries no findings.

type Result struct {
    // Findings are the decided properties, ordered by kind then by state name so
    // the report is reproducible.
    Findings []Finding
    // contains filtered or unexported fields
}

func Verify

func Verify[S comparable, E comparable, C any](m *state.Machine[S, E, C], opts ...Option) *Result

Verify checks behavioral properties of a Quenched machine and returns a Result carrying one Finding per decided property, each with a witness where one exists. The machine’s IR is read via its serialized form — no instance is cast and no guard or action is evaluated — so a machine built by the Forge DSL and one loaded from JSON verify identically.

With no options, Verify checks reachability of every declared state. Pass Reachable to restrict the pass to named target states. Options are additive: later property checks arrive as new option constructors without changing this signature.

Verify never returns nil and never panics: a machine whose IR cannot be read yields an empty result rather than an error, honoring the kernel’s no-panic contract for read-only inspection.

Example

ExampleVerify checks that an order machine’s terminal state is reachable and prints the event sequence that proves it, without ever firing an event.

package main

import (
  "fmt"

  "github.com/stablekernel/crucible/state"
  "github.com/stablekernel/crucible/state/verify"
)

func main() {
  m := state.Forge[string, string, any]("order").
    State("open").
    Transition("open").On("pay").GoTo("paid").
    State("paid").
    Transition("paid").On("ship").GoTo("shipped").
    State("shipped").Final().
    Initial("open").
    Quench()

  result := verify.Verify(m, verify.Reachable("shipped"))
  f, _ := result.For("shipped")
  fmt.Printf("shipped reachable: %t via %v\n", f.Reachable, f.Witness.Events())

}

Output

shipped reachable: true via [pay ship]

Example (Unreachable)

ExampleVerify_unreachable lists the states a machine declares but can never enter — the marquee reachability defect, found statically.

package main

import (
  "fmt"

  "github.com/stablekernel/crucible/state"
  "github.com/stablekernel/crucible/state/verify"
)

func main() {
  m := state.Forge[string, string, any]("order").
    State("open").
    Transition("open").On("close").GoTo("closed").
    State("closed").Final().
    State("orphan"). // nothing transitions here
    Initial("open").
    Quench()

  fmt.Println(verify.Verify(m).Unreachable())

}

Output

[orphan]

func (*Result) BoundedSim

func (r *Result) BoundedSim(label string) (Finding, bool)

BoundedSim returns the bounded-simulation finding for a label and whether one exists. A finding exists only for a label a SimulateBounded option requested. Its Reachable field is the bounded verdict — true when the oracle held across every configuration reachable within the depth bound — and its Witness, when the verdict is false, is the shortest trace to the rejected configuration, whose Target names that configuration. A holding verdict is a bounded guarantee only, not a proof of absence.

func (*Result) CanReach

func (r *Result) CanReach(stateName string) bool

CanReach reports whether the named state is reachable. An undeclared state is not reachable.

func (*Result) ConditionalReach

func (r *Result) ConditionalReach(target string) (Finding, bool)

ConditionalReach returns the conditional-reachability finding for a target and whether one exists. A finding exists only for a target a ReachAvoiding option requested that is also a declared state; its Reachable field is the satisfiability verdict (true when a route avoiding the forbidden set exists), and its Witness is the proving event sequence when satisfiable.

func (*Result) Coverage

func (r *Result) Coverage() (CoverageReport, bool)

Coverage returns the structural-coverage breakdown and whether one exists. A report exists only when a Coverage option was passed. Its Reachable companion finding (see KindCoverage) is true exactly when the report leaves nothing uncovered; the report itself carries the covered and uncovered states and transitions and their fractions.

func (*Result) For

func (r *Result) For(stateName string) (Finding, bool)

For returns the reachability finding for a single state and whether one exists. A state that is not declared in the machine has no finding.

func (*Result) Initial

func (r *Result) Initial() string

Initial returns the machine’s initial state name, the anchor a witness’s visited-state list begins at. It is "" when the machine declares no initial state.

func (*Result) Invariant

func (r *Result) Invariant(label string) (Finding, bool)

Invariant returns the invariant finding for an invariant label and whether one exists. A finding exists only for an invariant a CheckInvariant option requested; look up the label with Invariant.Label. Its Reachable field is the invariant verdict — true when the predicate holds in every reachable configuration — and its Witness, when the verdict is false, is the route to the nearest reachable configuration that violates the predicate, whose Target names that configuration.

func (*Result) Liveness

func (r *Result) Liveness(target string) (Finding, bool)

Liveness returns the liveness finding for a target and whether one exists. A finding exists only for a target an AlwaysEventually option requested that is also a declared state. Its Reachable field is the liveness verdict — true when the target is always eventually reachable from every reachable configuration — and its Witness, when the verdict is false, is the route to a reachable configuration from which the target can never be reached.

func (*Result) OK

func (r *Result) OK() bool

OK reports whether the result contains no defect: no checked state is unreachable.

func (*Result) String

func (r *Result) String() string

String renders the result as one line per finding, in finding order, so a report is human-readable and diffable. A reachability finding shows its witness event sequence when the state is reachable, or is marked unreachable; a conditional-reachability finding reads as satisfiable (with its avoid-free witness) or unsatisfiable.

func (*Result) Unreachable

func (r *Result) Unreachable() []string

Unreachable returns the names of every declared state that cannot be entered, in sorted order. An empty result means every checked state is reachable.

type SuiteOption

SuiteOption configures a CoveringSuite generation. Options compose left to right; with no options the generator emits an unbounded greedy covering suite.

type SuiteOption func(*suiteConfig)

func MaxScenarioLength

func MaxScenarioLength(n int) SuiteOption

MaxScenarioLength caps the number of events in any single generated scenario. A covering walk that would exceed the cap is split: the generator ends the current scenario and starts a fresh one from the initial configuration to pick up the remaining uncovered transitions, so the union still covers everything — just across more, shorter scenarios. A non-positive bound is treated as unbounded.

type Witness

Witness is the concrete evidence for a Finding: the route from the machine’s initial state to the finding’s state. It is the same path type the analysis package enumerates, so a witness is a first-class artifact a driver can replay — Witness.Events is exactly the event sequence to fire. An empty witness (no steps) is the initial state reaching itself, or the absence of evidence for a property that does not hold.

type Witness = analysis.Path

Generated by gomarkdoc