VisB

VisB is a plugin for ProB2-UI, the new user interface of ProB based on JavaFX and the ProB2-Java-API . It is included in the latest Snapshot builds of ProB2-UI, but can be downloaded at https://www3.hhu.de/stups/downloads/prob2/plugins/ for older version of ProB2-UI.

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

Installing VisB Plugin

To install VisB in the JavaFX-based ProB2-UI you need to:

1. Choose "Plugin Menu" in the Advanced menu 2. Click on the "Add Plugin..." button. 3. Select the VisB JAR file you have downloaded from https://www3.hhu.de/stups/downloads/prob2/plugins/ 4. Choose the "Open VisB" command in the Advanced menu

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

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.

For VisB event 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)
for, if this attribute is present the item will be replicated (see below)

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

VisB ExamplesSome examples can be found here. More details and examples will be added later.Citing VisBThis 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" }