diff --git a/internal/ltl/duality_test.go b/internal/ltl/duality_test.go new file mode 100644 index 0000000..8e92132 --- /dev/null +++ b/internal/ltl/duality_test.go @@ -0,0 +1,170 @@ +package ltl + +import ( + "math/rand/v2" + "testing" + "testing/quick" + "time" +) + +// dualityTrace holds the per-step truth of each predicate. The thunks read the +// current step out of the trace rather than counting their own invocations, so +// a formula and its negation see the same values no matter how many times each +// predicate is reduced. +type dualityTrace struct { + step int + values [2][]bool +} + +func newDualityTrace(random *rand.Rand, steps int) *dualityTrace { + trace := &dualityTrace{} + for index := range trace.values { + trace.values[index] = make([]bool, steps) + for step := range trace.values[index] { + trace.values[index][step] = random.IntN(2) == 0 + } + } + return trace +} + +func (t *dualityTrace) atoms() []Formula { + return []Formula{ + ThunkNamed("p0", func() (bool, error) { return t.values[0][t.step], nil }), + ThunkNamed("p1", func() (bool, error) { return t.values[1][t.step], nil }), + Pure(true), + Pure(false), + } +} + +// randomFormula draws a formula of at most the given depth over the atoms. +// Every operator the evaluator can reduce is reachable, including the bounded +// Always that only nnf produces. +func randomFormula(random *rand.Rand, depth int, atoms []Formula) Formula { + if depth == 0 { + return atoms[random.IntN(len(atoms))] + } + inner := func() Formula { return randomFormula(random, depth-1, atoms) } + bound := random.IntN(3) + 1 + switch random.IntN(12) { + case 0, 1: + return atoms[random.IntN(len(atoms))] + case 2: + return Not(inner()) + case 3: + return Next(inner()) + case 4: + return Now(inner()) + case 5: + return And(inner(), inner()) + case 6: + return Or(inner(), inner()) + case 7: + return Implies(inner(), inner()) + case 8: + return Always(inner()) + case 9: + return Eventually(inner()) + case 10: + if random.IntN(2) == 0 { + return EventuallyWithinSteps(inner(), bound) + } + return EventuallyWithin(inner(), time.Duration(bound)*time.Second) + default: + if random.IntN(2) == 0 { + return AlwaysFormula{Inner: inner(), StepBound: bound, HasStepBound: true} + } + return AlwaysFormula{Inner: inner(), Duration: time.Duration(bound) * time.Second} + } +} + +// TestNNF_ExcludedMiddleHoldsOnRandomTraces is the semantic counterpart to the +// describe()-comparing laws in nnf_test.go: those check that nnf produces the +// syntax the dual laws predict, this checks that the syntax it produces means +// the same thing. If any operator pair reduces non-dually then some trace makes +// a formula and its own nnf-negation both violate, so their disjunction +// violates and their conjunction holds. +func TestNNF_ExcludedMiddleHoldsOnRandomTraces(t *testing.T) { + const steps = 8 + law := func(seed uint64) bool { + random := rand.New(rand.NewPCG(seed, 0x9e3779b97f4a7c15)) + trace := newDualityTrace(random, steps) + formula := randomFormula(random, 3, trace.atoms()) + + tautology := NewEvaluator(Or(formula, nnf(Not(formula)))) + contradiction := NewEvaluator(And(formula, nnf(Not(formula)))) + for index := range steps { + trace.step = index + now := time.Unix(int64(index), 0) + if tautology.ObserveAtStep(now, index+1) == VerdictViolated { + t.Logf("seed %d: %s violated at step %d", seed, Describe(formula), index+1) + return false + } + if contradiction.ObserveAtStep(now, index+1) == VerdictHolds { + t.Logf("seed %d: %s held at step %d", seed, Describe(formula), index+1) + return false + } + } + return tautology.Finalize() != VerdictViolated + } + if err := quick.Check(law, &quick.Config{MaxCount: 2000}); err != nil { + t.Error(err) + } +} + +// TestNNF_BoundedAlwaysOverNextIsDual is the counterexample that showed nnf was +// not semantics preserving: phi = G<=1(X p) with p true only at the first step. +// Before the bounded operators were made dual, phi violated at step 2 and +// nnf(not phi) violated at step 1, so both a formula and its negation failed on +// one trace. Exactly one of the pair may violate. +func TestNNF_BoundedAlwaysOverNextIsDual(t *testing.T) { + step := 0 + predicate := ThunkNamed("p", func() (bool, error) { return step == 0, nil }) + formula := AlwaysFormula{Inner: Next(predicate), StepBound: 1, HasStepBound: true} + negated := nnf(Not(formula)) + + run := func(root Formula) Verdict { + step = 0 + evaluator := NewEvaluator(root) + for index := range 3 { + step = index + if evaluator.ObserveAtStep(time.Unix(int64(index), 0), index+1) == VerdictViolated { + return VerdictViolated + } + } + return evaluator.Finalize() + } + + if got := run(formula); got == VerdictViolated { + t.Errorf("G<=1(X p) = %v; the window closes on a deferred check, which is not a breach", got) + } + if got := run(negated); got != VerdictViolated { + t.Errorf("nnf(not G<=1(X p)) = %v, want violated", got) + } + if got := run(Or(formula, negated)); got == VerdictViolated { + t.Errorf("excluded middle violated: %v", got) + } + if got := run(And(formula, negated)); got != VerdictViolated { + t.Errorf("phi and not phi = %v, want violated", got) + } +} + +// TestEventually_PendingInnerSurvivesAsDisjunct locks the conjunct/disjunct +// mirror the duality rests on: Always keeps a pending inner as a conjunct of +// its residual, so Eventually must keep one as a disjunct. Dropping it made an +// inner that can only discharge on a later step unsatisfiable. +func TestEventually_PendingInnerSurvivesAsDisjunct(t *testing.T) { + values := []bool{false, true, false} + step := 0 + formula := EventuallyWithinSteps(Next(ThunkNamed("p", func() (bool, error) { + return values[step], nil + })), 2) + evaluator := NewEvaluator(formula) + + if got := evaluator.ObserveAtStep(time.Unix(0, 0), 1); got != VerdictPending { + t.Fatalf("step 1: got %v, want pending", got) + } + step = 1 + if got := evaluator.ObserveAtStep(time.Unix(1, 0), 2); got != VerdictHolds { + t.Errorf("step 2: got %v, want holds (X p armed at step 1 discharged here)", got) + } +} diff --git a/internal/ltl/evaluator.go b/internal/ltl/evaluator.go index 2d07194..98792d6 100644 --- a/internal/ltl/evaluator.go +++ b/internal/ltl/evaluator.go @@ -372,6 +372,9 @@ func reduce(formula Formula, now time.Time) reduceResult { if innerResult.status == statusHolds { return holds() } + // The window is measured in observations at which the inner could have + // discharged, so an inner that is merely pending has not discharged and + // the window closing on it is a violation. if concrete.HasStepBound && concrete.StepBound <= 1 { return violatedFrom(innerResult, concrete, "eventually bound exhausted") } @@ -382,6 +385,14 @@ func reduce(formula Formula, now time.Time) reduceResult { if concrete.HasStepBound { next.StepBound = concrete.StepBound - 1 } + // F(inner) unrolls to inner or X F(inner). A pending inner is a + // deferred way of satisfying the promise, so it is kept as a disjunct + // rather than dropped; dropping it is what made an inner that only + // resolves on a later step unsatisfiable, and it is the mirror of the + // conjunct Always keeps below. + if innerResult.status == statusPending { + return pending(OrFormula{Left: innerResult.formula, Right: next}) + } return pending(next) case ImpliesFormula: @@ -453,25 +464,20 @@ func reduce(formula Formula, now time.Time) reduceResult { if innerResult.status == statusViolated { 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. 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. + // A bounded Always must reduce exactly as its dual does, so that + // G<=n(f) and not F<=n(not f) agree on every trace. The dual of "the + // window closed on an inner that never definitely held, so violate" is + // "the window closed on an inner that was never definitely breached, so + // hold". A pending inner has not been breached inside the window, so it + // discharges vacuously here exactly as its negation violates on the + // Eventually side. if concrete.HasStepBound && concrete.StepBound <= 1 { - if innerResult.status == statusHolds { - return holds() - } - return pending(innerResult.formula) + return holds() } if concrete.HasDeadline && !now.Before(concrete.Deadline) { - if innerResult.status == statusHolds { - return holds() - } - return pending(innerResult.formula) + return holds() } next := concrete - next.Inner = concrete.Inner if concrete.HasStepBound { next.StepBound = concrete.StepBound - 1 } diff --git a/internal/ltl/false_negative_test.go b/internal/ltl/false_negative_test.go index 2a2b81c..1bac5c4 100644 --- a/internal/ltl/false_negative_test.go +++ b/internal/ltl/false_negative_test.go @@ -70,14 +70,32 @@ func TestImplies_TemporalAntecedent_FalseAntecedentHolds(t *testing.T) { } } -// A bounded Always whose inner is a still-pending deferred Next obligation must -// carry that obligation past the window, not drop it to holds. The pre-fix -// window-close branch returned holds() unconditionally and lost the violation. -func TestBoundedAlways_PendingInnerCarried(t *testing.T) { - inner := AlwaysFormula{Inner: Next(Thunk(thunkSeq(false))), StepBound: 1, HasStepBound: true} +// A bounded Always whose inner is definitely false inside the window violates. +// The pre-fix window-close branch returned holds() unconditionally and lost +// this; the breach check runs before the window check and must stay there. +func TestBoundedAlways_ViolatedInnerInsideWindow(t *testing.T) { + inner := AlwaysFormula{Inner: Thunk(thunkSeq(false)), StepBound: 1, HasStepBound: true} formula := Always(inner) if verdict, _ := runAndFinalize(formula, 3); verdict != VerdictViolated { - t.Fatalf("Always(boundedAlways(Next(false),1)): got %v, want violated", verdict) + t.Fatalf("Always(boundedAlways(false,1)): got %v, want violated", verdict) + } +} + +// A bounded Always whose inner is still a deferred Next obligation when the +// window closes discharges vacuously: nothing was breached inside the window. +// This is the exact dual of the bounded Eventually violating when its inner has +// not held by the time the window closes +// (TestEventuallyWithinSteps_NextInnerHitsBoundFirstStep), and the pair is what +// makes nnf's G/F dualisation semantics preserving. It costs the deferred check +// the window closed on: G<=n and F<=n both range over the observations at which +// their inner can definitely resolve, never past them. +func TestBoundedAlways_PendingInnerDischargesAtWindowClose(t *testing.T) { + inner := AlwaysFormula{Inner: Next(Thunk(thunkSeq(false))), StepBound: 1, HasStepBound: true} + if verdict, _ := runAndFinalize(Always(inner), 3); verdict != VerdictHolds { + t.Fatalf("Always(boundedAlways(Next(false),1)): got %v, want holds", verdict) + } + if verdict, _ := runAndFinalize(Always(nnf(Not(inner))), 3); verdict != VerdictViolated { + t.Fatalf("its negation: got %v, want violated", verdict) } }