Skip to content

Commit

Permalink
Update specs/quint/specs/reset/README.md
Browse files Browse the repository at this point in the history
Co-authored-by: Daniel <daniel.cason@informal.systems>
  • Loading branch information
josef-widder and cason authored Jun 26, 2024
1 parent 32847cc commit 36cbcab
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion specs/quint/specs/reset/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Check warning on line 48 in specs/quint/specs/reset/README.md

View workflow job for this annotation

GitHub Actions / Check spelling

"Canidate" should be "Candidate".
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.
Expand Down

0 comments on commit 36cbcab

Please sign in to comment.