Line 83: | Line 83: | ||
Finally, events can now be associated with various hovers. | Finally, events can now be associated with various hovers. | ||
For this you just need to add an attribute <tt>hovers</tt> which contains a list of JSON objects with | For this you just need to add an attribute <tt>hovers</tt> which contains a list of JSON objects with the following attributes: | ||
* <tt>id</tt>, this is the identifier of an object in the associated SVG file; this attribut is optional; if it is not present the id specified in the VisB event will be used. | * <tt>id</tt>, this is the identifier of an object in the associated SVG file; this attribut is optional; if it is not present the id specified in the VisB event will be used. | ||
* <tt>attr</tt> a valid SVG attribute | * <tt>attr</tt> a valid SVG attribute | ||
* <tt>enter</tt> a value which will be used when the mouse enters the area of the object | * <tt>enter</tt> a value which will be used when the mouse enters the area of the object | ||
* <tt>leave</tt> a value which will be used to restore the attribute when the mouse leaves the area | * <tt>leave</tt> 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. | |||
Here is an example VisB event with hovers: | Here is an example VisB event with hovers: | ||
<pre> | <pre> |
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.
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" ] } ] }
For VisB items every entry needs
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.
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"}] }
Some examples can be found here. More details and examples will be added later.
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" }