Below is a failing model. The failure is expected: The Generate action isn't fair, so the model can stutter after the init, and the always eventually assertion will never pass.
I'd specifically like to understand the simulation behavior this model sees. Here's the output from a given seed:
./fizz --simulation --max_runs 1000 --seed 1748536617242639 test.fizz
Simulation mode is enabled
Model checking test.json
configFileName: fizz.yaml
fizz.yaml not found. Using default options
StateSpaceOptions: options:{max_actions:2 max_concurrent_actions:2} deadlock_detection:false
Seed: 1748536617242639
processing: A
done processing: []
FAILED: Model checker failed. Deadlock/stuttering detected
seed: 1748536617242639
------
Init
--
state: {"history":"[]"}
------
Generate
--
state: {"history":"[\"A\"]"}
------
This is confusing for the following reasons:
- The print output shows that the
Process action happened, and did complete. However, the output states (shown here printed, in the html, etc) do not include that state.
- The failure reports
Deadlock/stuttering detected, and it's not clear what that means here, given that max_actions is 2 and we have apparently completed two actions (Generate, Process), so it shouldn't be a stutter. I would expect the failure to be due to the always eventually assertion failing.
- (When the
always eventually assertion is removed, the seed passes. (This might just be perturbing the RNG, but debuggability would be improved if it was possible to disable assertions without modifying the seed.)
---
options:
max_actions: 2
deadlock_detection: False
---
action Init:
history = []
action Generate:
history.append("A")
atomic fair<strong> action Process:
require len(history) > 0
event = fair any history
print("processing: " + str(event))
history.pop()
print("done processing: " + str(history))
always eventually assertion LotsOfElements:
return len(history) > 1000
Below is a failing model. The failure is expected: The Generate action isn't fair, so the model can stutter after the init, and the
always eventuallyassertion will never pass.I'd specifically like to understand the simulation behavior this model sees. Here's the output from a given seed:
This is confusing for the following reasons:
Processaction happened, and did complete. However, the output states (shown here printed, in the html, etc) do not include that state.Deadlock/stuttering detected, and it's not clear what that means here, given that max_actions is 2 and we have apparently completed two actions (Generate, Process), so it shouldn't be a stutter. I would expect the failure to be due to thealways eventually assertionfailing.always eventually assertionis removed, the seed passes. (This might just be perturbing the RNG, but debuggability would be improved if it was possible to disable assertions without modifying the seed.)