Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
33 changes: 31 additions & 2 deletions state/analysis/analysis.go
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,15 @@ const (
// 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"

// KindDuplicateState marks two distinct declared states that flatten to the
// same name. The analysis graph keys nodes by the state's rendered name, so a
// collision (two states in different regions or branches whose names render
// identically) would silently merge into one node and quietly mask the other
// state's reachability, dead-end, and liveness defects. Surfacing it as a
// finding makes the ambiguity explicit instead of analyzing a graph that does
// not match the declared machine.
KindDuplicateState Kind = "duplicate_state"
)

// Severity ranks a finding's seriousness.
Expand Down Expand Up @@ -154,6 +163,16 @@ func Analyze[S comparable, E comparable, C any](m *state.Machine[S, E, C], opts
}

var r Report
if cfg.enabled(KindDuplicateState) {
for _, name := range g.duplicates {
r.Findings = append(r.Findings, Finding{
Kind: KindDuplicateState,
Severity: SeverityError,
State: name,
Message: fmt.Sprintf("state %q is declared more than once; its analysis node collides and other declarations are masked", name),
})
}
}
if cfg.enabled(KindUnreachableState) {
checkUnreachable(g, &r)
}
Expand Down Expand Up @@ -271,6 +290,9 @@ type graph struct {
initial string
hasInitial bool
hasFinal bool
// duplicates names every state that collided with an already-recorded node
// during flatten, in declaration order, so Analyze can surface the ambiguity.
duplicates []string
}

// buildGraph serializes the machine to its IR and flattens the (possibly
Expand Down Expand Up @@ -349,8 +371,15 @@ func flatten[S comparable, E comparable, C any](g *graph, s *state.State[S, E, C
}
}

g.nodes[name] = n
g.order = append(g.order, name)
if _, exists := g.nodes[name]; exists {
// A second state flattened to a name already recorded: the graph would
// otherwise silently merge the two. Record the collision so Analyze reports
// it; keep the first node so the rest of the pass stays deterministic.
g.duplicates = append(g.duplicates, name)
} else {
g.nodes[name] = n
g.order = append(g.order, name)
}

for i := range s.Children {
flatten(g, &s.Children[i], name)
Expand Down
49 changes: 49 additions & 0 deletions state/analysis/analysis_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,55 @@ func TestUnreachableState(t *testing.T) {
}
}

// collKey is a state type whose String renders only its Name, so two distinct
// keys with the same Name collide when the analysis graph flattens them by their
// rendered name. It models the real hazard: distinct typed states (here in
// separate branches) that are indistinguishable once stringified.
type collKey struct {
ID int
Name string
}

func (c collKey) String() string { return c.Name }

// TestDuplicateState_CollisionIsReported proves that two distinct states whose
// rendered names collide are surfaced as a duplicate_state error rather than
// being silently merged into one analysis node.
func TestDuplicateState_CollisionIsReported(t *testing.T) {
a := collKey{ID: 1, Name: "dup"}
b := collKey{ID: 2, Name: "dup"}
final := collKey{ID: 3, Name: "done"}

m := state.Forge[collKey, string, any]("coll").
State(a).
Transition(a).On("go").GoTo(final).
State(b).
Transition(b).On("go").GoTo(final).
State(final).Final().
Initial(a).
Quench()

r := analysis.Analyze(m)
dups := r.OfKind(analysis.KindDuplicateState)
if len(dups) == 0 {
t.Fatalf("expected a duplicate_state finding for the colliding name; report:\n%s", r)
}
for _, f := range dups {
if f.State != "dup" {
t.Fatalf("duplicate_state finding state = %q, want dup", f.State)
}
if f.Severity != analysis.SeverityError {
t.Fatalf("duplicate_state finding should be an error, got %s", f.Severity)
}
}

// Without restricts the pass: excluding the kind suppresses the finding.
rr := analysis.Analyze(m, analysis.Without(analysis.KindDuplicateState))
if len(rr.OfKind(analysis.KindDuplicateState)) != 0 {
t.Fatalf("Without(KindDuplicateState) should suppress the finding; report:\n%s", rr)
}
}

func TestDeadTransition(t *testing.T) {
// The self-loop on the unreachable "orphan" can never fire.
m := forge("dead-transition").
Expand Down
8 changes: 4 additions & 4 deletions state/analysis/paths.go
Original file line number Diff line number Diff line change
Expand Up @@ -23,10 +23,10 @@ import (
// conformance harness draws from.

// 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`).
// 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 to
// reach Step[1].To, and so on. Each segment carries its source state (From), the
// fired event (Event), and the state reached (To).
type Step struct {
// Event is the string label of the event fired for this segment; "always" for an
// eventless transition traversed on the path.
Expand Down
36 changes: 36 additions & 0 deletions state/analysis/paths_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,42 @@ func TestShortestPaths_CoversAllReachable(t *testing.T) {
}
}

// TestPath_StatesAndEvents asserts Path.States renders the ordered states visited
// (initial first, Target last) and stays consistent with Path.Events: a path of n
// steps yields n events and n+1 states.
func TestPath_StatesAndEvents(t *testing.T) {
paths, err := analysis.ShortestPaths(feedbackMachine())
if err != nil {
t.Fatalf("ShortestPaths: %v", err)
}

// The empty path (initial state reaching itself) is just the initial state.
if got := paths["question"].States("question"); len(got) != 1 || got[0] != "question" {
t.Fatalf("States for the empty path = %v, want [question]", got)
}

// A two-step path to thanks via form: question -> form -> thanks.
simple, err := analysis.SimplePaths(feedbackMachine())
if err != nil {
t.Fatalf("SimplePaths: %v", err)
}
viaForm := simple["thanks"][1] // sorted shortest-first; [1] is the two-step route
states := viaForm.States("question")
wantStates := []string{"question", "form", "thanks"}
if len(states) != len(wantStates) {
t.Fatalf("States = %v, want %v", states, wantStates)
}
for i := range wantStates {
if states[i] != wantStates[i] {
t.Fatalf("States[%d] = %q, want %q (full %v)", i, states[i], wantStates[i], states)
}
}
// States is always one longer than Events (it includes the initial state).
if len(states) != len(viaForm.Events())+1 {
t.Fatalf("len(States)=%d, len(Events)=%d; want States == Events+1", len(states), len(viaForm.Events()))
}
}

// TestShortestPaths_MatchesPlanPath asserts that for each single target, the
// shortest path's length matches the kernel's PlanPath length on the same guard-free
// machine — ShortestPaths is the multi-target generalization of PlanPath.
Expand Down
16 changes: 16 additions & 0 deletions state/conformance/errors.go
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,22 @@ func (e *ErrUnknownEvent) Error() string {
return fmt.Sprintf("conformance: scenario references unknown event %q", e.Name)
}

// ErrInitialStateMismatch is returned when a scenario declares a non-empty
// InitialState that does not match the typed start state the caller resolved for
// the run. Running anyway would silently replay the event sequence from a
// different state than the serialized scenario describes, so the run is rejected.
type ErrInitialStateMismatch struct {
// Declared is the scenario's serialized InitialState.
Declared string
// Resolved is the rendered form of the typed start state passed by the caller.
Resolved string
}

func (e *ErrInitialStateMismatch) Error() string {
return fmt.Sprintf("conformance: scenario initial state %q does not match the resolved start state %q",
e.Declared, e.Resolved)
}

// Mismatch is one field-level divergence found by an oracle comparison.
type Mismatch struct {
// Scenario is the name of the scenario whose run diverged.
Expand Down
44 changes: 44 additions & 0 deletions state/conformance/internal_test.go
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
package conformance

import (
"testing"

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

// TestOutcomeName_AllKernelOutcomes asserts outcomeName renders every kernel
// Outcome by a distinct stable name, so a conformance trace never collapses two
// different failure classes onto the same label (which would make a regression
// compare equal). An out-of-range value falls back to "Unknown".
func TestOutcomeName_AllKernelOutcomes(t *testing.T) {
cases := []struct {
outcome state.Outcome
want string
}{
{state.OutcomeSuccess, "Success"},
{state.OutcomeInvalidTransition, "InvalidTransition"},
{state.OutcomeGuardFailed, "GuardFailed"},
{state.OutcomeGuardPanic, "GuardPanic"},
{state.OutcomePolicyDenied, "PolicyDenied"},
{state.OutcomeEffectError, "EffectError"},
{state.OutcomeAssignFailed, "AssignFailed"},
{state.Outcome(-1), "Unknown"},
{state.Outcome(9999), "Unknown"},
}

seen := map[string]state.Outcome{}
for _, tc := range cases {
got := outcomeName(tc.outcome)
if got != tc.want {
t.Fatalf("outcomeName(%d) = %q, want %q", tc.outcome, got, tc.want)
}
// Every named (non-Unknown) outcome must be distinct from the others, so a
// trace diff distinguishes the failure classes.
if tc.want != "Unknown" {
if prev, dup := seen[got]; dup {
t.Fatalf("outcomeName collision: %d and %d both render %q", prev, tc.outcome, got)
}
seen[got] = tc.outcome
}
}
}
26 changes: 22 additions & 4 deletions state/conformance/scenario.go
Original file line number Diff line number Diff line change
Expand Up @@ -156,20 +156,36 @@ func (r ScenarioResult[S]) Passed() bool {
// RunAgainst fires the scenario's event sequence against a freshly Cast instance
// of the machine and builds a ScenarioResult. The codec resolves each event name
// to its typed value; an unresolved name is a fatal scenario error. The entity
// is supplied by the caller (the kernel binds guards and actions to it) and the
// starting state is taken from the scenario.
// is supplied by the caller (the kernel binds guards and actions to it).
//
// The run starts from the typed startState the caller resolved. When the scenario
// also declares a non-empty InitialState, it must match startState's rendered
// form; a disagreement is reported as ErrInitialStateMismatch and the events are
// not fired, so a serialized scenario can never silently replay from a different
// state than it describes.
func RunAgainst[S comparable, E comparable, C any](
m *state.Machine[S, E, C],
sc Scenario,
entity C,
codec EventCodec[E],
startState S,
) ScenarioResult[S] {
res := ScenarioResult[S]{FinalState: startState}
tr := Trace{MachineID: m.Name(), FromState: sc.InitialState}

if sc.InitialState != "" {
if resolved := fmt.Sprint(startState); resolved != sc.InitialState {
res.Err = &ErrInitialStateMismatch{Declared: sc.InitialState, Resolved: resolved}
tr.ToState = resolved
res.Trace = tr
res.Assertions = evaluate(sc.Assertions, res)
return res
}
}

// Full trace is required so EffectsEmitted, GuardsEvaluated, and the cascade
// fields are populated for scenario assertion evaluation.
inst := m.Cast(entity, state.WithInitialState(startState), state.WithFullTrace[S]())
res := ScenarioResult[S]{FinalState: startState}
tr := Trace{MachineID: m.Name(), FromState: sc.InitialState}

for _, ev := range sc.Events {
typed, ok := codec.Resolve(ev.Event)
Expand Down Expand Up @@ -226,6 +242,8 @@ func outcomeName(o state.Outcome) string {
return "PolicyDenied"
case state.OutcomeEffectError:
return "EffectError"
case state.OutcomeAssignFailed:
return "AssignFailed"
default:
return "Unknown"
}
Expand Down
50 changes: 50 additions & 0 deletions state/conformance/units_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ package conformance_test

import (
"encoding/json"
"errors"
"strings"
"testing"

Expand Down Expand Up @@ -114,6 +115,55 @@ func TestRunAgainst_RecordsEffectsAndTrace(t *testing.T) {
}
}

func TestRunAgainst_InitialStateMismatchIsRejected(t *testing.T) {
m := buildDocMachine()
// The scenario declares it starts in Submitted, but the caller resolves the
// start state to draft: the events must not be replayed from the wrong state.
sc := conformance.Scenario{
MachineID: "document", InitialState: "Submitted",
Events: []conformance.Event{{Event: "Submit"}},
Assertions: []conformance.Assertion{
{Type: conformance.AssertNoErrors, Expected: true},
},
}
res := conformance.RunAgainst(m, sc, newDoc(), docCodec(), draft)

var mismatch *conformance.ErrInitialStateMismatch
if !errors.As(res.Err, &mismatch) {
t.Fatalf("err = %v, want *ErrInitialStateMismatch", res.Err)
}
if mismatch.Declared != "Submitted" || mismatch.Resolved != "Draft" {
t.Fatalf("mismatch = %+v, want Declared=Submitted Resolved=Draft", mismatch)
}
// No events were fired: the run aborted before stepping the instance.
if len(res.Trace.Steps) != 0 {
t.Fatalf("trace steps = %d, want 0 (run aborted)", len(res.Trace.Steps))
}
// The NoErrors assertion must observe the recorded error and fail.
if res.Passed() {
t.Fatal("a mismatched scenario must not pass its NoErrors assertion")
}
}

func TestRunAgainst_EmptyInitialStateSkipsCheck(t *testing.T) {
m := buildDocMachine()
// An empty InitialState defers entirely to the caller's start state.
sc := conformance.Scenario{
MachineID: "document",
Events: []conformance.Event{{Event: "Submit"}},
Assertions: []conformance.Assertion{
{Type: conformance.AssertNoErrors, Expected: true},
},
}
res := conformance.RunAgainst(m, sc, newDoc(), docCodec(), draft)
if res.Err != nil {
t.Fatalf("empty InitialState should skip the consistency check, got err %v", res.Err)
}
if len(res.Trace.Steps) != 1 {
t.Fatalf("trace steps = %d, want 1", len(res.Trace.Steps))
}
}

func TestRunAgainst_FailingAssertionsMarkedNotPassed(t *testing.T) {
m := buildDocMachine()
sc := conformance.Scenario{
Expand Down
Loading
Loading