fizzbee-io/fizzbee

Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications

fizzbee's Issues

Thanks for making this!

I enjoy this project. Thank you!

Run time failures in tutorial examples.

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

Where are the doc files located?

Where are the files that contain the tutorials/blog posts that appear in the website? I didn't find them in this repo using text search so I'm assuming they are somewhere else.

2pc example doesn't parse on macOS

> fizz ./examples/fizz/two_phase_commit.fizz

line 5:4 mismatched input '' expecting {'None', 'lambda', 'not', 'await', 'print', 'exec', 'True', 'False', 'any', '...', '+', '-', '~', STRING, DECIMAL_INTEGER, OCT_INTEGER, HEX_INTEGER, BIN_INTEGER, IMAG_NUMBER, FLOAT_NUMBER, '(', '{', '[', NAME}
line 5:4 extraneous input '' expecting {DEDENT, 'def', 'return', 'raise', 'from', 'import', 'nonlocal', 'global', 'assert', 'if', 'while', 'for', 'try', 'None', 'with', 'lambda', 'not', 'class', 'yield', 'del', 'pass', 'continue', 'break', 'async', 'await', 'print', 'exec', 'True', 'False', 'atomic', 'serial', 'parallel', 'oneof', 'any', 'action', 'func', 'fair', 'require', 'init', 'role', 'symmetric', 'invariants', 'always', 'eventually', '...', '*', '+', '-', '~', '@', STRING, LABEL, DECIMAL_INTEGER, OCT_INTEGER, HEX_INTEGER, BIN_INTEGER, IMAG_NUMBER, FLOAT_NUMBER, '(', '{', '[', NAME}
line 9:4 mismatched input '' expecting {'None', 'lambda', 'not', 'await', 'print', 'exec', 'True', 'False', 'any', '...', '+', '-', '~', STRING, DECIMAL_INTEGER, OCT_INTEGER, HEX_INTEGER, BIN_INTEGER, IMAG_NUMBER, FLOAT_NUMBER, '(', '{', '[', NAME}
line 9:4 mismatched input '' expecting <EOF>
Error: Compilation failed