Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Run time failures in tutorial examples. #61

Open
sriram-srinivasan opened this issue Jul 14, 2024 · 0 comments
Open

Run time failures in tutorial examples. #61

sriram-srinivasan opened this issue Jul 14, 2024 · 0 comments

Comments

@sriram-srinivasan
Copy link

As of commit 8aedd7a

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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant