diff --git a/mathematical/TransitiveClosure.ipynb b/mathematical/TransitiveClosure.ipynb
index b22706d8b6f5bb66300dc9669fb30167ebbc2688..9ef3b035c97fd8f767cec95ae284f8affb3045f7 100644
--- a/mathematical/TransitiveClosure.ipynb
+++ b/mathematical/TransitiveClosure.ipynb
@@ -1,15 +1,13 @@
{
"cells": [
{
- "cell_type": "code",
- "execution_count": null,
- "id": "d4a6c748",
+ "cell_type": "markdown",
+ "id": "3e5c4f83-91ee-49e3-9255-0741fe8ee31b",
"metadata": {
"vscode": {
"languageId": "plaintext"
}
},
- "outputs": [],
"source": [
"# Modeling transitive closure in B/Event-B\n",
"\n",
@@ -18,7 +16,7 @@
},
{
"cell_type": "code",
- "execution_count": 4,
+ "execution_count": 21,
"id": "964d8a32-2743-4f52-ab27-78dcfe798e11",
"metadata": {
"vscode": {
@@ -32,7 +30,7 @@
"Loaded machine: StateGraph"
]
},
- "execution_count": 4,
+ "execution_count": 21,
"metadata": {},
"output_type": "execute_result"
}
@@ -49,7 +47,7 @@
},
{
"cell_type": "code",
- "execution_count": 6,
+ "execution_count": 22,
"id": "0b8c470d",
"metadata": {
"vscode": {
@@ -64,7 +62,7 @@
"Executed operation: INITIALISATION()"
]
},
- "execution_count": 6,
+ "execution_count": 22,
"metadata": {},
"output_type": "execute_result"
}
@@ -75,7 +73,7 @@
},
{
"cell_type": "code",
- "execution_count": 7,
+ "execution_count": 23,
"id": "949c9b64",
"metadata": {
"vscode": {
@@ -85,12 +83,70 @@
"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 6.0.1 (20220911.1526)\n -->\n<!-- Title: state Pages: 1 -->\n<svg width=\"208pt\" height=\"184pt\"\n viewBox=\"0.00 0.00 208.00 184.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 180)\">\n<title>state</title>\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-180 204,-180 204,4 -4,4\"/>\n<g id=\"clust1\" class=\"cluster\">\n<title>cluster_States</title>\n<polygon fill=\"lightgrey\" stroke=\"lightgrey\" points=\"8,-8 8,-168 192,-168 192,-8 8,-8\"/>\n<text text-anchor=\"middle\" x=\"100\" y=\"-154.4\" font-family=\"Times,serif\" font-size=\"12.00\">States</text>\n</g>\n<!-- s3 -->\n<g id=\"node1\" class=\"node\">\n<title>s3</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"142,-139 88,-139 88,-103 142,-103 142,-139\"/>\n<text text-anchor=\"middle\" x=\"115\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">s3</text>\n</g>\n<!-- s3->s3 -->\n<g id=\"edge1\" class=\"edge\">\n<title>s3->s3</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M142.24,-129.15C152.02,-129.32 160,-126.61 160,-121 160,-117.58 157.04,-115.24 152.51,-113.97\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"152.56,-110.45 142.24,-112.85 151.8,-117.41 152.56,-110.45\"/>\n<text text-anchor=\"middle\" x=\"172\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">next</text>\n</g>\n<!-- s2 -->\n<g id=\"node2\" class=\"node\">\n<title>s2</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-139 16,-139 16,-103 70,-103 70,-139\"/>\n<text text-anchor=\"middle\" x=\"43\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">s2</text>\n</g>\n<!-- s1 -->\n<g id=\"node3\" class=\"node\">\n<title>s1</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"91,-52 37,-52 37,-16 91,-16 91,-52\"/>\n<text text-anchor=\"middle\" x=\"64\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">s1</text>\n</g>\n<!-- s2->s1 -->\n<g id=\"edge2\" class=\"edge\">\n<title>s2->s1</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M38.45,-102.96C36.6,-93.11 35.6,-80.61 39,-70 40,-66.87 41.4,-63.78 43.02,-60.82\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"46,-62.66 48.42,-52.35 40.09,-58.9 46,-62.66\"/>\n<text text-anchor=\"middle\" x=\"51\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">next</text>\n</g>\n<!-- s1->s2 -->\n<g id=\"edge3\" class=\"edge\">\n<title>s1->s2</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M65.74,-52.43C66.2,-62.18 65.91,-74.46 63,-85 62.17,-88.01 61.02,-91.03 59.69,-93.96\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"56.53,-92.47 55,-102.95 62.73,-95.71 56.53,-92.47\"/>\n<text text-anchor=\"middle\" x=\"77\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">next</text>\n</g>\n</g>\n</svg>\n",
+ "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 6.0.1 (20220911.1526)\n",
+ " -->\n",
+ "<!-- Title: state Pages: 1 -->\n",
+ "<svg width=\"208pt\" height=\"184pt\"\n",
+ " viewBox=\"0.00 0.00 208.00 184.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 180)\">\n",
+ "<title>state</title>\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-180 204,-180 204,4 -4,4\"/>\n",
+ "<g id=\"clust1\" class=\"cluster\">\n",
+ "<title>cluster_States</title>\n",
+ "<polygon fill=\"lightgrey\" stroke=\"lightgrey\" points=\"8,-8 8,-168 192,-168 192,-8 8,-8\"/>\n",
+ "<text text-anchor=\"middle\" x=\"100\" y=\"-154.4\" font-family=\"Times,serif\" font-size=\"12.00\">States</text>\n",
+ "</g>\n",
+ "<!-- s3 -->\n",
+ "<g id=\"node1\" class=\"node\">\n",
+ "<title>s3</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"142,-139 88,-139 88,-103 142,-103 142,-139\"/>\n",
+ "<text text-anchor=\"middle\" x=\"115\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">s3</text>\n",
+ "</g>\n",
+ "<!-- s3->s3 -->\n",
+ "<g id=\"edge1\" class=\"edge\">\n",
+ "<title>s3->s3</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M142.24,-129.15C152.02,-129.32 160,-126.61 160,-121 160,-117.58 157.04,-115.24 152.51,-113.97\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"152.56,-110.45 142.24,-112.85 151.8,-117.41 152.56,-110.45\"/>\n",
+ "<text text-anchor=\"middle\" x=\"172\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">next</text>\n",
+ "</g>\n",
+ "<!-- s2 -->\n",
+ "<g id=\"node2\" class=\"node\">\n",
+ "<title>s2</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-139 16,-139 16,-103 70,-103 70,-139\"/>\n",
+ "<text text-anchor=\"middle\" x=\"43\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">s2</text>\n",
+ "</g>\n",
+ "<!-- s1 -->\n",
+ "<g id=\"node3\" class=\"node\">\n",
+ "<title>s1</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"91,-52 37,-52 37,-16 91,-16 91,-52\"/>\n",
+ "<text text-anchor=\"middle\" x=\"64\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">s1</text>\n",
+ "</g>\n",
+ "<!-- s2->s1 -->\n",
+ "<g id=\"edge2\" class=\"edge\">\n",
+ "<title>s2->s1</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M38.45,-102.96C36.6,-93.11 35.6,-80.61 39,-70 40,-66.87 41.4,-63.78 43.02,-60.82\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"46,-62.66 48.42,-52.35 40.09,-58.9 46,-62.66\"/>\n",
+ "<text text-anchor=\"middle\" x=\"51\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">next</text>\n",
+ "</g>\n",
+ "<!-- s1->s2 -->\n",
+ "<g id=\"edge3\" class=\"edge\">\n",
+ "<title>s1->s2</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M65.74,-52.43C66.2,-62.18 65.91,-74.46 63,-85 62.17,-88.01 61.02,-91.03 59.69,-93.96\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"56.53,-92.47 55,-102.95 62.73,-95.71 56.53,-92.47\"/>\n",
+ "<text text-anchor=\"middle\" x=\"77\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">next</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>\n"
+ ],
"text/plain": [
"<Dot visualization: expr_as_graph [next]>"
]
},
- "execution_count": 7,
+ "execution_count": 23,
"metadata": {},
"output_type": "execute_result"
}
@@ -109,7 +165,7 @@
},
{
"cell_type": "code",
- "execution_count": 8,
+ "execution_count": 24,
"id": "31e1b59d",
"metadata": {
"vscode": {
@@ -126,7 +182,7 @@
"{(s1↦s1),(s1↦s2),(s2↦s1),(s2↦s2),(s3↦s3)}"
]
},
- "execution_count": 8,
+ "execution_count": 24,
"metadata": {},
"output_type": "execute_result"
}
@@ -137,7 +193,7 @@
},
{
"cell_type": "code",
- "execution_count": 12,
+ "execution_count": 25,
"id": "006bae98",
"metadata": {
"vscode": {
@@ -147,12 +203,84 @@
"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 6.0.1 (20220911.1526)\n -->\n<!-- Title: state Pages: 1 -->\n<svg width=\"246pt\" height=\"184pt\"\n viewBox=\"0.00 0.00 246.00 184.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 180)\">\n<title>state</title>\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-180 242,-180 242,4 -4,4\"/>\n<g id=\"clust1\" class=\"cluster\">\n<title>cluster_States</title>\n<polygon fill=\"lightgrey\" stroke=\"lightgrey\" points=\"8,-8 8,-168 230,-168 230,-8 8,-8\"/>\n<text text-anchor=\"middle\" x=\"119\" y=\"-154.4\" font-family=\"Times,serif\" font-size=\"12.00\">States</text>\n</g>\n<!-- s3 -->\n<g id=\"node1\" class=\"node\">\n<title>s3</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"182,-139 128,-139 128,-103 182,-103 182,-139\"/>\n<text text-anchor=\"middle\" x=\"155\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">s3</text>\n</g>\n<!-- s3->s3 -->\n<g id=\"edge1\" class=\"edge\">\n<title>s3->s3</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M182.24,-129.15C192.02,-129.32 200,-126.61 200,-121 200,-117.58 197.04,-115.24 192.51,-113.97\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"192.56,-110.45 182.24,-112.85 191.8,-117.41 192.56,-110.45\"/>\n<text text-anchor=\"middle\" x=\"211\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s2 -->\n<g id=\"node2\" class=\"node\">\n<title>s2</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-139 16,-139 16,-103 70,-103 70,-139\"/>\n<text text-anchor=\"middle\" x=\"43\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">s2</text>\n</g>\n<!-- s2->s2 -->\n<g id=\"edge2\" class=\"edge\">\n<title>s2->s2</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M70.24,-129.15C80.02,-129.32 88,-126.61 88,-121 88,-117.58 85.04,-115.24 80.51,-113.97\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"80.56,-110.45 70.24,-112.85 79.8,-117.41 80.56,-110.45\"/>\n<text text-anchor=\"middle\" x=\"99\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s1 -->\n<g id=\"node3\" class=\"node\">\n<title>s1</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"90,-52 36,-52 36,-16 90,-16 90,-52\"/>\n<text text-anchor=\"middle\" x=\"63\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">s1</text>\n</g>\n<!-- s2->s1 -->\n<g id=\"edge3\" class=\"edge\">\n<title>s2->s1</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M38.53,-102.99C36.7,-93.15 35.7,-80.65 39,-70 39.98,-66.83 41.36,-63.7 42.96,-60.68\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"46,-62.42 48.29,-52.07 40.05,-58.74 46,-62.42\"/>\n<text text-anchor=\"middle\" x=\"50\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s1->s2 -->\n<g id=\"edge4\" class=\"edge\">\n<title>s1->s2</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M64.13,-52.4C64.32,-62.14 63.79,-74.41 61,-85 60.25,-87.85 59.24,-90.73 58.08,-93.56\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"54.83,-92.26 53.73,-102.8 61.16,-95.24 54.83,-92.26\"/>\n<text text-anchor=\"middle\" x=\"74\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s1->s1 -->\n<g id=\"edge5\" class=\"edge\">\n<title>s1->s1</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M90.24,-42.15C100.02,-42.32 108,-39.61 108,-34 108,-30.58 105.04,-28.24 100.51,-26.97\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"100.56,-23.45 90.24,-25.85 99.8,-30.41 100.56,-23.45\"/>\n<text text-anchor=\"middle\" x=\"119\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n</g>\n</svg>\n",
+ "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 6.0.1 (20220911.1526)\n",
+ " -->\n",
+ "<!-- Title: state Pages: 1 -->\n",
+ "<svg width=\"246pt\" height=\"184pt\"\n",
+ " viewBox=\"0.00 0.00 246.00 184.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 180)\">\n",
+ "<title>state</title>\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-180 242,-180 242,4 -4,4\"/>\n",
+ "<g id=\"clust1\" class=\"cluster\">\n",
+ "<title>cluster_States</title>\n",
+ "<polygon fill=\"lightgrey\" stroke=\"lightgrey\" points=\"8,-8 8,-168 230,-168 230,-8 8,-8\"/>\n",
+ "<text text-anchor=\"middle\" x=\"119\" y=\"-154.4\" font-family=\"Times,serif\" font-size=\"12.00\">States</text>\n",
+ "</g>\n",
+ "<!-- s3 -->\n",
+ "<g id=\"node1\" class=\"node\">\n",
+ "<title>s3</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"182,-139 128,-139 128,-103 182,-103 182,-139\"/>\n",
+ "<text text-anchor=\"middle\" x=\"155\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">s3</text>\n",
+ "</g>\n",
+ "<!-- s3->s3 -->\n",
+ "<g id=\"edge1\" class=\"edge\">\n",
+ "<title>s3->s3</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M182.24,-129.15C192.02,-129.32 200,-126.61 200,-121 200,-117.58 197.04,-115.24 192.51,-113.97\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"192.56,-110.45 182.24,-112.85 191.8,-117.41 192.56,-110.45\"/>\n",
+ "<text text-anchor=\"middle\" x=\"211\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n",
+ "</g>\n",
+ "<!-- s2 -->\n",
+ "<g id=\"node2\" class=\"node\">\n",
+ "<title>s2</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-139 16,-139 16,-103 70,-103 70,-139\"/>\n",
+ "<text text-anchor=\"middle\" x=\"43\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">s2</text>\n",
+ "</g>\n",
+ "<!-- s2->s2 -->\n",
+ "<g id=\"edge2\" class=\"edge\">\n",
+ "<title>s2->s2</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M70.24,-129.15C80.02,-129.32 88,-126.61 88,-121 88,-117.58 85.04,-115.24 80.51,-113.97\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"80.56,-110.45 70.24,-112.85 79.8,-117.41 80.56,-110.45\"/>\n",
+ "<text text-anchor=\"middle\" x=\"99\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n",
+ "</g>\n",
+ "<!-- s1 -->\n",
+ "<g id=\"node3\" class=\"node\">\n",
+ "<title>s1</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"90,-52 36,-52 36,-16 90,-16 90,-52\"/>\n",
+ "<text text-anchor=\"middle\" x=\"63\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">s1</text>\n",
+ "</g>\n",
+ "<!-- s2->s1 -->\n",
+ "<g id=\"edge3\" class=\"edge\">\n",
+ "<title>s2->s1</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M38.53,-102.99C36.7,-93.15 35.7,-80.65 39,-70 39.98,-66.83 41.36,-63.7 42.96,-60.68\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"46,-62.42 48.29,-52.07 40.05,-58.74 46,-62.42\"/>\n",
+ "<text text-anchor=\"middle\" x=\"50\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n",
+ "</g>\n",
+ "<!-- s1->s2 -->\n",
+ "<g id=\"edge4\" class=\"edge\">\n",
+ "<title>s1->s2</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M64.13,-52.4C64.32,-62.14 63.79,-74.41 61,-85 60.25,-87.85 59.24,-90.73 58.08,-93.56\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"54.83,-92.26 53.73,-102.8 61.16,-95.24 54.83,-92.26\"/>\n",
+ "<text text-anchor=\"middle\" x=\"74\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n",
+ "</g>\n",
+ "<!-- s1->s1 -->\n",
+ "<g id=\"edge5\" class=\"edge\">\n",
+ "<title>s1->s1</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M90.24,-42.15C100.02,-42.32 108,-39.61 108,-34 108,-30.58 105.04,-28.24 100.51,-26.97\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"100.56,-23.45 90.24,-25.85 99.8,-30.41 100.56,-23.45\"/>\n",
+ "<text text-anchor=\"middle\" x=\"119\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>\n"
+ ],
"text/plain": [
"<Dot visualization: expr_as_graph [(\"cls1\",closure1(next))]>"
]
},
- "execution_count": 12,
+ "execution_count": 25,
"metadata": {},
"output_type": "execute_result"
}
@@ -172,7 +300,7 @@
},
{
"cell_type": "code",
- "execution_count": 16,
+ "execution_count": 26,
"id": "44c560e2",
"metadata": {
"vscode": {
@@ -195,14 +323,14 @@
"\tcls1 = {(s2↦s1),(s1↦s2),(s3↦s3),(s1↦s1),(s1↦s3),(s2↦s2)}"
]
},
- "execution_count": 16,
+ "execution_count": 26,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- "next <: cls1 & // the next relation is included in the transitive closure\n",
- "!s.(s:States => next[cls1[{s}]] <: cls1[{s}] ) // all successors are also included"
+ "next ⊆ cls1 & // the next relation is included in the transitive closure\n",
+ "∀s.(s:States ⇒ next[cls1[{s}]] ⊆ cls1[{s}] ) // all successors are also included"
]
},
{
@@ -216,7 +344,7 @@
},
{
"cell_type": "code",
- "execution_count": 19,
+ "execution_count": 27,
"id": "90d84935",
"metadata": {
"vscode": {
@@ -226,12 +354,91 @@
"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 6.0.1 (20220911.1526)\n -->\n<!-- Title: state Pages: 1 -->\n<svg width=\"246pt\" height=\"184pt\"\n viewBox=\"0.00 0.00 246.00 184.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 180)\">\n<title>state</title>\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-180 242,-180 242,4 -4,4\"/>\n<g id=\"clust1\" class=\"cluster\">\n<title>cluster_States</title>\n<polygon fill=\"lightgrey\" stroke=\"lightgrey\" points=\"8,-8 8,-168 230,-168 230,-8 8,-8\"/>\n<text text-anchor=\"middle\" x=\"119\" y=\"-154.4\" font-family=\"Times,serif\" font-size=\"12.00\">States</text>\n</g>\n<!-- s3 -->\n<g id=\"node1\" class=\"node\">\n<title>s3</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"182,-52 128,-52 128,-16 182,-16 182,-52\"/>\n<text text-anchor=\"middle\" x=\"155\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">s3</text>\n</g>\n<!-- s3->s3 -->\n<g id=\"edge1\" class=\"edge\">\n<title>s3->s3</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M182.24,-42.15C192.02,-42.32 200,-39.61 200,-34 200,-30.58 197.04,-28.24 192.51,-26.97\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"192.56,-23.45 182.24,-25.85 191.8,-30.41 192.56,-23.45\"/>\n<text text-anchor=\"middle\" x=\"211\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s2 -->\n<g id=\"node2\" class=\"node\">\n<title>s2</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-52 16,-52 16,-16 70,-16 70,-52\"/>\n<text text-anchor=\"middle\" x=\"43\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">s2</text>\n</g>\n<!-- s2->s2 -->\n<g id=\"edge2\" class=\"edge\">\n<title>s2->s2</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M70.24,-42.15C80.02,-42.32 88,-39.61 88,-34 88,-30.58 85.04,-28.24 80.51,-26.97\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"80.56,-23.45 70.24,-25.85 79.8,-30.41 80.56,-23.45\"/>\n<text text-anchor=\"middle\" x=\"99\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s1 -->\n<g id=\"node3\" class=\"node\">\n<title>s1</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"115,-139 61,-139 61,-103 115,-103 115,-139\"/>\n<text text-anchor=\"middle\" x=\"88\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">s1</text>\n</g>\n<!-- s2->s1 -->\n<g id=\"edge3\" class=\"edge\">\n<title>s2->s1</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M55.05,-52.09C58.77,-57.68 62.74,-64 66,-70 70.08,-77.5 74.01,-85.9 77.39,-93.65\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"74.22,-95.16 81.35,-103 80.67,-92.43 74.22,-95.16\"/>\n<text text-anchor=\"middle\" x=\"84\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s1->s3 -->\n<g id=\"edge4\" class=\"edge\">\n<title>s1->s3</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M101.56,-102.8C111.18,-90.59 124.27,-73.99 135.08,-60.28\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"138.02,-62.2 141.46,-52.18 132.52,-57.86 138.02,-62.2\"/>\n<text text-anchor=\"middle\" x=\"136\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s1->s2 -->\n<g id=\"edge5\" class=\"edge\">\n<title>s1->s2</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M60.95,-106.76C52.69,-101.25 44.58,-94.01 40,-85 36.48,-78.07 35.78,-69.89 36.36,-62.17\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"39.85,-62.49 37.81,-52.09 32.93,-61.49 39.85,-62.49\"/>\n<text text-anchor=\"middle\" x=\"51\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s1->s1 -->\n<g id=\"edge6\" class=\"edge\">\n<title>s1->s1</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M115.24,-129.15C125.02,-129.32 133,-126.61 133,-121 133,-117.58 130.04,-115.24 125.51,-113.97\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"125.56,-110.45 115.24,-112.85 124.8,-117.41 125.56,-110.45\"/>\n<text text-anchor=\"middle\" x=\"144\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n</g>\n</svg>\n",
+ "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 6.0.1 (20220911.1526)\n",
+ " -->\n",
+ "<!-- Title: state Pages: 1 -->\n",
+ "<svg width=\"246pt\" height=\"184pt\"\n",
+ " viewBox=\"0.00 0.00 246.00 184.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 180)\">\n",
+ "<title>state</title>\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-180 242,-180 242,4 -4,4\"/>\n",
+ "<g id=\"clust1\" class=\"cluster\">\n",
+ "<title>cluster_States</title>\n",
+ "<polygon fill=\"lightgrey\" stroke=\"lightgrey\" points=\"8,-8 8,-168 230,-168 230,-8 8,-8\"/>\n",
+ "<text text-anchor=\"middle\" x=\"119\" y=\"-154.4\" font-family=\"Times,serif\" font-size=\"12.00\">States</text>\n",
+ "</g>\n",
+ "<!-- s3 -->\n",
+ "<g id=\"node1\" class=\"node\">\n",
+ "<title>s3</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"182,-52 128,-52 128,-16 182,-16 182,-52\"/>\n",
+ "<text text-anchor=\"middle\" x=\"155\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">s3</text>\n",
+ "</g>\n",
+ "<!-- s3->s3 -->\n",
+ "<g id=\"edge1\" class=\"edge\">\n",
+ "<title>s3->s3</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M182.24,-42.15C192.02,-42.32 200,-39.61 200,-34 200,-30.58 197.04,-28.24 192.51,-26.97\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"192.56,-23.45 182.24,-25.85 191.8,-30.41 192.56,-23.45\"/>\n",
+ "<text text-anchor=\"middle\" x=\"211\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n",
+ "</g>\n",
+ "<!-- s2 -->\n",
+ "<g id=\"node2\" class=\"node\">\n",
+ "<title>s2</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-52 16,-52 16,-16 70,-16 70,-52\"/>\n",
+ "<text text-anchor=\"middle\" x=\"43\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">s2</text>\n",
+ "</g>\n",
+ "<!-- s2->s2 -->\n",
+ "<g id=\"edge2\" class=\"edge\">\n",
+ "<title>s2->s2</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M70.24,-42.15C80.02,-42.32 88,-39.61 88,-34 88,-30.58 85.04,-28.24 80.51,-26.97\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"80.56,-23.45 70.24,-25.85 79.8,-30.41 80.56,-23.45\"/>\n",
+ "<text text-anchor=\"middle\" x=\"99\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n",
+ "</g>\n",
+ "<!-- s1 -->\n",
+ "<g id=\"node3\" class=\"node\">\n",
+ "<title>s1</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"115,-139 61,-139 61,-103 115,-103 115,-139\"/>\n",
+ "<text text-anchor=\"middle\" x=\"88\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">s1</text>\n",
+ "</g>\n",
+ "<!-- s2->s1 -->\n",
+ "<g id=\"edge3\" class=\"edge\">\n",
+ "<title>s2->s1</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M55.05,-52.09C58.77,-57.68 62.74,-64 66,-70 70.08,-77.5 74.01,-85.9 77.39,-93.65\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"74.22,-95.16 81.35,-103 80.67,-92.43 74.22,-95.16\"/>\n",
+ "<text text-anchor=\"middle\" x=\"84\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n",
+ "</g>\n",
+ "<!-- s1->s3 -->\n",
+ "<g id=\"edge4\" class=\"edge\">\n",
+ "<title>s1->s3</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M101.56,-102.8C111.18,-90.59 124.27,-73.99 135.08,-60.28\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"138.02,-62.2 141.46,-52.18 132.52,-57.86 138.02,-62.2\"/>\n",
+ "<text text-anchor=\"middle\" x=\"136\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n",
+ "</g>\n",
+ "<!-- s1->s2 -->\n",
+ "<g id=\"edge5\" class=\"edge\">\n",
+ "<title>s1->s2</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M60.95,-106.76C52.69,-101.25 44.58,-94.01 40,-85 36.48,-78.07 35.78,-69.89 36.36,-62.17\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"39.85,-62.49 37.81,-52.09 32.93,-61.49 39.85,-62.49\"/>\n",
+ "<text text-anchor=\"middle\" x=\"51\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n",
+ "</g>\n",
+ "<!-- s1->s1 -->\n",
+ "<g id=\"edge6\" class=\"edge\">\n",
+ "<title>s1->s1</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M115.24,-129.15C125.02,-129.32 133,-126.61 133,-121 133,-117.58 130.04,-115.24 125.51,-113.97\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"125.56,-110.45 115.24,-112.85 124.8,-117.41 125.56,-110.45\"/>\n",
+ "<text text-anchor=\"middle\" x=\"144\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>\n"
+ ],
"text/plain": [
"<Dot visualization: expr_as_graph [(\"cls1\", {(s2↦s1),(s1↦s2),(s3↦s3),(s1↦s1),(s1↦s3),(s2↦s2)})]>"
]
},
- "execution_count": 19,
+ "execution_count": 27,
"metadata": {},
"output_type": "execute_result"
}
@@ -250,7 +457,7 @@
},
{
"cell_type": "code",
- "execution_count": 17,
+ "execution_count": 28,
"id": "28d0f48e",
"metadata": {
"vscode": {
@@ -284,13 +491,13 @@
"{(s1|->s1),(s1|->s2),(s2|->s1),(s2|->s2),(s2|->s3),(s3|->s1),(s3|->s2),(s3|->s3)}\n"
]
},
- "execution_count": 17,
+ "execution_count": 28,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- ":table {cls1 | next <: cls1 & !s.(s:States => next[cls1[{s}]] <: cls1[{s}] )}"
+ ":table {cls1 | next ⊆ cls1 & ∀s.(s:States ⇒ next[cls1[{s}]] ⊆ cls1[{s}] )}"
]
},
{
@@ -310,7 +517,7 @@
},
{
"cell_type": "code",
- "execution_count": 24,
+ "execution_count": 29,
"id": "4d178ab1",
"metadata": {
"vscode": {
@@ -330,24 +537,24 @@
"{(s1|->s1),(s1|->s2),(s2|->s1),(s2|->s2),(s3|->s3)}\n"
]
},
- "execution_count": 24,
+ "execution_count": 29,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":table {cls1 | \n",
- " next <: cls1 & !s.(s:States => next[cls1[{s}]] <: cls1[{s}]) // we satisfy our axioms\n",
- " &\n",
- " !other.(other <<: cls1 & next <: other => \n",
- " not ( !s.(s:States => next[other[{s}]] <: other[{s}]) )\n",
+ " next ⊆ cls1 & ∀s.(s:States ⇒ next[cls1[{s}]] ⊆ cls1[{s}]) // we satisfy our axioms\n",
+ " & // all smaller relations do not satisfy our axioms:\n",
+ " ∀other.(other ⊂ cls1 & next ⊆ other ⇒ \n",
+ " ¬ ( ∀s.(s:States ⇒ next[other[{s}]] ⊆ other[{s}]) )\n",
" )\n",
" }"
]
},
{
"cell_type": "code",
- "execution_count": 25,
+ "execution_count": 30,
"id": "c7c935b3",
"metadata": {
"vscode": {
@@ -357,12 +564,84 @@
"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 6.0.1 (20220911.1526)\n -->\n<!-- Title: state Pages: 1 -->\n<svg width=\"246pt\" height=\"184pt\"\n viewBox=\"0.00 0.00 246.00 184.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 180)\">\n<title>state</title>\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-180 242,-180 242,4 -4,4\"/>\n<g id=\"clust1\" class=\"cluster\">\n<title>cluster_States</title>\n<polygon fill=\"lightgrey\" stroke=\"lightgrey\" points=\"8,-8 8,-168 230,-168 230,-8 8,-8\"/>\n<text text-anchor=\"middle\" x=\"119\" y=\"-154.4\" font-family=\"Times,serif\" font-size=\"12.00\">States</text>\n</g>\n<!-- s3 -->\n<g id=\"node1\" class=\"node\">\n<title>s3</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"182,-139 128,-139 128,-103 182,-103 182,-139\"/>\n<text text-anchor=\"middle\" x=\"155\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">s3</text>\n</g>\n<!-- s3->s3 -->\n<g id=\"edge1\" class=\"edge\">\n<title>s3->s3</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M182.24,-129.15C192.02,-129.32 200,-126.61 200,-121 200,-117.58 197.04,-115.24 192.51,-113.97\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"192.56,-110.45 182.24,-112.85 191.8,-117.41 192.56,-110.45\"/>\n<text text-anchor=\"middle\" x=\"211\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s2 -->\n<g id=\"node2\" class=\"node\">\n<title>s2</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-139 16,-139 16,-103 70,-103 70,-139\"/>\n<text text-anchor=\"middle\" x=\"43\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">s2</text>\n</g>\n<!-- s2->s2 -->\n<g id=\"edge2\" class=\"edge\">\n<title>s2->s2</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M70.24,-129.15C80.02,-129.32 88,-126.61 88,-121 88,-117.58 85.04,-115.24 80.51,-113.97\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"80.56,-110.45 70.24,-112.85 79.8,-117.41 80.56,-110.45\"/>\n<text text-anchor=\"middle\" x=\"99\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s1 -->\n<g id=\"node3\" class=\"node\">\n<title>s1</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"90,-52 36,-52 36,-16 90,-16 90,-52\"/>\n<text text-anchor=\"middle\" x=\"63\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">s1</text>\n</g>\n<!-- s2->s1 -->\n<g id=\"edge3\" class=\"edge\">\n<title>s2->s1</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M38.53,-102.99C36.7,-93.15 35.7,-80.65 39,-70 39.98,-66.83 41.36,-63.7 42.96,-60.68\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"46,-62.42 48.29,-52.07 40.05,-58.74 46,-62.42\"/>\n<text text-anchor=\"middle\" x=\"50\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s1->s2 -->\n<g id=\"edge4\" class=\"edge\">\n<title>s1->s2</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M64.13,-52.4C64.32,-62.14 63.79,-74.41 61,-85 60.25,-87.85 59.24,-90.73 58.08,-93.56\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"54.83,-92.26 53.73,-102.8 61.16,-95.24 54.83,-92.26\"/>\n<text text-anchor=\"middle\" x=\"74\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s1->s1 -->\n<g id=\"edge5\" class=\"edge\">\n<title>s1->s1</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M90.24,-42.15C100.02,-42.32 108,-39.61 108,-34 108,-30.58 105.04,-28.24 100.51,-26.97\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"100.56,-23.45 90.24,-25.85 99.8,-30.41 100.56,-23.45\"/>\n<text text-anchor=\"middle\" x=\"119\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n</g>\n</svg>\n",
+ "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 6.0.1 (20220911.1526)\n",
+ " -->\n",
+ "<!-- Title: state Pages: 1 -->\n",
+ "<svg width=\"246pt\" height=\"184pt\"\n",
+ " viewBox=\"0.00 0.00 246.00 184.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 180)\">\n",
+ "<title>state</title>\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-180 242,-180 242,4 -4,4\"/>\n",
+ "<g id=\"clust1\" class=\"cluster\">\n",
+ "<title>cluster_States</title>\n",
+ "<polygon fill=\"lightgrey\" stroke=\"lightgrey\" points=\"8,-8 8,-168 230,-168 230,-8 8,-8\"/>\n",
+ "<text text-anchor=\"middle\" x=\"119\" y=\"-154.4\" font-family=\"Times,serif\" font-size=\"12.00\">States</text>\n",
+ "</g>\n",
+ "<!-- s3 -->\n",
+ "<g id=\"node1\" class=\"node\">\n",
+ "<title>s3</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"182,-139 128,-139 128,-103 182,-103 182,-139\"/>\n",
+ "<text text-anchor=\"middle\" x=\"155\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">s3</text>\n",
+ "</g>\n",
+ "<!-- s3->s3 -->\n",
+ "<g id=\"edge1\" class=\"edge\">\n",
+ "<title>s3->s3</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M182.24,-129.15C192.02,-129.32 200,-126.61 200,-121 200,-117.58 197.04,-115.24 192.51,-113.97\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"192.56,-110.45 182.24,-112.85 191.8,-117.41 192.56,-110.45\"/>\n",
+ "<text text-anchor=\"middle\" x=\"211\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n",
+ "</g>\n",
+ "<!-- s2 -->\n",
+ "<g id=\"node2\" class=\"node\">\n",
+ "<title>s2</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-139 16,-139 16,-103 70,-103 70,-139\"/>\n",
+ "<text text-anchor=\"middle\" x=\"43\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">s2</text>\n",
+ "</g>\n",
+ "<!-- s2->s2 -->\n",
+ "<g id=\"edge2\" class=\"edge\">\n",
+ "<title>s2->s2</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M70.24,-129.15C80.02,-129.32 88,-126.61 88,-121 88,-117.58 85.04,-115.24 80.51,-113.97\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"80.56,-110.45 70.24,-112.85 79.8,-117.41 80.56,-110.45\"/>\n",
+ "<text text-anchor=\"middle\" x=\"99\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n",
+ "</g>\n",
+ "<!-- s1 -->\n",
+ "<g id=\"node3\" class=\"node\">\n",
+ "<title>s1</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"90,-52 36,-52 36,-16 90,-16 90,-52\"/>\n",
+ "<text text-anchor=\"middle\" x=\"63\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">s1</text>\n",
+ "</g>\n",
+ "<!-- s2->s1 -->\n",
+ "<g id=\"edge3\" class=\"edge\">\n",
+ "<title>s2->s1</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M38.53,-102.99C36.7,-93.15 35.7,-80.65 39,-70 39.98,-66.83 41.36,-63.7 42.96,-60.68\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"46,-62.42 48.29,-52.07 40.05,-58.74 46,-62.42\"/>\n",
+ "<text text-anchor=\"middle\" x=\"50\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n",
+ "</g>\n",
+ "<!-- s1->s2 -->\n",
+ "<g id=\"edge4\" class=\"edge\">\n",
+ "<title>s1->s2</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M64.13,-52.4C64.32,-62.14 63.79,-74.41 61,-85 60.25,-87.85 59.24,-90.73 58.08,-93.56\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"54.83,-92.26 53.73,-102.8 61.16,-95.24 54.83,-92.26\"/>\n",
+ "<text text-anchor=\"middle\" x=\"74\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n",
+ "</g>\n",
+ "<!-- s1->s1 -->\n",
+ "<g id=\"edge5\" class=\"edge\">\n",
+ "<title>s1->s1</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M90.24,-42.15C100.02,-42.32 108,-39.61 108,-34 108,-30.58 105.04,-28.24 100.51,-26.97\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"100.56,-23.45 90.24,-25.85 99.8,-30.41 100.56,-23.45\"/>\n",
+ "<text text-anchor=\"middle\" x=\"119\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>\n"
+ ],
"text/plain": [
"<Dot visualization: expr_as_graph [(\"cls1\", {(s1↦s1),(s1↦s2),(s2↦s1),(s2↦s2),(s3↦s3)})]>"
]
},
- "execution_count": 25,
+ "execution_count": 30,
"metadata": {},
"output_type": "execute_result"
}
@@ -389,7 +668,7 @@
},
{
"cell_type": "code",
- "execution_count": 27,
+ "execution_count": 31,
"id": "73cc5e59",
"metadata": {
"vscode": {
@@ -412,18 +691,18 @@
"\tcls1 = {(s1↦s2),(s2↦s1),(s1↦s1),(s2↦s2),(s3↦s3)}"
]
},
- "execution_count": 27,
+ "execution_count": 31,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- "!(A,B).( A:States & B:States =>\n",
- " (A|->B : cls1 \n",
- " <=>\n",
- " (A|->B : next \n",
+ "∀(A,B).( A:States & B:States ⇒\n",
+ " (A↦B : cls1 \n",
+ " ⇔\n",
+ " (A↦B : next \n",
" or\n",
- " #C.(C:States & A|->C:next & C|->B:cls1)\n",
+ " ∃C.(C:States & A↦C:next & C↦B:cls1)\n",
" ) \n",
" ))"
]
@@ -438,7 +717,7 @@
},
{
"cell_type": "code",
- "execution_count": 29,
+ "execution_count": 32,
"id": "1dcb6a9d",
"metadata": {
"vscode": {
@@ -472,32 +751,124 @@
"{(s1|->s1),(s1|->s2),(s1|->s3),(s2|->s1),(s2|->s2),(s2|->s3),(s3|->s1),(s3|->s2),(s3|->s3)}\n"
]
},
- "execution_count": 29,
+ "execution_count": 32,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":table {cls1|\n",
- " !(A,B).( A:States & B:States =>\n",
- " (A|->B : cls1 \n",
- " <=>\n",
- " (A|->B : next \n",
+ " ∀(A,B).( A:States & B:States ⇒\n",
+ " (A↦B : cls1 \n",
+ " ⇔\n",
+ " (A↦B : next \n",
" or\n",
- " #C.(C:States & A|->C:next & C|->B:cls1)\n",
+ " ∃C.(C:States & A↦C:next & C↦B:cls1)\n",
" ) \n",
" ))}"
]
},
+ {
+ "cell_type": "markdown",
+ "id": "32f240ac-2754-4ce8-a241-65597ea97f50",
+ "metadata": {},
+ "source": [
+ "### ASCII versions of formulas"
+ ]
+ },
{
"cell_type": "code",
- "execution_count": null,
+ "execution_count": 33,
"id": "8e13128d",
"metadata": {
"vscode": {
"languageId": "plaintext"
}
},
+ "outputs": [
+ {
+ "data": {
+ "text/latex": [
+ "$\\mathit{next} \\subseteq \\mathit{cls1} \\wedge \\forall \\mathit{s}\\cdot (\\mathit{s} \\in \\mathit{States} \\mathbin\\Rightarrow \\mathit{next}[\\mathit{cls1}[\\{\\mathit{s}\\}]] \\subseteq \\mathit{cls1}[\\{\\mathit{s}\\}])$"
+ ],
+ "text/plain": [
+ "next ⊆ cls1 ∧ ∀s·(s ∈ States ⇒ next[cls1[{s}]] ⊆ cls1[{s}])"
+ ]
+ },
+ "execution_count": 33,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":prettyprint next <: cls1 & // the next relation is included in the transitive closure\n",
+ "!s.(s:States => next[cls1[{s}]] <: cls1[{s}] ) // all successors are also included"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 34,
+ "id": "cc138ea8-6190-44ce-a677-f3e0e05f47a2",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/latex": [
+ "$\\forall (\\mathit{A},\\mathit{B})\\cdot (\\mathit{A} \\in \\mathit{States} \\wedge \\mathit{B} \\in \\mathit{States} \\mathbin\\Rightarrow (\\mathit{A} \\mapsto \\mathit{B} \\in \\mathit{cls1}) \\mathbin\\Leftrightarrow (\\mathit{A} \\mapsto \\mathit{B} \\in \\mathit{next} \\vee \\exists \\mathit{C}\\cdot (\\mathit{C} \\in \\mathit{States} \\wedge \\mathit{A} \\mapsto \\mathit{C} \\in \\mathit{next} \\wedge \\mathit{C} \\mapsto \\mathit{B} \\in \\mathit{cls1})))$"
+ ],
+ "text/plain": [
+ "∀(A,B)·(A ∈ States ∧ B ∈ States ⇒ (A ↦ B ∈ cls1) ⇔ (A ↦ B ∈ next ∨ ∃C·(C ∈ States ∧ A ↦ C ∈ next ∧ C ↦ B ∈ cls1)))"
+ ]
+ },
+ "execution_count": 34,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":prettyprint ∀(A,B).( A:States & B:States ⇒\n",
+ " (A|->B : cls1 \n",
+ " <=>\n",
+ " (A|->B : next \n",
+ " or\n",
+ " #C.(C:States & A|->C:next & C|->B:cls1)\n",
+ " ) \n",
+ " ))"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 35,
+ "id": "b41471dc-cef6-4479-9704-0e3ef1115425",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/latex": [
+ "$\\mathit{next} \\subseteq \\mathit{cls1} \\wedge \\forall \\mathit{s}\\cdot (\\mathit{s} \\in \\mathit{States} \\mathbin\\Rightarrow \\mathit{next}[\\mathit{cls1}[\\{\\mathit{s}\\}]] \\subseteq \\mathit{cls1}[\\{\\mathit{s}\\}]) \\wedge \\forall \\mathit{other}\\cdot (\\mathit{other} \\subset \\mathit{cls1} \\wedge \\mathit{next} \\subseteq \\mathit{other} \\mathbin\\Rightarrow \\neg (\\forall \\mathit{s}\\cdot (\\mathit{s} \\in \\mathit{States} \\mathbin\\Rightarrow \\mathit{next}[\\mathit{other}[\\{\\mathit{s}\\}]] \\subseteq \\mathit{other}[\\{\\mathit{s}\\}])))$"
+ ],
+ "text/plain": [
+ "next ⊆ cls1 ∧ ∀s·(s ∈ States ⇒ next[cls1[{s}]] ⊆ cls1[{s}]) ∧ ∀other·(other ⊂ cls1 ∧ next ⊆ other ⇒ ¬(∀s·(s ∈ States ⇒ next[other[{s}]] ⊆ other[{s}])))"
+ ]
+ },
+ "execution_count": 35,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":prettyprint next ⊆ cls1 & ∀s.(s:States => next[cls1[{s}]] ⊆ cls1[{s}]) // we satisfy our axioms\n",
+ " & // all smaller relations do not satisfy our axioms:\n",
+ " ∀other.(other <<: cls1 & next ⊆ other ⇒ \n",
+ " not ( ∀s.(s:States ⇒ next[other[{s}]] <: other[{s}]) )\n",
+ " )"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "c51da9ad-2a9f-436e-beb9-3640ab24f7b5",
+ "metadata": {},
"outputs": [],
"source": []
}
diff --git a/mathematical/TransitiveClosure.pdf b/mathematical/TransitiveClosure.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..091e90bd57432c5af7bfdf58a5f07473be9264ab
Binary files /dev/null and b/mathematical/TransitiveClosure.pdf differ