From 36cbcab1aa8db4968c1a1760a5c2d2a343340835 Mon Sep 17 00:00:00 2001 From: Josef Widder <44643235+josef-widder@users.noreply.github.com> Date: Wed, 26 Jun 2024 12:22:04 +0200 Subject: [PATCH] Update specs/quint/specs/reset/README.md Co-authored-by: Daniel --- specs/quint/specs/reset/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/specs/quint/specs/reset/README.md b/specs/quint/specs/reset/README.md index 8b3b12253..b87147b41 100644 --- a/specs/quint/specs/reset/README.md +++ b/specs/quint/specs/reset/README.md @@ -45,7 +45,7 @@ We used `quint run` so that random simulation reaches a violation of the propert - `unsuccessfulResetWitness`: generates a trace where there was a reset on L2, and before a second block was added to L2 with the same fork ID, another reset happened -- `lastPossibleL1BlockWitness`: trace where in the previous L1 block there where no stale registrations(timed-out unfulfilled registrations), but the unfulfilled registrations from the previous block +- `lastPossibleL1BlockWitnessCanidate`: trace where in the previous L1 block there where no stale registrations(timed-out unfulfilled registrations), but the unfulfilled registrations from the previous block would become stale in the new block (as the time progressed). In this scenario, the proof comes in just in time. The registrations actually don't become stale. TODO: this is a corner case. Experiments showed that it doesn't exists. See discussion in qnt file.