State generated #1620
-
|
In TLA+ (vscode and toolbox) you can see the number of states and coverage during model checking. How can you do that with Quint? Thanks! |
Beta Was this translation helpful? Give feedback.
Replies: 1 comment 1 reply
-
|
Hi! The best way to achieve this in Quint is through TLC itself (the model checker used by vscode and toolbox for TLA+). This is not fully integrated yet, but you can run a script that takes care of most of the wrapping around it. We don't usually run TLC for Quint - we use either the simulator (on There are plans to enhance support for TLC in the near future, and also add more features to the simulator, including statistical coverage reporting stuff. |
Beta Was this translation helpful? Give feedback.
-
|
Thank you very much. This is very useful information. |
Beta Was this translation helpful? Give feedback.
Hi! The best way to achieve this in Quint is through TLC itself (the model checker used by vscode and toolbox for TLA+). This is not fully integrated yet, but you can run a script that takes care of most of the wrapping around it.
We don't usually run TLC for Quint - we use either the simulator (on
quint run) or the Apalache model checker (onquint verify). The simulator doesn't have coverage reporting yet, and even if it did, it would be only an estimate as it only covers some execution (not all of them). Apalache doesn't have coverage reporting because it doesn't enumerate all states - it does symbolic model checker with constraint solving, and therefore doesn't need to know how many sa…