"Note: you can also provide an optional <tt>viewBox</tt> attribute as a B string.\n",
"\n",
"### VISB_SVG_OBJECTS\n",
"\n",
"You can populate the empty SVG file with your own new objects using DEFINITIONS that start with <pre>VISB_SVG_OBJECTS</pre>.\n",
"Here is an example where we create one red circle:"
]
},
{
"cell_type":"code",
"execution_count":12,
"id":"22657ef0",
"execution_count":1,
"id":"629b2052",
"metadata":{},
"outputs":[
{
...
...
@@ -60,7 +62,7 @@
"Loaded machine: test1"
]
},
"execution_count":12,
"execution_count":1,
"metadata":{},
"output_type":"execute_result"
}
...
...
@@ -79,8 +81,8 @@
},
{
"cell_type":"code",
"execution_count":13,
"id":"9cf27405",
"execution_count":2,
"id":"ed27217b",
"metadata":{},
"outputs":[
{
...
...
@@ -89,7 +91,7 @@
"Executed operation: INITIALISATION()"
]
},
"execution_count":13,
"execution_count":2,
"metadata":{},
"output_type":"execute_result"
}
...
...
@@ -100,8 +102,8 @@
},
{
"cell_type":"code",
"execution_count":14,
"id":"5fd0cbbe",
"execution_count":3,
"id":"9e2e4225",
"metadata":{},
"outputs":[
{
...
...
@@ -283,7 +285,7 @@
"<VisB visualization>"
]
},
"execution_count":14,
"execution_count":3,
"metadata":{},
"output_type":"execute_result"
}
...
...
@@ -294,7 +296,7 @@
},
{
"cell_type":"markdown",
"id":"41725617",
"id":"b8d00549",
"metadata":{},
"source":[
"A VISB_SVG_OBJECT definition should either define a record or a set of records. The fields of the record specify the kind of object created and its initial attributes:\n",
"To dynamically update the SVG objects based on a B model's state you can specify <tt>VISB_SVG_UPDATES</tt> DEFINITIONS. They have the same form as <tt>VISB_SVG_OBJECTS</tt> DEFINITIONS, except you should not specify the <tt>svg_class</tt> attribute. In addition, the attribute values can depend on B variables.\n",
"With <tt>VISB_SVG_CONTENTS</tt> DEFINITIONS you can add additional static content to your SVG file. This is useful for CSS styles or arrow markers, for example.\n",
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 [[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]]
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
* 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 [https://rdcu.be/b4rqh published in the ABZ'2020 proceedings].
%% Cell type:markdown id:6942b823 tags:
%% Cell type:markdown id:53b80314 tags:
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:
<pre>
VISB_JSON_FILE == "";
</pre>
### VISB_SVG_BOX
With a VISB_SVG_BOX definition you can set the size of the generated empty SVG file:
<pre>
VISB_SVG_BOX == rec(height:formula, width:1800);
</pre>
Note: you can also provide an optional <tt>viewBox</tt> attribute as a B string.
### VISB_SVG_OBJECTS
You can populate the empty SVG file with your own new objects using DEFINITIONS that start with <pre>VISB_SVG_OBJECTS</pre>.
Here is an example where we create one red circle:
A VISB_SVG_OBJECT definition should either define a record or a set of records. The fields of the record specify the kind of object created and its initial attributes:
* usually all created object should have an id (so that you can later modify the attributes)
* you have to provide an <tt>svg_class</tt> attribute: circle, ellipse, line, path, polygon, polyline, rect, text
* you then can (and probably) should provide necessary attributes and initial values for your object
Note: <tt>id</tt> is a keyword in B and hence you have to use backquotes around it. Similarly, B does not allow identifiers with hyphens, hence you need surround such attributes (like <tt>stroke-width</tt>) with backquotes as well.
To dynamically update the SVG objects based on a B model's state you can specify <tt>VISB_SVG_UPDATES</tt> DEFINITIONS. They have the same form as <tt>VISB_SVG_OBJECTS</tt> DEFINITIONS, except you should not specify the <tt>svg_class</tt> attribute. In addition, the attribute values can depend on B variables.
Here is a small example:
%% Cell type:code id:7d8491f0 tags:
``` prob
::load
MACHINE test3
VARIABLES x
INVARIANT x:1..N
INITIALISATION x:=1
OPERATIONS inc = BEGIN x:= (x mod N)+1 END
DEFINITIONS
N == 5; WID==400.0;
VISB_JSON_FILE == "";
VISB_SVG_BOX == rec(height:100, width:WID+30.0);
VISB_SVG_OBJECTS == UNION(i).(i:1..N|
{rec(`id`:("circ",i), svg_class:"circle",
cx:real(i)*WID/real(N),cy:50, r:(30-i),
stroke:"black")});
VISB_SVG_UPDATES == UNION(i).(i:1..N|
{rec(`id`:("circ",i),
fill: IF i=x THEN "red" ELSE "gray" END,
`stroke-width`:IF i=x THEN 2.0 ELSE 0.5 END)});
END
```
%% Output
Loaded machine: test3
%% Cell type:code id:ea98b025 tags:
``` prob
:init
```
%% Output
Executed operation: INITIALISATION()
%% Cell type:code id:bb265467 tags:
``` prob
:show
```
%% Output
<VisB visualization>
%% Cell type:code id:d8d09a69 tags:
``` prob
:exec inc
```
%% Output
Executed operation: inc()
%% Cell type:code id:61d5ca71 tags:
``` prob
:show
```
%% Output
<VisB visualization>
%% Cell type:code id:2993ed34 tags:
``` prob
:table VISB_SVG_UPDATES
```
%% Output
|fill|id|stroke-width|
|---|---|---|
|"gray"|("circ"↦1)|0.5|
|"gray"|("circ"↦3)|0.5|
|"gray"|("circ"↦4)|0.5|
|"gray"|("circ"↦5)|0.5|
|"red"|("circ"↦2)|2.0|
fill id stroke-width
"gray" ("circ"|->1) 0.5
"gray" ("circ"|->3) 0.5
"gray" ("circ"|->4) 0.5
"gray" ("circ"|->5) 0.5
"red" ("circ"|->2) 2.0
%% Cell type:markdown id:7818407b tags:
### VISB_SVG_CONTENTS
With <tt>VISB_SVG_CONTENTS</tt> DEFINITIONS you can add additional static content to your SVG file. This is useful for CSS styles or arrow markers, for example.
Here is an example:
%% Cell type:code id:5bdcf602 tags:
``` prob
::load
MACHINE test4
VARIABLES x
INVARIANT x:1..N
INITIALISATION x:=1
OPERATIONS inc = BEGIN x:= (x mod N)+1 END
DEFINITIONS
N == 5; WID==400.0;
VISB_JSON_FILE == "";
VISB_SVG_BOX == rec(height:100, width:WID+30.0);
VISB_SVG_OBJECTS == UNION(i).(i:1..N|
{rec(`id`:("circ",i), svg_class:"circle",
cx:real(i)*WID/real(N),cy:50, r:(30-i))});
VISB_SVG_UPDATES == UNION(i).(i:1..N|
{rec(`id`:("circ",i),
class: IF i=x THEN "selected" ELSE "normal" END)});
Michael Leuschel <leuschel@uni-duesseldorf.de>