From fea42e289902208b0875e4651a2f078aa03b6ed3 Mon Sep 17 00:00:00 2001 From: PJ Date: Sun, 16 Aug 2026 01:03:25 +0530 Subject: [PATCH] docs(spec): an unbounded eventually is violated at run end --- pkg/spec/src/ltl.ts | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/pkg/spec/src/ltl.ts b/pkg/spec/src/ltl.ts index 3ef5b63..303dd80 100644 --- a/pkg/spec/src/ltl.ts +++ b/pkg/spec/src/ltl.ts @@ -12,9 +12,10 @@ export function next(predicate: () => boolean): Formula { return globalThis.__sanderling__.next(predicate); } -// An unbounded `eventually` never forces a violation within a finite run. -// Prefer `.within(n, unit)` when you want the verifier to fail a property -// that stalls. +// An unbounded `eventually` that never fires is violated when the run ends, +// with the reason "eventually never satisfied", so a goal the run does not +// reach is a violation every time. `.within(n, unit)` convicts at the step the +// window closes instead of at run end. export function eventually(predicate: () => boolean): EventuallyFormula { return globalThis.__sanderling__.eventually(predicate); }