m (Update ProB2-UI link) |
(Clarify that VisB is included in newer versions of ProB2-UI) |
||
Line 1: | Line 1: | ||
VisB is a | '''VisB''' is a visualisation tool for [[ProB2-UI]], the new user interface of ProB based on JavaFX and the ProB2-Java-API. | ||
It is included in | It is included in ProB2-UI version 1.1.0 and later, which [[Download#ProB2-UI using Java FX|can be downloaded here]]. | ||
Users of ProB2-UI version 1.0.0 can [[#Installing the VisB plugin for older ProB2-UI versions|install VisB as a plugin]]. | |||
[[File:ProB2UI_VisB_View.png|center|550px]] | [[File:ProB2UI_VisB_View.png|center|550px]] | ||
ProB Tcl/Tk and probcli version 1.11.0 and later also support VisB visualisations: | |||
* with <tt>probcli File.mch ... -visb VISBJSONFILE HTMLFILE</tt> you can export the animator's history to a self-contained HTML file including a visualisation of the states in the history | * with <tt>probcli File.mch ... -visb VISBJSONFILE HTMLFILE</tt> 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) | * 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) | ||
Line 12: | Line 14: | ||
== Using VisB == | == Using VisB == | ||
To start VisB choose the "Open VisB" command in the Visualisation menu. | To start VisB in ProB2-UI, choose the "Open VisB" command in the Visualisation menu. | ||
You can now choose a JSON file which builds on top of a SVG graphics file. | You can now choose a JSON file which builds on top of a SVG graphics file. | ||
Line 260: | Line 262: | ||
== Installing VisB | == 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 VisB in | To install the VisB plugin in ProB2-UI 1.0.0 you need to: | ||
1. | # [https://www3.hhu.de/stups/downloads/prob2/plugins/VisB-1.0.0.jar Download the VisB plugin jar file]. | ||
# In the "Advanced" menu of ProB2-UI, choose "Plugin Menu". | |||
# Click on the "Add Plugin..." button. | |||
# Select the VisB jar file that you have downloaded. | |||
# Choose the "Open VisB" command in the Advanced menu to start VisB. |
VisB is a visualisation tool 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:
An article about VisB has been published in the ABZ'2020 proceedings.
To start VisB in ProB2-UI, choose the "Open VisB" command in the Visualisation 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" ] } ] }
The main VisB Json file should contain an svg attribute with a relative or absolute path to the SVG file to be shown. 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).
For VisB items every entry needs
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.
For VisB event every entry needs
Additionally VisB now recognises for both items and events:
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:
Finally, events can now be associated with various hovers. For this you just need to add an attribute hovers which contains a list of JSON objects with the following attributes:
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"}] }
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" },
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"] }
In the nightly version of ProB Tcl/Tk it is already possible to include definitions in the VisB 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 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)))" }]
They are particularly useful for Event-B models (aus you can use REAL numbers and also have access to external functions such as LibraryStrings or LibraySVG). But they are not yet available in ProB2-UI.
Some examples can be found here. More details and examples will be added later.
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 also set the class using VisB items. This 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).
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" }
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: