informalsystems / informalsystems/modelator-py
Feature: generate multiple traces for an invariant violation using TLC
Open
- Dominant language
- Python
- Stars
- 27
- Forks
- 3
- PR merge metrics
- No merged PRs in 30d
Description
Users would like to generate multiple traces violating a single invariant using TLC.
It is possible to do this using TLC's '-continue' parameter. It just allows model checking to continue, using the same algorithm as normal but without the early breakout. This means
1. https://github.com/tlaplus/tlaplus/issues/690
2. TLC will continue to check unbounded state spaces.
this makes any solution that uses the technique a bit finicky.
Alternatives: use simulation mode.
Contributor guide
Assessment
This issue has not been assessed yet.