From a01e126ff969f8ba2995494cf77e12070abb3931 Mon Sep 17 00:00:00 2001 From: PJ Date: Mon, 1 Jun 2026 13:53:42 +0530 Subject: [PATCH] test(ltl): migrate thunk call sites to (bool,error) --- internal/ltl/evaluator_test.go | 10 +++++----- internal/ltl/finalize_test.go | 20 ++++++++++---------- internal/ltl/formula_test.go | 14 +++++++------- internal/ltl/nnf_test.go | 6 +++--- 4 files changed, 25 insertions(+), 25 deletions(-) diff --git a/internal/ltl/evaluator_test.go b/internal/ltl/evaluator_test.go index f93ecce..0f51dd8 100644 --- a/internal/ltl/evaluator_test.go +++ b/internal/ltl/evaluator_test.go @@ -36,10 +36,10 @@ func TestPure_FalseImmediatelyViolates(t *testing.T) { func TestThunk_TransitionFromHoldToViolate(t *testing.T) { values := []bool{true, true, false, true, true} step := 0 - evaluator := NewEvaluator(Always(Thunk(func() bool { + evaluator := NewEvaluator(Always(Thunk(func() (bool, error) { current := values[step] step++ - return current + return current, nil }))) wantSequence := []Verdict{ @@ -59,7 +59,7 @@ func TestThunk_TransitionFromHoldToViolate(t *testing.T) { func TestEvaluator_StickinessAfterViolation(t *testing.T) { state := true - evaluator := NewEvaluator(Always(Thunk(func() bool { return state }))) + evaluator := NewEvaluator(Always(Thunk(func() (bool, error) { return state, nil }))) if got := evaluator.Observe(); got != VerdictHolds { t.Fatalf("step 1: got %v, want holds", got) @@ -83,7 +83,7 @@ func TestEvaluator_TopLevelPureCountedAtEachStep(t *testing.T) { func TestEvaluator_TopLevelThunkRespectsObservation(t *testing.T) { state := true - evaluator := NewEvaluator(Thunk(func() bool { return state })) + evaluator := NewEvaluator(Thunk(func() (bool, error) { return state, nil })) if got := evaluator.Observe(); got != VerdictHolds { t.Errorf("expected holds, got %v", got) } @@ -107,7 +107,7 @@ func TestDescribe(t *testing.T) { if got := Describe(formula); !strings.Contains(got, "Always") || !strings.Contains(got, "Pure(true)") { t.Errorf("Describe wrong: %q", got) } - thunk := Always(Thunk(func() bool { return true })) + thunk := Always(Thunk(func() (bool, error) { return true, nil })) if got := Describe(thunk); !strings.Contains(got, "Thunk") { t.Errorf("Describe(thunk) wrong: %q", got) } diff --git a/internal/ltl/finalize_test.go b/internal/ltl/finalize_test.go index 6cd8263..d16a6b5 100644 --- a/internal/ltl/finalize_test.go +++ b/internal/ltl/finalize_test.go @@ -7,7 +7,7 @@ import ( ) func TestFinalize_UnboundedEventuallyUnmetIsViolated(t *testing.T) { - evaluator := NewEvaluator(Eventually(ThunkNamed("p", func() bool { return false }))) + evaluator := NewEvaluator(Eventually(ThunkNamed("p", func() (bool, error) { return false, nil }))) for index := range 3 { if got := evaluator.ObserveAt(time.Unix(int64(index), 0)); got != VerdictPending { t.Fatalf("step %d: got %v, want pending", index, got) @@ -19,7 +19,7 @@ func TestFinalize_UnboundedEventuallyUnmetIsViolated(t *testing.T) { } func TestFinalize_FinalStepNextIsViolated(t *testing.T) { - evaluator := NewEvaluator(Next(ThunkNamed("p", func() bool { return true }))) + 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) } @@ -51,7 +51,7 @@ func TestFinalize_BoundedAlwaysVacuouslyHolds(t *testing.T) { evaluator := NewEvaluator(EventuallyWithinSteps(Pure(false), 5)) evaluator.Observe() // The negated form of this is a bounded Always; build it directly. - bounded := NewEvaluator(Always(Not(EventuallyWithinSteps(ThunkNamed("p", func() bool { return false }), 5)))) + bounded := NewEvaluator(Always(Not(EventuallyWithinSteps(ThunkNamed("p", func() (bool, error) { return false, nil }), 5)))) bounded.Observe() if got := bounded.Finalize(); got == VerdictViolated { t.Errorf("bounded always should not finalize to violated, got %v", got) @@ -68,9 +68,9 @@ func TestEventuallyWithin_ViolatesIffNConsecutiveFalse(t *testing.T) { // trueAt < 0 means inner is never true. trueAt := int(trueAtSeed)%(bound+2) - 1 step := 0 - inner := ThunkNamed("p", func() bool { + inner := ThunkNamed("p", func() (bool, error) { current := trueAt >= 0 && step == trueAt - return current + return current, nil }) evaluator := NewEvaluator(EventuallyWithinSteps(inner, bound)) @@ -103,10 +103,10 @@ func TestViolationLatchIsMonotonic(t *testing.T) { values[index] = (seed>>uint(index))&1 == 1 } step := 0 - evaluator := NewEvaluator(Always(ThunkNamed("p", func() bool { + evaluator := NewEvaluator(Always(ThunkNamed("p", func() (bool, error) { current := values[step%len(values)] step++ - return current + return current, nil }))) seenViolated := false for index := range 16 { @@ -140,8 +140,8 @@ func TestCollapse_IdenticalObligationsMerge(t *testing.T) { func TestCollapse_DistinctPredicatesDoNotMerge(t *testing.T) { merged := collapse([]Formula{ - Eventually(ThunkNamed("p3", func() bool { return false })), - Eventually(ThunkNamed("p4", func() bool { return false })), + Eventually(ThunkNamed("p3", func() (bool, error) { return false, nil })), + Eventually(ThunkNamed("p4", func() (bool, error) { return false, nil })), }) if len(merged) != 2 { t.Errorf("distinct predicates must not merge, got %d", len(merged)) @@ -151,7 +151,7 @@ func TestCollapse_DistinctPredicatesDoNotMerge(t *testing.T) { func TestCollapse_NamedThunkLeakBoundsPendingSet(t *testing.T) { // Always(Eventually(sameThunk)): each step spawns an identical obligation. // Without collapse the pending set grows unboundedly. - evaluator := NewEvaluator(Always(Eventually(ThunkNamed("p", func() bool { return false })))) + evaluator := NewEvaluator(Always(Eventually(ThunkNamed("p", func() (bool, error) { return false, nil })))) for index := range 20 { evaluator.ObserveAt(time.Unix(int64(index), 0)) } diff --git a/internal/ltl/formula_test.go b/internal/ltl/formula_test.go index 44cabc0..f0b85af 100644 --- a/internal/ltl/formula_test.go +++ b/internal/ltl/formula_test.go @@ -50,7 +50,7 @@ func TestAlways_Now_ViolatesImmediately(t *testing.T) { func TestAlways_Next_PendingThenViolated(t *testing.T) { y := true - evaluator := NewEvaluator(Always(Next(Thunk(func() bool { return y })))) + evaluator := NewEvaluator(Always(Next(Thunk(func() (bool, error) { return y, nil })))) if got := evaluator.Observe(); got != VerdictPending { t.Errorf("step 1: got %v, want pending", got) @@ -62,7 +62,7 @@ func TestAlways_Next_PendingThenViolated(t *testing.T) { } func TestAlways_Next_StaysPendingWhileInnerHolds(t *testing.T) { - evaluator := NewEvaluator(Always(Next(Thunk(func() bool { return true })))) + evaluator := NewEvaluator(Always(Next(Thunk(func() (bool, error) { return true, nil })))) for index := range 3 { if got := evaluator.ObserveAt(time.Unix(int64(index), 0)); got != VerdictPending { t.Errorf("step %d: got %v, want pending", index+1, got) @@ -76,8 +76,8 @@ func TestAlways_NowImpliesEventuallyWithin_ViolatesWhenYLate(t *testing.T) { xValues := []bool{true, false, false, false, false} yValues := []bool{false, false, false, true, true} step := 0 - predX := Thunk(func() bool { return xValues[step] }) - predY := Thunk(func() bool { return yValues[step] }) + predX := Thunk(func() (bool, error) { return xValues[step], nil }) + predY := Thunk(func() (bool, error) { return yValues[step], nil }) formula := Always(Implies(Now(predX), EventuallyWithinSteps(predY, 3))) evaluator := NewEvaluator(formula) @@ -107,8 +107,8 @@ func TestAlways_NowImpliesEventuallyWithin_HoldsWhenYInBound(t *testing.T) { xValues := []bool{true, false, false} yValues := []bool{false, false, true} step := 0 - predX := Thunk(func() bool { return xValues[step] }) - predY := Thunk(func() bool { return yValues[step] }) + predX := Thunk(func() (bool, error) { return xValues[step], nil }) + predY := Thunk(func() (bool, error) { return yValues[step], nil }) formula := Always(Implies(Now(predX), EventuallyWithinSteps(predY, 3))) evaluator := NewEvaluator(formula) @@ -231,7 +231,7 @@ func TestMarshalJSON_NextAndThunkAndError(t *testing.T) { if string(body) != `{"op":"next","arg":{"op":"true"}}` { t.Errorf("next marshal wrong: %s", body) } - body, _ = json.Marshal(Thunk(func() bool { return true })) + body, _ = json.Marshal(Thunk(func() (bool, error) { return true, nil })) if string(body) != `{"op":"predicate"}` { t.Errorf("thunk marshal wrong: %s", body) } diff --git a/internal/ltl/nnf_test.go b/internal/ltl/nnf_test.go index c510356..4ab4ac2 100644 --- a/internal/ltl/nnf_test.go +++ b/internal/ltl/nnf_test.go @@ -14,7 +14,7 @@ func leafFor(seed uint8) Formula { case 1: return Pure(false) default: - return ThunkNamed("p", func() bool { return true }) + return ThunkNamed("p", func() (bool, error) { return true, nil }) } } @@ -66,7 +66,7 @@ func TestNNF_BoundedEventuallyDualKeepsBound(t *testing.T) { } func TestNNF_PushesNotToThunkLeaf(t *testing.T) { - formula := nnf(Always(Not(Always(ThunkNamed("p", func() bool { return true }))))) + formula := nnf(Always(Not(Always(ThunkNamed("p", func() (bool, error) { return true, nil }))))) always, ok := formula.(AlwaysFormula) if !ok { t.Fatalf("expected AlwaysFormula, got %T", formula) @@ -85,7 +85,7 @@ func TestNNF_PushesNotToThunkLeaf(t *testing.T) { } func TestNNF_NotAlwaysTrueViaEvaluatorReportsViolated(t *testing.T) { - evaluator := NewEvaluator(Always(Not(Always(ThunkNamed("p", func() bool { return true }))))) + evaluator := NewEvaluator(Always(Not(Always(ThunkNamed("p", func() (bool, error) { return true, nil }))))) for index := range 4 { if got := evaluator.ObserveAt(time.Unix(int64(index), 0)); got == VerdictViolated { t.Fatalf("step %d latched violated prematurely", index)