FizzBee generates multiple visualizations and diagrams. So far you would have seen,
automatically generated state diagrams. In addition to state diagrams, FizzBee also
generates sequence diagrams and algorithm visualizations.
These are helpful in understanding the algorithm and the system behavior.
Feature
Description
Pseudo Code to Visualizations
Generates sequence, state, and algorithm diagrams directly from high-level, Python-like pseudo code.
Zero Extra Effort
Visualizations are created directly from your pseudo code with no additional manual input required.
Interactive Experience
Provides a dynamic, whiteboard-like interface to explore states, transitions, and scenarios in real time.
Comprehensive Simulation
Automatically simulates complex scenarios like non-atomic operations, crashes, message loss, concurrency, and visualizes all possible states.
Correctness Assertion
Enables adding assertions to ensure the design meets safety and liveness requirements.
Easy to Use
Familiar Python-like syntax reduces the learning curve compared to other formal methods tools.
Enable whiteboard visualizations
On the fizzbee playground, you can enable the whiteboard visualizations by setting
the Enable Whiteboard checkbox. Then click Run button.
Once the model checking is done, you can see a link to the Explorer in the Console.
Clicking on the Explorer link will open the explorer in a new tab.
Example 1: Two phase commit
Before we go over the tutorial, let’s see a complete working example.
NUM_PARTICIPANTS=2role Coordinator:
action Init:
self.prepared = set() self.state ="init" action Write:
if self.state !="init":
return self.state ="working"for rm in self.PARTICIPANTS:
vote= rm.Prepare()ifvote=='aborted':
self.Abort()return self.prepared.add(rm.ID) self.Commit() fair action Timeout:
if self.state !="committed":
self.Abort() fair action Restart:
if self.state =="committed":
for rm in self.PARTICIPANTS:
rm.Commit() func Abort():
self.state ="aborted"for rm in self.PARTICIPANTS:
rm.Abort() func Commit():
if self.state =='working' and len(self.prepared)== len(self.PARTICIPANTS):
self.state ='committed'for rm in self.PARTICIPANTS:
rm.Commit()role Participant:
action Init:
self.state ="working" fair action Timeout:
if self.state =="working":
self.state ="aborted" func Prepare():
if self.state !='working':
return self.state
oneof:
self.state ='prepared' self.state ='aborted'return self.state
func Commit():
self.state ='committed' func Abort():
self.state ='aborted'always assertion ResMgrsConsistent:
for rm1 in participants:
for rm2 in participants:
if rm1.state =='committed' and rm2.state =='aborted':
return False
return True
eventually always assertion Terminated:
return coordinator.state in ('committed', 'aborted')action Init:
participants=[]for i in range(NUM_PARTICIPANTS):
p= Participant(ID=i) participants.append(p)coordinator= Coordinator(PARTICIPANTS=participants)
Enable Enable Whiteboard checkbox, and Run.
Once the model checker completes, click on Communication Diagram link in the console.
This will show the block diagram for the two phase commit protocol.
On the left, you will see various buttons for the actions. Click on the Coordinator#0.Write button.
it should start the sequence diagram. Continue to click on the buttons to see the sequence diagram.
If you always choose the success path, you will see eventually both the participants and the coordinator
reach the committed state.
You can explorer most possible sequences and states.
Example 2: Insertion Sort
Let’s try another visualization - the Insertion Sort algorithm. FizzBee is a formal
verification language, so verifying Insertion Sort is not the best use case. But this introduces
the visualization capabilities.
If you look at the insertion_sort method, the code is actually a working python code
(with only the method definition syntax being different)
Checkpoint
Checkpoint is similar to breakpoint in debugger, but this is not running the code during exploration
instead it executes the model and checkpoints the state at various points.
There are default checkpoints at the start of each action, any non-determinism
or when there are any yields.
You can set explicit checkpoints using `checkpoint`.
---
deadlock_detection: falseoptions:
max_actions: 1---
atomic action InsertionSort:
insertion_sort(arr)atomic func insertion_sort(arr):
if len(arr) <= 1:
return# If the array has 0 or 1 element, it is already sorted, so returnfor i in range(1, len(arr)): # Iterate over the array starting from the second elementcur= i
ins= i-1
key= arr[i]# Store the current element as the key to be inserted in the right positionj= i-1
`checkpoint`while j >=0 and key < arr[j]: # Move elements greater than key one position aheadins= j
arr[j+1]= arr[j]# Shift elements to the right`checkpoint` j -=1 arr[j+1]= key # Insert the key in the correct positionaction Init:
# Sorting the array [12, 11, 13, 5, 6] using insertionSort# arr = [5, 3, 2, 4, 1]arr=[12, 11, 13, 5, 6]# arr = ["a12", "a11", "a13", "a5", "a6", "a1"]cur= len(arr)ins= -1
key= arr[0]
Run the above code in the playground with Enable Whiteboard checked.
Click on the Explorer link in the console
Play around by clicking the buttons. It will only show the states, there are no
sequence diagrams for this example. (Sequence diagrams are only generated when there are roles)
While the states are shown, with cur and ins variable, it would be nicer
to show them as pointers to the position in the array. This information is not
available in the spec so far. So this should be added as an additional config.
Click on buttons to see the states change as the algorithm progresses.
Basic Usage
FizzBee is not a usual visualization tool, it is a design specification system.
You can model your design in an python-like language and use that to validate the design
to check for issues like concurrency, consistency, fault tolerance, then model performance
like error ratio, tail latency distribution and more.
As a design specification, FizzBee generates various visualizations to help you understand
the system behavior that can be shard with your team. This makes it easier to explain the design
for your team to review, saving significant amount of time.
In the document, we will do a quick overview of the language necessary to generate the visualizations
and skip the model checking parts.
Python datatypes
FizzBee uses a variant of Python syntax, and for the most part relies on Starlark for evaluating expressions.
So all the standard Python datatypes like int, float, str, list, dict etc are supported.
The top section is the frontmatter, where you can set various model checking options.
In this example, our spec just initializes the variables, and there are no action after that.
So effectively, this implies the system cannot progress after the Init, so it is considered a deadlock
For this example, we are just suppressing this error.
Run this example with the whiteboard enabled, then click on the Explorer link in the console.
Actions are the basic building blocks of the system. They can either represent steps triggered
by the user or the components that are external to the system being modelled.
Open the playground, and try the whiteboard. This time you will see, the elements list
that is initially empty. On the left, click on the Produce button,
then pick an element to add to the list.
you will see the elements getting updated. Once an element is added, you would see
two actions Produce and Consume available (as shown in the image below). Click on Consume to remove the element.
Gcluster_null.elementselementselements213
Try Produce multiple times to fill to capacity, then you will see Produce action is not enabled anymore.
This should explain how require and any keywords work
Array index
We saw how to display the datastructure. Many times, we would want to see
how the data access. Since the index information is not preserved, we need to
add a bit of extra configuration.
In the above example, we saw how each action is a step in the system. Let us try slightly
more complex example where we have a loop.
This is a simple example of summing the elements in the array.
As a trivial example, there is only one action and none of these have any states.
Since there are no states, the system does not explore what happens if receiver is not available or if the message is lost,
or the receiver processed it, but the response was lost and so on.
When you run it, and open the explorer, you will see the states of the caller and server.
Obviously,
Both the caller and server are in the init state.
When you click on the Send button, the caller changes to calling, and server changes to init state.
At the point, wo possible things can happen.
i. Happy case: Continue by clicking thread-0. The server changes to done state. You’ll also see a sequence diagram.
ii. Error case: Error case: Click on crash. This path implies, either the caller crashed before sending or server crashed before the server processed the request. So the caller will continue to think it is in calling state.
You can similarly try crash after the server processed the request, and see the server in done state and caller in calling state.
Finally, you can try crash after the caller received the response, and see the caller in done state and server in done state.
An example state where the caller is in calling state and server is in done state is shown below.
Gcluster_Caller#0Caller#0cluster_Server#0Server#0Caller#0.statestate = callingServer#0.statestate = donerr = role Caller#0r->Caller#0_placeholderss = role Server#0s->Server#0_placeholder
Now, go back to the first example with two-phase commit and try to understand the behavior.
Conclusion
FizzBee is a powerful tool to model and visualize the system behavior. In addition to checking for
correctness, it can also be used to generate visualizations that can be shared with the team to explain the design.
The best of all, unlike any other formal verification system,
FizzBee uses python’ish language making it easy to ramp up on day 1.
In other visualization tools, you will have to manually create the sequences. Most likely, you won’t
be able to create the sequences for all the important paths. But with FizzBee, you can explore all possible paths.
Also, by describing your system design in a precise language, it doubles as a system specification language
replacing significant portions of the design document.