fix(verifier): refresh predicate errors per step

EvaluateProperties short-circuits once an Always-property latches to
violated, so the underlying goja predicate stops being called and
formula.err keeps whatever it threw at step 1. The runner logs
PredicateError every step a property is violated, which made every
subsequent log line repeat the step-1 throw. That looks like the spec
runtime is seeing stale state, but it is just stale error reporting.

EvaluateProperties now invokes every registered predicate once per step
purely to refresh formula.err. Verdicts are unaffected. The thunk
itself stops latching so the new value wins on whichever path runs first.
This commit is contained in:
pj committed 2026-04-26 15:44:01 +07:00
1 parent a2b4b4290b
commit 9abd0511bd
2 files changed
+25 -6

No files matched your search

+4 -3
View File
@@ -14,9 +14,10 @@ type extractorState struct {
type formulaState struct {
predicate goja.Callable
// err latches the first goja error returned by predicate. The thunk
// returns false on error so the LTL evaluator marks the property
// violated; PredicateError surfaces the underlying cause.
// err holds the goja error from this thunk's most recent invocation, or
// nil if the latest call succeeded. The thunk returns false on error so
// the LTL evaluator marks the property violated; PredicateError surfaces
// the underlying cause for the current step.
err error
}