fizzbee-io / fizzbee

Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications
https://fizzbee.io
Apache License 2.0
150 stars 8 forks source link

call statement causes crash state that triggers deadlock #105

Open tekumara opened 1 week ago

tekumara commented 1 week ago

Using a call statement causes a crash state to be generated that leads to a deadlock - should this happen?

Given:

---
action_options:
    Human.Input:
        max_actions: 2
        max_concurrent_actions: 1
---

role Human:

  action Input:
    input = None
    response = ui.history[-1] if ui.history else None
    if not response:
        input = ("Human","a")

    require input
    ui.input(input)
    pass    # ... more happens here ...

role ChatUI:
  action Init:
    self.history = []

  func input(input):
    self.history.append(input)
    pass    # ... more happens here ...

action Init:
  h = Human()
  ui = ChatUI()

I hit an unexpected deadlock because of a crash:

DEADLOCK detected
FAILED: Model checker failed
------
Init
--
state: {"h":"role Human#0 (fields())","ui":"role ChatUI#0 (fields(history = []))"}
------
Human#0.Input
--
state: {"h":"role Human#0 (fields())","ui":"role ChatUI#0 (fields(history = []))"}
------
thread-0
--
state: {"h":"role Human#0 (fields())","ui":"role ChatUI#0 (fields(history = []))"}
------
thread-0
--
state: {"h":"role Human#0 (fields())","ui":"role ChatUI#0 (fields(history = []))"}
------
thread-0
--
state: {"h":"role Human#0 (fields())","ui":"role ChatUI#0 (fields(history = [(\"Human\", \"a\")]))"}
------
crash
--
state: {"h":"role Human#0 (fields())","ui":"role ChatUI#0 (fields(history = [(\"Human\", \"a\")]))"}
------
Human#0.Input
--
state: {"h":"role Human#0 (fields())","ui":"role ChatUI#0 (fields(history = [(\"Human\", \"a\")]))"}
------
crash
--
state: {"h":"role Human#0 (fields())","ui":"role ChatUI#0 (fields(history = [(\"Human\", \"a\")]))"}
------

I wasn't expecting this crash to cause a deadlock.

If however if I make the python statement a call statement, eg:

diff --git a/dl.fizz b/dl.fizz
index aa07973..2eeecbf 100644
--- a/dl.fizz
+++ b/dl.fizz
@@ -14,7 +14,7 @@ role Human:
         input = ("Human","a")

     require input
-    ui.input(input)
+    ui.history.append(input)
     pass    # ... more happens here ...

 role ChatUI:

The crash goes away and there are no deadlocks.