Symbolic guard analysis

Plain static analysis treats every guard as opaque, so it won’t report an overlap between two guarded transitions on the same event. state/verify/symbolic closes that gap by reasoning over the Core guard tree as data (comparison and boolean structure over context fields) instead of running it.

Four questions over a guard node and the machine’s ContextSchema:

g := state.And(
    state.Field[string]("status").Eq(state.Str[string]("paid")),
    state.Field[string]("total").Gt(state.Float[string](10)),
)

symbolic.Satisfiable(g, schema)   // is there any context that makes g true?
symbolic.Contradiction(g, schema) // is g unsatisfiable: a dead branch?
symbolic.Disjoint(a, b, schema)   // can a and b never both be true at once?

Disjoint is the load-bearing one. Two competing transitions on the same event are safe, provably deterministic, exactly when their guards are disjoint. Contradiction finds guards that can never fire: a dead branch you can delete.

To sweep a whole machine, Overlaps walks every same-event transition pair and reports the ones that are not provably disjoint:

overlaps, err := symbolic.Overlaps(m)
for _, o := range overlaps {
    fmt.Printf("ambiguous on %v from %v: %v vs %v\n", o.On, o.From, o.ToA, o.ToB)
}

The analysis is conservative. It reasons precisely over the Core guard forms: Eq, Ne, Lt/Le/Gt/Ge, In, And/Or/Not over typed fields. Anything it can’t see through, such as an opaque host Guard("ext"), a Rich predicate, a CEL expression, or a StateIn check, it treats as “unknown” and assumes satisfiable. So a clean Overlaps report over Core guards is a real guarantee of determinism; a flagged pair over opaque guards is a “can’t prove it, look closer,” never a false alarm of safety.