fix(ltl): eliminate implies and bounded-always false-negatives

Rewrite a -> b to (not a) or b in NNF so a pending temporal antecedent
can no longer defer the whole implication and drop a consequent that was
false at the current step. Carry a pending inner past a bounded-Always
window close instead of dropping it to holds, so a deferred obligation is
resolved by a later step or Finalize.

internal/ltl/evaluator.go

@@ -347,18 +347,14 @@ func reduce(formula Formula, now time.Time) reduceResult {
 		return pending(next)
 
 	case ImpliesFormula:
-		antecedent := reduce(concrete.Antecedent, now)
+		// NewEvaluator runs nnf, which rewrites a -> b to (not a) or b, so this
-		switch antecedent.status {
+		// case is unreachable from a normal evaluator. A directly-constructed
-		case statusHolds:
+		// formula reduced here is evaluated through the same equivalence so a
-			return reduce(concrete.Consequent, now)
+		// pending antecedent cannot drop the consequent.
-		case statusViolated:
+		return reduce(OrFormula{
-			return holds()
+			Left:  pushNot(concrete.Antecedent),
-		case statusPending:
+			Right: nnf(concrete.Consequent),
-			return pending(ImpliesFormula{
+		}, now)
-				Antecedent: antecedent.formula,
-				Consequent: concrete.Consequent,
-			})
-		}
 
 	case OrFormula:
 		left := reduce(concrete.Left, now)
@@ -420,13 +416,21 @@ func reduce(formula Formula, now time.Time) reduceResult {
 			return violatedFrom(innerResult, concrete, "always inner violated")
 		}
 		// 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
+		// closes without a breach it is vacuously satisfied. A pending inner at
-		// the window a pending inner cannot be deferred, so it resolves to holds.
+		// the closing step is a deferred obligation (a strong next, or an inner
+		// liveness that has not discharged); it must be carried so a later step
+		// or Finalize resolves it, never dropped to holds.
 		if concrete.HasStepBound && concrete.StepBound <= 1 {
-			return holds()
+			if innerResult.status == statusHolds {
+				return holds()
+			}
+			return pending(innerResult.formula)
 		}
 		if concrete.HasDeadline && !now.Before(concrete.Deadline) {
-			return holds()
+			if innerResult.status == statusHolds {
+				return holds()
+			}
+			return pending(innerResult.formula)
 		}
 		next := concrete
 		next.Inner = concrete.Inner

internal/ltl/nnf.go

@@ -26,9 +26,13 @@ func nnf(formula Formula) Formula {
 	case OrFormula:
 		return OrFormula{Left: nnf(concrete.Left), Right: nnf(concrete.Right)}
 	case ImpliesFormula:
-		return ImpliesFormula{
+		// a -> b is rewritten to (not a) or b so the consequent is always
-			Antecedent: nnf(concrete.Antecedent),
+		// reduced live each step. Keeping it as ImpliesFormula let a pending
-			Consequent: nnf(concrete.Consequent),
+		// (temporal) antecedent defer the whole implication and silently drop a
+		// consequent that was false at the current step.
+		return OrFormula{
+			Left:  pushNot(concrete.Antecedent),
+			Right: nnf(concrete.Consequent),
 		}
 	default:
 		return formula