VisB: Difference between revisions

VisB is a visualisation feature of ProB based on SVG graphics and HTML.

Initially VisB was developed for ProB2-UI, the new user interface of ProB based on JavaFX and the ProB2-Java-API. It is included in ProB2-UI version 1.1.0 and later, which can be downloaded here. Users of ProB2-UI version 1.0.0 can install VisB as a plugin.

ProB Tcl/Tk and probcli version 1.11.0 and later also support VisB visualisations:

• with probcli File.mch ... -visb VISBJSONFILE HTMLFILE you can export the animator's history to a self-contained HTML file including a visualisation of the states in the history
• in ProB Tcl/Tk you can visualise the current state or the history using a VisB visualisation file (it is shown in an external browser) by right clicking in the "State Properties" or the "History" pane.

Hovers work in both cases, but unlike in ProB2-UI, you cannot click to perform events.

An article about VisB has been published in the ABZ'2020 proceedings.

Using VisB

To start VisB in ProB2-UI, choose the "Open VisB" command in the Visualisation menu, or right-click in the "State Properties" pane of ProB Tcl/Tk and select "View Current State in VisB".

You can now choose a JSON file which builds on top of a SVG graphics file. The JSON file contains a reference to a SVG file, along with entries to modify attributes based on the current state of a B model and entries which specify how VisB should react to clicks on the SVG. The SVG file should contain object ids which are referenced in the JSON file.

Here is a sample file:

{
  "svg":"Train2.svg",
  "items":[
    {
      "id":"Train1_rect",
      "attr":"visibility",
      "value":"IF 1:TRAIN THEN \"visible\" ELSE \"hidden\" END"
    },
    {
      "id":"Train1_rect",
      "attr":"fill",
      "value":"IF train_speed(1)>0 THEN \"blue\" ELSE \"orange\" END"
    },
    {
      "id":"Train1_rect",
      "attr":"x",
      "value":"train_back_loc(1)*10+20"
    },
    {
      "id":"Train1_rect",
      "attr":"width",
      "value":"train_length(1)*10"
    }
    ],
  "events":[
    {
      "id":"Train1_rect",
      "event":"Train_Move1",
      "predicates":[
        "1=1"
      ]
    }
    ]
}

VisB Attributes

At the top-level a VisB JSON file contains these attributes:

• svg
• model-name
• include
• svg_objects
• definitions
• items
• events

Below we explain them in more detail.

SVG file and inclusion

The main VisB Json file should contain an svg attribute with a relative or absolute path to the SVG file to be shown.

The model-name attribute is optional; if set ProB will emit a warning if the B model's name does not match the value of this attribute.

One can also include subsidiary VisB Json files using the include attribute with again a relative or absolut path to another Json file:

{
  "svg":"my_svg_file.svg",
  "include":"subsidiary_visb_file.json",
  "items":[
...
}

The svg attribute in subsidiary files will be ignored. You can override the VisB items in the included file (i.e., a VisB item for an id and attribute in the top-level file will override items for the same id and attribute in the included files).

Items and Events

For VisB items every entry needs

• id, this is the identifier of an object in the associated SVG file
• attr a valid SVG attribute
• value a B formula which will be evaluated in the current state of a model and yields a new value for the above attribute.

Note that the formula can make use of the REAL datatype and also use many of the external functions e.g. from LibraryStrings or LibraySVG. Here is an example VisB Item:

  "items":[
    {
      "id": "train1_rect",
      "attr": "x",
      "value":"100.0 + train_left(train1)"
    } ]

As of version 1.12.2, ProB allows you to use a single attribute whose name is the SVG attribute being set, rather than two attributes (attr, value). With this you can set multiple SVG attributes in one VisB item. For example, you can now write:

  "items":[
    {
      "id": "train1_rect",
      "x":"100.0 + train_left(train1)",
      "y":"20.0 + train_bottom(train1)"
    } ]

For VisB events every entry needs

• id, this is the identifier of an object in the associated SVG file
• event a valid B operation or event of the loaded formal model
• predicates an optional list of B predicates, which can be used to set parameters of the B operation that is executed upon a click

Additionally VisB now recognises for both items and events:

• ignore, if this attribute is present the item will be ignored
• repeat, if this attribute is present the item will be replicated (see below). This construct requires a list of strings.
• for, if this attribute is present the item will be replicated (see below). The for construct requires from and to with integer values as sub arguments. As of version 1.11.1 you can also use constant B integer expressions accessing just the sets.
• optional, if this boolean attribute is true an event will be ignored if the event name is not a valid top-level event/operation in the model. An item will be ignored if the identifiers in the formula do not exists (i.e., errors during type checking will be ignored)
• override, if this boolean attribute is true no warnings will be generated if another VisB item for the same attribute and id is overriden (as of version 1.11.1)

Other attributes will be ignored. E.g, one can use a comment attribute to add comments to the VisB items.

When executing an event, VisB now performs the following replacements within the predicates of the event:

• %shiftKey is replaced by TRUE if the shift key was pressed during the click, FALSE otherwise
• %metaKey is replaced by TRUE if the shift key was pressed during the click, FALSE otherwise
• %pageX is replaced by the x coordinate of the click relative to the top-left of the entire VisB SVG
• %pageY is replaced by the y coordinate of the click relative to the top-left of the entire VisB SVG

Finally, VisB events can be associated with mouse hover actions. For this you just need to add an attribute hovers which contains a list of JSON objects with the following attributes:

• id, this is the identifier of an object in the associated SVG file; this attribute is optional; if it is not present the id specified in the VisB event will be used.
• attr a valid SVG attribute
• enter a value which will be used when the mouse enters the area of the object
• leave a value which will be used to restore the attribute when the mouse leaves the area

Note that the enter and leave values have to be static at the moment; in future we plan to allow B formulas here and also apply the repetition/replacement mechanism specified above. If you just wish to attach a hover to an SVG object (and no B operation/event) you can set the event field of the VisB event to the empty string ("event":""). You should not use attributes for the hover which are set by VisB items.

Here is an example VisB event with hovers:

   {
      "id": "button",
      "event": "toggle_button",
      "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
                 { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
    }

A VisB event can now also contain an list of items with the attributes id, attr, enabled and disabled. When the associated event is enabled, the attribute of the SVG object with the given id is set to the value provided in the enabled attribute, otherwise the disabled attribute value is used. As above the item id is optional and defaults to the id of the VisB event. Here is an example VisB event with hovers and an items list:

    {
      "id": "button",
      "event": "press_button",
      "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"}],
      "items": [{"attr":"fill", "disabled":"\"green\"", "enabled":"\"red\""}]
    },

Replication / Loops

You can use the repeat and for attributes to replicate a VisB item or event. Replication consists in duplicating the item or event, and replacing %0 within the identifier and value attributes of the time with the repeated string or integer.

For example, the repeat instruction below will result in the creation of three VisB items, one for id txt_ttd1, for txt_ttd2, and one for txt_ttd3. The value formula for txt_ttd1 is "IF 1: dom(TTD) THEN visb_ttd_back(%0) ELSE -1000 END".

    {
     "repeat": ["1","2","3"],
      "id":"txt_ttd%0",
      "attr":"x",
      "value":"IF %0: dom(TTD) THEN visb_ttd_back(%0) ELSE -1000 END"
    },

A for loop can be used instead for the above example as follows:

    {
     "for": {"from":1, "to":3},
      "id":"txt_ttd%0",
      "attr":"x",
      "value":"IF %0: dom(TTD) THEN visb_ttd_back(%0) ELSE -1000 END"
    },

The for loop also allows an optional step attribute.

It is possible to apply both repeat and for attributes at the same time, as this example shows. (The exact details of multiple iterations for a VisB item might change in future.)

  {
     "repeat": [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20],
     "for": {"from":1, "to":20},
      "id": "tile%1x%0",
      "event": "TryQueen",
      "hovers": [{ "attr":"opacity", "enter":"0.5", "leave":"1"}],
      "predicates" : ["i=%1","j=%0"] 
    }

As of version 1.11.0 you can also use nested for loops. As of version 1.11.1 of ProB you can also use B expressions for the from, to and step attributes of a for loop. However, these expressions must be evaluable without having access to any constants or variables. Indeed, the for and repeat loops are processed once when loading a VisB file, independently of any given state. So, you can only access identifiers of SETS section of a B machine. It may still be useful, e.g., to iterate over an enumerated or deferred set (TRAINS below):

  {
     "for": {"from":1, "to":"card(TRAINS)"},
...
    }

The INT_TO_ENUM external function available as of ProB 1.11.1 can be useful in expressions here to convert the iteration variable back to an enumerated or deferred set element. For example, INT_TO_ENUM(TRAINS,1) refers to the first element of the set TRAINS.

VisB Definitions (in JSON file)

As of ProB Tcl/Tk 1.11.0 it is possible to include local definitions in the VisB JSON file. Each definition has a name and a value formula. Definitions are evaluated in order of appearance (a later definition can thus refer to an ealier one) and are evaluated in a state before evaluating VisB items.

  "definitions":[
    { "name":"xscale",
      "value" : "(100.0 / real(NrOfTrackElements))"
    },
    { "name":"visb_train_rear",
      "value" : "%x.(x:dom(train_rear)|xscale * real(train_rear(x)))"
    }]

The VisB definitions are particularly useful for Event-B models (as you can use REAL numbers and also have access to external functions such as LibraryStrings or LibraySVG). But they are not yet available for events in ProB2-UI.

VisB Additional SVG Objects

As of version 1.12.0 of ProB Tcl/Tk you can add new SVG objects to your SVG file. You can use for and repeat loops (see above) to create an arbitrary number of objects. This is useful for making flexible visualisations which work with an arbitrary number of objects. The same rules and limitations for for/repeat loops apply as for items above.

Every entry in the svg_objects list

• an svg_class attribute, which can be, e.g., line, circle, rect, ...
• an object id attribute
• an optional comment attribute
• any other attribute will be used to create the SVG object and should be valid for the specified svg_class

Here is an example (taken from here) where NOBJS is a DEFINITION inside a B machine:

  "svg_objects":[
    {
      "for":{"from":1,"to":"NOBJS"}, 
      "svg_class":"circle",
      "id":"body%0",
      "cx":"45",
      "cy":"15",
      "r":"10",
      "stroke":"black",
      "stroke-width":"0.5",
      "fill":"green"
    } ]

Here is another example where TRAINS is a deferred or enumerated set of the B model being visualised:

  "svg_objects":[
    {
      "for":{"from":1,"to":"card(TRAINS)"}, 
      "svg_class":"rect",
      "id":"fresh_train_rect%0",
      "x":"0",
      "y":"0",
      "height":"10",
      "width":"20",
      "comment":"train current position rectangle"
    }
  ]

VisB DEFINITIONS

As of version 1.12 you can also provide many of the VisB annotations via B DEFINITIONS. This can be done in addition to a VisB JSON file or completely replacing the JSON file.

By adding this definition to your B machine you specify that you wish to use an empty SVG file as base:

  VISB_JSON_FILE == "";

With a VISB_SVG_BOX definition you can set the size of the generated empty SVG file:

  VISB_SVG_BOX == rec(height:floor(vscale)*25+20, width:1800);

Note: you can also provide an optional viewBox attribute as a B string.

Via VISB_SVG_CONTENTS definitions you can add new textual content to the base SVG file:

   VISB_SVG_CONTENTS == '''
   <defs>
...
```;

With definitions starting with with VISB_SVG_OBJECTS you can add new SVG objects:

  VISB_SVG_OBJECTS1 == rec(`svg_class`:"rect",`id`:"i1",x:20,y:20,height:20,width:20,fill:"blue");
  VISB_SVG_OBJECTS2 == rec(`svg_class`:"circle",`id`:"i2",cx:30,cy:30,r:20,fill:"red");

Each definition can either add a single record or add a set of records in one go. The definition should only depend on base sets or constants of the model (see, however, notes for ProB 1.13.0 or later below). In addition the constants used in the above definitions should only have one possible value. For example, suppose that the constant P has 5 elements then this will create 5 SVG lines. Observe that we use the new Event-B-style set comprehension for convenience and that tuples can be used for the id field..

  VISB_SVG_OBJECTS3 == {i•i:P|rec(`svg_class`:"line",`id`:("line",i),x1:0,y1:i,x2:i,y2:i)};

Similarly, you can use VISB_SVG_UPDATES definitions to specify attributes that depend on the value of constants and variables of the animated B model:

  VISB_SVG_UPDATES1== rec(`id`:"i2",fill: IF x>0 THEN "red" ELSE "green" END);

Hovers can be defined using VISB_SVG_HOVER definitions (only for objects that have been created with VISB_SVG_OBJECTS) and click events can be defined using VISB_SVG_EVENTS definitions with attributes id, event and optionally predicate. Here is a minimal example that just uses the VisB DEFINITIONS without any external JSON or SVG file:

MACHINE button_def
// An example that uses VisB DEFINITIONS instead of a JSON and SVG file
DEFINITIONS 
  VISB_JSON_FILE == "";
  VISB_SVG_BOX == rec(height:200, width:240);
  VISB_SVG_OBJECTS == rec(`id`:"button", svg_class:"circle",
     cx:"100",cy:"100", r:"80", stroke:"black", `stroke-width`:"3");
  VISB_SVG_UPDATES == rec(`id`:"button",
     fill: IF button=TRUE THEN "green" ELSE "red" END);
  VISB_SVG_HOVERS == rec(`id`:"button",
     stroke:"gray", `stroke-width`:"5");
  VISB_SVG_EVENTS == rec(`id`:"button", event:"toggle_button", predicate:"btrue")
VARIABLES button
INVARIANT button:BOOL
INITIALISATION button := FALSE
OPERATIONS
  toggle_button = BEGIN
    button:= bool(button=FALSE)
  END
END

As of version 1.13.0 of ProB you can also use dynamic expressions in object definitions; the above definitions can thus be written more compactly:

  VISB_SVG_OBJECTS == rec(`id`:"button", svg_class:"circle",
     cx:"100",cy:"100", r:"80", stroke:"black", `stroke-width`:"3",
     fill: IF button=TRUE THEN "green" ELSE "red" END,
    event:"toggle_button");
  VISB_SVG_HOVERS == rec(`id`:"button",
     stroke:"gray", `stroke-width`:"5");

In 1.13.0 you can also use a "children" attribute to specify groups. The children attribute should evaluate to a set of strings pointing to ids of SVG objects. The following example shows this for for defining the children of "mygroup". Also observe the use of the new template string syntax for the transform attribute.

    VISB_SVG_FILE == "";
    VISB_SVG_BOX == rec(height:400, width:450);
    VISB_SVG_OBJECTS1 == {i•i:0..9|rec(`id`:("r",i), svg_class:"rect",
                                   fill:IF i=x THEN "red" ELSE "green" END,
                                   x:10+10*i, y:100, height:20, width:4)};
    VISB_SVG_OBJECTS2 == rec(`id`:"mygroup", svg_class:"g",
                             children: {i•i:0..9|("r",i)},
                             transform:```rotate(${x*40},50,100)```
                            )

Examples

Some examples can be found here. We have a small Jupyter notebook manual on the DEFINITION features of VisB. More details and examples will be added later.

Caveats

• Beware that you need to escape quotation marks and slashes in the JSON file for fields containing B expressions. Also, you cannot use newline.
• Hovers are currently evaluated once statically and cannot make use of B expressions. To make hover information dependent on the state, use the visibility attribute to make hidden SVG objects (which can be adapted depending on the state using VisB items) visible. The train VisB example illustrates this idea.

Tips and Tricks

It is sometimes useful to use simple coordinates for your VisB items and B expressions, e.g. x coordinates of 0..100. You can quite often do this and use the SVG transform attribute to scale and move the SVG object to the right place. The simple train VisB example shows how to do this. In essence your SVG file can contain this:

  <polygon id = "ttd_polyline"
       points="0,0 100,0"
       stroke="gray" fill="none"
       transform="translate(10,22.5)" />

and the VisB JSON file contains this, making use of LibrarySVG.def (automatically available) external function svg_axis:

    {
      "id":"ttd_polyline",
      "attr":"points",
      "value":"svg_axis({0} \\/ ran(%tt.(tt:TTDS|1+max(TTD_TrackElements(tt)))),100.0/real(TrackElementNumber+1),100.0,2.0)",
      "comment":"show ticks for TTD Limits"
    },

Observe that we had to escape the slash of the union operator. Also observe, that we are able to use floating numbers in the new version of ProB, which is very useful for VisB visualisations.

It can be useful to use style and class to make it easier to change your color scheme or other styling attributes within your visualisation consistently. Again, the simple train VisB example shows how to do this. E.g., your SVG file could contain towards the top this definition:

    <style id="style_ttd_ts_mp">
        .ttd {
            stroke : none;
            stroke-width: 0.2;
            opacity: 0.7
        }
        .red-occupied-ttd {
            fill : red
        }
   </style>

Later you can then use it to style your objects:

  <polygon id = "occupied_ttd_polygon"
       points="0,0 0,2 10,2 10,0 70,0 70,1 90,1 90,0"
       class = "ttd red-occupied-ttd"
       transform="translate(10,23)" />

You can then modify the class using VisB items. Classes can also be useful for hovers, by simply exchanging one style for another when the mouse is over an objects (again, see the train example). Recent versions of ProB also support adding and removing a class, which is useful for hovers when the class is modified by VisB items:

   {
      "id":"train_polygon_tr1",
      "event":"TrainMoveForward",
      "hovers": [{ "attr":"class", "enter":"+train-hover", "leave":"-train-hover"}]
 }

Debugging and HTML Export

In classical B models you can store your default VisB visualisation in the DEFINITIONS section:

  DEFINITIONS
    VISB_JSON_FILE == "TwoTrains.json"

For debugging it can be useful to use VisB within ProB Tcl/Tk: if you choose to visualise the current state with VisB, ProB will generate a stand-alone HTML file which is opened in a browser. In the browser you can open the (Javascript) developer console and you will be alerted to warnings and errors (which unfortunately, are currently not shown in ProB2-UI). Upon changing the state in the animator, the HTML file will be regenerated and the VisB file re-loaded if necessary. The HTML export also displays hovers, but cannot react to clicks. The HTML export is also available in ProB2-UI (in the export menu in the top-right corner).

ProB can also export the entire animation history to a standalone HTML file that can be passed to other persons (without requiring access to the B model or to ProB). In ProB Tcl/Tk you can right-click on the history pane and choose "View History in VisB". In probcli you can use the command -visb JSONFILE HTMLFILE to export the history. In ProB2-UI you can click on the export icon in the upper right hand corner:

The ProB2-UI table visualisation view (Visualisation menu) also contains tables to help debug VisB items and events:

This view is also available in ProB Tcl/Tk in the Visualize menu (States submenu). ProB2-UI also has another inspection view that can be obtained by clicking on the "i" (info) icon in the the VisB toolbar.

Using the VisB exported HTML file

You should be able to open the exported HTML using a regular browser. Within the web page (see the image below) you can then do the following:

• single step through the trace by clicking the "Forward" and "Backward" buttons, or clicking on individual steps of the trace
• execute the entire trace nd see changes to the visualisation by clicking one of the "Run Trace" buttons
• you can inspect the value of the sets, constants and variables at every step by expanding the corresponding tabs

Some meta information can be found at the bottom of the trace.

Citing VisB

This is the Bibtex entry for an article about VisB in the ABZ'2020 proceedings:

@inproceedings{WerthLeuschel:abz2020,
  author    = {Michelle Werth and Michael Leuschel},
  title     = {{VisB}: A Lightweight Tool to Visualize Formal Models with {SVG} Graphics},
  booktitle = {Proceedings ABZ 2020},
  editor="Raschke, Alexander and M{\'e}ry, Dominique and Houdek, Frank",
  year      = {2020},
  series = {LNCS 12071},
  pages = "260--265",
  isbn="978-3-030-48077-6"
}

Installing the VisB plugin for older ProB2-UI versions

Note: The following instructions are for ProB2-UI version 1.0.0 only. On current versions of ProB2-UI (1.1.0 and later), VisB is included by default and does not need to be installed separately.

To install the VisB plugin in ProB2-UI 1.0.0 you need to:

1. Download the VisB plugin jar file.
2. In the "Advanced" menu of ProB2-UI, choose "Plugin Menu".
3. Click on the "Add Plugin..." button.
4. Select the VisB jar file that you have downloaded.
5. Choose the "Open VisB" command in the Advanced menu to start VisB.