Simulation mode running more actions than configured, incorrectly updating state

[ANorwell]

Here is a model and associated simulation run:

---
options:
    max_actions: 2
deadlock_detection: False
---

action Init:
    history = []

fair 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

 ./fizz --simulation --max_runs 1000 --seed 1748538852856350 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: 1748538852856350
processing: A
done processing: ["A"]
processing: A
done processing: ["A"]
FAILED: Model checker failed. Invariant:  LotsOfElements
seed: 1748538852856350
------
Init
--
state: {"history":"[]"}
------
Generate
--
state: {"history":"[\"A\"]"}
------
Generate
--
state: {"history":"[\"A\", \"A\"]"}
------
Process
--
state: {"history":"[\"A\", \"A\"]"}
------
Writen graph json: out/run_2025-05-29_13-17-42/error-graph.json
Writen graph dotfile: out/run_2025-05-29_13-17-42/error-graph.dot
To generate an image file, run:
dot -Tsvg out/run_2025-05-29_13-17-42/error-graph.dot -o error-graph.svg && open error-graph.svg
Writen error states as html: out/run_2025-05-29_13-17-42/error-states.html
To open:
open out/run_2025-05-29_13-17-42/error-states.html

The result here is quite confusing for several reasons:

• Even though max_actions is 2, it seems to be running 4 actions: the Generate, Generate, Process shown in the output, and also a second Process that was run according to stdout, but not shown in the output (also seen in Confusing simulation mode Deadlock/stuttering detected #214)
• The state field doesn't seem to be being updated properly. stdout shows that it has been modified (has only one element), but the actual state shown in the output doesn't reflect that (still has two elements), and the second, repeated execution of Process again starts with two elements.

[jp-fizzbee]

Actually, similar to previous issue #214, the trace got truncated. The intended trace was,

FAILED: Model checker failed. Invariant:  LotsOfElements
seed: 1748538852856350
------
Init
--
state: {"history":"[]"}
------
Generate
--
state: {"history":"[\"A\"]"}
------
Generate
--
state: {"history":"[\"A\", \"A\"]"}
------
Process
--
state: {"history":"[\"A\", \"A\"]"}
------
Any:event="A"
--
state: {"history":"[\"A\"]"}
------

The non-deterministic choice got truncated.

I see the confusion with the stack length and the max_actions, because of both non-obvious arbitrary behavior and simulation feature was never documented. Let me explain the current behavior, but I think I should fix that as this will lead to unexpected behavior.

Simulation mode without liveness checks

Here, the max_actions would behave as expected. The seed will be used to make all non-deterministic choices.

• next action
• any or oneof choices
• yield points

Simulation mode with liveness checks

Unlike exhaustive model checking, in simulation we cannot simply rely on cycle detection because fairness checking is not possible. So, we randomly choose a cut-off point, say k between [0 and max_actions] based on the seed, until then, we don't do any cycle detection and execute all actions similar to the simulation mode without liveness checks until the cutoff point instead of max_actions. Once the cutoff point is reached, we only execute fair actions, and enable cycle detection. This way, we could do liveness checks. Here, one issue is, to determine how many more actions to execute. Probably, I should have used the new upper limit to still be max_actions, so (max_actions-k) actions would be executed with cycle detection and liveness enabled. This would have been the expected behavior.
The issue was, in the first phase we ran all actions until the cutoff point without cycle detection. This leads to many cycle being unrolled and so trace length could have significant duplicates, so for larger values of k, there won't be enough steps left for a meaningful liveness check. I wanted to pad more steps and intended to set the new max_actions as original max_actions + k, but for some reason, I picked 2 * max_actions. (If I remember right, since k was arbitrary and chosen by the random seed, I wanted to make this deterministic and say, in simulation mode when liveness assertions are made, the max trace length can be up to 2*max_actions instead of having to explain max_actions + some arbitrary delta where the delta could be up to max_actions.)

That's why you would see traces up to 2 * max_actions when liveness assertions are made.

If actions count exceeds 2*max_actions without finding a cycle, then liveness and deadlock issues will not be reported.

This is purely based on a few tests I ran to increase the likelihood of finding bugs quickly. (Without this naive and hacky heuristic, either the users have to explicitly set a much larger max_actions, that will take a lot longer to find some bugs as breadth will not be explored. If they didn't, many liveness issues will not be reported)

[jp-fizzbee]

In #214, you raised the point of assertions impacting the trace execution. As explained above, when switching from 0 liveness assertion to 1 or more liveness assertion, one step changes - selecting the random cutoff point. This impacts the trace execution when adding first liveness assertion or removing the last liveness assertion.

Oneway to keep the same behavior is, to keep a dummy liveness assertion that always return True. This will fix the issue.

[ANorwell]

Thanks, that description makes sense. I think I'm understanding liveness more in terms of the graph. My understanding now:

• In exhaustive mode with no max_actions, I can see that if there's a cycle or terminal node where the liveness check fails, that's failing, whereas if there's a cycle or leaf node where the liveness check passes, that's allowed.
• In exhaustive mode with max_actions, we just treat the resulting pruned graph in the same way. e.g., if a node that is terminal due to max_actions passes a eventually always check, then the model passes -- even if without max_actions that node would not be terminal and the check would have subsequently failed.
• In simulation mode, each simulation has a single path of up to 2 * max_actions (with only fair actions in the last 2 * max_actions - k actions). There might or might not be a cycle at the end of the path. If the entire cycle or terminal node passes the eventually always check then that simulation run passes.

edit: It seems my understanding above is wrong. This model, with a failing terminal node, fails under exhaustive mode but passes under simulation mode:

---
options:
    max_actions: 2
deadlock_detection: False
---

action Init:
    history = []

fair action Generate:
    history.append("A")

eventually always assertion False:
    return False

This model (with a cycle) fails under simulation mode:

---
options:
    max_actions: 3
deadlock_detection: True
---

action Init:
    history = []

fair action Generate:
    if len(history) < 2:
        history.append("A")
    else:
        history.clear()

eventually always assertion FalseFalse:
    return False #len(history) == 100

always assertion Debug:
    print(str(history))
    return True

[ANorwell]

It might be nice if 2 * max_actions - k, the number of fair actions to run at the end, was configurable? In eventual consistent systems, the model implementer will have a sense of, now that the user is no longer making changes, how long it takes for the system to reach stability.