From 183401941902232bada2f5163fd2039acb025296 Mon Sep 17 00:00:00 2001
From: PJ <ipriyanshujain@gmail.com>
Date: Mon, 1 Jun 2026 14:11:26 +0530
Subject: [PATCH] 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 | 36 ++++++++++++++++++++----------------
 internal/ltl/nnf.go       | 10 +++++++---
 2 files changed, 27 insertions(+), 19 deletions(-)

diff --git a/internal/ltl/evaluator.go b/internal/ltl/evaluator.go
index a9ec0f3..79224c7 100644
--- a/internal/ltl/evaluator.go
+++ b/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)
-		switch antecedent.status {
-		case statusHolds:
-			return reduce(concrete.Consequent, now)
-		case statusViolated:
-			return holds()
-		case statusPending:
-			return pending(ImpliesFormula{
-				Antecedent: antecedent.formula,
-				Consequent: concrete.Consequent,
-			})
-		}
+		// NewEvaluator runs nnf, which rewrites a -> b to (not a) or b, so this
+		// case is unreachable from a normal evaluator. A directly-constructed
+		// formula reduced here is evaluated through the same equivalence so a
+		// pending antecedent cannot drop the consequent.
+		return reduce(OrFormula{
+			Left:  pushNot(concrete.Antecedent),
+			Right: nnf(concrete.Consequent),
+		}, now)
 
 	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
-		// the window a pending inner cannot be deferred, so it resolves to holds.
+		// closes without a breach it is vacuously satisfied. A pending inner at
+		// 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
diff --git a/internal/ltl/nnf.go b/internal/ltl/nnf.go
index 9d7c74c..51d07ca 100644
--- a/internal/ltl/nnf.go
+++ b/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{
-			Antecedent: nnf(concrete.Antecedent),
-			Consequent: nnf(concrete.Consequent),
+		// a -> b is rewritten to (not a) or b so the consequent is always
+		// reduced live each step. Keeping it as ImpliesFormula let a pending
+		// (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