From 60b315d7b6b8ab688812a5797298ec7fc702d804 Mon Sep 17 00:00:00 2001 From: Joshua Temple Date: Sun, 31 May 2026 16:14:54 -0400 Subject: [PATCH] feat: detect competing-transition overlaps via symbolic disjointness Signed-off-by: Joshua Temple --- state/verify/symbolic/overlaps.go | 94 ++++++++++++++++++++++++++ state/verify/symbolic/overlaps_test.go | 81 ++++++++++++++++++++++ 2 files changed, 175 insertions(+) create mode 100644 state/verify/symbolic/overlaps.go create mode 100644 state/verify/symbolic/overlaps_test.go diff --git a/state/verify/symbolic/overlaps.go b/state/verify/symbolic/overlaps.go new file mode 100644 index 0000000..2db60b0 --- /dev/null +++ b/state/verify/symbolic/overlaps.go @@ -0,0 +1,94 @@ +package symbolic + +import ( + "fmt" + + "github.com/stablekernel/crucible/state" +) + +// Overlap reports two competing transitions — the same source state firing on the +// same event — whose guards are not provably disjoint, so both can be enabled at +// once: a candidate nondeterminism the analyzer could not rule out. +type Overlap[S comparable, E comparable] struct { + // From is the shared source state, On the shared event. + From S + On E + // ToA and ToB are the two competing transitions' targets. + ToA S + ToB S +} + +// Overlaps scans a machine for competing transitions (same source, same event) +// whose guards are not provably disjoint. It is conservative: a pair is reported +// unless the analyzer can PROVE the guards mutually exclusive, so transitions +// guarded only by opaque guards (named Go-func or Rich) — or unguarded — are +// reported as potential overlaps. An empty result means every same-source/same-event +// pair is provably disjoint, i.e. the machine is provably deterministic on its +// guarded choices over the analyzable Core guards. +func Overlaps[S comparable, E comparable, C any](m *state.Machine[S, E, C]) ([]Overlap[S, E], error) { + js, err := m.ToJSON() + if err != nil { + return nil, fmt.Errorf("symbolic: serialize machine: %w", err) + } + ir, err := state.LoadFromJSON[S, E, C](js) + if err != nil { + return nil, fmt.Errorf("symbolic: load machine IR: %w", err) + } + + var schema state.ContextSchema + if ir.Context != nil { + schema = *ir.Context + } + + // Collect every state, descending into compound children and parallel regions. + var states []state.State[S, E, C] + var collect func(ss []state.State[S, E, C]) + collect = func(ss []state.State[S, E, C]) { + for i := range ss { + states = append(states, ss[i]) + collect(ss[i].Children) + for r := range ss[i].Regions { + collect(ss[i].Regions[r].States) + } + } + } + collect(ir.States) + + type key struct { + from S + on E + } + var overlaps []Overlap[S, E] + for si := range states { + groups := map[key][]state.Transition[S, E, C]{} + for _, t := range states[si].Transitions { + k := key{from: t.From, on: t.On} + groups[k] = append(groups[k], t) + } + for k, ts := range groups { + for i := 0; i < len(ts); i++ { + for j := i + 1; j < len(ts); j++ { + if !Disjoint(transitionGuard(ts[i]), transitionGuard(ts[j]), schema) { + overlaps = append(overlaps, Overlap[S, E]{From: k.from, On: k.on, ToA: ts[i].To, ToB: ts[j].To}) + } + } + } + } + } + return overlaps, nil +} + +// transitionGuard builds the effective guard of a transition: the conjunction of its +// named-ref guards (each an opaque leaf to the analyzer) and its composite GuardExpr. +// A transition with no guard yields the empty conjunction, which the analyzer treats +// as always-true (the transition is always enabled). +func transitionGuard[S comparable, E comparable, C any](t state.Transition[S, E, C]) state.GuardNode[S] { + var nodes []state.GuardNode[S] + for _, g := range t.Guards { + nodes = append(nodes, state.Guard[S](g.Name)) + } + if t.GuardExpr != nil { + nodes = append(nodes, *t.GuardExpr) + } + return state.And(nodes...) +} diff --git a/state/verify/symbolic/overlaps_test.go b/state/verify/symbolic/overlaps_test.go new file mode 100644 index 0000000..6347b73 --- /dev/null +++ b/state/verify/symbolic/overlaps_test.go @@ -0,0 +1,81 @@ +package symbolic_test + +import ( + "testing" + + "github.com/stablekernel/crucible/state" + "github.com/stablekernel/crucible/state/verify/symbolic" +) + +// overlapMachine builds a one-source machine whose two transitions on "go" are +// guarded by the supplied Core expressions, with the ctx schema attached. +func overlapMachine(t *testing.T, ga, gb state.GuardNode[string]) *state.Machine[string, string, ctx] { + t.Helper() + return state.Forge[string, string, ctx]("m"). + WithContextSchema(state.SchemaOf[ctx]()). + State("s"). + Transition("s").On("go").GoTo("a").WhenExpr(ga). + Transition("s").On("go").GoTo("b").WhenExpr(gb). + State("a"). + State("b"). + Initial("s"). + Quench() +} + +func TestOverlaps_DisjointGuardsAreClean(t *testing.T) { + m := overlapMachine(t, + f("status").Eq(state.Str[string]("paid")), + f("status").Eq(state.Str[string]("open"))) + got, err := symbolic.Overlaps(m) + if err != nil { + t.Fatalf("Overlaps: %v", err) + } + if len(got) != 0 { + t.Fatalf("Overlaps = %+v, want none (guards are disjoint)", got) + } +} + +func TestOverlaps_OverlappingGuardsAreReported(t *testing.T) { + m := overlapMachine(t, + f("total").Gt(state.Float[string](5)), + f("total").Gt(state.Float[string](10))) + got, err := symbolic.Overlaps(m) + if err != nil { + t.Fatalf("Overlaps: %v", err) + } + if len(got) != 1 { + t.Fatalf("Overlaps = %+v, want one overlap (total>5 and total>10 both hold at 20)", got) + } + o := got[0] + if o.From != "s" || o.On != "go" { + t.Fatalf("overlap = %+v, want From=s On=go", o) + } + if o.ToA != "a" || o.ToB != "b" { + t.Fatalf("overlap targets = %v/%v, want a/b", o.ToA, o.ToB) + } +} + +func TestOverlaps_OpaqueGuardsAreConservativelyReported(t *testing.T) { + // Named-ref guards are opaque to the analyzer, so it cannot prove them disjoint + // and reports the pair — a false positive is the safe direction for + // nondeterminism detection. + def := state.Forge[string, string, ctx]("m"). + WithContextSchema(state.SchemaOf[ctx]()). + Guard("ga", func(state.GuardCtx[ctx]) bool { return true }). + Guard("gb", func(state.GuardCtx[ctx]) bool { return true }). + State("s"). + Transition("s").On("go").GoTo("a").WhenExpr(state.Guard[string]("ga")). + Transition("s").On("go").GoTo("b").WhenExpr(state.Guard[string]("gb")). + State("a"). + State("b"). + Initial("s"). + Quench() + + got, err := symbolic.Overlaps(def) + if err != nil { + t.Fatalf("Overlaps: %v", err) + } + if len(got) != 1 { + t.Fatalf("Overlaps = %+v, want one (opaque guards not provably disjoint)", got) + } +}