From c5b40c1406dbd8a8e596d1e4e731fe85c62bed9f Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Thu, 21 Jun 2018 13:51:24 +0200
Subject: [PATCH] Add :dot command
---
notebooks/tests/dot.ipynb | 435 ++++++++++++++++++
.../java/de/prob2/jupyter/ProBKernel.java | 2 +
.../de/prob2/jupyter/commands/DotCommand.java | 119 +++++
3 files changed, 556 insertions(+)
create mode 100644 notebooks/tests/dot.ipynb
create mode 100644 src/main/java/de/prob2/jupyter/commands/DotCommand.java
diff --git a/notebooks/tests/dot.ipynb b/notebooks/tests/dot.ipynb
new file mode 100644
index 0000000..5f54acb
--- /dev/null
+++ b/notebooks/tests/dot.ipynb
@@ -0,0 +1,435 @@
+{
+ "cells": [
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "```\n",
+ ":dot COMMAND [FORMULA]\n",
+ "```\n",
+ "\n",
+ "Execute and show a dot visualization."
+ ],
+ "text/plain": [
+ ":dot COMMAND [FORMULA]\n",
+ "\n",
+ "Execute and show a dot visualization."
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":help :dot"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+ "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+ "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
+ " -->\n",
+ "<!-- Title: visited_states Pages: 1 -->\n",
+ "<svg width=\"84pt\" height=\"50pt\"\n",
+ " viewBox=\"0.00 0.00 84.33 50.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 46)\">\n",
+ "<title>visited_states</title>\n",
+ "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-46 80.3328,-46 80.3328,4 -4,4\"/>\n",
+ "<!-- root -->\n",
+ "<g id=\"node1\" class=\"node\">\n",
+ "<title>root</title>\n",
+ "<polygon fill=\"none\" stroke=\"#f4e3c1\" stroke-width=\"2\" points=\"38.1664,0 76.4999,-31.5 -.1671,-31.5 38.1664,0\"/>\n",
+ "<text text-anchor=\"middle\" x=\"38.1664\" y=\"-17.9\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">root</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>"
+ ],
+ "text/plain": [
+ "<Dot visualization: state_space []>"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot state_space"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 0: $initialise_machine()"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "metadata": {
+ "scrolled": false
+ },
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+ "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+ "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
+ " -->\n",
+ "<!-- Title: visited_states Pages: 1 -->\n",
+ "<svg width=\"115pt\" height=\"215pt\"\n",
+ " viewBox=\"0.00 0.00 115.17 215.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 211)\">\n",
+ "<title>visited_states</title>\n",
+ "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-211 111.1664,-211 111.1664,4 -4,4\"/>\n",
+ "<!-- root -->\n",
+ "<g id=\"node1\" class=\"node\">\n",
+ "<title>root</title>\n",
+ "<polygon fill=\"none\" stroke=\"#f4e3c1\" stroke-width=\"2\" points=\"38.1664,-165 76.4999,-196.5 -.1671,-196.5 38.1664,-165\"/>\n",
+ "<text text-anchor=\"middle\" x=\"38.1664\" y=\"-182.9\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">root</text>\n",
+ "</g>\n",
+ "<!-- 0 -->\n",
+ "<g id=\"node2\" class=\"node\">\n",
+ "<title>0</title>\n",
+ "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"65.1664,-14.5442 65.1664,-29.4558 49.3502,-40 26.9826,-40 11.1664,-29.4558 11.1664,-14.5442 26.9826,-4 49.3502,-4 65.1664,-14.5442\"/>\n",
+ "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"69.1664,-12.4034 69.1664,-31.5966 50.5613,-44 25.7715,-44 7.1664,-31.5966 7.1664,-12.4034 25.7715,0 50.5613,0 69.1664,-12.4034\"/>\n",
+ "</g>\n",
+ "<!-- root->0 -->\n",
+ "<g id=\"edge1\" class=\"edge\">\n",
+ "<title>root->0</title>\n",
+ "<path fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"1,5\" d=\"M38.1664,-164.8956C38.1664,-136.9146 38.1664,-87.2613 38.1664,-54.4833\"/>\n",
+ "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"41.6665,-54.0698 38.1664,-44.0699 34.6665,-54.0699 41.6665,-54.0698\"/>\n",
+ "<text text-anchor=\"middle\" x=\"72.6664\" y=\"-101.4\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">INITIALISATION</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>"
+ ],
+ "text/plain": [
+ "<Dot visualization: state_space []>"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot state_space"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+ "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+ "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
+ " -->\n",
+ "<!-- Title: g Pages: 1 -->\n",
+ "<svg width=\"124pt\" height=\"62pt\"\n",
+ " viewBox=\"0.00 0.00 123.97 61.74\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 57.7401)\">\n",
+ "<title>g</title>\n",
+ "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-57.7401 119.9655,-57.7401 119.9655,4 -4,4\"/>\n",
+ "<!-- Noderoot -->\n",
+ "<g id=\"node1\" class=\"node\">\n",
+ "<title>Noderoot</title>\n",
+ "<ellipse fill=\"#b3ee3a\" stroke=\"#000000\" cx=\"57.9828\" cy=\"-26.8701\" rx=\"57.9655\" ry=\"26.7407\"/>\n",
+ "<text text-anchor=\"middle\" x=\"57.9828\" y=\"-30.6701\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">(TRUE:BOOL)</text>\n",
+ "<text text-anchor=\"middle\" x=\"57.9828\" y=\"-15.6701\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\"> true</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>"
+ ],
+ "text/plain": [
+ "<Dot visualization: invariant []>"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot invariant"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+ "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+ "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
+ " -->\n",
+ "<!-- Title: state Pages: 1 -->\n",
+ "<svg width=\"117pt\" height=\"218pt\"\n",
+ " viewBox=\"0.00 0.00 117.00 218.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 214)\">\n",
+ "<title>state</title>\n",
+ "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-214 113,-214 113,4 -4,4\"/>\n",
+ "<!-- 3 -->\n",
+ "<g id=\"node1\" class=\"node\">\n",
+ "<title>3</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"95,-210 41,-210 41,-174 95,-174 95,-210\"/>\n",
+ "<text text-anchor=\"middle\" x=\"68\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">3</text>\n",
+ "</g>\n",
+ "<!-- 1 -->\n",
+ "<g id=\"node2\" class=\"node\">\n",
+ "<title>1</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"54,-123 0,-123 0,-87 54,-87 54,-123\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "</g>\n",
+ "<!-- 3->1 -->\n",
+ "<g id=\"edge1\" class=\"edge\">\n",
+ "<title>3->1</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M57.4067,-173.9028C54.2401,-168.2424 50.8543,-161.9262 48,-156 44.3773,-148.4784 40.7864,-140.1646 37.6258,-132.4706\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"40.861,-131.1345 33.8825,-123.1626 34.3665,-133.7464 40.861,-131.1345\"/>\n",
+ "<text text-anchor=\"middle\" x=\"62\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">[2,3,1]</text>\n",
+ "</g>\n",
+ "<!-- 2 -->\n",
+ "<g id=\"node3\" class=\"node\">\n",
+ "<title>2</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"85,-36 31,-36 31,0 85,0 85,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"58\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
+ "</g>\n",
+ "<!-- 1->2 -->\n",
+ "<g id=\"edge3\" class=\"edge\">\n",
+ "<title>1->2</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M33.4232,-86.9735C37.6629,-75.0751 43.3015,-59.2508 48.1083,-45.7606\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"51.5254,-46.598 51.585,-36.0034 44.9315,-44.2484 51.5254,-46.598\"/>\n",
+ "<text text-anchor=\"middle\" x=\"59\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">[2,3,1]</text>\n",
+ "</g>\n",
+ "<!-- 2->3 -->\n",
+ "<g id=\"edge2\" class=\"edge\">\n",
+ "<title>2->3</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M69.0675,-36.0594C71.9014,-41.6127 74.5551,-47.8793 76,-54 86.4155,-98.1206 80.9466,-110.9374 76,-156 75.7188,-158.5616 75.3283,-161.2076 74.8697,-163.8482\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"71.4058,-163.3196 72.8517,-173.8153 78.2666,-164.7087 71.4058,-163.3196\"/>\n",
+ "<text text-anchor=\"middle\" x=\"95\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">[2,3,1]</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>"
+ ],
+ "text/plain": [
+ "<Dot visualization: expr_as_graph [{(1,2),(2,3),(3,1)}]>"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot expr_as_graph {1|->2, 2|->3, 3|->1}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+ "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+ "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
+ " -->\n",
+ "<!-- Title: g Pages: 1 -->\n",
+ "<svg width=\"332pt\" height=\"209pt\"\n",
+ " viewBox=\"0.00 0.00 332.00 209.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 205)\">\n",
+ "<title>g</title>\n",
+ "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-205 328,-205 328,4 -4,4\"/>\n",
+ "<!-- Noderoot -->\n",
+ "<g id=\"node1\" class=\"node\">\n",
+ "<title>Noderoot</title>\n",
+ "<ellipse fill=\"#b3ee3a\" stroke=\"#000000\" cx=\"27\" cy=\"-47\" rx=\"27\" ry=\"26.7407\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-50.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">=</text>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-35.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\"> true</text>\n",
+ "</g>\n",
+ "<!-- Node1 -->\n",
+ "<g id=\"node2\" class=\"node\">\n",
+ "<title>Node1</title>\n",
+ "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"144,-94 90,-94 90,-56 144,-56 144,-94\"/>\n",
+ "<text text-anchor=\"middle\" x=\"117\" y=\"-78.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">+</text>\n",
+ "<text text-anchor=\"middle\" x=\"117\" y=\"-63.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\"> 2</text>\n",
+ "</g>\n",
+ "<!-- Node1->Noderoot -->\n",
+ "<g id=\"edge1\" class=\"edge\">\n",
+ "<title>Node1->Noderoot</title>\n",
+ "<path fill=\"none\" stroke=\"#000000\" d=\"M89.997,-66.5991C81.4036,-63.9256 71.7618,-60.9259 62.6543,-58.0924\"/>\n",
+ "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"63.6446,-54.7351 53.0563,-55.1064 61.5651,-61.4191 63.6446,-54.7351\"/>\n",
+ "</g>\n",
+ "<!-- Node2 -->\n",
+ "<g id=\"node3\" class=\"node\">\n",
+ "<title>Node2</title>\n",
+ "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"234,-149 180,-149 180,-111 234,-111 234,-149\"/>\n",
+ "<text text-anchor=\"middle\" x=\"207\" y=\"-133.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">*</text>\n",
+ "<text text-anchor=\"middle\" x=\"207\" y=\"-118.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\"> 2</text>\n",
+ "</g>\n",
+ "<!-- Node2->Node1 -->\n",
+ "<g id=\"edge2\" class=\"edge\">\n",
+ "<title>Node2->Node1</title>\n",
+ "<path fill=\"none\" stroke=\"#000000\" d=\"M179.997,-113.4982C171.5314,-108.3248 162.0484,-102.5296 153.0611,-97.0373\"/>\n",
+ "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"154.6529,-93.9083 144.295,-91.6803 151.0027,-99.8813 154.6529,-93.9083\"/>\n",
+ "</g>\n",
+ "<!-- Node3 -->\n",
+ "<g id=\"node4\" class=\"node\">\n",
+ "<title>Node3</title>\n",
+ "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"324,-201 270,-201 270,-165 324,-165 324,-201\"/>\n",
+ "<text text-anchor=\"middle\" x=\"297\" y=\"-179.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "</g>\n",
+ "<!-- Node3->Node2 -->\n",
+ "<g id=\"edge3\" class=\"edge\">\n",
+ "<title>Node3->Node2</title>\n",
+ "<path fill=\"none\" stroke=\"#000000\" d=\"M269.997,-167.0983C261.5314,-162.1129 252.0484,-156.5285 243.0611,-151.236\"/>\n",
+ "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"244.6879,-148.1322 234.295,-146.0737 241.1358,-154.1641 244.6879,-148.1322\"/>\n",
+ "</g>\n",
+ "<!-- Node4 -->\n",
+ "<g id=\"node5\" class=\"node\">\n",
+ "<title>Node4</title>\n",
+ "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"324,-147 270,-147 270,-111 324,-111 324,-147\"/>\n",
+ "<text text-anchor=\"middle\" x=\"297\" y=\"-125.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
+ "</g>\n",
+ "<!-- Node4->Node2 -->\n",
+ "<g id=\"edge4\" class=\"edge\">\n",
+ "<title>Node4->Node2</title>\n",
+ "<path fill=\"none\" stroke=\"#000000\" d=\"M269.997,-129.3C261.9723,-129.3892 253.0335,-129.4885 244.4691,-129.5837\"/>\n",
+ "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"244.2554,-126.0857 234.295,-129.6967 244.3333,-133.0853 244.2554,-126.0857\"/>\n",
+ "</g>\n",
+ "<!-- Node5 -->\n",
+ "<g id=\"node6\" class=\"node\">\n",
+ "<title>Node5</title>\n",
+ "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"234,-93 180,-93 180,-55 234,-55 234,-93\"/>\n",
+ "<text text-anchor=\"middle\" x=\"207\" y=\"-77.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">/</text>\n",
+ "<text text-anchor=\"middle\" x=\"207\" y=\"-62.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\"> 0</text>\n",
+ "</g>\n",
+ "<!-- Node5->Node1 -->\n",
+ "<g id=\"edge5\" class=\"edge\">\n",
+ "<title>Node5->Node1</title>\n",
+ "<path fill=\"none\" stroke=\"#000000\" d=\"M179.997,-74.3C171.9723,-74.3892 163.0335,-74.4885 154.4691,-74.5837\"/>\n",
+ "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"154.2554,-71.0857 144.295,-74.6967 154.3333,-78.0853 154.2554,-71.0857\"/>\n",
+ "</g>\n",
+ "<!-- Node6 -->\n",
+ "<g id=\"node7\" class=\"node\">\n",
+ "<title>Node6</title>\n",
+ "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"324,-93 270,-93 270,-57 324,-57 324,-93\"/>\n",
+ "<text text-anchor=\"middle\" x=\"297\" y=\"-71.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">3</text>\n",
+ "</g>\n",
+ "<!-- Node6->Node5 -->\n",
+ "<g id=\"edge6\" class=\"edge\">\n",
+ "<title>Node6->Node5</title>\n",
+ "<path fill=\"none\" stroke=\"#000000\" d=\"M269.997,-74.7C261.9723,-74.6108 253.0335,-74.5115 244.4691,-74.4163\"/>\n",
+ "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"244.3333,-70.9147 234.295,-74.3033 244.2554,-77.9143 244.3333,-70.9147\"/>\n",
+ "</g>\n",
+ "<!-- Node7 -->\n",
+ "<g id=\"node8\" class=\"node\">\n",
+ "<title>Node7</title>\n",
+ "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"324,-39 270,-39 270,-3 324,-3 324,-39\"/>\n",
+ "<text text-anchor=\"middle\" x=\"297\" y=\"-17.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">4</text>\n",
+ "</g>\n",
+ "<!-- Node7->Node5 -->\n",
+ "<g id=\"edge7\" class=\"edge\">\n",
+ "<title>Node7->Node5</title>\n",
+ "<path fill=\"none\" stroke=\"#000000\" d=\"M269.997,-36.9017C261.5314,-41.8871 252.0484,-47.4715 243.0611,-52.764\"/>\n",
+ "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"241.1358,-49.8359 234.295,-57.9263 244.6879,-55.8678 241.1358,-49.8359\"/>\n",
+ "</g>\n",
+ "<!-- Node8 -->\n",
+ "<g id=\"node9\" class=\"node\">\n",
+ "<title>Node8</title>\n",
+ "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"144,-38 90,-38 90,0 144,0 144,-38\"/>\n",
+ "<text text-anchor=\"middle\" x=\"117\" y=\"-22.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">card</text>\n",
+ "<text text-anchor=\"middle\" x=\"117\" y=\"-7.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\"> 2</text>\n",
+ "</g>\n",
+ "<!-- Node8->Noderoot -->\n",
+ "<g id=\"edge8\" class=\"edge\">\n",
+ "<title>Node8->Noderoot</title>\n",
+ "<path fill=\"none\" stroke=\"#000000\" d=\"M89.997,-27.4009C81.4036,-30.0744 71.7618,-33.0741 62.6543,-35.9076\"/>\n",
+ "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"61.5651,-32.5809 53.0563,-38.8936 63.6446,-39.2649 61.5651,-32.5809\"/>\n",
+ "</g>\n",
+ "<!-- Node9 -->\n",
+ "<g id=\"node10\" class=\"node\">\n",
+ "<title>Node9</title>\n",
+ "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"234,-37 180,-37 180,-1 234,-1 234,-37\"/>\n",
+ "<text text-anchor=\"middle\" x=\"207\" y=\"-15.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{1,2}</text>\n",
+ "</g>\n",
+ "<!-- Node9->Node8 -->\n",
+ "<g id=\"edge9\" class=\"edge\">\n",
+ "<title>Node9->Node8</title>\n",
+ "<path fill=\"none\" stroke=\"#000000\" d=\"M179.997,-19C171.9723,-19 163.0335,-19 154.4691,-19\"/>\n",
+ "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"154.295,-15.5001 144.295,-19 154.2949,-22.5001 154.295,-15.5001\"/>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>"
+ ],
+ "text/plain": [
+ "<Dot visualization: formula_tree [1*2+3/4=card({1,2})]>"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot formula_tree 1*2 + 3/4 = card({1, 2})"
+ ]
+ }
+ ],
+ "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": 2
+}
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index 7fa6e85..c71c8c1 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -25,6 +25,7 @@ import de.prob2.jupyter.commands.Command;
import de.prob2.jupyter.commands.CommandExecutionException;
import de.prob2.jupyter.commands.CommandUtils;
import de.prob2.jupyter.commands.ConstantsCommand;
+import de.prob2.jupyter.commands.DotCommand;
import de.prob2.jupyter.commands.EvalCommand;
import de.prob2.jupyter.commands.ExecCommand;
import de.prob2.jupyter.commands.GroovyCommand;
@@ -148,6 +149,7 @@ public final class ProBKernel extends BaseKernel {
this.commands.put(":exec", injector.getInstance(ExecCommand.class));
this.commands.put(":constants", injector.getInstance(ConstantsCommand.class));
this.commands.put(":init", injector.getInstance(InitialiseCommand.class));
+ this.commands.put(":dot", injector.getInstance(DotCommand.class));
this.commands.put(":assert", injector.getInstance(AssertCommand.class));
this.commands.put(":time", injector.getInstance(TimeCommand.class));
this.commands.put(":groovy", injector.getInstance(GroovyCommand.class));
diff --git a/src/main/java/de/prob2/jupyter/commands/DotCommand.java b/src/main/java/de/prob2/jupyter/commands/DotCommand.java
new file mode 100644
index 0000000..6d8d556
--- /dev/null
+++ b/src/main/java/de/prob2/jupyter/commands/DotCommand.java
@@ -0,0 +1,119 @@
+package de.prob2.jupyter.commands;
+
+import java.io.IOException;
+import java.io.UncheckedIOException;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.util.Collections;
+import java.util.List;
+import java.util.regex.Matcher;
+import java.util.stream.Collectors;
+import java.util.stream.Stream;
+
+import com.google.inject.Inject;
+
+import de.prob.animator.command.GetAllDotCommands;
+import de.prob.animator.command.GetSvgForVisualizationCommand;
+import de.prob.animator.domainobjects.DynamicCommandItem;
+import de.prob.animator.domainobjects.FormulaExpand;
+import de.prob.animator.domainobjects.IEvalElement;
+import de.prob.statespace.AnimationSelector;
+import de.prob.statespace.Trace;
+
+import de.prob2.jupyter.ProBKernel;
+import de.prob2.jupyter.UserErrorException;
+
+import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
+import io.github.spencerpark.jupyter.kernel.display.DisplayData;
+
+import org.jetbrains.annotations.NotNull;
+
+public final class DotCommand implements Command {
+ private final @NotNull AnimationSelector animationSelector;
+
+ @Inject
+ private DotCommand(final @NotNull AnimationSelector animationSelector) {
+ super();
+
+ this.animationSelector = animationSelector;
+ }
+
+ @Override
+ public @NotNull String getSyntax() {
+ return ":dot COMMAND [FORMULA]";
+ }
+
+ @Override
+ public @NotNull String getShortHelp() {
+ return "Execute and show a dot visualization.";
+ }
+
+ @Override
+ public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
+ final List<String> split = CommandUtils.splitArgs(argString, 2);
+ assert !split.isEmpty();
+ final String command = split.get(0);
+ final List<IEvalElement> args;
+ if (split.size() > 1) {
+ args = Collections.singletonList(this.animationSelector.getCurrentTrace().getModel().parseFormula(split.get(1), FormulaExpand.EXPAND));
+ } else {
+ args = Collections.emptyList();
+ }
+
+ final Trace trace = this.animationSelector.getCurrentTrace();
+ final GetAllDotCommands cmd1 = new GetAllDotCommands(trace.getCurrentState());
+ trace.getStateSpace().execute(cmd1);
+ final DynamicCommandItem item = cmd1.getCommands().stream()
+ .filter(i -> command.equals(i.getCommand()))
+ .findAny()
+ .orElseThrow(() -> new UserErrorException("No such dot command: " + command));
+
+ final Path outPath;
+ try {
+ outPath = Files.createTempFile(null, "svg");
+ } catch (final IOException e) {
+ throw new UncheckedIOException("Failed to create temp file", e);
+ }
+ final GetSvgForVisualizationCommand cmd2 = new GetSvgForVisualizationCommand(trace.getCurrentState(), item, outPath.toFile(), args);
+ trace.getStateSpace().execute(cmd2);
+ final String svg;
+ try (final Stream<String> lines = Files.lines(outPath)) {
+ svg = lines.collect(Collectors.joining("\n"));
+ } catch (final IOException e) {
+ throw new UncheckedIOException("Failed to read dot output", e);
+ }
+ final DisplayData result = new DisplayData(String.format("<Dot visualization: %s %s>", command, args));
+ result.putSVG(svg);
+ return result;
+ }
+
+ @Override
+ public @NotNull ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+ final int cmdNameEnd;
+ final Matcher argSplitMatcher = CommandUtils.ARG_SPLIT_PATTERN.matcher(argString);
+ if (argSplitMatcher.find()) {
+ cmdNameEnd = argSplitMatcher.start();
+ } else {
+ cmdNameEnd = argString.length();
+ }
+
+ if (cmdNameEnd < at) {
+ // Cursor is in the formula part of the arguments, provide B completions.
+ final ReplacementOptions replacements = CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString.substring(cmdNameEnd), at - cmdNameEnd);
+ return CommandUtils.offsetReplacementOptions(replacements, cmdNameEnd);
+ } else {
+ // Cursor is in the first part of the arguments, provide possible command names.
+ final Trace trace = this.animationSelector.getCurrentTrace();
+ final GetAllDotCommands cmd = new GetAllDotCommands(trace.getCurrentState());
+ trace.getStateSpace().execute(cmd);
+ final String prefix = argString.substring(0, at);
+ final List<String> commands = cmd.getCommands().stream()
+ .filter(DynamicCommandItem::isAvailable)
+ .map(DynamicCommandItem::getCommand)
+ .filter(s -> s.startsWith(prefix))
+ .sorted()
+ .collect(Collectors.toList());
+ return new ReplacementOptions(commands, 0, argString.length());
+ }
+ }
+}
--
GitLab