State Space Visualization: Difference between revisions

ProB provides several user-friendly visualization features to help the user to analyze and understand the behavior of his B specification. This feedback is very beneficial to the understanding of the B specification since human perception is good at identifying structural similarities and symmetries. For more information on this particular topic, the reader can refer to ^[1] and ^[2].

In this page we discuss the visualization of the state space of a specification. Visualizing individual states can be visualized using animation functions, Custom_Graph definitions or using VisB.

The visualization features of the state space are in the "Visualize" menu, and comprise the command (visualize) "Statespace" and all the commands of the sub-menu "Statespace Projections". It is important to understand that those commands operate on the state space computed by ProB at the current point during the animation. Each time the user animates the B specification, the state space computed by ProB can be expanded if the selected operations lead to states not already computed by ProB. As shown in the following figure, the command (visualize) "Statespace" displays a diagram corresponding to the state space currently explored by the animation in a separate window.

Graph Nodes

ProB displays the state space as a graph whose nodes correspond to states that are differentiated by their shapes and colors and arcs correspond to operations. The operations are all those that are displayed in the Enabled Operations pane except backtrack, which is only useful for animation. Four types of nodes are visualized in ProB:

• root The point before the B machine is initialized when it has no state;
• current The current state during the animation;
• normal The states that have been already computed during the animation;
• open The states that are reachable from the normal states by an enabled operation.

In addition to its type, a node can indicate that it corresponds to an invariant violation, which is displayed by a color filling as shown in the following figure

Finally, if you have specified a goal predicate (either using a DEFINITION GOAL == P or by using a command such as "Find state satisfying predicate...") then those predicates are coloured in orange. Many of the colours and shapes can be changed by adapting the corresponding preferences. A list of preferences is now shown automatically in ProB Tcl/Tk.

Statespace Projections

The sub-menu "Statespace Projections" contains several other commands that provide useful views on the state space.

• Transition Diagram for Custom Expression ...
• Signature-Merge Reduced Statespace...
• DFA Reduced Statespace
• Subgraph leading to Invariant Violation
• Subgraph for GOAL

Transition Diagram

The first command allows you to enter an expression (in B syntax). The command will then merge all states with the same value for that expression into an equivalence class node. In other words, the state space is projected onto the values of the expression. The generated graph contains only transitions which change the value of that expression (unless the DOT_LOOPS preference is set to true). The command allows one to project the state space onto a single variable, a subset of variables (by using a tuple (v1,v2,...,vk) as expression). You can increase the projection by using B operators such as card, ran, dom or any other B operator. A more detailed explanation is given in ^[2]. The command can also be called from probcli using these commands (in conjunction with other commands like --model-check):

probcli -dotexpr transition_diagram EXPR DOTFILE

The generated dot file can be viewed with a viewer like dotty or can be converted, e.g., to PDF using:

dot -Tpdf <DOTFILE >PDFFILE

Here is an example where a faulty lift model has been projected onto the expression

curfloor / 3

Signature and DFA Merge

The two next commands in the menu "View Visited States|View" provide a means to display a simplified version of the state space. A more detailed explanation is given in ^[1].

The command "Signature-Merge Reduced Statespace" displays a state space where nodes sharing the same output arcs are collapsed into one node. The command "Reducted Deterministic Automaton of Visited States" removes the non-determinacy of the state space graph. The command "Select Operations & Arguments for Reduction" is used to specify which operations and arguments are affected by the previous transformations.

Sub Graphs

The two last commands of the "Statespace Projections" sub-menu display subgraphs of the state space. The command "Subgraph for Invariant Violation" displays the subgraph of nodes which violate the invariant, while the command "Subgraph of nodes satisfying GOAL" displays the subgraph where goals (discussed in Temporal Model Checking) are satisfied.

As of December 2015, there is also a sub-menu "Statespace Fast Rendering", which enables one to visualize larger state spaces more effectively. Some sample visualizations can be found here.

Other Visualization Commands

The "Visualize" menu contains several other sub-menus, to visualize traces and individual states. The command "Shortest Trace to Current State" displays the shortest sequence of nodes in the state space starting from the root node and leading to the current node. The command "Current State" displays the current node and its successor nodes.

Preferences of the Visualization

Many aspects of the visualization can be configured in the "Graphical Viewer Preferences"... preference window of the "Preferences" menu. This includes changing the shapes and colors of the various nodes (using the notation of the dot tool, see Dot-Shapes and Dot-Colors). For selecting the colors, a color picker is available via the button Pick. The user can also select which labels to display on the nodes (value of variables) and arcs (operation arguments and return value of functions), and their font size.

The default graph viewer in ProB is dotty, which is from the Graphviz package. ProB enables the user to display the graph using a PostScript viewer by setting the preference Use PostScript Viewer in the Graphical Viewer Preferences to true.... The PostScript file is generated by the dot tool. The path to the PostScript viewer can be set in the "Path/Command" for PostScript Viewer preference. The "Pick" button can be used to select the path. WARNING: All paths to files and folders should use the / character to separate the folders and should be absolute.

Using a postscript viewer rather than dotty has several advantages and several drawbacks. Firstly, the assignment of node shapes and colors is more accurately realized by dot (and therefore PostScript). Dotty on the other hand is much easier to use when state spaces are large thanks to the birds-eye view. A PostScript viewer also has the advantage that the PostScript file may be used to capture visualizations for publication purposes.

At present, the distinction between using a PostScript viewer as opposed to dotty comes down to the difference in functionality between the !GraphViz utilities dot and dotty. The main differences with respect to visualization in ProB are are:

• For Postscript: Support for more visualization shapes (for example, the shape double-octagon appears as a box on dotty);
• Against PostScript: dot does not support the addition of shapes to arcs. With moderately large graphs, Dot may put nodes outside of the printable or viewable area. Examining large graphs in a PostScript viewer may be slow (it may be awkward to use pan and zoom). There is less support for information on arcs (for example, dotted lines).
• For Dotty: Graphs can be modified. Dotty includes a birds-eye viewer which is useful for examining large graphs.
• Against Dotty: Dotty may crash if the graph is too big or complex (and on Solaris and Linux if non-standard mouse buttons are used).

References