diff --git a/sks/2_Relationen.ipynb b/sks/2_Relationen.ipynb index 0566fc7e77b376bfb82dc0b14a5f8691dc9fde4e..6d32b8db4951625086d9d13759b724800166631f 100644 --- a/sks/2_Relationen.ipynb +++ b/sks/2_Relationen.ipynb @@ -4,7 +4,30 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "# Relationen in B" + "# Relationen in B\n", + "\n", + "Relationen sind ein wichtiger Bestandteil der B Sprache.\n", + "Sie bauen auf Paaren auf." + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Changed language for user input to Event-B (forced)" + ] + }, + "execution_count": 7, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":language event_b" ] }, { @@ -18,7 +41,7 @@ }, { "cell_type": "code", - "execution_count": 20, + "execution_count": 8, "metadata": {}, "outputs": [ { @@ -30,7 +53,7 @@ "({TRUE}↦2)" ] }, - "execution_count": 20, + "execution_count": 8, "metadata": {}, "output_type": "execute_result" } @@ -48,7 +71,7 @@ }, { "cell_type": "code", - "execution_count": 21, + "execution_count": 9, "metadata": {}, "outputs": [ { @@ -60,7 +83,7 @@ "FALSE" ] }, - "execution_count": 21, + "execution_count": 9, "metadata": {}, "output_type": "execute_result" } @@ -78,7 +101,7 @@ }, { "cell_type": "code", - "execution_count": 24, + "execution_count": 10, "metadata": {}, "outputs": [ { @@ -90,7 +113,7 @@ "TRUE" ] }, - "execution_count": 24, + "execution_count": 10, "metadata": {}, "output_type": "execute_result" } @@ -111,7 +134,7 @@ }, { "cell_type": "code", - "execution_count": 25, + "execution_count": 12, "metadata": {}, "outputs": [ { @@ -123,18 +146,18 @@ "{(FALSE↦1),(FALSE↦2),(TRUE↦1),(TRUE↦2)}" ] }, - "execution_count": 25, + "execution_count": 12, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "{a,b | a:BOOL & b:1..2}" + "{a↦b | a:BOOL & b:1..2}" ] }, { "cell_type": "code", - "execution_count": 26, + "execution_count": 15, "metadata": {}, "outputs": [ { @@ -146,18 +169,18 @@ "{(FALSE↦1),(FALSE↦2),(TRUE↦1),(TRUE↦2)}" ] }, - "execution_count": 26, + "execution_count": 15, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "{p | ∃(a,b).( a:BOOL ∧ b:1..2 ∧ p=a↦b)}" + "{p | ∃a,b. a:BOOL ∧ b:1..2 ∧ p=a↦b}" ] }, { "cell_type": "code", - "execution_count": 29, + "execution_count": 16, "metadata": {}, "outputs": [ { @@ -169,7 +192,7 @@ "{(FALSE↦1),(FALSE↦2),(TRUE↦1),(TRUE↦2)}" ] }, - "execution_count": 29, + "execution_count": 16, "metadata": {}, "output_type": "execute_result" } @@ -190,7 +213,27 @@ }, { "cell_type": "code", - "execution_count": 31, + "execution_count": 22, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Changed language for user input to classical B (forced)" + ] + }, + "execution_count": 22, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":language classical_b" + ] + }, + { + "cell_type": "code", + "execution_count": 23, "metadata": {}, "outputs": [ { @@ -202,108 +245,99 @@ "<!-- Generated by graphviz version 2.28.0 (20110509.1545)\n", " -->\n", "<!-- Title: state Pages: 1 -->\n", - "<svg width=\"299pt\" height=\"134pt\"\n", - " viewBox=\"0.00 0.00 299.00 134.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 130)\">\n", + "<svg width=\"171pt\" height=\"224pt\"\n", + " viewBox=\"0.00 0.00 170.77 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=\"white\" stroke=\"white\" points=\"-4,5 -4,-130 296.001,-130 296.001,5 -4,5\"/>\n", - "<!-- TRUE -->\n", - "<g id=\"node1\" class=\"node\"><title>TRUE</title>\n", - "<ellipse fill=\"#698b22\" stroke=\"#698b22\" cx=\"68.0015\" cy=\"-108\" rx=\"36.3712\" ry=\"18\"/>\n", - "<text text-anchor=\"middle\" x=\"68.0015\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">TRUE</text>\n", - "</g>\n", - "<!-- 4 -->\n", - "<g id=\"node3\" class=\"node\"><title>4</title>\n", - "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"216.001,-36 162.001,-36 162.001,-0 216.001,-0 216.001,-36\"/>\n", - "<text text-anchor=\"middle\" x=\"189.001\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">4</text>\n", - "</g>\n", - "<!-- TRUE->4 -->\n", - "<g id=\"edge2\" class=\"edge\"><title>TRUE->4</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M82.1319,-90.8892C92.5029,-79.6693 107.325,-64.8342 122.236,-54 131.639,-47.1676 142.553,-40.8634 152.799,-35.5432\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"154.589,-38.5606 161.957,-30.947 151.45,-32.3043 154.589,-38.5606\"/>\n", - "<text text-anchor=\"middle\" x=\"130.384\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n", - "</g>\n", + "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-220 167.766,-220 167.766,5 -4,5\"/>\n", "<!-- 3 -->\n", - "<g id=\"node5\" class=\"node\"><title>3</title>\n", - "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"138.001,-36 84.0015,-36 84.0015,-0 138.001,-0 138.001,-36\"/>\n", - "<text text-anchor=\"middle\" x=\"111.001\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n", + "<g id=\"node1\" class=\"node\"><title>3</title>\n", + "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"130,-216 76,-216 76,-180 130,-180 130,-216\"/>\n", + "<text text-anchor=\"middle\" x=\"103\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n", "</g>\n", - "<!-- TRUE->3 -->\n", - "<g id=\"edge4\" class=\"edge\"><title>TRUE->3</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M51.8267,-91.7805C42.3723,-80.9807 33.6568,-66.2812 41.2357,-54 45.2928,-47.4255 59.5763,-39.7642 74.1715,-33.2884\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"75.8753,-36.367 83.7034,-29.2275 73.1316,-29.9271 75.8753,-36.367\"/>\n", - "<text text-anchor=\"middle\" x=\"49.3844\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n", + "<!-- 3->3 -->\n", + "<g id=\"edge2\" class=\"edge\"><title>3->3</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M130.241,-206.242C140.024,-206.419 148,-203.672 148,-198 148,-194.544 145.038,-192.173 140.51,-190.889\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"140.564,-187.374 130.241,-189.758 139.797,-194.332 140.564,-187.374\"/>\n", + "<text text-anchor=\"middle\" x=\"155.383\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n", "</g>\n", "<!-- 2 -->\n", - "<g id=\"node7\" class=\"node\"><title>2</title>\n", - "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"54.0015,-36 0.00146183,-36 0.00146183,-0 54.0015,-0 54.0015,-36\"/>\n", - "<text text-anchor=\"middle\" x=\"27.0015\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n", + "<g id=\"node4\" class=\"node\"><title>2</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\">2</text>\n", "</g>\n", - "<!-- TRUE->2 -->\n", - "<g id=\"edge6\" class=\"edge\"><title>TRUE->2</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M37.2146,-98.1916C24.3571,-92.8238 10.6976,-84.5144 3.23566,-72 -1.87717,-63.4253 0.518668,-53.5564 5.38031,-44.6766\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"8.36669,-46.5042 10.8771,-36.2111 2.49575,-42.6921 8.36669,-46.5042\"/>\n", - "<text text-anchor=\"middle\" x=\"11.3844\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n", + "<!-- 3->2 -->\n", + "<g id=\"edge4\" class=\"edge\"><title>3->2</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M75.9214,-184.195C66.1603,-178.51 55.7185,-171.039 48.2342,-162 41.9875,-154.456 37.3994,-144.839 34.1203,-135.874\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"37.3848,-134.596 30.9556,-126.174 30.73,-136.767 37.3848,-134.596\"/>\n", + "<text text-anchor=\"middle\" x=\"56.3829\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n", "</g>\n", "<!-- 1 -->\n", - "<g id=\"node9\" class=\"node\"><title>1</title>\n", - "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"291.001,-36 237.001,-36 237.001,-0 291.001,-0 291.001,-36\"/>\n", - "<text text-anchor=\"middle\" x=\"264.001\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n", + "<g id=\"node6\" class=\"node\"><title>1</title>\n", + "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"130,-36 76,-36 76,-0 130,-0 130,-36\"/>\n", + "<text text-anchor=\"middle\" x=\"103\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n", "</g>\n", - "<!-- TRUE->1 -->\n", - "<g id=\"edge8\" class=\"edge\"><title>TRUE->1</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M100.305,-99.6636C121.161,-94.0459 148.342,-85.025 170.001,-72 180.035,-65.9664 179.54,-60.5629 189.236,-54 192.891,-51.5258 210.341,-43.3284 227.463,-35.4887\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"229.204,-38.5414 236.852,-31.2087 226.301,-32.172 229.204,-38.5414\"/>\n", - "<text text-anchor=\"middle\" x=\"197.384\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n", + "<!-- 3->1 -->\n", + "<g id=\"edge6\" class=\"edge\"><title>3->1</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M103,-179.933C103,-148.966 103,-83.2989 103,-46.1292\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"106.5,-46.0157 103,-36.0157 99.5001,-46.0158 106.5,-46.0157\"/>\n", + "<text text-anchor=\"middle\" x=\"110.383\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n", "</g>\n", - "<!-- FALSE -->\n", - "<g id=\"node10\" class=\"node\"><title>FALSE</title>\n", - "<ellipse fill=\"brown\" stroke=\"brown\" cx=\"192.001\" cy=\"-108\" rx=\"40.3147\" ry=\"18\"/>\n", - "<text text-anchor=\"middle\" x=\"192.001\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">FALSE</text>\n", + "<!-- 2->3 -->\n", + "<g id=\"edge8\" class=\"edge\"><title>2->3</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M45.8607,-126.285C51.5522,-131.775 57.694,-137.987 63,-144 70.6296,-152.647 78.404,-162.628 85.0452,-171.581\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"82.3012,-173.758 91.0236,-179.773 87.9555,-169.632 82.3012,-173.758\"/>\n", + "<text text-anchor=\"middle\" x=\"84.3829\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n", "</g>\n", - "<!-- FALSE->4 -->\n", - "<g id=\"edge10\" class=\"edge\"><title>FALSE->4</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M201.824,-90.3971C206.773,-80.0038 211.124,-66.297 208.001,-54 207.243,-51.0137 206.173,-48.0066 204.923,-45.0763\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"208.051,-43.5054 200.476,-36.0975 201.778,-46.6121 208.051,-43.5054\"/>\n", - "<text text-anchor=\"middle\" x=\"217.384\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n", + "<!-- 2->2 -->\n", + "<g id=\"edge10\" class=\"edge\"><title>2->2</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M54.2408,-116.242C64.0239,-116.419 72,-113.672 72,-108 72,-104.544 69.0382,-102.173 64.5105,-100.889\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"64.5639,-97.3739 54.2408,-99.7581 63.7975,-104.332 64.5639,-97.3739\"/>\n", + "<text text-anchor=\"middle\" x=\"79.3829\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n", "</g>\n", - "<!-- FALSE->3 -->\n", - "<g id=\"edge12\" class=\"edge\"><title>FALSE->3</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M174.766,-91.3634C168.466,-85.4492 161.381,-78.5603 155.236,-72 146.955,-63.1602 138.319,-53.0399 130.898,-44.0279\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"133.497,-41.6771 124.47,-36.1316 128.069,-46.0964 133.497,-41.6771\"/>\n", - "<text text-anchor=\"middle\" x=\"163.384\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n", + "<!-- 2->1 -->\n", + "<g id=\"edge12\" class=\"edge\"><title>2->1</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M30.9556,-89.8256C34.181,-78.6924 39.6365,-64.3833 48.2342,-54 53.4966,-47.6446 60.2211,-42.0643 67.1431,-37.3347\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"69.326,-40.0963 75.9214,-31.8047 65.5948,-34.1735 69.326,-40.0963\"/>\n", + "<text text-anchor=\"middle\" x=\"56.3829\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n", + "</g>\n", + "<!-- 1->3 -->\n", + "<g id=\"edge14\" class=\"edge\"><title>1->3</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M110.927,-36.1399C113.22,-41.7288 115.504,-48.0328 117,-54 128.67,-100.56 128.67,-115.44 117,-162 116.322,-164.704 115.483,-167.477 114.553,-170.221\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"111.173,-169.268 110.927,-179.86 117.724,-171.733 111.173,-169.268\"/>\n", + "<text text-anchor=\"middle\" x=\"132.383\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n", "</g>\n", - "<!-- FALSE->2 -->\n", - "<g id=\"edge14\" class=\"edge\"><title>FALSE->2</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M156.035,-99.6936C133.993,-94.2067 105.78,-85.3174 83.2357,-72 70.5333,-64.4965 58.3672,-53.6596 48.6206,-43.7377\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"51.0878,-41.2528 41.6702,-36.3991 46.0055,-46.0664 51.0878,-41.2528\"/>\n", - "<text text-anchor=\"middle\" x=\"91.3844\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n", + "<!-- 1->2 -->\n", + "<g id=\"edge16\" class=\"edge\"><title>1->2</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M91.0236,-36.2273C83.3881,-46.8556 73.0679,-60.5901 63,-72 59.9324,-75.4764 56.5856,-79.0191 53.2079,-82.4505\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"50.5105,-80.1954 45.8607,-89.7154 55.4324,-85.173 50.5105,-80.1954\"/>\n", + "<text text-anchor=\"middle\" x=\"84.3829\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n", "</g>\n", - "<!-- FALSE->1 -->\n", - "<g id=\"edge16\" class=\"edge\"><title>FALSE->1</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M209.206,-91.636C215.411,-85.7514 222.287,-78.8115 228.001,-72 235.079,-63.5638 242.067,-53.7263 247.975,-44.8329\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"250.978,-46.6346 253.487,-36.3411 245.107,-42.8233 250.978,-46.6346\"/>\n", - "<text text-anchor=\"middle\" x=\"247.384\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n", + "<!-- 1->1 -->\n", + "<g id=\"edge18\" class=\"edge\"><title>1->1</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M130.241,-26.2419C140.024,-26.4192 148,-23.6719 148,-18 148,-14.5437 145.038,-12.1734 140.51,-10.8891\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"140.564,-7.3739 130.241,-9.75806 139.797,-14.3318 140.564,-7.3739\"/>\n", + "<text text-anchor=\"middle\" x=\"155.383\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n", "</g>\n", "</g>\n", "</svg>" ], "text/plain": [ - "<Dot visualization: expr_as_graph [(\"rel\",BOOL*(1..4))]>" + "<Dot visualization: expr_as_graph [(\"rel\",(1..3)*(1..3))]>" ] }, - "execution_count": 31, + "execution_count": 23, "metadata": {}, "output_type": "execute_result" } ], "source": [ - ":dot expr_as_graph (\"rel\",BOOL × (1..4))" + ":dot expr_as_graph (\"rel\",(1..3) × (1..3))" ] }, { "cell_type": "code", - "execution_count": 32, + "execution_count": 24, "metadata": {}, "outputs": [ { @@ -396,7 +430,7 @@ "<Dot visualization: expr_as_graph [(\"rel\",(1..3)*(1..3))]>" ] }, - "execution_count": 32, + "execution_count": 24, "metadata": {}, "output_type": "execute_result" } @@ -407,7 +441,7 @@ }, { "cell_type": "code", - "execution_count": 35, + "execution_count": 25, "metadata": {}, "outputs": [ { @@ -464,18 +498,18 @@ "<Dot visualization: expr_as_graph [(\"rel\",{(1,3),(3,2),(2,3)})]>" ] }, - "execution_count": 35, + "execution_count": 25, "metadata": {}, "output_type": "execute_result" } ], "source": [ - ":dot expr_as_graph (\"rel\",{1|->3,3|->2, 2|->3})" + ":dot expr_as_graph (\"rel\",{1↦3,3↦2, 2↦3})" ] }, { "cell_type": "code", - "execution_count": 34, + "execution_count": 26, "metadata": {}, "outputs": [ { @@ -487,7 +521,7 @@ "{(1↦1),(1↦2),(1↦3),(2↦1),(2↦2),(2↦3),(3↦1),(3↦2),(3↦3)}" ] }, - "execution_count": 34, + "execution_count": 26, "metadata": {}, "output_type": "execute_result" } @@ -498,16 +532,63 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 27, "metadata": {}, - "outputs": [], + "outputs": [ + { + "data": { + "text/markdown": [ + "|Elements|\n", + "|---|\n", + "|$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$|\n", + "|$\\{(1\\mapsto 1)\\}$|\n", + "|$\\{(1\\mapsto 1),(1\\mapsto 2)\\}$|\n", + "|$\\{(1\\mapsto 1),(2\\mapsto 1)\\}$|\n", + "|$\\{(1\\mapsto 1),(2\\mapsto 2)\\}$|\n", + "|$\\{(1\\mapsto 2)\\}$|\n", + "|$\\{(1\\mapsto 1),(1\\mapsto 2),(2\\mapsto 1)\\}$|\n", + "|$\\{(1\\mapsto 1),(1\\mapsto 2),(2\\mapsto 2)\\}$|\n", + "|$\\{(1\\mapsto 2),(2\\mapsto 1)\\}$|\n", + "|$\\{(1\\mapsto 2),(2\\mapsto 2)\\}$|\n", + "|$\\{(1\\mapsto 1),(1\\mapsto 2),(2\\mapsto 1),(2\\mapsto 2)\\}$|\n", + "|$\\{(2\\mapsto 1)\\}$|\n", + "|$\\{(1\\mapsto 1),(2\\mapsto 1),(2\\mapsto 2)\\}$|\n", + "|$\\{(1\\mapsto 2),(2\\mapsto 1),(2\\mapsto 2)\\}$|\n", + "|$\\{(2\\mapsto 1),(2\\mapsto 2)\\}$|\n", + "|$\\{(2\\mapsto 2)\\}$|\n" + ], + "text/plain": [ + "Elements\n", + "{}\n", + "{(1|->1)}\n", + "{(1|->1),(1|->2)}\n", + "{(1|->1),(2|->1)}\n", + "{(1|->1),(2|->2)}\n", + "{(1|->2)}\n", + "{(1|->1),(1|->2),(2|->1)}\n", + "{(1|->1),(1|->2),(2|->2)}\n", + "{(1|->2),(2|->1)}\n", + "{(1|->2),(2|->2)}\n", + "{(1|->1),(1|->2),(2|->1),(2|->2)}\n", + "{(2|->1)}\n", + "{(1|->1),(2|->1),(2|->2)}\n", + "{(1|->2),(2|->1),(2|->2)}\n", + "{(2|->1),(2|->2)}\n", + "{(2|->2)}\n" + ] + }, + "execution_count": 27, + "metadata": {}, + "output_type": "execute_result" + } + ], "source": [ ":table POW((1..2)×(1..2))" ] }, { "cell_type": "code", - "execution_count": 40, + "execution_count": 28, "metadata": {}, "outputs": [ { @@ -552,7 +633,7 @@ "{(TRUE|->2)}\n" ] }, - "execution_count": 40, + "execution_count": 28, "metadata": {}, "output_type": "execute_result" } @@ -563,7 +644,7 @@ }, { "cell_type": "code", - "execution_count": 43, + "execution_count": 29, "metadata": {}, "outputs": [ { @@ -575,18 +656,18 @@ "{(3↦3)}" ] }, - "execution_count": 43, + "execution_count": 29, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "{1|->3,3|->2, 3|->3} /\\ id(1..3)" + "{1↦3,3↦2, 3↦3} /\\ id(1..3)" ] }, { "cell_type": "code", - "execution_count": 44, + "execution_count": 30, "metadata": {}, "outputs": [ { @@ -643,7 +724,7 @@ "<Dot visualization: expr_as_graph [(\"rel\",id(1..3))]>" ] }, - "execution_count": 44, + "execution_count": 30, "metadata": {}, "output_type": "execute_result" } @@ -652,6 +733,26 @@ ":dot expr_as_graph (\"rel\",id(1..3))" ] }, + { + "cell_type": "code", + "execution_count": 31, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Changed language for user input to Event-B (forced)" + ] + }, + "execution_count": 31, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":language event_b" + ] + }, { "cell_type": "markdown", "metadata": {}, @@ -665,7 +766,7 @@ }, { "cell_type": "code", - "execution_count": 52, + "execution_count": 32, "metadata": {}, "outputs": [ { @@ -677,18 +778,25 @@ "{2,3}" ] }, - "execution_count": 52, + "execution_count": 32, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "{1|->3,3|->2, 3|->3} [ {3} ]" + "{1↦3,3↦2, 3↦3} [ {3} ]" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Das relational image kann man auch so ausdrücken:" ] }, { "cell_type": "code", - "execution_count": 53, + "execution_count": 33, "metadata": {}, "outputs": [ { @@ -708,18 +816,25 @@ "\tr = {(1↦3),(3↦2),(3↦3)}" ] }, - "execution_count": 53, + "execution_count": 33, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "r={1|->3,3|->2, 3|->3} & img3 = {y | 3|->y : r}" + "r={1↦3,3↦2, 3↦3} & img3 = {y | 3↦y : r}" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Wenn man das Paar umdreht kann man von der Zielmenge rückwärts mögliche Eingaben bestimmen:" ] }, { "cell_type": "code", - "execution_count": 54, + "execution_count": 34, "metadata": {}, "outputs": [ { @@ -739,18 +854,25 @@ "\tr = {(1↦3),(3↦2),(3↦3)}" ] }, - "execution_count": 54, + "execution_count": 34, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "r={1|->3,3|->2, 3|->3} & img3 = {y | y|->3 : r}" + "r={1↦3,3↦2, 3↦3} & img3 = {y | y↦3 : r}" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Bequemer geht dies mit dem relationalen Abbild und dem Umkehroperator ```~```" ] }, { "cell_type": "code", - "execution_count": 56, + "execution_count": 36, "metadata": {}, "outputs": [ { @@ -762,13 +884,20 @@ "{1,3}" ] }, - "execution_count": 56, + "execution_count": 36, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "{1|->3,3|->2, 3|->3}~[{3}]" + "{1↦3,3↦2, 3↦3}~[{3}]" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Mit dom und ran kann man die Domäne und den Wertebereich einer Relation berrechnen:" ] }, { @@ -791,7 +920,7 @@ } ], "source": [ - "dom({1|->3,3|->2, 3|->4})" + "dom({1↦3,3↦2, 3↦4})" ] }, { @@ -814,12 +943,19 @@ } ], "source": [ - "ran({1|->3,3|->2, 3|->4})" + "ran({1↦3,3↦2, 3↦4})" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Man kann Relationen mit dem ```;``` Operator verketten:" ] }, { "cell_type": "code", - "execution_count": 60, + "execution_count": 38, "metadata": {}, "outputs": [ { @@ -831,13 +967,20 @@ "{(1↦2),(1↦44)}" ] }, - "execution_count": 60, + "execution_count": 38, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "({1|->3,3|->2, 3|->4} ; {1|->3,3|->2, 3|->44})" + "({1↦3,3↦2, 3↦4} ; {1↦3,3↦2, 3↦44})" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Mit dem Override Operator ```<+``` kann man eine Relation an bestimmten Stellen überschreiben:" ] }, { @@ -860,12 +1003,19 @@ } ], "source": [ - "{11 |-> TRUE, 22|->FALSE,22|->TRUE} <+ {22|->TRUE,33|->FALSE}" + "{11 ↦ TRUE, 22 ↦ FALSE,22 ↦ TRUE} <+ {22↦TRUE,33↦FALSE}" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Mit dem Domain Restriction Operator ```<|``` kann man eine Relation auf eine Domäne einschränken. Es gibt insgesamt vier Operatoren um Relationen einzuschränken ```<|```, ```<<|```, ```|>```, ```|>>```." ] }, { "cell_type": "code", - "execution_count": 69, + "execution_count": 42, "metadata": {}, "outputs": [ { @@ -877,18 +1027,18 @@ "{(22↦FALSE),(22↦TRUE)}" ] }, - "execution_count": 69, + "execution_count": 42, "metadata": {}, "output_type": "execute_result" } ], "source": [ - " {22} <| {11 |-> TRUE, 22|->FALSE,22|->TRUE, 33|->FALSE} " + " {22} <| {11 ↦ TRUE, 22 ↦ FALSE,22 ↦ TRUE, 33 ↦ FALSE} " ] }, { "cell_type": "code", - "execution_count": 67, + "execution_count": 43, "metadata": {}, "outputs": [ { @@ -900,18 +1050,18 @@ "{FALSE,TRUE}" ] }, - "execution_count": 67, + "execution_count": 43, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "{11 |-> TRUE, 22|->FALSE,22|->TRUE, 33|->FALSE} [{22}]" + "{11 ↦ TRUE, 22 ↦ FALSE,22 ↦ TRUE, 33 ↦ FALSE} [{22}]" ] }, { "cell_type": "code", - "execution_count": 71, + "execution_count": 44, "metadata": {}, "outputs": [ { @@ -923,13 +1073,13 @@ "{(11↦TRUE)}" ] }, - "execution_count": 71, + "execution_count": 44, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "{11} <| {11 |-> TRUE, 22|->FALSE,22|->TRUE, 33|->FALSE} |> {TRUE}" + "{11} <| {11 ↦ TRUE, 22 ↦ FALSE,22 ↦ TRUE, 33 ↦ FALSE} |> {TRUE}" ] }, { @@ -941,19 +1091,19 @@ }, { "cell_type": "code", - "execution_count": 73, + "execution_count": 45, "metadata": {}, "outputs": [ { "data": { "text/markdown": [ - "$\\{(2\\mapsto 2),(3\\mapsto 3)\\}$" + "$\\{2,3\\}$" ], "text/plain": [ - "{(2↦2),(3↦3)}" + "{2,3}" ] }, - "execution_count": 73, + "execution_count": 45, "metadata": {}, "output_type": "execute_result" } @@ -964,7 +1114,7 @@ }, { "cell_type": "code", - "execution_count": 75, + "execution_count": 46, "metadata": {}, "outputs": [ { @@ -1009,7 +1159,7 @@ "{(TRUE|->2)}\n" ] }, - "execution_count": 75, + "execution_count": 46, "metadata": {}, "output_type": "execute_result" } @@ -1020,7 +1170,7 @@ }, { "cell_type": "code", - "execution_count": 76, + "execution_count": 47, "metadata": {}, "outputs": [ { @@ -1041,7 +1191,7 @@ "{(FALSE|->2),(TRUE|->2)}\n" ] }, - "execution_count": 76, + "execution_count": 47, "metadata": {}, "output_type": "execute_result" } @@ -1052,7 +1202,7 @@ }, { "cell_type": "code", - "execution_count": 84, + "execution_count": 48, "metadata": {}, "outputs": [ { @@ -1064,18 +1214,18 @@ "{2800}" ] }, - "execution_count": 84, + "execution_count": 48, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "{11|->2800, 22|->3500}[{11}]" + "{11↦2800, 22↦3500}[{11}]" ] }, { "cell_type": "code", - "execution_count": 87, + "execution_count": 49, "metadata": {}, "outputs": [ { @@ -1087,18 +1237,25 @@ "2800" ] }, - "execution_count": 87, + "execution_count": 49, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "({11|->2800,22|->3500}(11))" + "({11↦2800,22↦3500}(11))" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Mit dem Lambda Operator ```%``` kann man Funktionen erstellen:" ] }, { "cell_type": "code", - "execution_count": 90, + "execution_count": 51, "metadata": {}, "outputs": [ { @@ -1110,18 +1267,25 @@ "{(0↦1),(1↦2),(2↦3),(3↦4),(4↦5),(5↦6),(6↦7),(7↦8),(8↦9),(9↦0)}" ] }, - "execution_count": 90, + "execution_count": 51, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "%x.(x:0..9|(x+1) mod 10)" + "(%x.x:0..9|(x+1) mod 10)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Dies ist äquivalent zu:" ] }, { "cell_type": "code", - "execution_count": 91, + "execution_count": 53, "metadata": {}, "outputs": [ { @@ -1133,13 +1297,13 @@ "{(0↦1),(1↦2),(2↦3),(3↦4),(4↦5),(5↦6),(6↦7),(7↦8),(8↦9),(9↦0)}" ] }, - "execution_count": 91, + "execution_count": 53, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "{x,result | x:0..9 & result = (x+1) mod 10}" + "{x↦result | x:0..9 & result = (x+1) mod 10}" ] }, {