From 9bf9f8ad93f087de0cc5395b56ec3c84330fc833 Mon Sep 17 00:00:00 2001 From: Josef Widder <44643235+josef-widder@users.noreply.github.com> Date: Wed, 26 Jun 2024 12:24:22 +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 dd363b064..8a2b67212 100644 --- a/specs/quint/specs/reset/README.md +++ b/specs/quint/specs/reset/README.md @@ -16,7 +16,7 @@ We used `quint run` to conduct random simulation, and checked that the invariant - Local L2 invariants - `monotonicForkIDInv`: ForkID on L2 is non-decreasing - - `monotonicStagedSeqInv`: "highest staged" variable on L2 is non-decreasing + - `monotonicStagedSeqInv`: the `highest_staged_seq_num` variable on L2 blocks is non-decreasing. This variable stores the sequenced number of the latest registration that is staged in L2. - `strictlyMonotonicHeightInv`: L2 height strictly monotonic - `stagedInv`: we only have unstaged registrations which have seq_num greater than `highest_staged_seq_num`