diff --git a/internal/ltl/evaluator.go b/internal/ltl/evaluator.go index 3f8fa07..c98f293 100644 --- a/internal/ltl/evaluator.go +++ b/internal/ltl/evaluator.go @@ -33,17 +33,27 @@ func (v Verdict) String() string { // violates, the overall verdict latches to Violated. type Evaluator struct { root Formula - pending []Formula + pending []obligation violated bool steps int violation *Violation } +// obligation pairs a residual formula with the step that spawned it, so a +// deferred check (a next, a pending eventually) that fails on a later step can +// be attributed to the step that created the obligation. +type obligation struct { + formula Formula + origin int +} + // Violation is the witness for a latched verdict: the failing sub-formula, a -// human-readable reason, and the observation step it fired at. A thrown -// predicate carries the goja error text as its reason and sets IsError; a plain -// false carries "predicate false"; Finalize fills it for liveness obligations -// that never discharged. +// human-readable reason, and the step the failed obligation originated at. For +// an immediate predicate failure that is the observation step itself; for a +// deferred obligation (next, eventually) it is the earlier step that spawned +// it, the one that caused the violation. A thrown predicate carries the goja +// error text as its reason and sets IsError; a plain false carries "predicate +// false"; Finalize fills it for liveness obligations that never discharged. type Violation struct { Formula Formula Reason string @@ -62,19 +72,29 @@ func (e *Evaluator) Observe() Verdict { return e.ObserveAt(time.Now()) } -// ObserveAt is like Observe but takes the current step time explicitly. +// ObserveAt is like Observe but takes the current step time explicitly. Steps +// are numbered by an internal counter starting at 1; callers whose step +// numbering can skip observations should use ObserveAtStep instead. func (e *Evaluator) ObserveAt(now time.Time) Verdict { + return e.ObserveAtStep(now, e.steps+1) +} + +// ObserveAtStep is like ObserveAt but labels the observation with the caller's +// step index, so violation witnesses carry the caller's numbering even when +// some steps were never observed (for example transitional steps the verifier +// skips). +func (e *Evaluator) ObserveAtStep(now time.Time, step int) Verdict { if e.violated { return VerdictViolated } - e.steps++ + e.steps = step - fresh := rootObligation(e.root) + fresh := obligation{formula: rootObligation(e.root), origin: step} obligations := append(e.pending, fresh) e.pending = e.pending[:0] - for _, obligation := range obligations { - result := reduce(obligation, now) + for _, entry := range obligations { + result := reduce(entry.formula, now) switch result.status { case statusHolds: // drop @@ -83,11 +103,11 @@ func (e *Evaluator) ObserveAt(now time.Time) Verdict { e.pending = nil e.violation = result.witness if e.violation != nil { - e.violation.Step = e.steps + e.violation.Step = entry.origin } return VerdictViolated case statusPending: - e.pending = append(e.pending, result.formula) + e.pending = append(e.pending, obligation{formula: result.formula, origin: entry.origin}) } } @@ -100,21 +120,22 @@ func (e *Evaluator) ObserveAt(now time.Time) Verdict { } // collapse removes structurally-identical obligations, keeping the first -// occurrence in order. Distinct predicates never merge because ThunkFormula's -// name participates in its describe() key, so deduping cannot hide a violation. -func collapse(obligations []Formula) []Formula { +// occurrence in order so the surviving entry carries the earliest origin step. +// Distinct predicates never merge because ThunkFormula's name participates in +// its describe() key, so deduping cannot hide a violation. +func collapse(obligations []obligation) []obligation { if len(obligations) < 2 { return obligations } seen := make(map[string]struct{}, len(obligations)) result := obligations[:0] - for _, obligation := range obligations { - key := obligation.describe() + for _, entry := range obligations { + key := entry.formula.describe() if _, ok := seen[key]; ok { continue } seen[key] = struct{}{} - result = append(result, obligation) + result = append(result, entry) } return result } @@ -127,14 +148,14 @@ func (e *Evaluator) Finalize() Verdict { if e.violated { return VerdictViolated } - for _, obligation := range e.pending { - if finalize(obligation) == statusViolated { + for _, entry := range e.pending { + if finalize(entry.formula) == statusViolated { e.violated = true e.pending = nil e.violation = &Violation{ - Formula: obligation, - Reason: finalizeReason(obligation), - Step: e.steps, + Formula: entry.formula, + Reason: finalizeReason(entry.formula), + Step: entry.origin, } return VerdictViolated } @@ -224,9 +245,9 @@ func (e *Evaluator) Residual() Formula { if len(e.pending) == 0 { return PureFormula{Value: true} } - combined := e.pending[0] - for _, formula := range e.pending[1:] { - combined = AndFormula{Left: combined, Right: formula} + combined := e.pending[0].formula + for _, entry := range e.pending[1:] { + combined = AndFormula{Left: combined, Right: entry.formula} } return combined } @@ -258,11 +279,6 @@ type reduceResult struct { func holds() reduceResult { return reduceResult{status: statusHolds} } -// violated reports a violation without an attached witness. Used where the -// failing sub-formula is recovered from a child result whose own witness is -// carried up by violatedFrom. -func violated() reduceResult { return reduceResult{status: statusViolated} } - // violatedWith reports a violation that originates at the given sub-formula // with the given reason. The reason distinguishes a thrown predicate from a // plain false so callers (and the replay UI) can render the cause. diff --git a/internal/ltl/finalize_test.go b/internal/ltl/finalize_test.go index d16a6b5..2679127 100644 --- a/internal/ltl/finalize_test.go +++ b/internal/ltl/finalize_test.go @@ -128,20 +128,23 @@ func TestViolationLatchIsMonotonic(t *testing.T) { } func TestCollapse_IdenticalObligationsMerge(t *testing.T) { - merged := collapse([]Formula{ - Next(Pure(true)), - Next(Pure(true)), - Next(Pure(true)), + 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([]Formula{ - Eventually(ThunkNamed("p3", func() (bool, error) { return false, nil })), - Eventually(ThunkNamed("p4", func() (bool, error) { return false, nil })), + 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)) diff --git a/internal/ltl/witness_test.go b/internal/ltl/witness_test.go index 6e4c580..69a6ba5 100644 --- a/internal/ltl/witness_test.go +++ b/internal/ltl/witness_test.go @@ -71,6 +71,80 @@ func TestViolation_FinalizeFillsWitness(t *testing.T) { } } +func TestViolation_NextAttributesOriginStep(t *testing.T) { + // always(next(p)): the obligation spawned at step 2 is checked against + // step 3's state; the violation belongs to step 2, the step that caused it. + values := []bool{true, false} + step := 0 + evaluator := NewEvaluator(Always(Next(ThunkNamed("p", func() (bool, error) { + current := values[step] + step++ + return current, nil + })))) + if got := evaluator.ObserveAt(time.Unix(0, 0)); got != VerdictPending { + t.Fatalf("step 1: got %v, want pending", got) + } + if got := evaluator.ObserveAt(time.Unix(1, 0)); got != VerdictPending { + t.Fatalf("step 2: got %v, want pending", got) + } + if got := evaluator.ObserveAt(time.Unix(2, 0)); got != VerdictViolated { + t.Fatalf("step 3: got %v, want violated", got) + } + witness := evaluator.Violation() + if witness == nil { + t.Fatal("Violation = nil, want non-nil") + } + if witness.Step != 2 { + t.Errorf("Step = %d, want 2 (the step that spawned the next obligation)", witness.Step) + } +} + +func TestViolation_FinalizeAttributesOriginStep(t *testing.T) { + evaluator := NewEvaluator(Always(Next(ThunkNamed("p", func() (bool, error) { + return true, nil + })))) + evaluator.ObserveAt(time.Unix(0, 0)) + evaluator.ObserveAt(time.Unix(1, 0)) + if got := evaluator.Finalize(); got != VerdictViolated { + t.Fatalf("Finalize = %v, want violated", got) + } + witness := evaluator.Violation() + if witness == nil { + t.Fatal("Violation = nil after Finalize, want non-nil") + } + if witness.Step != 2 { + t.Errorf("Step = %d, want 2 (the step whose next obligation has no successor)", witness.Step) + } +} + +func TestViolation_ObserveAtStepUsesCallerNumbering(t *testing.T) { + // The caller skips step 5 (a transitional step the verifier never saw); the + // origin must carry the caller's labels, not a contiguous internal count. + values := []bool{true, false} + step := 0 + evaluator := NewEvaluator(Always(Next(ThunkNamed("p", func() (bool, error) { + current := values[step] + step++ + return current, nil + })))) + if got := evaluator.ObserveAtStep(time.Unix(0, 0), 3); got != VerdictPending { + t.Fatalf("step 3: got %v, want pending", got) + } + if got := evaluator.ObserveAtStep(time.Unix(1, 0), 4); got != VerdictPending { + t.Fatalf("step 4: got %v, want pending", got) + } + if got := evaluator.ObserveAtStep(time.Unix(2, 0), 6); got != VerdictViolated { + t.Fatalf("step 6: got %v, want violated", got) + } + witness := evaluator.Violation() + if witness == nil { + t.Fatal("Violation = nil, want non-nil") + } + if witness.Step != 4 { + t.Errorf("Step = %d, want 4 (caller-labeled origin, not detection step 6)", witness.Step) + } +} + func TestViolation_NilBeforeViolation(t *testing.T) { evaluator := NewEvaluator(Always(Pure(true))) evaluator.Observe()