Understanding the Simulator

Quint's simulator generates samples of executions valid for the model and check invariants at each state of those executions. It is not a verification tool, but it can find violations - sometimes faster than the model checker. Given a model and properties (invariants only, temporal properties are not supported), the simulator will output one of the following:

Output: OK

OK means: it could not find a violation in the explored executions. There might still be an issue.

Running... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 99% | ETA: 1s | 9999/10000 samples
An example execution:
 
[State 0] { balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 0) }
 
[State 1] { balances: Map("alice" -> 0, "bob" -> 37, "charlie" -> 0) }
 
[State 2] { balances: Map("alice" -> 0, "bob" -> 79, "charlie" -> 0) }
 
[State 3] { balances: Map("alice" -> 0, "bob" -> 3, "charlie" -> 0) }
 
[State 4] { balances: Map("alice" -> 0, "bob" -> 90, "charlie" -> 0) }
 
[State 5] { balances: Map("alice" -> 0, "bob" -> 90, "charlie" -> 79) }
 
[ok] No violation found (2459ms).
You may increase --max-samples and --max-steps.
Use --verbosity to produce more (or less) output.
Use --seed=0xe924b0166c3c5 to reproduce.

By default, the simulator will include an example execution, which can be useful to understand the model. To disable it, run it with lower verbosity (--verbosity=1).

Output: Violation

Violation means: there is for sure is a violation, and it will provide a counter-example.

An example execution:
 
[State 0] { balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 0) }
 
[State 1] { balances: Map("alice" -> -63, "bob" -> 0, "charlie" -> 0) }
 
[violation] Found an issue (44ms).
Use --seed=0x4e85b3a53f7ef to reproduce.
Use --verbosity=3 to show executions.
error: Invariant violated

While a model checker's counter-example is always minimal, the simulator one is not - there might exist another counter-example that is smaller.

When to use it

The simulator is a good tool to be used to find some initial bugs and potential problems with the model, as it will quickly find any violation that is likely enough to occur in the number of samples inspected. After some iteration fixing those problems, you get to the point where the simulator runs for a few hours and can't find any bug. Then it is the time to run a model checker and go after the verification. Using the model checker to find the first bugs results in longer feedback cycles, making the simulator a valuable in the process of writing and validating a specification.