feat(ltl): attribute violations to the obligation origin step

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()