feat(ltl): NNF in NewEvaluator, bounded-always, Finalize, collapse

Apply nnf on construction, reduce bounded Always symmetric to bounded
Eventually (vacuous holds once the window closes), add Finalize to
resolve undischarged liveness obligations to Violated at run end, and
collapse structurally-identical pending obligations.

internal/ltl/evaluator.go

@@ -34,10 +34,11 @@ type Evaluator struct {
 	root     Formula
 	pending  []Formula
 	violated bool
+	steps    int
 }
 
 func NewEvaluator(formula Formula) *Evaluator {
-	return &Evaluator{root: formula}
+	return &Evaluator{root: nnf(formula)}
 }
 
 // Observe evaluates the formula against the current state and returns the
@@ -52,6 +53,7 @@ func (e *Evaluator) ObserveAt(now time.Time) Verdict {
 	if e.violated {
 		return VerdictViolated
 	}
+	e.steps++
 
 	fresh := rootObligation(e.root)
 	obligations := append(e.pending, fresh)
@@ -71,12 +73,98 @@ func (e *Evaluator) ObserveAt(now time.Time) Verdict {
 		}
 	}
 
+	e.pending = collapse(e.pending)
+
 	if len(e.pending) > 0 {
 		return VerdictPending
 	}
 	return VerdictHolds
 }
 
+// collapse removes structurally-identical obligations, keeping the first
+// occurrence in order. Distinct predicates never merge because ThunkFormula's
+// name participates in its describe() key, so deduping cannot hide a violation.
+func collapse(obligations []Formula) []Formula {
+	if len(obligations) < 2 {
+		return obligations
+	}
+	seen := make(map[string]struct{}, len(obligations))
+	result := obligations[:0]
+	for _, obligation := range obligations {
+		key := obligation.describe()
+		if _, ok := seen[key]; ok {
+			continue
+		}
+		seen[key] = struct{}{}
+		result = append(result, obligation)
+	}
+	return result
+}
+
+// Finalize reports the terminal verdict for the run. Pending obligations that
+// can never be discharged by a future step (an unbounded eventually that never
+// fired, a strong next with no successor) resolve to Violated; safety
+// obligations that were never breached resolve to Holds.
+func (e *Evaluator) Finalize() Verdict {
+	if e.violated {
+		return VerdictViolated
+	}
+	for _, obligation := range e.pending {
+		if finalize(obligation) == statusViolated {
+			e.violated = true
+			e.pending = nil
+			return VerdictViolated
+		}
+	}
+	return VerdictHolds
+}
+
+// finalize collapses a pending obligation to its terminal status assuming no
+// further steps will occur.
+func finalize(formula Formula) residualStatus {
+	switch concrete := formula.(type) {
+	case PureFormula:
+		if concrete.Value {
+			return statusHolds
+		}
+		return statusViolated
+	case ThunkFormula:
+		return statusViolated
+	case EventuallyFormula:
+		return statusViolated
+	case NextFormula:
+		return statusViolated
+	case AlwaysFormula:
+		return statusHolds
+	case NowFormula:
+		return finalize(concrete.Inner)
+	case NotFormula:
+		switch finalize(concrete.Inner) {
+		case statusViolated:
+			return statusHolds
+		default:
+			return statusViolated
+		}
+	case AndFormula:
+		if finalize(concrete.Left) == statusViolated || finalize(concrete.Right) == statusViolated {
+			return statusViolated
+		}
+		return statusHolds
+	case OrFormula:
+		if finalize(concrete.Left) == statusHolds || finalize(concrete.Right) == statusHolds {
+			return statusHolds
+		}
+		return statusViolated
+	case ImpliesFormula:
+		if finalize(concrete.Antecedent) == statusViolated {
+			return statusHolds
+		}
+		return finalize(concrete.Consequent)
+	default:
+		return statusHolds
+	}
+}
+
 // Residual returns a single Formula describing what the evaluator still has
 // to prove after the most recent ObserveAt. PureFormula{true} means the
 // property holds for the run so far; PureFormula{false} means it has latched
@@ -233,11 +321,30 @@ func reduce(formula Formula, now time.Time) reduceResult {
 		}
 
 	case AlwaysFormula:
+		// First-reduction deadline resolution mirrors EventuallyFormula so a
+		// relative duration becomes a stable absolute deadline.
+		if !concrete.HasDeadline && concrete.Duration > 0 {
+			concrete.Deadline = now.Add(concrete.Duration)
+			concrete.HasDeadline = true
+		}
 		innerResult := reduce(concrete.Inner, now)
 		if innerResult.status == statusViolated {
 			return violated()
 		}
-		next := AlwaysFormula{Inner: concrete.Inner}
+		// A bounded Always is the dual of a bounded Eventually: once the window
+		// closes without a breach it is vacuously satisfied. At the last step in
+		// the window a pending inner cannot be deferred, so it resolves to holds.
+		if concrete.HasStepBound && concrete.StepBound <= 1 {
+			return holds()
+		}
+		if concrete.HasDeadline && !now.Before(concrete.Deadline) {
+			return holds()
+		}
+		next := concrete
+		next.Inner = concrete.Inner
+		if concrete.HasStepBound {
+			next.StepBound = concrete.StepBound - 1
+		}
 		if innerResult.status == statusHolds {
 			return pending(next)
 		}