Skip to content
Crucible logo Crucible

state/analysis

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

Package analysis performs static model-checking over a Quenched Crucible state machine. It reasons about a machine’s serializable IR — the same graph the kernel runs and the visualizers render — and reports structural defects a human is unlikely to catch by eye: states that can never be entered, transitions that can never fire, ambiguous event handling, dead ends, and states that can never reach completion.

The analysis is purely static. It never casts an instance, never fires an event, and never evaluates a guard or action — guards and actions are opaque host functions, referenced in the IR by name only, so their runtime truth is invisible to a static pass. Every check therefore reasons about the graph’s shape, not its behavior, and the package documents where that boundary makes a finding exact versus heuristic.

This is the analysis a code-first state-machine library cannot offer: because Crucible’s canonical machine is a serializable IR rather than a tangle of closures, the whole transition graph is inspectable as data. The machine config is similarly serializable, but it ships no equivalent static model-checker; here the checks fall out almost for free from the IR plus the breadth-first reachability the kernel already uses for path planning.

Usage

Section titled “Usage”
report := analysis.Analyze(machine)
for _, f := range report.Findings {
  fmt.Printf("%s [%s] %s\n", f.Severity, f.Kind, f.Message)
}

Analyze accepts a [state.Machine] built either by the Forge DSL or loaded from JSON via LoadFromJSON+Provide; both yield the same IR, so both analyze identically. Restrict the pass to a subset of checks with Only or Without.

The package imports only [state] and the standard library, preserving the kernel’s stdlib-only dependency stance.

Index

Section titled “Index”

func ShortestPaths

Section titled “func ShortestPaths”
func ShortestPaths[S comparable, E comparable, C any](m *state.Machine[S, E, C]) (map[string]Path, error)

ShortestPaths returns the shortest event sequence from the machine’s initial state to each reachable state, keyed by target state name — the `getShortestPaths` analog. It is the multi-target generalization of the kernel’s PlanPath: a breadth-first walk over the static transition graph yields, for every reachable state, one minimal path (fewest events). The initial state maps to the empty path.

It is guard-agnostic, exactly like the analysis reachability checks: guards are opaque host funcs a static pass cannot evaluate, and a guard only ever removes an edge at run time, so a state reachable here is reachable in some run, and a path found here is the shortest ignoring guard truth. For a single target whose shortest route uses no guarded edge, ShortestPaths agrees with PlanPath; where PlanPath’s entity disables a guarded edge it may return a longer path or none, while ShortestPaths reports the guard-free minimum.

The returned map is deterministic: each path is the BFS-minimal one, with ties broken by the declaration order of edges out of each state.

func SimplePaths

Section titled “func SimplePaths”
func SimplePaths[S comparable, E comparable, C any](m *state.Machine[S, E, C]) (map[string][]Path, error)

SimplePaths returns every acyclic (simple) path from the machine’s initial state to each reachable state, keyed by target state name — the `getSimplePaths` analog. A simple path visits no state twice, so enumeration always terminates even on a machine with cycles: a depth-first walk that refuses to re-enter a state already on the current path cannot loop. Each reachable state maps to the (possibly several) simple paths that reach it; the initial state maps to a single empty path.

Like ShortestPaths it is guard-agnostic — paths are enumerated over the static edges without evaluating guards — so the result is the full structural scenario set, the same exhaustive enumeration a conformance harness draws coverage from. Paths to each target are returned in a deterministic order: discovered by a declaration-order depth-first walk, then sorted by length and by their event sequence so the set is reproducible.

type Finding

Section titled “type Finding”

Finding is a single classified result of a static analysis. State names the state the finding concerns; Transition is set (as “from -on-> to”) only for transition-scoped findings.

type Finding struct {
    Kind       Kind
    Severity   Severity
    State      string
    Transition string
    Message    string
}

type Kind

Section titled “type Kind”

Kind names a category of structural defect a static pass can find.

type Kind string

The kinds of finding Analyze reports. Each is documented as exact (the IR proves it) or heuristic (the IR strongly suggests it, but a guard’s runtime truth could change the verdict).

const (
    // KindUnreachableState marks a declared state with no inbound path from the
    // initial state over the transition graph. Exact: the graph proves it, since
    // reachability ignores guards (a guard can only ever remove an edge at run
    // time, never add one, so a statically unreachable state is unreachable in
    // every run).
    KindUnreachableState Kind = "unreachable_state"


    // KindDeadTransition marks a transition whose source state is itself
    // unreachable, so the edge can never fire. Exact, for the same reason as
    // KindUnreachableState. A transition that is live but whose guard is always
    // false is out of scope: guards are opaque host funcs and cannot be evaluated
    // statically.
    KindDeadTransition Kind = "dead_transition"


    // KindNondeterministic marks a state with two or more enabled transitions
    // that a static reader cannot disambiguate: multiple guardless transitions on
    // the same event, or multiple guardless eventless ("always") transitions.
    // Exact for the guardless case — nothing at run time can break the tie. A
    // guarded overlap (same event, but each transition carries a guard) is not
    // reported: whether the guards are mutually exclusive is a runtime property
    // the IR cannot decide.
    KindNondeterministic Kind = "nondeterministic"


    // KindDeadEnd marks a non-final state with no outgoing transitions: a state
    // you can enter but never leave, yet which is not declared terminal.
    // Heuristic: a state legitimately may be terminal-by-convention without the
    // IsFinal flag, or be left only by a parent/region transition in an HSM, so
    // this is a warning, not an error.
    KindDeadEnd Kind = "dead_end"


    // KindCannotReachFinal marks a state from which no final state is reachable
    // over the transition graph, in a machine that declares at least one final
    // state: an instance there can never complete. Heuristic, because the edges
    // out of the state may be guarded and the static graph treats every guarded
    // edge as traversable; if the only paths to a final state run through guards
    // that are always false at run time, the state is stuck despite looking live
    // here. Skipped entirely when the machine declares no final states.
    KindCannotReachFinal Kind = "cannot_reach_final"
)

type Option

Section titled “type Option”

Option configures an Analyze pass. Options compose: Only then Without narrows further. With no options every check runs.

type Option func(*config)

func Only

Section titled “func Only”
func Only(kinds ...Kind) Option

Only restricts the pass to the named kinds. Repeated Only calls union their kinds.

func Without

Section titled “func Without”
func Without(kinds ...Kind) Option

Without excludes the named kinds from the pass. Applied after Only.

type Path

Section titled “type Path”

Path is one route from the machine’s initial state to a target state: the ordered events to fire and the states visited along the way. The empty path (no steps) is the initial state reaching itself. Events returns just the event labels — the input a driver would FireSeq to walk the path.

type Path struct {
    // Target is the state this path ends at.
    Target string
    // Steps are the ordered segments from the initial state to Target.
    Steps []Step
}

func (Path) Events

Section titled “func (Path) Events”
func (p Path) Events() []string

Events returns the ordered event labels of the path — the sequence a host would fire to drive an instance from the initial state to Target. An eventless segment contributes “always” (the machine auto-fires it; a driver need not).

func (Path) States

Section titled “func (Path) States”
func (p Path) States(initial string) []string

States returns the ordered states visited, starting at the initial state and ending at Target.

type Report

Section titled “type Report”

Report is the full set of findings from a single Analyze pass. The zero Report (no findings) means the machine has no defects the enabled checks could find.

type Report struct {
    Findings []Finding
}

func Analyze

Section titled “func Analyze”
func Analyze[S comparable, E comparable, C any](m *state.Machine[S, E, C], opts ...Option) Report

Analyze runs the enabled static checks over a Quenched machine and returns a classified Report. The machine’s IR is read via its serialized form, so a machine built by the Forge DSL and one loaded from JSON analyze identically. The entity type parameter is unused at run time — no instance is cast and no guard or action is evaluated — but is required to name the machine’s type.

By default every check runs. Pass Only to restrict the pass to named kinds, or Without to exclude kinds. Findings are returned in a deterministic order: grouped by check, then by state name (and event), so the report is stable across runs.

Example

ExampleAnalyze statically checks an order machine that carries two deliberate defects: a “lost” state nothing can reach, and a non-final “stuck” state with no way out. The report names both without ever firing an event.

package main


import (
  "fmt"


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


func main() {
  m := state.Forge[string, string, any]("order").
    State("open").
    Transition("open").On("pay").GoTo("paid").
    Transition("open").On("hold").GoTo("stuck").
    State("paid").
    Transition("paid").On("ship").GoTo("closed").
    State("stuck"). // non-final, no way out -> dead end
    State("closed").Final().
    State("lost"). // declared but nothing transitions to it -> unreachable
    Transition("lost").On("found").GoTo("open").
    Initial("open").
    Quench()


  report := analysis.Analyze(m)
  for _, f := range report.Findings {
    fmt.Printf("%s [%s] %s\n", f.Severity, f.Kind, f.State)
  }


}

Output

Section titled “Output”
error [unreachable_state] lost
error [dead_transition] lost
warning [dead_end] stuck
warning [cannot_reach_final] stuck

func (Report) Empty

Section titled “func (Report) Empty”
func (r Report) Empty() bool

Empty reports whether the analysis found nothing.

func (Report) HasErrors

Section titled “func (Report) HasErrors”
func (r Report) HasErrors() bool

HasErrors reports whether any finding is an error-severity (IR-proven) defect.

func (Report) OfKind

Section titled “func (Report) OfKind”
func (r Report) OfKind(k Kind) []Finding

OfKind returns the findings of a single kind, in report order.

func (Report) String

Section titled “func (Report) String”
func (r Report) String() string

String renders the report as one line per finding, in report order.

type Severity

Section titled “type Severity”

Severity ranks a finding’s seriousness.

type Severity string

Finding severities. Error marks a defect the IR proves; Warning marks a heuristic finding a human should confirm.

const (
    SeverityError   Severity = "error"
    SeverityWarning Severity = "warning"
)

type Step

Section titled “type Step”

Step is one segment of a path: the event that fires from the segment’s source state, and the destination state it leads to. A path is read as: starting at the initial state, fire Step[0].Event to reach Step[0].To, then Step[1].Event, and so on. A path segment carries its event plus the resulting `state`).

type Step struct {
    // Event is the string label of the event fired for this segment; "always" for an
    // eventless transition traversed on the path.
    Event string
    // From is the state the segment is fired from.
    From string
    // To is the state reached after firing Event.
    To  string
}

Generated by gomarkdoc