feat: detect competing-transition overlaps via symbolic disjointness

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...)
+}

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)
+	}
+}