From c0079c758aba6a7d1d8eb4bc03798a5a4856c6de Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Thu, 13 Jul 2023 20:40:17 +0200
Subject: [PATCH] update VisB manual
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
notebooks/manual/VisB_Features.ipynb | 982 ++++++++++++++++++++++++++-
1 file changed, 955 insertions(+), 27 deletions(-)
diff --git a/notebooks/manual/VisB_Features.ipynb b/notebooks/manual/VisB_Features.ipynb
index 68f0a5a..3e61b72 100644
--- a/notebooks/manual/VisB_Features.ipynb
+++ b/notebooks/manual/VisB_Features.ipynb
@@ -2,7 +2,7 @@
"cells": [
{
"cell_type": "markdown",
- "id": "5b53d563",
+ "id": "5850e2ad",
"metadata": {},
"source": [
"# VisB\n",
@@ -10,9 +10,7 @@
"\n",
"Initially VisB was developed for [[ProB2-UI]], the new user interface of ProB based on JavaFX and the ProB2-Java-API.\n",
"It is included in ProB2-UI version 1.1.0 and later, which [[Download#ProB2-UI using Java FX|can be downloaded here]].\n",
- "Users of ProB2-UI version 1.0.0 can [[#Installing the VisB plugin for older ProB2-UI versions|install VisB as a plugin]].\n",
"\n",
- "[[File:ProB2UI_VisB_View.png|center|550px]]\n",
"\n",
"ProB Tcl/Tk and probcli version 1.11.0 and later also support VisB visualisations:\n",
"\n",
@@ -25,7 +23,7 @@
},
{
"cell_type": "markdown",
- "id": "6942b823",
+ "id": "53b80314",
"metadata": {},
"source": [
"As of version 1.12 you can also provide many of the VisB annotations via B DEFINITIONS.\n",
@@ -37,6 +35,8 @@
" VISB_JSON_FILE == \"\";\n",
"</pre>\n",
"\n",
+ "### VISB_SVG_BOX\n",
+ "\n",
"With a VISB_SVG_BOX definition you can set the size of the generated empty SVG file:\n",
"<pre>\n",
" VISB_SVG_BOX == rec(height:formula, width:1800);\n",
@@ -44,14 +44,16 @@
"\n",
"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",
@@ -307,8 +309,8 @@
},
{
"cell_type": "code",
- "execution_count": 27,
- "id": "764ca933",
+ "execution_count": 4,
+ "id": "669da81c",
"metadata": {},
"outputs": [
{
@@ -317,7 +319,7 @@
"Loaded machine: test2"
]
},
- "execution_count": 27,
+ "execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
@@ -338,8 +340,8 @@
},
{
"cell_type": "code",
- "execution_count": 28,
- "id": "f9945f44",
+ "execution_count": 5,
+ "id": "5846d13f",
"metadata": {},
"outputs": [
{
@@ -348,7 +350,7 @@
"Executed operation: INITIALISATION()"
]
},
- "execution_count": 28,
+ "execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
@@ -359,8 +361,8 @@
},
{
"cell_type": "code",
- "execution_count": 29,
- "id": "5b769d49",
+ "execution_count": 6,
+ "id": "64d5cc55",
"metadata": {},
"outputs": [
{
@@ -546,7 +548,7 @@
"<VisB visualization>"
]
},
- "execution_count": 29,
+ "execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
@@ -557,8 +559,8 @@
},
{
"cell_type": "code",
- "execution_count": 30,
- "id": "00c70a05",
+ "execution_count": 7,
+ "id": "1cddf7f4",
"metadata": {},
"outputs": [
{
@@ -581,7 +583,7 @@
"400.0\t50\t\"red\"\t(\"circ\"|->5)\t25\t\"black\"\t2\t\"circle\"\n"
]
},
- "execution_count": 30,
+ "execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
@@ -590,10 +592,936 @@
":table VISB_SVG_OBJECTS"
]
},
+ {
+ "cell_type": "markdown",
+ "id": "7c892901",
+ "metadata": {},
+ "source": [
+ "### VISB_SVG_UPDATES\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",
+ "\n",
+ "Here is a small example:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "id": "7d8491f0",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: test3"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE test3\n",
+ "VARIABLES x\n",
+ "INVARIANT x:1..N\n",
+ "INITIALISATION x:=1\n",
+ "OPERATIONS inc = BEGIN x:= (x mod N)+1 END\n",
+ "DEFINITIONS\n",
+ " N == 5; WID==400.0;\n",
+ " VISB_JSON_FILE == \"\";\n",
+ " VISB_SVG_BOX == rec(height:100, width:WID+30.0);\n",
+ " VISB_SVG_OBJECTS == UNION(i).(i:1..N|\n",
+ " {rec(`id`:(\"circ\",i), svg_class:\"circle\",\n",
+ " cx:real(i)*WID/real(N),cy:50, r:(30-i),\n",
+ " stroke:\"black\")});\n",
+ " VISB_SVG_UPDATES == UNION(i).(i:1..N|\n",
+ " {rec(`id`:(\"circ\",i),\n",
+ " fill: IF i=x THEN \"red\" ELSE \"gray\" END,\n",
+ " `stroke-width`:IF i=x THEN 2.0 ELSE 0.5 END)});\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 9,
+ "id": "ea98b025",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: INITIALISATION()"
+ ]
+ },
+ "execution_count": 9,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "id": "bb265467",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/html": [
+ "<!DOCTYPE html>\n",
+ "<html>\n",
+ "<head>\n",
+ " <!-- html file generated by ProB from a VisB visualization -->\n",
+ " <meta name=\"viewport\" content=\"width=device-width, initial-scale=1.0\">\n",
+ " <meta http-equiv=\"content-type\" content=\"text/html; charset=utf-8\">\n",
+ " <script>\n",
+ " function setAttr(id, attribute, value){\n",
+ "\t\t\tvar obj = document.getElementById(id);\n",
+ "\t\t\tif (obj == null) {\n",
+ "\t\t\t if (id != \"visb_debug_messages\") {\n",
+ "\t\t\t\t console.error(\"Unknown SVG id \" + id + \" for attribute \" + attribute);\n",
+ "\t\t\t\t}\n",
+ "\t\t\t} else if(attribute==\"text\") {\n",
+ "\t\t\t\tobj.textContent = value;\n",
+ "\t\t\t} else if(attribute==\"class\" && value != \"\") {\n",
+ "\t\t\t if(value[0]==\"+\") {\n",
+ "\t\t\t obj.classList.add(value.substr(1));\n",
+ "\t\t\t } else if(value[0]==\"-\") {\n",
+ "\t\t\t obj.classList.remove(value.substr(1));\n",
+ "\t\t\t } else {\n",
+ "\t\t\t\t obj.setAttribute(attribute, value);\n",
+ "\t\t\t }\n",
+ "\t\t\t} else {\n",
+ "\t\t\t\tobj.setAttribute(attribute, value);\n",
+ "\t\t\t}\n",
+ " }\n",
+ "\t\tfunction sleep(ms) {\n",
+ "\t\t return new Promise(resolve => setTimeout(resolve, ms));\n",
+ "\t\t}\n",
+ "\t\tvar lastSelectedRow = 0;\n",
+ "\t\tfunction highlightRow(id) {\n",
+ " if (lastSelectedRow>0) {setAttr(\"row\"+lastSelectedRow,\"bgcolor\",\"\")};\n",
+ " setAttr(\"row\"+id,\"bgcolor\",\"yellow\");\n",
+ " lastSelectedRow = id;\n",
+ "\t\t}\n",
+ "\t\tfunction backStep() {\n",
+ "\t\t if (lastSelectedRow>1) {\n",
+ "\t\t var prev = lastSelectedRow-1;\n",
+ "\t\t document.getElementById(\"row\"+prev).click();\n",
+ "\t\t }\n",
+ "\t\t}\n",
+ "\t\tfunction forwardStep() {\n",
+ "\t\t if (lastSelectedRow>0) {\n",
+ "\t\t var nxt = lastSelectedRow+1;\n",
+ "\t\t var row = document.getElementById(\"row\"+(nxt));\n",
+ "\t\t if (row != null) { row.click() };\n",
+ "\t\t }\n",
+ "\t\t}\n",
+ " </script>\n",
+ " \n",
+ "\t<style>\n",
+ "\ttable {\n",
+ "\t font-family: arial, sans-serif;\n",
+ "\t font-size: 11px;\n",
+ "\t border-collapse: collapse;\n",
+ "\t width: 100%;\n",
+ "\t}\n",
+ "\ttd, th {\n",
+ "\t border: 1px solid #dddddd;\n",
+ "\t text-align: left;\n",
+ "\t padding: 2px;\n",
+ "\t}\n",
+ "/* \n",
+ "\ttr:nth-child(even) {\n",
+ "\t background-color: #dddddd;\n",
+ "\t}\n",
+ " */\n",
+ "\t</style> \n",
+ "\t\n",
+ "\t<style>\n",
+ "\t.collapsible {\n",
+ "\t cursor: pointer;\n",
+ "\t}\n",
+ "\t.collapsible-style {\n",
+ "\t background-color: #777;\n",
+ "\t color: white;\n",
+ "\t padding: 6px;\n",
+ "\t width: 100%;\n",
+ "\t border: none;\n",
+ "\t text-align: left;\n",
+ "\t outline: none;\n",
+ "\t font-size: 12px;\n",
+ "\t}\n",
+ "\n",
+ "\t.active, .collapsible:hover {\n",
+ "\t background-color: #555;\n",
+ "\t}\n",
+ "\t\n",
+ "\t.collapsible:after {\n",
+ "\t content: '\\002B';\n",
+ "\t color: white;\n",
+ "\t font-weight: bold;\n",
+ "\t float: right;\n",
+ "\t margin-left: 5px;\n",
+ "\t}\n",
+ "\n",
+ "\t.active:after {\n",
+ "\t content: \"\\2212\";\n",
+ "\t}\n",
+ "\n",
+ "\t.coll-content-hid {\n",
+ "\t padding: 0 12px;\n",
+ "\t display: none;\n",
+ "\t overflow: hidden;\n",
+ "\t background-color: #f1f1f1;\n",
+ "\t}\n",
+ "\t.coll-content-vis {\n",
+ "\t padding: 0 12px;\n",
+ "\t display: block;\n",
+ "\t overflow: hidden;\n",
+ "\t background-color: #f1f1f1;\n",
+ "\t}\n",
+ "\t.visb-messages {\n",
+ "\t text-align: left;\n",
+ "\t outline: none;\n",
+ "\t font-size: 12px;\n",
+ "\t font-family: arial, sans-serif;\n",
+ "\t}\n",
+ " </style>\n",
+ "\n",
+ " \n",
+ "\n",
+ " <script>\n",
+ " function visualise0(stepNr) {\n",
+ " setAttr(\"visb_debug_messages\",\"text\",\"Step \"+stepNr+\"/1, State ID: 0\");\n",
+ "Extracting SVG updates from VISB_SVG_UPDATES\n",
+ " setAttr(\"circ2\",\"fill\",\"gray\");\n",
+ " setAttr(\"circ2\",\"stroke-width\",\"0.5\");\n",
+ " setAttr(\"circ3\",\"fill\",\"gray\");\n",
+ " setAttr(\"circ3\",\"stroke-width\",\"0.5\");\n",
+ " setAttr(\"circ4\",\"fill\",\"gray\");\n",
+ " setAttr(\"circ4\",\"stroke-width\",\"0.5\");\n",
+ " setAttr(\"circ5\",\"fill\",\"gray\");\n",
+ " setAttr(\"circ5\",\"stroke-width\",\"0.5\");\n",
+ " setAttr(\"circ1\",\"fill\",\"red\");\n",
+ " setAttr(\"circ1\",\"stroke-width\",\"2.0\");\n",
+ " highlightRow(stepNr);\n",
+ " }\n",
+ " async function runAll(delay) {\n",
+ " visualise0(1);\n",
+ " setAttr(\"visb_debug_messages\",\"text\",\"Step: 1/1, State ID: 0, Event: \");\n",
+ " await sleep(delay);\n",
+ " }\n",
+ " </script>\n",
+ "\n",
+ " <script> function registerHovers() {} </script>\n",
+ " </head>\n",
+ "<body>\n",
+ " <button type=\"button\" class=\"collapsible collapsible-style\">SVG Visualisation</button>\n",
+ " <div text-align=\"left\"> \n",
+ " \n",
+ "\n",
+ "<svg xmlns=\"http://www.w3.org/2000/svg\"\n",
+ " width=\"430.0\" height=\"100\" viewBox=\"0 0 430.0 100\" >\n",
+ "Extracting SVG updates from VISB_SVG_UPDATES\n",
+ " <circle id=\"circ1\" cx=\"80.0\" cy=\"50\" fill=\"red\" r=\"29\" stroke=\"black\" stroke-width=\"2.0\"></circle>\n",
+ " <circle id=\"circ2\" cx=\"160.0\" cy=\"50\" fill=\"gray\" r=\"28\" stroke=\"black\" stroke-width=\"0.5\"></circle>\n",
+ " <circle id=\"circ3\" cx=\"240.0\" cy=\"50\" fill=\"gray\" r=\"27\" stroke=\"black\" stroke-width=\"0.5\"></circle>\n",
+ " <circle id=\"circ4\" cx=\"320.0\" cy=\"50\" fill=\"gray\" r=\"26\" stroke=\"black\" stroke-width=\"0.5\"></circle>\n",
+ " <circle id=\"circ5\" cx=\"400.0\" cy=\"50\" fill=\"gray\" r=\"25\" stroke=\"black\" stroke-width=\"0.5\"></circle>\n",
+ "</svg>\n",
+ " </div>\n",
+ " <script> visualise0(1); </script>\n",
+ " </div>\n",
+ " <script> registerHovers() </script>\n",
+ " \n",
+ "<script>\n",
+ "var collapsibles = document.getElementsByClassName(\"collapsible\");\n",
+ "var ii;\n",
+ "\n",
+ "for (ii = 0; ii < collapsibles.length; ii++) {\n",
+ " collapsibles[ii].addEventListener(\"click\", function() {\n",
+ " this.classList.toggle(\"active\");\n",
+ " var content = this.nextElementSibling;\n",
+ " if (content.style.display === \"block\") {\n",
+ " content.style.display = \"none\";\n",
+ " } else {\n",
+ " content.style.display = \"block\";\n",
+ " }\n",
+ " });\n",
+ "}\n",
+ "</script>\n",
+ "\n",
+ "</body>\n",
+ "</html>\n",
+ "\n"
+ ],
+ "text/plain": [
+ "<VisB visualization>"
+ ]
+ },
+ "execution_count": 10,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 11,
+ "id": "d8d09a69",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: inc()"
+ ]
+ },
+ "execution_count": 11,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec inc"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "id": "61d5ca71",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/html": [
+ "<!DOCTYPE html>\n",
+ "<html>\n",
+ "<head>\n",
+ " <!-- html file generated by ProB from a VisB visualization -->\n",
+ " <meta name=\"viewport\" content=\"width=device-width, initial-scale=1.0\">\n",
+ " <meta http-equiv=\"content-type\" content=\"text/html; charset=utf-8\">\n",
+ " <script>\n",
+ " function setAttr(id, attribute, value){\n",
+ "\t\t\tvar obj = document.getElementById(id);\n",
+ "\t\t\tif (obj == null) {\n",
+ "\t\t\t if (id != \"visb_debug_messages\") {\n",
+ "\t\t\t\t console.error(\"Unknown SVG id \" + id + \" for attribute \" + attribute);\n",
+ "\t\t\t\t}\n",
+ "\t\t\t} else if(attribute==\"text\") {\n",
+ "\t\t\t\tobj.textContent = value;\n",
+ "\t\t\t} else if(attribute==\"class\" && value != \"\") {\n",
+ "\t\t\t if(value[0]==\"+\") {\n",
+ "\t\t\t obj.classList.add(value.substr(1));\n",
+ "\t\t\t } else if(value[0]==\"-\") {\n",
+ "\t\t\t obj.classList.remove(value.substr(1));\n",
+ "\t\t\t } else {\n",
+ "\t\t\t\t obj.setAttribute(attribute, value);\n",
+ "\t\t\t }\n",
+ "\t\t\t} else {\n",
+ "\t\t\t\tobj.setAttribute(attribute, value);\n",
+ "\t\t\t}\n",
+ " }\n",
+ "\t\tfunction sleep(ms) {\n",
+ "\t\t return new Promise(resolve => setTimeout(resolve, ms));\n",
+ "\t\t}\n",
+ "\t\tvar lastSelectedRow = 0;\n",
+ "\t\tfunction highlightRow(id) {\n",
+ " if (lastSelectedRow>0) {setAttr(\"row\"+lastSelectedRow,\"bgcolor\",\"\")};\n",
+ " setAttr(\"row\"+id,\"bgcolor\",\"yellow\");\n",
+ " lastSelectedRow = id;\n",
+ "\t\t}\n",
+ "\t\tfunction backStep() {\n",
+ "\t\t if (lastSelectedRow>1) {\n",
+ "\t\t var prev = lastSelectedRow-1;\n",
+ "\t\t document.getElementById(\"row\"+prev).click();\n",
+ "\t\t }\n",
+ "\t\t}\n",
+ "\t\tfunction forwardStep() {\n",
+ "\t\t if (lastSelectedRow>0) {\n",
+ "\t\t var nxt = lastSelectedRow+1;\n",
+ "\t\t var row = document.getElementById(\"row\"+(nxt));\n",
+ "\t\t if (row != null) { row.click() };\n",
+ "\t\t }\n",
+ "\t\t}\n",
+ " </script>\n",
+ " \n",
+ "\t<style>\n",
+ "\ttable {\n",
+ "\t font-family: arial, sans-serif;\n",
+ "\t font-size: 11px;\n",
+ "\t border-collapse: collapse;\n",
+ "\t width: 100%;\n",
+ "\t}\n",
+ "\ttd, th {\n",
+ "\t border: 1px solid #dddddd;\n",
+ "\t text-align: left;\n",
+ "\t padding: 2px;\n",
+ "\t}\n",
+ "/* \n",
+ "\ttr:nth-child(even) {\n",
+ "\t background-color: #dddddd;\n",
+ "\t}\n",
+ " */\n",
+ "\t</style> \n",
+ "\t\n",
+ "\t<style>\n",
+ "\t.collapsible {\n",
+ "\t cursor: pointer;\n",
+ "\t}\n",
+ "\t.collapsible-style {\n",
+ "\t background-color: #777;\n",
+ "\t color: white;\n",
+ "\t padding: 6px;\n",
+ "\t width: 100%;\n",
+ "\t border: none;\n",
+ "\t text-align: left;\n",
+ "\t outline: none;\n",
+ "\t font-size: 12px;\n",
+ "\t}\n",
+ "\n",
+ "\t.active, .collapsible:hover {\n",
+ "\t background-color: #555;\n",
+ "\t}\n",
+ "\t\n",
+ "\t.collapsible:after {\n",
+ "\t content: '\\002B';\n",
+ "\t color: white;\n",
+ "\t font-weight: bold;\n",
+ "\t float: right;\n",
+ "\t margin-left: 5px;\n",
+ "\t}\n",
+ "\n",
+ "\t.active:after {\n",
+ "\t content: \"\\2212\";\n",
+ "\t}\n",
+ "\n",
+ "\t.coll-content-hid {\n",
+ "\t padding: 0 12px;\n",
+ "\t display: none;\n",
+ "\t overflow: hidden;\n",
+ "\t background-color: #f1f1f1;\n",
+ "\t}\n",
+ "\t.coll-content-vis {\n",
+ "\t padding: 0 12px;\n",
+ "\t display: block;\n",
+ "\t overflow: hidden;\n",
+ "\t background-color: #f1f1f1;\n",
+ "\t}\n",
+ "\t.visb-messages {\n",
+ "\t text-align: left;\n",
+ "\t outline: none;\n",
+ "\t font-size: 12px;\n",
+ "\t font-family: arial, sans-serif;\n",
+ "\t}\n",
+ " </style>\n",
+ "\n",
+ " \n",
+ "\n",
+ " <script>\n",
+ " function visualise1(stepNr) {\n",
+ " setAttr(\"visb_debug_messages\",\"text\",\"Step \"+stepNr+\"/1, State ID: 1\");\n",
+ "Extracting SVG updates from VISB_SVG_UPDATES\n",
+ " setAttr(\"circ1\",\"fill\",\"gray\");\n",
+ " setAttr(\"circ1\",\"stroke-width\",\"0.5\");\n",
+ " setAttr(\"circ3\",\"fill\",\"gray\");\n",
+ " setAttr(\"circ3\",\"stroke-width\",\"0.5\");\n",
+ " setAttr(\"circ4\",\"fill\",\"gray\");\n",
+ " setAttr(\"circ4\",\"stroke-width\",\"0.5\");\n",
+ " setAttr(\"circ5\",\"fill\",\"gray\");\n",
+ " setAttr(\"circ5\",\"stroke-width\",\"0.5\");\n",
+ " setAttr(\"circ2\",\"fill\",\"red\");\n",
+ " setAttr(\"circ2\",\"stroke-width\",\"2.0\");\n",
+ " highlightRow(stepNr);\n",
+ " }\n",
+ " async function runAll(delay) {\n",
+ " visualise1(1);\n",
+ " setAttr(\"visb_debug_messages\",\"text\",\"Step: 1/1, State ID: 1, Event: \");\n",
+ " await sleep(delay);\n",
+ " }\n",
+ " </script>\n",
+ "\n",
+ " <script> function registerHovers() {} </script>\n",
+ " </head>\n",
+ "<body>\n",
+ " <button type=\"button\" class=\"collapsible collapsible-style\">SVG Visualisation</button>\n",
+ " <div text-align=\"left\"> \n",
+ " \n",
+ "\n",
+ "<svg xmlns=\"http://www.w3.org/2000/svg\"\n",
+ " width=\"430.0\" height=\"100\" viewBox=\"0 0 430.0 100\" >\n",
+ "Extracting SVG updates from VISB_SVG_UPDATES\n",
+ " <circle id=\"circ1\" cx=\"80.0\" cy=\"50\" fill=\"gray\" r=\"29\" stroke=\"black\" stroke-width=\"0.5\"></circle>\n",
+ " <circle id=\"circ2\" cx=\"160.0\" cy=\"50\" fill=\"red\" r=\"28\" stroke=\"black\" stroke-width=\"2.0\"></circle>\n",
+ " <circle id=\"circ3\" cx=\"240.0\" cy=\"50\" fill=\"gray\" r=\"27\" stroke=\"black\" stroke-width=\"0.5\"></circle>\n",
+ " <circle id=\"circ4\" cx=\"320.0\" cy=\"50\" fill=\"gray\" r=\"26\" stroke=\"black\" stroke-width=\"0.5\"></circle>\n",
+ " <circle id=\"circ5\" cx=\"400.0\" cy=\"50\" fill=\"gray\" r=\"25\" stroke=\"black\" stroke-width=\"0.5\"></circle>\n",
+ "</svg>\n",
+ " </div>\n",
+ " <script> visualise1(1); </script>\n",
+ " </div>\n",
+ " <script> registerHovers() </script>\n",
+ " \n",
+ "<script>\n",
+ "var collapsibles = document.getElementsByClassName(\"collapsible\");\n",
+ "var ii;\n",
+ "\n",
+ "for (ii = 0; ii < collapsibles.length; ii++) {\n",
+ " collapsibles[ii].addEventListener(\"click\", function() {\n",
+ " this.classList.toggle(\"active\");\n",
+ " var content = this.nextElementSibling;\n",
+ " if (content.style.display === \"block\") {\n",
+ " content.style.display = \"none\";\n",
+ " } else {\n",
+ " content.style.display = \"block\";\n",
+ " }\n",
+ " });\n",
+ "}\n",
+ "</script>\n",
+ "\n",
+ "</body>\n",
+ "</html>\n",
+ "\n"
+ ],
+ "text/plain": [
+ "<VisB visualization>"
+ ]
+ },
+ "execution_count": 12,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 13,
+ "id": "2993ed34",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|fill|id|stroke-width|\n",
+ "|---|---|---|\n",
+ "|\"gray\"|(\"circ\"↦1)|0.5|\n",
+ "|\"gray\"|(\"circ\"↦3)|0.5|\n",
+ "|\"gray\"|(\"circ\"↦4)|0.5|\n",
+ "|\"gray\"|(\"circ\"↦5)|0.5|\n",
+ "|\"red\"|(\"circ\"↦2)|2.0|\n"
+ ],
+ "text/plain": [
+ "fill\tid\tstroke-width\n",
+ "\"gray\"\t(\"circ\"|->1)\t0.5\n",
+ "\"gray\"\t(\"circ\"|->3)\t0.5\n",
+ "\"gray\"\t(\"circ\"|->4)\t0.5\n",
+ "\"gray\"\t(\"circ\"|->5)\t0.5\n",
+ "\"red\"\t(\"circ\"|->2)\t2.0\n"
+ ]
+ },
+ "execution_count": 13,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table VISB_SVG_UPDATES"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "7818407b",
+ "metadata": {},
+ "source": [
+ "### VISB_SVG_CONTENTS\n",
+ "\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",
+ "Here is an example:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 14,
+ "id": "5bdcf602",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: test4"
+ ]
+ },
+ "execution_count": 14,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE test4\n",
+ "VARIABLES x\n",
+ "INVARIANT x:1..N\n",
+ "INITIALISATION x:=1\n",
+ "OPERATIONS inc = BEGIN x:= (x mod N)+1 END\n",
+ "DEFINITIONS\n",
+ " N == 5; WID==400.0;\n",
+ " VISB_JSON_FILE == \"\";\n",
+ " VISB_SVG_BOX == rec(height:100, width:WID+30.0);\n",
+ " VISB_SVG_OBJECTS == UNION(i).(i:1..N|\n",
+ " {rec(`id`:(\"circ\",i), svg_class:\"circle\",\n",
+ " cx:real(i)*WID/real(N),cy:50, r:(30-i))});\n",
+ " VISB_SVG_UPDATES == UNION(i).(i:1..N|\n",
+ " {rec(`id`:(\"circ\",i),\n",
+ " class: IF i=x THEN \"selected\" ELSE \"normal\" END)});\n",
+ " VISB_SVG_CONTENTS == '''\n",
+ " <style>\n",
+ " .selected {\n",
+ " fill: red;\n",
+ " stroke : black;\n",
+ " stroke-width: 2.0\n",
+ " }\n",
+ " .normal {\n",
+ " fill : gray;\n",
+ " stroke : none\n",
+ " }\n",
+ " </style>\n",
+ "''';\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 15,
+ "id": "366c7bfc",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: INITIALISATION()"
+ ]
+ },
+ "execution_count": 15,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 16,
+ "id": "569344f3",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/html": [
+ "<!DOCTYPE html>\n",
+ "<html>\n",
+ "<head>\n",
+ " <!-- html file generated by ProB from a VisB visualization -->\n",
+ " <meta name=\"viewport\" content=\"width=device-width, initial-scale=1.0\">\n",
+ " <meta http-equiv=\"content-type\" content=\"text/html; charset=utf-8\">\n",
+ " <script>\n",
+ " function setAttr(id, attribute, value){\n",
+ "\t\t\tvar obj = document.getElementById(id);\n",
+ "\t\t\tif (obj == null) {\n",
+ "\t\t\t if (id != \"visb_debug_messages\") {\n",
+ "\t\t\t\t console.error(\"Unknown SVG id \" + id + \" for attribute \" + attribute);\n",
+ "\t\t\t\t}\n",
+ "\t\t\t} else if(attribute==\"text\") {\n",
+ "\t\t\t\tobj.textContent = value;\n",
+ "\t\t\t} else if(attribute==\"class\" && value != \"\") {\n",
+ "\t\t\t if(value[0]==\"+\") {\n",
+ "\t\t\t obj.classList.add(value.substr(1));\n",
+ "\t\t\t } else if(value[0]==\"-\") {\n",
+ "\t\t\t obj.classList.remove(value.substr(1));\n",
+ "\t\t\t } else {\n",
+ "\t\t\t\t obj.setAttribute(attribute, value);\n",
+ "\t\t\t }\n",
+ "\t\t\t} else {\n",
+ "\t\t\t\tobj.setAttribute(attribute, value);\n",
+ "\t\t\t}\n",
+ " }\n",
+ "\t\tfunction sleep(ms) {\n",
+ "\t\t return new Promise(resolve => setTimeout(resolve, ms));\n",
+ "\t\t}\n",
+ "\t\tvar lastSelectedRow = 0;\n",
+ "\t\tfunction highlightRow(id) {\n",
+ " if (lastSelectedRow>0) {setAttr(\"row\"+lastSelectedRow,\"bgcolor\",\"\")};\n",
+ " setAttr(\"row\"+id,\"bgcolor\",\"yellow\");\n",
+ " lastSelectedRow = id;\n",
+ "\t\t}\n",
+ "\t\tfunction backStep() {\n",
+ "\t\t if (lastSelectedRow>1) {\n",
+ "\t\t var prev = lastSelectedRow-1;\n",
+ "\t\t document.getElementById(\"row\"+prev).click();\n",
+ "\t\t }\n",
+ "\t\t}\n",
+ "\t\tfunction forwardStep() {\n",
+ "\t\t if (lastSelectedRow>0) {\n",
+ "\t\t var nxt = lastSelectedRow+1;\n",
+ "\t\t var row = document.getElementById(\"row\"+(nxt));\n",
+ "\t\t if (row != null) { row.click() };\n",
+ "\t\t }\n",
+ "\t\t}\n",
+ " </script>\n",
+ " \n",
+ "\t<style>\n",
+ "\ttable {\n",
+ "\t font-family: arial, sans-serif;\n",
+ "\t font-size: 11px;\n",
+ "\t border-collapse: collapse;\n",
+ "\t width: 100%;\n",
+ "\t}\n",
+ "\ttd, th {\n",
+ "\t border: 1px solid #dddddd;\n",
+ "\t text-align: left;\n",
+ "\t padding: 2px;\n",
+ "\t}\n",
+ "/* \n",
+ "\ttr:nth-child(even) {\n",
+ "\t background-color: #dddddd;\n",
+ "\t}\n",
+ " */\n",
+ "\t</style> \n",
+ "\t\n",
+ "\t<style>\n",
+ "\t.collapsible {\n",
+ "\t cursor: pointer;\n",
+ "\t}\n",
+ "\t.collapsible-style {\n",
+ "\t background-color: #777;\n",
+ "\t color: white;\n",
+ "\t padding: 6px;\n",
+ "\t width: 100%;\n",
+ "\t border: none;\n",
+ "\t text-align: left;\n",
+ "\t outline: none;\n",
+ "\t font-size: 12px;\n",
+ "\t}\n",
+ "\n",
+ "\t.active, .collapsible:hover {\n",
+ "\t background-color: #555;\n",
+ "\t}\n",
+ "\t\n",
+ "\t.collapsible:after {\n",
+ "\t content: '\\002B';\n",
+ "\t color: white;\n",
+ "\t font-weight: bold;\n",
+ "\t float: right;\n",
+ "\t margin-left: 5px;\n",
+ "\t}\n",
+ "\n",
+ "\t.active:after {\n",
+ "\t content: \"\\2212\";\n",
+ "\t}\n",
+ "\n",
+ "\t.coll-content-hid {\n",
+ "\t padding: 0 12px;\n",
+ "\t display: none;\n",
+ "\t overflow: hidden;\n",
+ "\t background-color: #f1f1f1;\n",
+ "\t}\n",
+ "\t.coll-content-vis {\n",
+ "\t padding: 0 12px;\n",
+ "\t display: block;\n",
+ "\t overflow: hidden;\n",
+ "\t background-color: #f1f1f1;\n",
+ "\t}\n",
+ "\t.visb-messages {\n",
+ "\t text-align: left;\n",
+ "\t outline: none;\n",
+ "\t font-size: 12px;\n",
+ "\t font-family: arial, sans-serif;\n",
+ "\t}\n",
+ " </style>\n",
+ "\n",
+ " \n",
+ "\n",
+ " <script>\n",
+ " function visualise0(stepNr) {\n",
+ " setAttr(\"visb_debug_messages\",\"text\",\"Step \"+stepNr+\"/1, State ID: 0\");\n",
+ "Extracting SVG updates from VISB_SVG_UPDATES\n",
+ " setAttr(\"circ2\",\"class\",\"normal\");\n",
+ " setAttr(\"circ3\",\"class\",\"normal\");\n",
+ " setAttr(\"circ4\",\"class\",\"normal\");\n",
+ " setAttr(\"circ5\",\"class\",\"normal\");\n",
+ " setAttr(\"circ1\",\"class\",\"selected\");\n",
+ " highlightRow(stepNr);\n",
+ " }\n",
+ " async function runAll(delay) {\n",
+ " visualise0(1);\n",
+ " setAttr(\"visb_debug_messages\",\"text\",\"Step: 1/1, State ID: 0, Event: \");\n",
+ " await sleep(delay);\n",
+ " }\n",
+ " </script>\n",
+ "\n",
+ " <script> function registerHovers() {} </script>\n",
+ " </head>\n",
+ "<body>\n",
+ " <button type=\"button\" class=\"collapsible collapsible-style\">SVG Visualisation</button>\n",
+ " <div text-align=\"left\"> \n",
+ " \n",
+ "\n",
+ "<svg xmlns=\"http://www.w3.org/2000/svg\"\n",
+ " width=\"430.0\" height=\"100\" viewBox=\"0 0 430.0 100\" >\n",
+ "Detected VISB_SVG_CONTENTS (requires_nothing)\n",
+ "\n",
+ " <style>\n",
+ " .selected {\n",
+ " fill: red;\n",
+ " stroke : black;\n",
+ " stroke-width: 2.0\n",
+ " }\n",
+ " .normal {\n",
+ " fill : gray;\n",
+ " stroke : none\n",
+ " }\n",
+ " </style>\n",
+ "\n",
+ "Extracting SVG updates from VISB_SVG_UPDATES\n",
+ " <circle id=\"circ1\" class=\"selected\" cx=\"80.0\" cy=\"50\" r=\"29\"></circle>\n",
+ " <circle id=\"circ2\" class=\"normal\" cx=\"160.0\" cy=\"50\" r=\"28\"></circle>\n",
+ " <circle id=\"circ3\" class=\"normal\" cx=\"240.0\" cy=\"50\" r=\"27\"></circle>\n",
+ " <circle id=\"circ4\" class=\"normal\" cx=\"320.0\" cy=\"50\" r=\"26\"></circle>\n",
+ " <circle id=\"circ5\" class=\"normal\" cx=\"400.0\" cy=\"50\" r=\"25\"></circle>\n",
+ "</svg>\n",
+ " </div>\n",
+ " <script> visualise0(1); </script>\n",
+ " </div>\n",
+ " <script> registerHovers() </script>\n",
+ " \n",
+ "<script>\n",
+ "var collapsibles = document.getElementsByClassName(\"collapsible\");\n",
+ "var ii;\n",
+ "\n",
+ "for (ii = 0; ii < collapsibles.length; ii++) {\n",
+ " collapsibles[ii].addEventListener(\"click\", function() {\n",
+ " this.classList.toggle(\"active\");\n",
+ " var content = this.nextElementSibling;\n",
+ " if (content.style.display === \"block\") {\n",
+ " content.style.display = \"none\";\n",
+ " } else {\n",
+ " content.style.display = \"block\";\n",
+ " }\n",
+ " });\n",
+ "}\n",
+ "</script>\n",
+ "\n",
+ "</body>\n",
+ "</html>\n",
+ "\n"
+ ],
+ "text/plain": [
+ "<VisB visualization>"
+ ]
+ },
+ "execution_count": 16,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 17,
+ "id": "caeb65b3",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|class|id|\n",
+ "|---|---|\n",
+ "|\"normal\"|(\"circ\"↦2)|\n",
+ "|\"normal\"|(\"circ\"↦3)|\n",
+ "|\"normal\"|(\"circ\"↦4)|\n",
+ "|\"normal\"|(\"circ\"↦5)|\n",
+ "|\"selected\"|(\"circ\"↦1)|\n"
+ ],
+ "text/plain": [
+ "class\tid\n",
+ "\"normal\"\t(\"circ\"|->2)\n",
+ "\"normal\"\t(\"circ\"|->3)\n",
+ "\"normal\"\t(\"circ\"|->4)\n",
+ "\"normal\"\t(\"circ\"|->5)\n",
+ "\"selected\"\t(\"circ\"|->1)\n"
+ ]
+ },
+ "execution_count": 17,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table VISB_SVG_UPDATES"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 18,
+ "id": "09c42864",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|cx|cy|id|r|svg_class|\n",
+ "|---|---|---|---|---|\n",
+ "|80.0|50|(\"circ\"↦1)|29|\"circle\"|\n",
+ "|160.0|50|(\"circ\"↦2)|28|\"circle\"|\n",
+ "|240.0|50|(\"circ\"↦3)|27|\"circle\"|\n",
+ "|320.0|50|(\"circ\"↦4)|26|\"circle\"|\n",
+ "|400.0|50|(\"circ\"↦5)|25|\"circle\"|\n"
+ ],
+ "text/plain": [
+ "cx\tcy\tid\tr\tsvg_class\n",
+ "80.0\t50\t(\"circ\"|->1)\t29\t\"circle\"\n",
+ "160.0\t50\t(\"circ\"|->2)\t28\t\"circle\"\n",
+ "240.0\t50\t(\"circ\"|->3)\t27\t\"circle\"\n",
+ "320.0\t50\t(\"circ\"|->4)\t26\t\"circle\"\n",
+ "400.0\t50\t(\"circ\"|->5)\t25\t\"circle\"\n"
+ ]
+ },
+ "execution_count": 18,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table VISB_SVG_OBJECTS"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "a215c22b",
+ "metadata": {},
+ "outputs": [],
+ "source": []
+ },
{
"cell_type": "code",
"execution_count": null,
- "id": "2222fff4",
+ "id": "caffd470",
"metadata": {},
"outputs": [],
"source": []
--
GitLab