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 46e4ac9 commit 751250d
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 @@ -36,7 +36,7 @@ This also means that the invariants hold under `--step "stepNoRegs"` (as there a
We used `quint run` so that random simulation reaches a violation of the properties. The resulting trace ends in an interesting state (that is defined by the negation of the property; in the text below we describe the reached state directly)

- `staleWitness`: generates a trace where the last block on L1 contains a stale registration
- `resetWitness`: generates a trace where the last block on L2 comes after a reset (new forkID)
- `resetWitness`: generates a trace where there is a reset in L2, showing the first block after the reset, which has a forkID > 0
- `resetAfterProofWitness`: as above, while ensuring that before the reset a proof was accepted on L1 (i.e., provenHeight > 0)
- `forkProvedWitness`: generates a trace where a block produced by L2 after a fork is accepted on L1
- `ConfirmedWitness`: generates a trace where in the last L1 block a registration was confirmed
Expand Down

0 comments on commit 751250d

Please sign in to comment.