VisB: Difference between revisions

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

@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"
}