Deadlock detection fails when max_actions are exhausted

[tekumara]

I've noticed that the deadlock detection fails when max_actions are exhausted, even if there are enabled actions that could make progress.

eg:

---
deadlock_detection: true
options:
    max_actions: 4
    max_concurrent_actions: 3
---


always eventually assertion BalanceMatchTotal:
  total = 0
  for balance in balances.values():
    total += balance
  return total == 5

action Init:
  balances = {'Alice': 3, 'Bob': 2}
  wire_requests = []

atomic action Wire:
  any amount in range(1,10):
    if balances['Alice'] >= amount:
      balances['Alice'] -= amount
      wire_requests.append(('Alice', 'Bob', amount))

atomic fair action DepositWireTransfer:
  any req in wire_requests:
    balances[req[1]] += req[2]
    wire_requests.remove(req)

# Add this temporarily until we fix Bob to transfer money to Alice
atomic action NoOp:
  pass

Fails with:

Model checking bank.json
configFileName: fizz.yaml
fizz.yaml not found. Using default options
StateSpaceOptions: options:{max_actions:4 max_concurrent_actions:3} deadlock_detection:true
Nodes: 39, queued: 0, elapsed: 7.599875ms
Time taken for model checking: 7.619125ms
Writen graph dotfile: out/run_2024-09-29_09-50-36/graph.dot
To generate svg, run: 
dot -Tsvg out/run_2024-09-29_09-50-36/graph.dot -o graph.svg && open graph.svg
Max Depth 8
DEADLOCK detected
FAILED: Model checker failed
------
Init
--
state: {"balances":"{\"Alice\": 3, \"Bob\": 2}","wire_requests":"[]"}
------
Wire
--
state: {"balances":"{\"Alice\": 3, \"Bob\": 2}","wire_requests":"[]"}
------
Any:amount=1
--
state: {"balances":"{\"Alice\": 2, \"Bob\": 2}","wire_requests":"[(\"Alice\", \"Bob\", 1)]"}
------
Wire
--
state: {"balances":"{\"Alice\": 2, \"Bob\": 2}","wire_requests":"[(\"Alice\", \"Bob\", 1)]"}
------
Any:amount=1
--
state: {"balances":"{\"Alice\": 1, \"Bob\": 2}","wire_requests":"[(\"Alice\", \"Bob\", 1), (\"Alice\", \"Bob\", 1)]"}
------
Wire
--
state: {"balances":"{\"Alice\": 1, \"Bob\": 2}","wire_requests":"[(\"Alice\", \"Bob\", 1), (\"Alice\", \"Bob\", 1)]"}
------
Any:amount=1
--
state: {"balances":"{\"Alice\": 0, \"Bob\": 2}","wire_requests":"[(\"Alice\", \"Bob\", 1), (\"Alice\", \"Bob\", 1), (\"Alice\", \"Bob\", 1)]"}
------
DepositWireTransfer
--
state: {"balances":"{\"Alice\": 0, \"Bob\": 2}","wire_requests":"[(\"Alice\", \"Bob\", 1), (\"Alice\", \"Bob\", 1), (\"Alice\", \"Bob\", 1)]"}
------
Any:req=("Alice", "Bob", 1)
--
state: {"balances":"{\"Alice\": 0, \"Bob\": 3}","wire_requests":"[(\"Alice\", \"Bob\", 1), (\"Alice\", \"Bob\", 1)]"}
------
Writen graph json: out/run_2024-09-29_09-50-36/error-graph.json
Writen graph dotfile: out/run_2024-09-29_09-50-36/error-graph.dot
To generate an image file, run: 
dot -Tsvg out/run_2024-09-29_09-50-36/error-graph.dot -o error-graph.svg && open error-graph.svg

If max_actions: 5 then this will pass.

In another case I have, it doesn't matter how large I make max_actions. The model checker cycles between an action and a fair action until it hits max_actions and then declares a deadlock detected.

[tekumara]

An even more minimal example that fails:

---
action_options:
    Append:
        max_actions: 2
---

action Init:
    history = []

action Append:
    history.append("A")

[jp-fizzbee]

For now, I am not sure what the expected behavior should be.

• The intent for max_actions was just some safety check in case of some modeling bugs so it doesn't go on an infinite loop. - At action level limit some disruptive actions that will cause the state space to grow indefinitely.

For now, skipping deadlock errors if max_actions is reached at the total.
#97

[tekumara]

FYI - I'm still experiencing a deadlock when running with 1fd9b76 and setting max_actions, eg:

---
action_options:
    Append:
        max_actions: 2
---

action Init:
    history = []

action Append:
    history.append("A")

Produces:

❯ fizz 1.fizz
Model checking 1.json
configFileName: fizz.yaml
fizz.yaml not found. Using default options
StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2} action_options:{key:"Append" value:{max_actions:2}}
Nodes: 3, queued: 0, elapsed: 792.375µs
Time taken for model checking: 803.25µs
Writen graph dotfile: out/run_2024-12-01_15-34-45/graph.dot
To generate svg, run: 
dot -Tsvg out/run_2024-12-01_15-34-45/graph.dot -o graph.svg && open graph.svg
DEADLOCK detected
FAILED: Model checker failed
------
Init
--
state: {"history":"[]"}
------
Append
--
state: {"history":"[\"A\"]"}
------
Append
--
state: {"history":"[\"A\", \"A\"]"}
------
Writen graph json: out/run_2024-12-01_15-34-45/error-graph.json
Writen graph dotfile: out/run_2024-12-01_15-34-45/error-graph.dot
To generate an image file, run: 
dot -Tsvg out/run_2024-12-01_15-34-45/error-graph.dot -o error-graph.svg && open error-graph.svg
Writen error states as html: out/run_2024-12-01_15-34-45/error-states.html
To open: 
open out/run_2024-12-01_15-34-45/error-states.html