Implements simulation mode.
Adds flag --simulation and an optional seed with --seed numeric to reproduce the failure case.
Runs in a single thread, but you can start multiple processes to parallelize
Supports deadlock detection
Liveness checks mostly work, but there are some false positives that will be fixed soon.
To run without liveness check, the cases are explored randomly until the path reaches the max_actions (default=100) and at each step checks for the safety constraints, without maintaining visited nodes or cycle detection..
With liveness enabled (that is at least one liveness assertion), the paths would be explored randomly until a max length (0, max_actions), without maintaining visited nodes or cycle detection. Once this random path length is reached, only fair actions will be scheduled going forward, and starts maintaining visited nodes to enable cycle detection.
If no fair action could be enabled, it will be considered stuttering. If a cycle is found, it will check for always eventually and eventually always property in the cycle.
Note: If the cycle is detected, we do not check if the cycle match the fairness criteria. So this could lead to false positives with error.
Implements simulation mode. Adds flag
--simulationand an optional seed with--seed numericto reproduce the failure case.To run without liveness check, the cases are explored randomly until the path reaches the max_actions (default=100) and at each step checks for the safety constraints, without maintaining visited nodes or cycle detection..
With liveness enabled (that is at least one liveness assertion), the paths would be explored randomly until a max length (0, max_actions), without maintaining visited nodes or cycle detection. Once this random path length is reached, only fair actions will be scheduled going forward, and starts maintaining visited nodes to enable cycle detection. If no fair action could be enabled, it will be considered stuttering. If a cycle is found, it will check for always eventually and eventually always property in the cycle.
Note: If the cycle is detected, we do not check if the cycle match the fairness criteria. So this could lead to false positives with error.