fix(ltl): treat next obligations as vacuous at run end

internal/ltl/evaluator.go

@@ -140,10 +140,11 @@ func collapse(obligations []obligation) []obligation {
 	return result
 }
 
-// Finalize reports the terminal verdict for the run. Pending obligations that
+// Finalize reports the terminal verdict for the run. A liveness promise that
-// can never be discharged by a future step (an unbounded eventually that never
+// never discharged (an eventually that never fired) resolves to Violated. A
-// fired, a strong next with no successor) resolve to Violated; safety
+// deferred state check (the residue of a next) has no successor state to
-// obligations that were never breached resolve to Holds.
+// evaluate against, so it is indefinite and resolves vacuously to Holds: the
+// run ended before the obligation could be checked, which is not a failure.
 func (e *Evaluator) Finalize() Verdict {
 	if e.violated {
 		return VerdictViolated
@@ -177,17 +178,18 @@ func finalizeReason(formula Formula) string {
 	switch formula.(type) {
 	case EventuallyFormula:
 		return "eventually never satisfied"
-	case NextFormula:
-		return "next obligation unmet at run end"
-	case ThunkFormula:
-		return "obligation unmet at run end"
 	default:
 		return "liveness obligation unmet at run end"
 	}
 }
 
 // finalize collapses a pending obligation to its terminal status assuming no
-// further steps will occur.
+// further steps will occur. Three-valued: a pending thunk or next is the
+// residue of a deferred state check with no state left to check, so it is
+// indefinite (statusPending) rather than violated; only a liveness promise
+// (an eventually that never fired) is a definite end-of-run violation.
+// Connectives combine with Kleene semantics so an indefinite sub-formula
+// never manufactures a definite verdict.
 func finalize(formula Formula) residualStatus {
 	switch concrete := formula.(type) {
 	case PureFormula:
@@ -196,11 +198,11 @@ func finalize(formula Formula) residualStatus {
 		}
 		return statusViolated
 	case ThunkFormula:
-		return statusViolated
+		return statusPending
 	case EventuallyFormula:
 		return statusViolated
 	case NextFormula:
-		return statusViolated
+		return statusPending
 	case AlwaysFormula:
 		return statusHolds
 	case NowFormula:
@@ -209,24 +211,34 @@ func finalize(formula Formula) residualStatus {
 		switch finalize(concrete.Inner) {
 		case statusViolated:
 			return statusHolds
-		default:
+		case statusHolds:
 			return statusViolated
+		default:
+			return statusPending
 		}
 	case AndFormula:
-		if finalize(concrete.Left) == statusViolated || finalize(concrete.Right) == statusViolated {
+		left, right := finalize(concrete.Left), finalize(concrete.Right)
+		if left == statusViolated || right == statusViolated {
 			return statusViolated
 		}
+		if left == statusPending || right == statusPending {
+			return statusPending
+		}
 		return statusHolds
 	case OrFormula:
-		if finalize(concrete.Left) == statusHolds || finalize(concrete.Right) == statusHolds {
+		left, right := finalize(concrete.Left), finalize(concrete.Right)
+		if left == statusHolds || right == statusHolds {
 			return statusHolds
 		}
+		if left == statusPending || right == statusPending {
+			return statusPending
+		}
 		return statusViolated
 	case ImpliesFormula:
-		if finalize(concrete.Antecedent) == statusViolated {
+		return finalize(OrFormula{
-			return statusHolds
+			Left:  NotFormula{Inner: concrete.Antecedent},
-		}
+			Right: concrete.Consequent,
-		return finalize(concrete.Consequent)
+		})
 	default:
 		return statusHolds
 	}

internal/ltl/finalize_test.go

@@ -18,13 +18,32 @@ func TestFinalize_UnboundedEventuallyUnmetIsViolated(t *testing.T) {
 	}
 }
 
-func TestFinalize_FinalStepNextIsViolated(t *testing.T) {
+func TestFinalize_FinalStepNextIsVacuouslyHolds(t *testing.T) {
+	// A next obligation pending at run end has no successor state to check;
+	// the run ending before the check is not a failure (weak next at the
+	// trace boundary).
 	evaluator := NewEvaluator(Next(ThunkNamed("p", func() (bool, error) { return true, nil })))
 	if got := evaluator.Observe(); got != VerdictPending {
 		t.Fatalf("step 1: got %v, want pending", got)
 	}
-	if got := evaluator.Finalize(); got != VerdictViolated {
+	if got := evaluator.Finalize(); got != VerdictHolds {
-		t.Errorf("Finalize = %v, want violated", got)
+		t.Errorf("Finalize = %v, want holds", got)
+	}
+	if witness := evaluator.Violation(); witness != nil {
+		t.Errorf("Violation = %+v, want nil for a vacuous next", witness)
+	}
+}
+
+func TestFinalize_AlwaysNextNeverReportsAtRunEnd(t *testing.T) {
+	// always(next(p)): every step spawns a deferred check and the last one is
+	// always pending when the run ends. That residue must not surface as an
+	// end-of-run violation.
+	evaluator := NewEvaluator(Always(Next(ThunkNamed("p", func() (bool, error) { return true, nil }))))
+	for index := range 3 {
+		evaluator.ObserveAt(time.Unix(int64(index), 0))
+	}
+	if got := evaluator.Finalize(); got != VerdictHolds {
+		t.Errorf("Finalize = %v, want holds", got)
 	}
 }
 

internal/ltl/witness_test.go

@@ -100,11 +100,14 @@ func TestViolation_NextAttributesOriginStep(t *testing.T) {
 }
 
 func TestViolation_FinalizeAttributesOriginStep(t *testing.T) {
-	evaluator := NewEvaluator(Always(Next(ThunkNamed("p", func() (bool, error) {
+	// An eventually that never fires is reported by Finalize at the step the
-		return true, nil
+	// obligation was first spawned (collapse keeps the earliest origin).
-	}))))
+	evaluator := NewEvaluator(Eventually(ThunkNamed("p", func() (bool, error) {
+		return false, nil
+	})))
 	evaluator.ObserveAt(time.Unix(0, 0))
 	evaluator.ObserveAt(time.Unix(1, 0))
+	evaluator.ObserveAt(time.Unix(2, 0))
 	if got := evaluator.Finalize(); got != VerdictViolated {
 		t.Fatalf("Finalize = %v, want violated", got)
 	}
@@ -112,8 +115,8 @@ func TestViolation_FinalizeAttributesOriginStep(t *testing.T) {
 	if witness == nil {
 		t.Fatal("Violation = nil after Finalize, want non-nil")
 	}
-	if witness.Step != 2 {
+	if witness.Step != 1 {
-		t.Errorf("Step = %d, want 2 (the step whose next obligation has no successor)", witness.Step)
+		t.Errorf("Step = %d, want 1 (the step the eventually obligation was spawned)", witness.Step)
 	}
 }