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

Run time failures in tutorial examples. #61

Open sriram-srinivasan opened 3 months ago

sriram-srinivasan commented 3 months ago

As of commit 8aedd7a8891ed2b8699e549cae963a4b2d351b36

This is a catalog of different failures. If there are examples where it failed as intended, it'd be good to have a line in the examples' output saying so. Better still to convert them to tests.

Liveness failure reported on the following:

   03-multiple-serial-counters/Counter.fizz
   10-coins-to-dice-atomic-3sided/ThreeSidedDie.fizz
   16-elements-counter-parallel/Counter.fizz
   24-while-stmt-atomic/FairCoin.fizz
   26-unfair-coin-toss-while/FairCoin.fizz
   27-unfair-coin-toss-while-noreset/FairCoin.fizz
   28-unfair-coin-toss-while-return/FairCoin.fizz
   30-unfair-coin-toss-method/FairCoin.fizz
   31-fair-die-from-coin-toss-method/FairDie.fizz
   34-simple-hour-clock/HourClock.fizz
   37-unfair-coin-toss-labels/FairCoin.fizz
   38-two-dice-with-coins/TwoDice.fizz
   40-simple-hour-clock-init-action/HourClock.fizz
   41-strict-liveness/Counter.fizz     

Model checking failure on two examples:

         Model checking examples/tutorials/15-elements-counter-serial/Counter.json
         FAILED: Model checker failed. Invariant:  
         ------
         Init
         --
         state: {"ELEMENTS":"[1 2 3]","count":"0","elements":"[]"}
         ------
         Add
         --
         state: {"ELEMENTS":"[1 2 3]","count":"0","elements":"[]"}
         ------

         --
         state: {"ELEMENTS":"[1 2 3]","count":"0","elements":"[1]"}
         ------     

   18-for-stmt-serial/ForLoop.fizz  
         FAILED: Model checker failed. Invariant:  
         ------
         Init
         --
         state: {"count":"3","elements":"[1 2 3]"}
         ------
         Remove
         --
         state: {"count":"2","elements":"[2 3]"}
         ------
         thread-0
         --
         state: {"count":"1","elements":"[3]"}
         ------
         Remove
         --
         state: {"count":"0","elements":"[]"}
         ------
         thread-0
         --
         state: {"count":"-1","elements":"[]"}
         ------

A panic during execution

   49-roles/SimpleRoles.fizz  
         E0714 14:14:25.926486   53437 starlark.go:18] Error evaluating expr: SimpleRoles.fizz:54:16: undefined: state
         panic: Line 54: Error evaluating expr: state

         goroutine 1 [running]:
         github.com/fizzbee-io/fizzbee/modelchecker.(*Process).PanicOnError(...)
             modelchecker/processor.go:556
         github.com/fizzbee-io/fizzbee/modelchecker.(*Thread).executeStatement(0x140002ce990)
             modelchecker/thread.go:673 +0x2318
         github.com/fizzbee-io/fizzbee/modelchecker.(*Thread).Execute(0x140002ce990)
             modelchecker/thread.go:421 +0x164
         github.com/fizzbee-io/fizzbee/modelchecker.(*Processor).processNode(0x140001e5590, 0x140002d25a0)
             modelchecker/processor.go:865 +0x128
         github.com/fizzbee-io/fizzbee/modelchecker.(*Processor).Start(0x140001e5590)
             modelchecker/processor.go:821 +0x6e0
         main.startModelChecker({0x14000016600?, 0x1400018ff18?}, 0x140001e5590)
             main.go:187 +0x78
         main.main()
             main.go:94 +0x730