Whiteboard Visualizations

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.

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.

Before we go over the tutorial, let’s see a complete working example.

1. Open the Two Phase Commit example in the play ground

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86

NUM_PARTICIPANTS = 2

role 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()

      if vote == '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)

2. Enable Enable Whiteboard checkbox, and Run.
3. 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.

4. Click on the Explorer link in the console.
5. You would see the Init state of the system

5. 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.

6. Play around with the explorer to see what happens when a participant aborted.

7. You can explorer most possible sequences and states.

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 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`.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38

---
deadlock_detection: false
options:
       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 return

	for i in range(1, len(arr)): # Iterate over the array starting from the second element
        cur = i
        ins = i-1
        
		key = arr[i] # Store the current element as the key to be inserted in the right position
		
        j = i-1  
        `checkpoint`  
    	while j >= 0 and key < arr[j]: # Move elements greater than key one position ahead
                ins = j
    			arr[j+1] = arr[j] # Shift elements to the right
                
                `checkpoint`  
    			j -= 1
                
		arr[j+1] = key # Insert the key in the correct position

action 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]

1. Run the above code in the playground with Enable Whiteboard checked.
2. Click on the Explorer link in the console
3. 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)
4. 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.

5. On the left-bottom, you will see the Config text area. Insert the following code.

   variables:
     cur:
       index_of: arr
     ins:
       index_of: arr
   

6. Click on buttons to see the states change as the algorithm progresses.

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.

For more details on the language, refer to the FizzBee Language Reference.

In the document, we will do a quick overview of the language necessary to generate the visualizations and skip the model checking parts.

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.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11

---
deadlock_detection: false
---

action Init:
    elements = [4, 2, 1, 5, 3]
    cursor = 3
    matrix = [[1, 2, 3], [4, 5, 6], [7, 8, 9]]
    obj = {"store_id": 1001, "city": "San Francisco", "sqft": 12000.5}
    ordered = [ ("store_id", 1001), ("city", "San Francisco"), ("sqft", 12000.5)]
    obj_array = [{"name": "Alice", "color": "blue", "score": 10}, {"name": "Bob", "color": "green", "score": 9.5, "lang": ["English", "Spanish"]}]

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.

You should see something like,

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.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11

action Init:
    elements = []

action Produce:
    require len(elements) < 4
    x = any range(4)
    elements.append(x)

action Consume:
    require len(elements) > 0
    elements.pop(0)

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.

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

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.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16

action Init:
    elements = [1, 2, 3, 4, 5]
    cursor = -1
    value = None

atomic action MoveCursor: 
    if cursor > len(elements):
        cursor = -1
        value = None
    elif cursor < len(elements) - 1:
        cursor += 1
        value = elements[cursor]
    else:
        cursor += 1
        value = None
        

I will show the block diagram like this.

Now, to specify the cursor variable points to the index of the elements array,

On the left bottom text area, set

variables:
  cursor:
    index_of: elements

Now, click the MoveCursor buttons. You will see a diagram like this.

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.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15

action Init:
    elements = [1, 2, 3, 4, 5]
    cursor = -1
    sum = 0

atomic action Sum:
    require sum == 0
    for i in range(0, len(elements)):
        cursor = i
        sum += elements[i]

atomic action Restart:
    require sum != 0
    cursor = -1
    sum = 0

One action Sum sums the results, and the next action Restart resets the sum and cursor.

If you run this, you will see the sum being calculated. But you will not see the intermediate steps.

The states graph will show,

To see the intermediate steps, we can add a checkpoint in the loop.

*** 7,12 ****
--- 7,13 ----
  atomic action Sum:
      require sum == 0
      for i in range(0, len(elements)):
+         `checkpoint` 
          cursor = i
          sum += elements[i]

Run and open the states graph, you will see a lot more intermediate steps.

Then, open the explorer. Similar to previous example, set the cursor.

variables:
  cursor:
    index_of: elements

Now, click the Sum button and play.

To role more about roles, see Roles

Let us take a simple message passing example.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12

role Sender:
    action Process:
        receiver.Greet("Alice")
        pass

role Receiver:
    func Greet(name):
        return "Hello " + name

action Init:
    sender = Sender()
    receiver = Receiver()

Once you run with the whiteboard enabled, open the explorer, and click Process button, you will see the sequence diagram.

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.

Example: State updates with message passing

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

---
deadlock_detection: false
---
role Caller:
  action Init:
    self.state = 'init'

  action Send:
    require self.state == 'init'

    self.state = 'calling'
    res = s.Process()
    self.state = 'done'

role Server:
  action Init:
    self.state = 'init'

  func Process():
    self.state = 'done'

action Init:
  r = Caller()
  s = Server()

When you run it, and open the explorer, you will see the states of the caller and server. Obviously,

1. Both the caller and server are in the init state.
2. When you click on the Send button, the caller changes to calling, and server changes to init state.
3. 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.
4. You can similarly try crash after the server processed the request, and see the server in done state and caller in calling state.
5. 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.

Now, go back to the first example with two-phase commit and try to understand the behavior.

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.