diegomrsantos opened a new pull request, #4277: URL: https://github.com/apache/iggy/pull/4277
A persisted purge cutoff can outlive the volatile operation history it describes, causing fresh operations that reuse those numbers to be treated as purged. These Quint models make the recovery assumptions explicit and compare candidate rules, including bookmark cleanup, retries, and state transfer with rollback. This separates the model and supporting files from #4130 so that the recovery fix can proceed independently. The README identifies the implementation snapshot behind the model and its limits. Passing checks apply to the modeled configurations, not to conformance of the Rust implementation. The PR is a draft for reviewing the assumptions and deciding how to maintain the model, including the proposed quick suite in CI. CI wiring and Quint Connect integration are not included. Validation on this branch ran `check.py --suite=quick`, covering type checks, 19 deterministic scenarios, and sampled simulations. All 11 commands matched their expected outcomes, including the intentional counterexamples. Markdown lint and whitespace checks passed. The model logic and runner are unchanged from the version extracted from #4130. -- This is an automated message from the Apache Git Service. To respond to the message, please log on to GitHub and use the URL above to go to the specific comment. To unsubscribe, e-mail: [email protected] For queries about this service, please contact Infrastructure at: [email protected]
