From f6d5d1f34f149c89fed1ea6b5f62ff3a63104285 Mon Sep 17 00:00:00 2001 From: PJ Date: Sat, 6 Jun 2026 12:45:52 +0530 Subject: [PATCH] test(ltl): table-test finalize Kleene connective combinations --- internal/ltl/finalize_test.go | 43 +++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/internal/ltl/finalize_test.go b/internal/ltl/finalize_test.go index 11dd577..a0c0fd9 100644 --- a/internal/ltl/finalize_test.go +++ b/internal/ltl/finalize_test.go @@ -146,6 +146,49 @@ func TestViolationLatchIsMonotonic(t *testing.T) { } } +// TestFinalize_KleeneConnectives locks the soundness guarantee in finalize's +// doc comment: an indefinite (pending) operand must never let a connective +// manufacture a definite verdict. Bug class: a pending side collapsing to +// holds/violated at run end, making sanderling lie about pass/fail. +func TestFinalize_KleeneConnectives(t *testing.T) { + pure := func(v bool) Formula { return PureFormula{Value: v} } + pendingThunk := ThunkFormula{Name: "t", Func: func() (bool, error) { return true, nil }} + eventuallyViolated := EventuallyFormula{Inner: PureFormula{Value: false}} + nextPending := NextFormula{Inner: PureFormula{Value: true}} + alwaysHolds := AlwaysFormula{Inner: PureFormula{Value: true}} + + cases := []struct { + name string + formula Formula + want residualStatus + }{ + {"and-pending-violated", AndFormula{Left: pendingThunk, Right: eventuallyViolated}, statusViolated}, + {"and-violated-pending", AndFormula{Left: nextPending, Right: eventuallyViolated}, statusViolated}, + {"and-pending-holds", AndFormula{Left: pendingThunk, Right: alwaysHolds}, statusPending}, + {"and-holds-holds", AndFormula{Left: pure(true), Right: alwaysHolds}, statusHolds}, + + {"or-pending-violated", OrFormula{Left: pendingThunk, Right: eventuallyViolated}, statusPending}, + {"or-pending-holds", OrFormula{Left: pendingThunk, Right: alwaysHolds}, statusHolds}, + {"or-violated-violated", OrFormula{Left: pure(false), Right: eventuallyViolated}, statusViolated}, + + {"not-pending", NotFormula{Inner: pendingThunk}, statusPending}, + {"not-violated", NotFormula{Inner: eventuallyViolated}, statusHolds}, + {"not-holds", NotFormula{Inner: alwaysHolds}, statusViolated}, + + {"implies-pending-violated", ImpliesFormula{Antecedent: pendingThunk, Consequent: eventuallyViolated}, statusPending}, + {"implies-holds-violated", ImpliesFormula{Antecedent: alwaysHolds, Consequent: eventuallyViolated}, statusViolated}, + {"implies-violated-pending", ImpliesFormula{Antecedent: eventuallyViolated, Consequent: nextPending}, statusHolds}, + + {"now-violated", NowFormula{Inner: eventuallyViolated}, statusViolated}, + {"now-pending", NowFormula{Inner: nextPending}, statusPending}, + } + for _, tc := range cases { + if got := finalize(tc.formula); got != tc.want { + t.Errorf("%s: finalize = %v, want %v", tc.name, got, tc.want) + } + } +} + func TestCollapse_IdenticalObligationsMerge(t *testing.T) { merged := collapse([]obligation{ {formula: Next(Pure(true)), origin: 1},