informalsystems / informalsystems/modelator
Add timeout option and default timeout for running model checking.
Open
enhancement
- Dominant language
- Python
- Stars
- 72
- Forks
- 6
- PR merge metrics
- No merged PRs in 30d
Description
Users should be able to specify when they want model checking to stop.
While Apalache has a limit in the trace length that is checked, it can still take much longer than the user is ready to wait (depending on the model).
TLC does not have the length limit and could run forever.
Contributor guide
Assessment
This issue has not been assessed yet.