sanderling/internal/ltl/finalize_test.go

package ltl

import (
	"testing"
	"testing/quick"
	"time"
)

func TestFinalize_UnboundedEventuallyUnmetIsViolated(t *testing.T) {
	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)
		}
	}
	if got := evaluator.Finalize(); got != VerdictViolated {
		t.Errorf("Finalize = %v, want violated", got)
	}
}

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 != VerdictHolds {
		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)
	}
}

func TestFinalize_HoldingRunStaysHolds(t *testing.T) {
	evaluator := NewEvaluator(Always(Pure(true)))
	evaluator.Observe()
	if got := evaluator.Finalize(); got != VerdictHolds {
		t.Errorf("Finalize = %v, want holds", got)
	}
}

func TestFinalize_AlreadyViolatedStaysViolated(t *testing.T) {
	evaluator := NewEvaluator(Always(Pure(false)))
	if got := evaluator.Observe(); got != VerdictViolated {
		t.Fatalf("expected violated, got %v", got)
	}
	if got := evaluator.Finalize(); got != VerdictViolated {
		t.Errorf("Finalize = %v, want violated", got)
	}
}

func TestFinalize_BoundedAlwaysVacuouslyHolds(t *testing.T) {
	// A bounded Always whose window never closed (still pending) is safe.
	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, 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)
	}
}

// TestEventuallyWithin_ViolatesIffNConsecutiveFalse locks the bounded
// eventually contract: with a step bound of n and an inner that is false for
// the first n observations, the verdict violates exactly at step n, and with at
// least one true observation inside the window it holds.
func TestEventuallyWithin_ViolatesIffNConsecutiveFalse(t *testing.T) {
	law := func(boundSeed uint8, trueAtSeed uint8) bool {
		bound := int(boundSeed%5) + 1
		// trueAt < 0 means inner is never true.
		trueAt := int(trueAtSeed)%(bound+2) - 1
		step := 0
		inner := ThunkNamed("p", func() (bool, error) {
			current := trueAt >= 0 && step == trueAt
			return current, nil
		})
		evaluator := NewEvaluator(EventuallyWithinSteps(inner, bound))

		satisfiedInWindow := trueAt >= 0 && trueAt < bound
		var final Verdict = VerdictPending
		for index := range bound {
			step = index
			final = evaluator.ObserveAt(time.Unix(int64(index), 0))
			if final == VerdictHolds || final == VerdictViolated {
				break
			}
		}

		if satisfiedInWindow {
			return final == VerdictHolds
		}
		return final == VerdictViolated
	}
	if err := quick.Check(law, nil); err != nil {
		t.Error(err)
	}
}

// TestViolationLatchIsMonotonic locks: once an evaluator reports Violated, every
// subsequent observation (and Finalize) stays Violated regardless of inputs.
func TestViolationLatchIsMonotonic(t *testing.T) {
	law := func(seed uint64) bool {
		values := make([]bool, 8)
		for index := range values {
			values[index] = (seed>>uint(index))&1 == 1
		}
		step := 0
		evaluator := NewEvaluator(Always(ThunkNamed("p", func() (bool, error) {
			current := values[step%len(values)]
			step++
			return current, nil
		})))
		seenViolated := false
		for index := range 16 {
			got := evaluator.ObserveAt(time.Unix(int64(index), 0))
			if got == VerdictViolated {
				seenViolated = true
			} else if seenViolated {
				return false
			}
		}
		if seenViolated && evaluator.Finalize() != VerdictViolated {
			return false
		}
		return true
	}
	if err := quick.Check(law, nil); err != nil {
		t.Error(err)
	}
}

// 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},
		{formula: Next(Pure(true)), origin: 2},
		{formula: Next(Pure(true)), origin: 3},
	})
	if len(merged) != 1 {
		t.Errorf("expected 1 obligation after collapse, got %d", len(merged))
	}
	if merged[0].origin != 1 {
		t.Errorf("collapse must keep the earliest origin, got %d", merged[0].origin)
	}
}

func TestCollapse_DistinctPredicatesDoNotMerge(t *testing.T) {
	merged := collapse([]obligation{
		{formula: Eventually(ThunkNamed("p3", func() (bool, error) { return false, nil }))},
		{formula: Eventually(ThunkNamed("p4", func() (bool, error) { return false, nil }))},
	})
	if len(merged) != 2 {
		t.Errorf("distinct predicates must not merge, got %d", len(merged))
	}
}

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, error) { return false, nil }))))
	for index := range 20 {
		evaluator.ObserveAt(time.Unix(int64(index), 0))
	}
	if len(evaluator.pending) > 2 {
		t.Errorf("pending set leaked to %d obligations", len(evaluator.pending))
	}
}