How does the implicit crash action work in serial block modifiers?

[TSPMP]

I am referring to the serial block modifier example

---
options:
  max_actions: 10
  max_concurrent_actions: 2
---

action Init:
  a = 0
  b = 0

serial action Add:
  a = (a + 1) % 3
  b = (b + 1) % 3

All traces I write here are assumed to be taken from the initial state.

If I go to the explorer in the playground then I can simulate the trace

Add -> crash

which indicates that the first thread can crash. I can also go from the initial state

Add -> Add

which interleaves another Add action after the first Add action in another thread. Now, I would expect that the two threads can crash independently but there is only one crash action active. After taking the crash action, i.e.

Add -> Add -> crash

I have the actions Add and action-1 available which would indicate that the second thread crashes. But now I would expect that also the first thread can still crash which is not available.

Is this a bug or is my understanding of the serial block modifier wrong?

[jayaprabhakar]

But now I would expect that also the first thread can still crash which is not available.

That's a great question. From the observable state space perspective, the second thread crashing at this point is exactly the same as the first thread crashes before the Add was called.

That is,
Add (a=1,b=0) -> Add (a=2,b=0) -> crash-action-1 (state space not generated)
is exactly equivalent to

Add (a=1,b=0) -> crash -> Add (a=2,b=0)

In both the cases, the observable state is the same, thread alive 1, current thread is action-2, program counter also matches).

So FizzBee optimizes the state spaces and simplifies the graph to include only one since scenario (always crash implies the currently active these crashed)

[TSPMP]

@jayaprabhakar - Thank you, that makes me understand a little better how fizzbee behaves there. I have a follow-up question then 😄: in the generated state graph I was looking for the equivalent state for the trace

Add -> crash -> Add -> crash

which is the state

a = 2, b = 0, no threads alive

and found it here

but it is reached in the state graph through another trace. It looked to me that the Actions: 5, Forks: 10 should be the minimal number of Actions and Forks to reach that state but I guess that is not true because the aforementioned trace

Add -> crash -> Add -> crash

would reach this with Actions: 2, Forks: 4. How should I interpret the Actions, Forks values in the state graph?