diff --git a/notebooks/tests/dot.ipynb b/notebooks/tests/dot.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..5f54acbe074cbb0799c563d7d4a543325e9de65c
--- /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&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>root&#45;&gt;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&#45;&gt;1 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>3&#45;&gt;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&#45;&gt;2 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>1&#45;&gt;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&#45;&gt;3 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>2&#45;&gt;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&#45;&gt;Noderoot -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>Node1&#45;&gt;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&#45;&gt;Node1 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>Node2&#45;&gt;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&#45;&gt;Node2 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>Node3&#45;&gt;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&#45;&gt;Node2 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>Node4&#45;&gt;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&#45;&gt;Node1 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>Node5&#45;&gt;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&#45;&gt;Node5 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>Node6&#45;&gt;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&#45;&gt;Node5 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>Node7&#45;&gt;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&#45;&gt;Noderoot -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>Node8&#45;&gt;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&#45;&gt;Node8 -->\n",
+       "<g id=\"edge9\" class=\"edge\">\n",
+       "<title>Node9&#45;&gt;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 7fa6e8510eaa546ddfb5763bac4f11a2b96b1010..c71c8c123d10013d34fc99d373777d2e3f9324c4 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 0000000000000000000000000000000000000000..6d8d55653e051915e861613ae982046f63080acb
--- /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());
+		}
+	}
+}