diff --git a/notebooks/tests/dot.ipynb b/notebooks/tests/dot.ipynb index 1d2f627fb545ddd615b5c2abe60d1e3816b2588e..0b94af53aa03a033a534d9fe2ddbde6cca697184 100644 --- a/notebooks/tests/dot.ipynb +++ b/notebooks/tests/dot.ipynb @@ -34,7 +34,7 @@ "* `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\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", + "* `formula_tree` - Formula Tree: Show predicate and sub-expressions as a tree\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" ], @@ -65,7 +65,7 @@ "* `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\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", + "* `formula_tree` - Formula Tree: Show predicate and sub-expressions as a tree\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" ] @@ -96,7 +96,7 @@ } ], "source": [ - ":pref DOT=/opt/local/bin/dot" + ":pref DOT=/usr/local/bin/dot" ] }, { @@ -457,6 +457,178 @@ "cell_type": "code", "execution_count": 9, "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Preference changed: DOT_ENGINE = circo\n" + ] + }, + "execution_count": 9, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":pref DOT_ENGINE=circo" + ] + }, + { + "cell_type": "code", + "execution_count": 10, + "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: state Pages: 1 -->\n", + "<svg width=\"243pt\" height=\"235pt\"\n", + " viewBox=\"0.00 0.00 243.39 234.72\" 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 230.72)\">\n", + "<title>state</title>\n", + "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-230.72 240.386,-230.72 240.386,5 -4,5\"/>\n", + "<!-- 4 -->\n", + "<g id=\"node1\" class=\"node\"><title>4</title>\n", + "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"166.103,-36 112.103,-36 112.103,-0 166.103,-0 166.103,-36\"/>\n", + "<text text-anchor=\"middle\" x=\"139.103\" y=\"-13.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=\"235.386,-131.36 181.386,-131.36 181.386,-95.3602 235.386,-95.3602 235.386,-131.36\"/>\n", + "<text text-anchor=\"middle\" x=\"208.386\" y=\"-109.16\" 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=\"M146.096,-36.3277C154.534,-50.7471 168.707,-70.9379 181.466,-87.0605\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"178.949,-89.5137 187.971,-95.0686 184.383,-85.1 178.949,-89.5137\"/>\n", + "<text text-anchor=\"middle\" x=\"151.781\" y=\"-65.4941\" 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=\"M159.485,-36.2526C171.39,-50.4825 185.902,-70.3727 196.114,-86.4179\"/>\n", + "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"193.373,-88.6448 201.577,-95.3489 199.344,-84.992 193.373,-88.6448\"/>\n", + "<text text-anchor=\"middle\" x=\"169.799\" y=\"-63.1352\" 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=\"54,-190.296 1.42109e-14,-190.296 1.42109e-14,-154.296 54,-154.296 54,-190.296\"/>\n", + "<text text-anchor=\"middle\" x=\"27\" y=\"-168.096\" 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=\"M126.024,-36.0017C106.385,-63.0326 69.1556,-114.274 46.3626,-145.646\"/>\n", + "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"43.3895,-143.783 40.3432,-153.931 49.0526,-147.898 43.3895,-143.783\"/>\n", + "<text text-anchor=\"middle\" x=\"94.1931\" y=\"-92.6237\" 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=\"54,-72.4243 0,-72.4243 0,-36.4243 54,-36.4243 54,-72.4243\"/>\n", + "<text text-anchor=\"middle\" x=\"27\" y=\"-50.2243\" 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=\"M111.966,-26.8173C97.6137,-31.4806 79.779,-37.2754 64.1603,-42.3502\"/>\n", + "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"62.7045,-39.143 54.2756,-45.562 64.8677,-45.8004 62.7045,-39.143\"/>\n", + "<text text-anchor=\"middle\" x=\"91.063\" y=\"-40.3838\" 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=\"M181.277,-117.045C149.974,-124.882 98.3616,-141.388 63.5383,-154.508\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"62.2655,-151.247 54.1924,-158.108 64.7821,-157.779 62.2655,-151.247\"/>\n", + "<text text-anchor=\"middle\" x=\"125.407\" y=\"-142.576\" 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=\"M181.217,-127.538C150.038,-139.854 98.7636,-156.649 63.9685,-166.04\"/>\n", + "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"62.974,-162.682 54.1813,-168.593 64.741,-169.456 62.974,-162.682\"/>\n", + "<text text-anchor=\"middle\" x=\"125.593\" y=\"-152.589\" 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=\"166.103,-226.72 112.103,-226.72 112.103,-190.72 166.103,-190.72 166.103,-226.72\"/>\n", + "<text text-anchor=\"middle\" x=\"139.103\" y=\"-204.52\" 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=\"M139.103,-190.433C139.103,-157.04 139.103,-85.9864 139.103,-46.3026\"/>\n", + "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"142.603,-46.2317 139.103,-36.2317 135.603,-46.2317 142.603,-46.2317\"/>\n", + "<text text-anchor=\"middle\" x=\"133.103\" y=\"-114.168\" 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=\"M152.461,-190.334C162.879,-175.995 177.49,-155.885 189.165,-139.816\"/>\n", + "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"192.257,-141.514 195.303,-131.367 186.594,-137.4 192.257,-141.514\"/>\n", + "<text text-anchor=\"middle\" x=\"162.813\" y=\"-154.875\" 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=\"M111.966,-199.903C97.6137,-195.24 79.779,-189.445 64.1603,-184.37\"/>\n", + "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"64.8677,-180.92 54.2756,-181.158 62.7045,-187.577 64.8677,-180.92\"/>\n", + "<text text-anchor=\"middle\" x=\"85.063\" y=\"-197.937\" 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=\"M126.024,-190.719C106.385,-163.688 69.1556,-112.447 46.3626,-81.0746\"/>\n", + "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"49.0526,-78.8226 40.3432,-72.7896 43.3895,-82.9371 49.0526,-78.8226\"/>\n", + "<text text-anchor=\"middle\" x=\"78.1931\" y=\"-137.697\" 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=\"M54.1553,-63.2476C85.368,-73.3892 136.758,-90.0869 171.557,-101.394\"/>\n", + "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"170.749,-104.811 181.342,-104.573 172.913,-98.154 170.749,-104.811\"/>\n", + "<text text-anchor=\"middle\" x=\"115.856\" y=\"-68.1207\" 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=\"M27,-72.5835C27,-91.5634 27,-121.61 27,-143.764\"/>\n", + "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"23.5001,-143.922 27,-153.922 30.5001,-143.922 23.5001,-143.922\"/>\n", + "<text text-anchor=\"middle\" x=\"33\" y=\"-103.974\" 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": 10, + "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": 11, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Preference changed: DOT_ENGINE = dot\n" + ] + }, + "execution_count": 11, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":pref DOT_ENGINE=dot" + ] + }, + { + "cell_type": "code", + "execution_count": 12, + "metadata": {}, "outputs": [ { "data": { @@ -579,7 +751,7 @@ "<Dot visualization: formula_tree [1*2+3/4=card({1,2})]>" ] }, - "execution_count": 9, + "execution_count": 12, "metadata": {}, "output_type": "execute_result" } @@ -587,6 +759,13 @@ "source": [ ":dot formula_tree 1*2 + 3/4 = card({1, 2})" ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": {