From 812e1ac5280f6dfe96f23c328deb899d8de9967a Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@cs.uni-duesseldorf.de>
Date: Thu, 5 Jul 2018 16:45:32 +0200
Subject: [PATCH] add expr as graph example with two relations
---
notebooks/tests/dot.ipynb | 420 +++++++++++++++++++++++---------------
1 file changed, 261 insertions(+), 159 deletions(-)
diff --git a/notebooks/tests/dot.ipynb b/notebooks/tests/dot.ipynb
index c0bd454..1d2f627 100644
--- a/notebooks/tests/dot.ipynb
+++ b/notebooks/tests/dot.ipynb
@@ -33,7 +33,7 @@
"* `enable_graph` - Enable Graph: Show enabling graph of events\n",
"* `dependence_graph` - Dependence Graph: Show dependence graph of events\n",
"* `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS\n",
- "* `expr_as_graph` - Expression Graph: Show expression value as a graph (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)\n",
+ "* `expr_as_graph` - Expression Graph: Show expression value as a graph\n",
"* `formula_tree` - Formula Tree: Show predicate and sub-expressions as a tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)\n",
"* `transition_diagram` - Transition Diagram Projection: Project state space onto expression values\n",
"* `predicate_dependency` - Predicate Dependency Graph: Show dependence graph of conjuncts of a predicate\n"
@@ -64,7 +64,7 @@
"* `enable_graph` - Enable Graph: Show enabling graph of events\n",
"* `dependence_graph` - Dependence Graph: Show dependence graph of events\n",
"* `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS\n",
- "* `expr_as_graph` - Expression Graph: Show expression value as a graph (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)\n",
+ "* `expr_as_graph` - Expression Graph: Show expression value as a graph\n",
"* `formula_tree` - Formula Tree: Show predicate and sub-expressions as a tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)\n",
"* `transition_diagram` - Transition Diagram Projection: Project state space onto expression values\n",
"* `predicate_dependency` - Predicate Dependency Graph: Show dependence graph of conjuncts of a predicate\n"
@@ -87,7 +87,7 @@
{
"data": {
"text/plain": [
- "Preference changed: DOT = /opt/local/bin/dot\n"
+ "Preference changed: DOT = /usr/local/bin/dot\n"
]
},
"execution_count": 2,
@@ -110,19 +110,18 @@
"<?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",
+ "<!-- Generated by graphviz version 2.28.0 (20110509.1545)\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",
+ "<svg width=\"98pt\" height=\"54pt\"\n",
+ " viewBox=\"0.00 0.00 98.00 54.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 50)\">\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",
+ "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-50 95,-50 95,5 -4,5\"/>\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 id=\"node1\" class=\"node\"><title>root</title>\n",
+ "<polygon fill=\"none\" stroke=\"#f4e3c1\" stroke-width=\"2\" points=\"45,-0.699556 90.1952,-34.1502 -0.195189,-34.1502 45,-0.699556\"/>\n",
+ "<text text-anchor=\"middle\" x=\"45\" y=\"-19.4\" font-family=\"Times,serif\" font-size=\"12.00\">root</text>\n",
"</g>\n",
"</g>\n",
"</svg>"
@@ -173,32 +172,29 @@
"<?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",
+ "<!-- Generated by graphviz version 2.28.0 (20110509.1545)\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",
+ "<svg width=\"145pt\" height=\"220pt\"\n",
+ " viewBox=\"0.00 0.00 144.95 220.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 216)\">\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",
+ "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-216 141.951,-216 141.951,5 -4,5\"/>\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 id=\"node1\" class=\"node\"><title>root</title>\n",
+ "<polygon fill=\"none\" stroke=\"#f4e3c1\" stroke-width=\"2\" points=\"45,-166.7 90.1952,-200.15 -0.195189,-200.15 45,-166.7\"/>\n",
+ "<text text-anchor=\"middle\" x=\"45\" y=\"-185.4\" font-family=\"Times,serif\" font-size=\"12.00\">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 id=\"node3\" class=\"node\"><title>0</title>\n",
+ "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"72,-14.5442 72,-29.4558 56.1838,-40 33.8162,-40 18,-29.4558 18,-14.5442 33.8162,-4 56.1838,-4 72,-14.5442\"/>\n",
+ "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"76,-12.4034 76,-31.5966 57.3949,-44 32.6051,-44 14,-31.5966 14,-12.4034 32.6051,-3.55271e-15 57.3949,-0 76,-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 id=\"edge2\" class=\"edge\"><title>root->0</title>\n",
+ "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"1,5\" d=\"M45,-166.429C45,-137.862 45,-87.272 45,-54.4477\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"48.5001,-54.0544 45,-44.0545 41.5001,-54.0545 48.5001,-54.0544\"/>\n",
+ "<text text-anchor=\"middle\" x=\"90.9756\" y=\"-101.4\" font-family=\"Times,serif\" font-size=\"12.00\">INITIALISATION</text>\n",
"</g>\n",
"</g>\n",
"</svg>"
@@ -227,20 +223,19 @@
"<?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",
+ "<!-- Generated by graphviz version 2.28.0 (20110509.1545)\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",
+ "<svg width=\"156pt\" height=\"66pt\"\n",
+ " viewBox=\"0.00 0.00 156.00 66.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 62)\">\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",
+ "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-62 153,-62 153,5 -4,5\"/>\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 id=\"node1\" class=\"node\"><title>Noderoot</title>\n",
+ "<ellipse fill=\"#b3ee3a\" stroke=\"black\" cx=\"74\" cy=\"-29\" rx=\"73.3839\" ry=\"29.3315\"/>\n",
+ "<text text-anchor=\"middle\" x=\"74\" y=\"-33.2\" font-family=\"Times,serif\" font-size=\"14.00\">(TRUE:BOOL)</text>\n",
+ "<text text-anchor=\"middle\" x=\"74\" y=\"-16.4\" font-family=\"Times,serif\" font-size=\"14.00\"> true</text>\n",
"</g>\n",
"</g>\n",
"</svg>"
@@ -269,52 +264,46 @@
"<?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",
+ "<!-- Generated by graphviz version 2.28.0 (20110509.1545)\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",
+ "<svg width=\"127pt\" height=\"224pt\"\n",
+ " viewBox=\"0.00 0.00 127.32 224.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 220)\">\n",
"<title>state</title>\n",
- "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-214 113,-214 113,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-220 124.321,-220 124.321,5 -4,5\"/>\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 id=\"node1\" class=\"node\"><title>3</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"90,-216 36,-216 36,-180 90,-180 90,-216\"/>\n",
+ "<text text-anchor=\"middle\" x=\"63\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">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 id=\"node3\" class=\"node\"><title>1</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"54,-126 0,-126 0,-90 54,-90 54,-126\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">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 id=\"edge2\" class=\"edge\"><title>3->1</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M49.2014,-179.992C45.3133,-174.512 41.4054,-168.238 38.6788,-162 35.1373,-153.898 32.6229,-144.614 30.8585,-136.103\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"34.2966,-135.447 29.0596,-126.237 27.4101,-136.703 34.2966,-135.447\"/>\n",
+ "<text text-anchor=\"middle\" x=\"56.6606\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">[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 id=\"node4\" class=\"node\"><title>2</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"88,-36 34,-36 34,-0 88,-0 88,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"61\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">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 id=\"edge6\" class=\"edge\"><title>1->2</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M29.219,-89.8308C30.9674,-79.2243 33.9239,-65.4924 38.6788,-54 39.9462,-50.9367 41.4789,-47.8441 43.1405,-44.8318\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"46.2118,-46.5164 48.3761,-36.145 40.2165,-42.903 46.2118,-46.5164\"/>\n",
+ "<text text-anchor=\"middle\" x=\"56.6606\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">[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 id=\"edge4\" class=\"edge\"><title>2->3</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M70.075,-36.3529C72.4959,-41.8463 74.7771,-48.0422 76,-54 85.6512,-101.02 84.4904,-114.757 76,-162 75.5116,-164.717 74.8259,-167.499 74.022,-170.249\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"70.6475,-169.301 70.7342,-179.896 77.2732,-171.56 70.6475,-169.301\"/>\n",
+ "<text text-anchor=\"middle\" x=\"100.661\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">[2,3,1]</text>\n",
"</g>\n",
"</g>\n",
"</svg>"
@@ -343,132 +332,245 @@
"<?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",
+ "<!-- Generated by graphviz version 2.28.0 (20110509.1545)\n",
+ " -->\n",
+ "<!-- Title: state Pages: 1 -->\n",
+ "<svg width=\"219pt\" height=\"404pt\"\n",
+ " viewBox=\"0.00 0.00 218.84 404.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 400)\">\n",
+ "<title>state</title>\n",
+ "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-400 215.838,-400 215.838,5 -4,5\"/>\n",
+ "<!-- 4 -->\n",
+ "<g id=\"node1\" class=\"node\"><title>4</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"124.948,-306 70.9475,-306 70.9475,-270 124.948,-270 124.948,-306\"/>\n",
+ "<text text-anchor=\"middle\" x=\"97.9475\" y=\"-283.8\" font-family=\"Times,serif\" font-size=\"14.00\">4</text>\n",
+ "</g>\n",
+ "<!-- 2 -->\n",
+ "<g id=\"node3\" class=\"node\"><title>2</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"58.9475,-126 4.94753,-126 4.94753,-90 58.9475,-90 58.9475,-126\"/>\n",
+ "<text text-anchor=\"middle\" x=\"31.9475\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
+ "</g>\n",
+ "<!-- 4->2 -->\n",
+ "<g id=\"edge2\" class=\"edge\"><title>4->2</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M79.4272,-269.961C66.2891,-256.654 49.5582,-236.956 41.1817,-216 30.8927,-190.26 29.44,-158.329 30.0304,-136.079\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"33.5307,-136.142 30.4545,-126.004 26.5369,-135.848 33.5307,-136.142\"/>\n",
+ "<text text-anchor=\"middle\" x=\"52.8304\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">half</text>\n",
+ "</g>\n",
+ "<!-- 4->2 -->\n",
+ "<g id=\"edge16\" class=\"edge\"><title>4->2</title>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M70.9473,-272.847C51.4272,-260.789 26.9824,-241.382 18.0569,-216 8.83003,-189.761 14.9797,-157.963 21.7727,-135.882\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"25.1635,-136.776 24.9901,-126.183 18.5195,-134.573 25.1635,-136.776\"/>\n",
+ "<text text-anchor=\"middle\" x=\"24.3928\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
+ "</g>\n",
+ "<!-- 1 -->\n",
+ "<g id=\"node5\" class=\"node\"><title>1</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"129.948,-36 75.9475,-36 75.9475,-0 129.948,-0 129.948,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"102.948\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- 4->1 -->\n",
+ "<g id=\"edge18\" class=\"edge\"><title>4->1</title>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M109.897,-269.857C118.764,-256.032 130.12,-235.711 134.948,-216 149.703,-155.756 128.178,-83.4427 113.895,-45.3934\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"117.149,-44.1048 110.27,-36.0468 110.623,-46.6358 117.149,-44.1048\"/>\n",
+ "<text text-anchor=\"middle\" x=\"144.393\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
+ "</g>\n",
+ "<!-- 3 -->\n",
+ "<g id=\"node9\" class=\"node\"><title>3</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"125.948,-216 71.9475,-216 71.9475,-180 125.948,-180 125.948,-216\"/>\n",
+ "<text text-anchor=\"middle\" x=\"98.9475\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
+ "</g>\n",
+ "<!-- 4->3 -->\n",
+ "<g id=\"edge14\" class=\"edge\"><title>4->3</title>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M98.1451,-269.614C98.2857,-257.24 98.4774,-240.369 98.6382,-226.22\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"102.14,-226.09 98.7538,-216.05 95.1403,-226.01 102.14,-226.09\"/>\n",
+ "<text text-anchor=\"middle\" x=\"104.393\" y=\"-238.8\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
+ "</g>\n",
+ "<!-- 2->1 -->\n",
+ "<g id=\"edge4\" class=\"edge\"><title>2->1</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M42.193,-89.6496C48.8044,-78.9749 57.8815,-65.2349 67.1817,-54 70.1283,-50.4405 73.3943,-46.8493 76.7199,-43.3931\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"79.4053,-45.6571 83.9943,-36.1077 74.4518,-40.7111 79.4053,-45.6571\"/>\n",
+ "<text text-anchor=\"middle\" x=\"78.8304\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">half</text>\n",
+ "</g>\n",
+ "<!-- 2->1 -->\n",
+ "<g id=\"edge24\" class=\"edge\"><title>2->1</title>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M30.8599,-89.8335C30.9946,-78.7035 32.8318,-64.3952 40.0569,-54 46.609,-44.5732 56.5585,-37.4047 66.6229,-32.0877\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"68.2814,-35.1745 75.8038,-27.7137 65.2706,-28.8551 68.2814,-35.1745\"/>\n",
+ "<text text-anchor=\"middle\" x=\"46.3928\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
+ "</g>\n",
+ "<!-- 5 -->\n",
+ "<g id=\"node6\" class=\"node\"><title>5</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"164.948,-396 110.948,-396 110.948,-360 164.948,-360 164.948,-396\"/>\n",
+ "<text text-anchor=\"middle\" x=\"137.948\" y=\"-373.8\" font-family=\"Times,serif\" font-size=\"14.00\">5</text>\n",
+ "</g>\n",
+ "<!-- 5->4 -->\n",
+ "<g id=\"edge6\" class=\"edge\"><title>5->4</title>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M130.045,-359.614C124.31,-346.998 116.45,-329.705 109.943,-315.391\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"113.022,-313.706 105.698,-306.05 106.65,-316.602 113.022,-313.706\"/>\n",
+ "<text text-anchor=\"middle\" x=\"127.393\" y=\"-328.8\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
+ "</g>\n",
+ "<!-- 5->2 -->\n",
+ "<g id=\"edge10\" class=\"edge\"><title>5->2</title>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M111.655,-359.97C81.5625,-338.779 33.7685,-299.527 13.0569,-252 -6.11999,-207.994 -1.65568,-190.035 11.9475,-144 12.8313,-141.009 14.0135,-137.999 15.3633,-135.067\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"18.5295,-136.566 20.0865,-126.086 12.334,-133.307 18.5295,-136.566\"/>\n",
+ "<text text-anchor=\"middle\" x=\"19.3928\" y=\"-238.8\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
+ "</g>\n",
+ "<!-- 5->1 -->\n",
+ "<g id=\"edge12\" class=\"edge\"><title>5->1</title>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M159.632,-359.929C177.511,-343.78 199.948,-317.781 199.948,-289 199.948,-289 199.948,-289 199.948,-107 199.948,-72.8845 166.628,-48.5304 139.045,-34.2143\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"140.485,-31.0219 129.967,-29.7444 137.393,-37.3019 140.485,-31.0219\"/>\n",
+ "<text text-anchor=\"middle\" x=\"205.393\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
+ "</g>\n",
+ "<!-- 5->3 -->\n",
+ "<g id=\"edge8\" class=\"edge\"><title>5->3</title>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M139.495,-359.637C140.907,-338.206 141.741,-300.818 133.948,-270 129.962,-254.24 122.187,-237.885 114.975,-224.851\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"117.906,-222.925 109.886,-216.002 111.838,-226.415 117.906,-222.925\"/>\n",
+ "<text text-anchor=\"middle\" x=\"144.393\" y=\"-283.8\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
+ "</g>\n",
+ "<!-- 3->2 -->\n",
+ "<g id=\"edge20\" class=\"edge\"><title>3->2</title>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M85.7105,-179.614C75.8278,-166.634 62.1765,-148.704 51.1031,-134.16\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"53.7716,-131.887 44.9291,-126.05 48.2021,-136.127 53.7716,-131.887\"/>\n",
+ "<text text-anchor=\"middle\" x=\"77.3928\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
+ "</g>\n",
+ "<!-- 3->1 -->\n",
+ "<g id=\"edge22\" class=\"edge\"><title>3->1</title>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M99.3311,-179.933C100.027,-148.966 101.503,-83.2989 102.338,-46.1292\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"105.84,-46.0919 102.565,-36.0157 98.8413,-45.9345 105.84,-46.0919\"/>\n",
+ "<text text-anchor=\"middle\" x=\"107.393\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>"
+ ],
+ "text/plain": [
+ "<Dot visualization: expr_as_graph [(\"gt\",{x,y|x:1..5 & y:1..5 & x>y})]>"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot expr_as_graph (\"gt\",{x,y|x:1..5 & y:1..5 & x>y},\"half\",{y,x|x:1..5 & y:1..5 & x+x=y})"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 9,
+ "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.28.0 (20110509.1545)\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",
+ "<svg width=\"336pt\" height=\"215pt\"\n",
+ " viewBox=\"0.00 0.00 336.00 215.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 211)\">\n",
"<title>g</title>\n",
- "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-205 328,-205 328,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-211 333,-211 333,5 -4,5\"/>\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 id=\"node1\" class=\"node\"><title>Noderoot</title>\n",
+ "<ellipse fill=\"#b3ee3a\" stroke=\"black\" cx=\"29\" cy=\"-50\" rx=\"29.3598\" ry=\"29.3315\"/>\n",
+ "<text text-anchor=\"middle\" x=\"29\" y=\"-54.2\" font-family=\"Times,serif\" font-size=\"14.00\">=</text>\n",
+ "<text text-anchor=\"middle\" x=\"29\" y=\"-37.4\" font-family=\"Times,serif\" font-size=\"14.00\"> 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 id=\"node2\" class=\"node\"><title>Node1</title>\n",
+ "<polygon fill=\"white\" stroke=\"black\" points=\"148,-100.602 94,-100.602 94,-59.3981 148,-59.3981 148,-100.602\"/>\n",
+ "<text text-anchor=\"middle\" x=\"121\" y=\"-84.2\" font-family=\"Times,serif\" font-size=\"14.00\">+</text>\n",
+ "<text text-anchor=\"middle\" x=\"121\" y=\"-67.4\" font-family=\"Times,serif\" font-size=\"14.00\"> 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 id=\"edge2\" class=\"edge\"><title>Node1->Noderoot</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M93.9683,-71.3228C85.4283,-68.4761 75.7727,-65.2576 66.5999,-62.2\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"67.5052,-58.8125 56.9115,-58.9705 65.2915,-65.4532 67.5052,-58.8125\"/>\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 id=\"node4\" class=\"node\"><title>Node2</title>\n",
+ "<polygon fill=\"white\" stroke=\"black\" points=\"238,-158.602 184,-158.602 184,-117.398 238,-117.398 238,-158.602\"/>\n",
+ "<text text-anchor=\"middle\" x=\"211\" y=\"-142.2\" font-family=\"Times,serif\" font-size=\"14.00\">*</text>\n",
+ "<text text-anchor=\"middle\" x=\"211\" y=\"-125.4\" font-family=\"Times,serif\" font-size=\"14.00\"> 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 id=\"edge4\" class=\"edge\"><title>Node2->Node1</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M183.597,-120.598C175.08,-114.984 165.51,-108.677 156.498,-102.737\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"158.357,-99.7706 148.081,-97.1898 154.504,-105.615 158.357,-99.7706\"/>\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 id=\"node6\" class=\"node\"><title>Node3</title>\n",
+ "<polygon fill=\"white\" stroke=\"black\" points=\"328,-207 274,-207 274,-171 328,-171 328,-207\"/>\n",
+ "<text text-anchor=\"middle\" x=\"301\" y=\"-184.8\" font-family=\"Times,serif\" font-size=\"14.00\">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 id=\"edge6\" class=\"edge\"><title>Node3->Node2</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M273.597,-173.698C265.168,-168.813 255.707,-163.33 246.776,-158.155\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"248.488,-155.101 238.081,-153.115 244.978,-161.158 248.488,-155.101\"/>\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 id=\"node8\" class=\"node\"><title>Node4</title>\n",
+ "<polygon fill=\"white\" stroke=\"black\" points=\"328,-153 274,-153 274,-117 328,-117 328,-153\"/>\n",
+ "<text text-anchor=\"middle\" x=\"301\" y=\"-130.8\" font-family=\"Times,serif\" font-size=\"14.00\">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 id=\"edge8\" class=\"edge\"><title>Node4->Node2</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M273.597,-135.9C265.607,-136.172 256.689,-136.476 248.176,-136.767\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"247.956,-133.272 238.081,-137.111 248.194,-140.268 247.956,-133.272\"/>\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 id=\"node10\" class=\"node\"><title>Node5</title>\n",
+ "<polygon fill=\"white\" stroke=\"black\" points=\"238,-98.6019 184,-98.6019 184,-57.3981 238,-57.3981 238,-98.6019\"/>\n",
+ "<text text-anchor=\"middle\" x=\"211\" y=\"-82.2\" font-family=\"Times,serif\" font-size=\"14.00\">/</text>\n",
+ "<text text-anchor=\"middle\" x=\"211\" y=\"-65.4\" font-family=\"Times,serif\" font-size=\"14.00\"> 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 id=\"edge10\" class=\"edge\"><title>Node5->Node1</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M183.597,-78.6001C175.607,-78.7817 166.689,-78.9843 158.176,-79.1778\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"157.999,-75.6808 148.081,-79.4072 158.158,-82.679 157.999,-75.6808\"/>\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 id=\"node12\" class=\"node\"><title>Node6</title>\n",
+ "<polygon fill=\"white\" stroke=\"black\" points=\"328,-98 274,-98 274,-62 328,-62 328,-98\"/>\n",
+ "<text text-anchor=\"middle\" x=\"301\" y=\"-75.8\" font-family=\"Times,serif\" font-size=\"14.00\">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 id=\"edge12\" class=\"edge\"><title>Node6->Node5</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M273.597,-79.3999C265.607,-79.2183 256.689,-79.0157 248.176,-78.8222\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"248.158,-75.321 238.081,-78.5928 247.999,-82.3192 248.158,-75.321\"/>\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 id=\"node14\" class=\"node\"><title>Node7</title>\n",
+ "<polygon fill=\"white\" stroke=\"black\" points=\"328,-44 274,-44 274,-8 328,-8 328,-44\"/>\n",
+ "<text text-anchor=\"middle\" x=\"301\" y=\"-21.8\" font-family=\"Times,serif\" font-size=\"14.00\">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 id=\"edge14\" class=\"edge\"><title>Node7->Node5</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M273.597,-41.6017C265.168,-46.5827 255.707,-52.1733 246.776,-57.4503\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"244.91,-54.4879 238.081,-62.5885 248.471,-60.5144 244.91,-54.4879\"/>\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 id=\"node16\" class=\"node\"><title>Node8</title>\n",
+ "<polygon fill=\"white\" stroke=\"black\" points=\"148,-40.6019 94,-40.6019 94,0.601905 148,0.601905 148,-40.6019\"/>\n",
+ "<text text-anchor=\"middle\" x=\"121\" y=\"-24.2\" font-family=\"Times,serif\" font-size=\"14.00\">card</text>\n",
+ "<text text-anchor=\"middle\" x=\"121\" y=\"-7.4\" font-family=\"Times,serif\" font-size=\"14.00\"> 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 id=\"edge16\" class=\"edge\"><title>Node8->Noderoot</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M93.9683,-28.6772C85.4283,-31.5239 75.7727,-34.7424 66.5999,-37.8\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"65.2915,-34.5468 56.9115,-41.0295 67.5052,-41.1875 65.2915,-34.5468\"/>\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 id=\"node18\" class=\"node\"><title>Node9</title>\n",
+ "<polygon fill=\"white\" stroke=\"black\" points=\"238,-38 184,-38 184,-2 238,-2 238,-38\"/>\n",
+ "<text text-anchor=\"middle\" x=\"211\" y=\"-15.8\" font-family=\"Times,serif\" font-size=\"14.00\">{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 id=\"edge18\" class=\"edge\"><title>Node9->Node8</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M183.597,-20C175.607,-20 166.689,-20 158.176,-20\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"158.081,-16.5001 148.081,-20 158.081,-23.5001 158.081,-16.5001\"/>\n",
"</g>\n",
"</g>\n",
"</svg>"
@@ -477,7 +579,7 @@
"<Dot visualization: formula_tree [1*2+3/4=card({1,2})]>"
]
},
- "execution_count": 8,
+ "execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
--
GitLab