From cea4acafb5f3066b8a286771665423fcab2f3c10 Mon Sep 17 00:00:00 2001 From: Michael Leuschel <leuschel@uni-duesseldorf.de> Date: Thu, 13 Jul 2023 19:41:54 +0200 Subject: [PATCH] add VisB features notebook Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de> --- notebooks/manual/VisB_Features.ipynb | 617 +++++++++++++++++++++++++++ 1 file changed, 617 insertions(+) create mode 100644 notebooks/manual/VisB_Features.ipynb diff --git a/notebooks/manual/VisB_Features.ipynb b/notebooks/manual/VisB_Features.ipynb new file mode 100644 index 0000000..68f0a5a --- /dev/null +++ b/notebooks/manual/VisB_Features.ipynb @@ -0,0 +1,617 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "id": "5b53d563", + "metadata": {}, + "source": [ + "# VisB\n", + "\n", + "\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", + "* 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\n", + "* 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.\n", + "Hovers work in both cases, but unlike in ProB2-UI, you cannot click to perform events.\n", + "\n", + "An article about VisB has been [https://rdcu.be/b4rqh published in the ABZ'2020 proceedings].\n" + ] + }, + { + "cell_type": "markdown", + "id": "6942b823", + "metadata": {}, + "source": [ + "As of version 1.12 you can also provide many of the VisB annotations via B DEFINITIONS.\n", + "This can be done in addition to a VisB JSON file or completely replacing the JSON file.\n", + "\n", + "By adding this definition to your B machine you specify that you wish to use an empty\n", + "SVG file as base:\n", + "<pre>\n", + " VISB_JSON_FILE == \"\";\n", + "</pre>\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", + "</pre>\n", + "\n", + "Note: you can also provide an optional <tt>viewBox</tt> attribute as a B string.\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", + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Loaded machine: test1" + ] + }, + "execution_count": 12, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "::load\n", + "MACHINE test1\n", + "DEFINITIONS\n", + " VISB_JSON_FILE == \"\";\n", + " VISB_SVG_BOX == rec(height:100, width:400);\n", + " VISB_SVG_OBJECTS == rec(`id`:\"button\", svg_class:\"circle\",\n", + " cx:200,cy:50, r:30, fill: \"red\",\n", + " stroke:\"black\", `stroke-width`:2);\n", + "END" + ] + }, + { + "cell_type": "code", + "execution_count": 13, + "id": "9cf27405", + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Executed operation: INITIALISATION()" + ] + }, + "execution_count": 13, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":init" + ] + }, + { + "cell_type": "code", + "execution_count": 14, + "id": "5fd0cbbe", + "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", + " 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=\"400\" height=\"100\" viewBox=\"0 0 400 100\" >\n", + " <circle id=\"button\" cx=\"200\" cy=\"50\" fill=\"red\" r=\"30\" stroke=\"black\" stroke-width=\"2\"></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": 14, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":show" + ] + }, + { + "cell_type": "markdown", + "id": "41725617", + "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", + "* usually all created object should have an id (so that you can later modify the attributes)\n", + "* you have to provide an <tt>svg_class</tt> attribute: circle, ellipse, line, path, polygon, polyline, rect, text\n", + "* you then can (and probably) should provide necessary attributes and initial values for your object\n", + "\n", + "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." + ] + }, + { + "cell_type": "code", + "execution_count": 27, + "id": "764ca933", + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Loaded machine: test2" + ] + }, + "execution_count": 27, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "::load\n", + "MACHINE test2\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), fill: \"red\",\n", + " stroke:\"black\", `stroke-width`:2)});\n", + "END" + ] + }, + { + "cell_type": "code", + "execution_count": 28, + "id": "f9945f44", + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Executed operation: INITIALISATION()" + ] + }, + "execution_count": 28, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":init" + ] + }, + { + "cell_type": "code", + "execution_count": 29, + "id": "5b769d49", + "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", + " 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", + " <circle id=\"circ1\" cx=\"80.0\" cy=\"50\" fill=\"red\" r=\"29\" stroke=\"black\" stroke-width=\"2\"></circle>\n", + " <circle id=\"circ2\" cx=\"160.0\" cy=\"50\" fill=\"red\" r=\"28\" stroke=\"black\" stroke-width=\"2\"></circle>\n", + " <circle id=\"circ3\" cx=\"240.0\" cy=\"50\" fill=\"red\" r=\"27\" stroke=\"black\" stroke-width=\"2\"></circle>\n", + " <circle id=\"circ4\" cx=\"320.0\" cy=\"50\" fill=\"red\" r=\"26\" stroke=\"black\" stroke-width=\"2\"></circle>\n", + " <circle id=\"circ5\" cx=\"400.0\" cy=\"50\" fill=\"red\" r=\"25\" stroke=\"black\" stroke-width=\"2\"></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": 29, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":show" + ] + }, + { + "cell_type": "code", + "execution_count": 30, + "id": "00c70a05", + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "|cx|cy|fill|id|r|stroke|stroke-width|svg_class|\n", + "|---|---|---|---|---|---|---|---|\n", + "|80.0|50|\"red\"|(\"circ\"↦1)|29|\"black\"|2|\"circle\"|\n", + "|160.0|50|\"red\"|(\"circ\"↦2)|28|\"black\"|2|\"circle\"|\n", + "|240.0|50|\"red\"|(\"circ\"↦3)|27|\"black\"|2|\"circle\"|\n", + "|320.0|50|\"red\"|(\"circ\"↦4)|26|\"black\"|2|\"circle\"|\n", + "|400.0|50|\"red\"|(\"circ\"↦5)|25|\"black\"|2|\"circle\"|\n" + ], + "text/plain": [ + "cx\tcy\tfill\tid\tr\tstroke\tstroke-width\tsvg_class\n", + "80.0\t50\t\"red\"\t(\"circ\"|->1)\t29\t\"black\"\t2\t\"circle\"\n", + "160.0\t50\t\"red\"\t(\"circ\"|->2)\t28\t\"black\"\t2\t\"circle\"\n", + "240.0\t50\t\"red\"\t(\"circ\"|->3)\t27\t\"black\"\t2\t\"circle\"\n", + "320.0\t50\t\"red\"\t(\"circ\"|->4)\t26\t\"black\"\t2\t\"circle\"\n", + "400.0\t50\t\"red\"\t(\"circ\"|->5)\t25\t\"black\"\t2\t\"circle\"\n" + ] + }, + "execution_count": 30, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":table VISB_SVG_OBJECTS" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "2222fff4", + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "ProB 2", + "language": "prob", + "name": "prob2" + }, + "language_info": { + "codemirror_mode": "prob2_jupyter_repl", + "file_extension": ".prob", + "mimetype": "text/x-prob2-jupyter-repl", + "name": "prob" + } + }, + "nbformat": 4, + "nbformat_minor": 5 +} -- GitLab