diff --git a/notebooks/presentations/BadHonnef_2019.ipynb b/notebooks/presentations/BadHonnef_2019.ipynb
index 8c5bb599f5ed8dd5cf8b1925ca020a140ee4b8bf..20dfdad1a2ba5497d18bdf2adcd711e48a6476e6 100644
--- a/notebooks/presentations/BadHonnef_2019.ipynb
+++ b/notebooks/presentations/BadHonnef_2019.ipynb
@@ -12,6 +12,7 @@
"\n",
"### David Geleßus, Michael Leuschel\n",
"### Bad Honnef, 2019\n",
+ "#### 36. Workshop der GI-Fachgruppe Programmiersprachen und Rechenkonzepte\n",
"\n",
""
]
@@ -62,6 +63,7 @@
"* Browserbasierte Notebook-Oberfläche\n",
"* Open Source und plattformübergreifend\n",
"* Stammt aus der Python-Community, in Python implementiert\n",
+ "* ACM System Software Award 2017\n",
"* Jupyter-Notebooks können aber verschiedene Programmiersprachen verwenden\n",
"* Dazu trennt Jupyter strikt zwischen Frontend und Kernel:\n",
" * Das allgemeine **Frontend** implementiert z. B. Benutzeroberfläche und Dateiformat\n",
@@ -84,6 +86,7 @@
"* Grundlage: Solver für Prädikatenlogik, Mengentheorie mit Relationen, Funktionen und Arithmetik.\n",
"* Unterstützt hauptsächlich B-Spezifikationen (klassisches B, Event-B)\n",
"* Versteht auch andere Sprachen wie TLA<sup>+</sup> und CSP<sub>M</sub>\n",
+ "* Verschiedene Solver Backends (CLP, SAT, SMT), verschiedene Modelchecking Backends (Prolog, parB, C für LTL, LTSMin [sym,seq,par], TLC)\n",
"* ProBs APIs sind für alle Sprachen gleich\n",
" * Der ProB 2-Jupyter-Kernel unterstützt daher (fast) alle Sprachen, die ProB versteht"
]
@@ -93,13 +96,15 @@
"metadata": {},
"source": [
"## Einsatz von ProB in der Industrie\n",
- "* Datenvalidierung: Siemens (Paris Line 1, Barcelona, Alger, ...), Alstom (Amsterdam,...), Thales (Schweiz,...), RATP, SNCF, ...\n",
+ "* Datenvalidierung: Siemens (Paris Line 1, Barcelona, Alger, ...), Alstom (Amsterdam,...), Thales (Schweiz, Dänemark, Slovenien, Thailand,...), RATP, SNCF, ...\n",
"* Zertifizierung als T2 Werkzeug nach EN50128\n",
"* Validierung von Systemmodellen: ClearSy (Octys, ...),...\n",
"* Ausführung formaler Modelle in Echtzeit\n",
" * SlotTool \n",
" * Hybrid Level 3 - ETCS (Thales, ProRail/Network Rail/DB), Video der Deutschen Bahn: https://www.youtube.com/watch?v=FjKnugbmrP4\n",
- ""
+ "\n",
+ "\n",
+ "* Anmerkung: in etwa 30% aller CBTC U-Bahnen weltweit benutzen B."
]
},
{
@@ -143,30 +148,30 @@
},
{
"cell_type": "code",
- "execution_count": 1,
+ "execution_count": 48,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$\\{2,3,5,7,11,13,17,19,23,29,31,37,41,43,47\\}$"
+ "$\\{2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,89,97,101,103,107,109,113,127,131,137,139,149,151,157,163,167,173,179,181,191,193,197,199,211,223,227,229,233,239,241,251,257,263,269,271,277,281,283,293,307,311,313,317,331,337,347,349,353,359,367,373,379,383,389,397,401,409,419,421,431,433,439,443,449,457,461,463,467,479,487,491,499\\}$"
],
"text/plain": [
- "{2,3,5,7,11,13,17,19,23,29,31,37,41,43,47}"
+ "{2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,89,97,101,103,107,109,113,127,131,137,139,149,151,157,163,167,173,179,181,191,193,197,199,211,223,227,229,233,239,241,251,257,263,269,271,277,281,283,293,307,311,313,317,331,337,347,349,353,359,367,373,379,383,389,397,401,409,419,421,431,433,439,443,449,457,461,463,467,479,487,491,499}"
]
},
- "execution_count": 1,
+ "execution_count": 48,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- "{x | x > 1 & x < 50 & not(#y.(y > 1 & y < x & x mod y = 0))}"
+ "{x | x > 1 & x < 500 & not(#y.(y > 1 & y < x & x mod y = 0))}"
]
},
{
"cell_type": "code",
- "execution_count": 2,
+ "execution_count": 49,
"metadata": {},
"outputs": [
{
@@ -178,7 +183,7 @@
"x > 1 ∧ x < 50 ∧ ¬(∃y·(y > 1 ∧ y < x ∧ x mod y = 0))"
]
},
- "execution_count": 2,
+ "execution_count": 49,
"metadata": {},
"output_type": "execute_result"
}
@@ -200,7 +205,7 @@
},
{
"cell_type": "code",
- "execution_count": 3,
+ "execution_count": 50,
"metadata": {},
"outputs": [
{
@@ -212,7 +217,7 @@
"{2,3,5,7,11,13,17,19,23,29,31,37,41,43,47}"
]
},
- "execution_count": 3,
+ "execution_count": 50,
"metadata": {},
"output_type": "execute_result"
}
@@ -234,7 +239,7 @@
},
{
"cell_type": "code",
- "execution_count": 4,
+ "execution_count": 51,
"metadata": {},
"outputs": [
{
@@ -266,7 +271,7 @@
"\tO = 0"
]
},
- "execution_count": 4,
+ "execution_count": 51,
"metadata": {},
"output_type": "execute_result"
}
@@ -294,7 +299,7 @@
},
{
"cell_type": "code",
- "execution_count": 5,
+ "execution_count": 52,
"metadata": {},
"outputs": [
{
@@ -309,7 +314,7 @@
"9\t5\t6\t7\t1\t0\t8\t2\n"
]
},
- "execution_count": 5,
+ "execution_count": 52,
"metadata": {},
"output_type": "execute_result"
}
@@ -342,7 +347,50 @@
},
{
"cell_type": "code",
- "execution_count": 6,
+ "execution_count": 53,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(2\\mapsto 1),(3\\mapsto 1),(3\\mapsto 2),(4\\mapsto 1),(4\\mapsto 2),(4\\mapsto 3),(5\\mapsto 1),(5\\mapsto 2),(5\\mapsto 3),(5\\mapsto 4)\\}$"
+ ],
+ "text/plain": [
+ "{(2↦1),(3↦1),(3↦2),(4↦1),(4↦2),(4↦3),(5↦1),(5↦2),(5↦3),(5↦4)}"
+ ]
+ },
+ "execution_count": 53,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{x,y|x:1..5 & y:1..5 & x>y}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 54,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Preference changed: DOT_ENGINE = circo\n"
+ ]
+ },
+ "execution_count": 54,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":pref DOT_ENGINE=circo"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 84,
"metadata": {},
"outputs": [
{
@@ -451,153 +499,13 @@
"<Dot visualization: expr_as_graph [(\"k5\",{x,y|x:1..5 & y:1..5 & x>y})]>"
]
},
- "execution_count": 6,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- ":dot expr_as_graph (\"k5\",{x,y|x:1..5 & y:1..5 & x>y})"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 7,
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "Preference changed: DOT_ENGINE = circo\n"
- ]
- },
- "execution_count": 7,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- ":pref DOT_ENGINE=circo"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 8,
- "metadata": {},
- "outputs": [
- {
- "data": {
- "image/svg+xml": [
- "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
- "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
- " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
- "<!-- Generated by graphviz version 2.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",
- "<!-- 5 -->\n",
- "<g id=\"node1\" class=\"node\"><title>5</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\">5</text>\n",
- "</g>\n",
- "<!-- 4 -->\n",
- "<g id=\"node3\" class=\"node\"><title>4</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\">4</text>\n",
- "</g>\n",
- "<!-- 5->4 -->\n",
- "<g id=\"edge2\" class=\"edge\"><title>5->4</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M152.461,-36.3864C162.879,-50.7254 177.49,-70.8353 189.165,-86.9044\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"186.594,-89.3207 195.303,-95.3536 192.257,-85.2062 186.594,-89.3207\"/>\n",
- "<text text-anchor=\"middle\" x=\"179.813\" y=\"-50.4454\" font-family=\"Times,serif\" font-size=\"14.00\">k5</text>\n",
- "</g>\n",
- "<!-- 3 -->\n",
- "<g id=\"node5\" class=\"node\"><title>3</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\">3</text>\n",
- "</g>\n",
- "<!-- 5->3 -->\n",
- "<g id=\"edge4\" class=\"edge\"><title>5->3</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M126.024,-36.0017C106.385,-63.0326 69.1556,-114.274 46.3626,-145.646\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"43.3895,-143.783 40.3432,-153.931 49.0526,-147.898 43.3895,-143.783\"/>\n",
- "<text text-anchor=\"middle\" x=\"95.1931\" y=\"-93.6237\" font-family=\"Times,serif\" font-size=\"14.00\">k5</text>\n",
- "</g>\n",
- "<!-- 2 -->\n",
- "<g id=\"node7\" class=\"node\"><title>2</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\">2</text>\n",
- "</g>\n",
- "<!-- 5->2 -->\n",
- "<g id=\"edge6\" class=\"edge\"><title>5->2</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M139.103,-36.2871C139.103,-69.6799 139.103,-140.734 139.103,-180.418\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"135.603,-180.489 139.103,-190.489 142.603,-180.489 135.603,-180.489\"/>\n",
- "<text text-anchor=\"middle\" x=\"131.103\" y=\"-104.152\" font-family=\"Times,serif\" font-size=\"14.00\">k5</text>\n",
- "</g>\n",
- "<!-- 1 -->\n",
- "<g id=\"node9\" class=\"node\"><title>1</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\">1</text>\n",
- "</g>\n",
- "<!-- 5->1 -->\n",
- "<g id=\"edge8\" class=\"edge\"><title>5->1</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M111.966,-26.8173C97.6137,-31.4806 79.779,-37.2754 64.1603,-42.3502\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" 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\">k5</text>\n",
- "</g>\n",
- "<!-- 4->3 -->\n",
- "<g id=\"edge10\" class=\"edge\"><title>4->3</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M181.231,-122.183C150.018,-132.325 98.6277,-149.023 63.8291,-160.33\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"62.4733,-157.09 54.0443,-163.509 64.6364,-163.747 62.4733,-157.09\"/>\n",
- "<text text-anchor=\"middle\" x=\"125.53\" y=\"-147.056\" font-family=\"Times,serif\" font-size=\"14.00\">k5</text>\n",
- "</g>\n",
- "<!-- 4->2 -->\n",
- "<g id=\"edge12\" class=\"edge\"><title>4->2</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M195.027,-131.747C184.609,-146.086 169.999,-166.196 158.324,-182.265\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"155.231,-180.566 152.185,-190.714 160.895,-184.681 155.231,-180.566\"/>\n",
- "<text text-anchor=\"middle\" x=\"185.676\" y=\"-159.806\" font-family=\"Times,serif\" font-size=\"14.00\">k5</text>\n",
- "</g>\n",
- "<!-- 4->1 -->\n",
- "<g id=\"edge14\" class=\"edge\"><title>4->1</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M181.231,-104.537C150.018,-94.3953 98.6277,-77.6976 63.8291,-66.3908\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"64.6364,-62.9731 54.0443,-63.2116 62.4733,-69.6305 64.6364,-62.9731\"/>\n",
- "<text text-anchor=\"middle\" x=\"119.53\" y=\"-91.2639\" font-family=\"Times,serif\" font-size=\"14.00\">k5</text>\n",
- "</g>\n",
- "<!-- 3->2 -->\n",
- "<g id=\"edge16\" class=\"edge\"><title>3->2</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M54.1369,-181.113C68.4889,-185.777 86.3236,-191.571 101.942,-196.646\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"101.235,-200.096 111.827,-199.858 103.398,-193.439 101.235,-200.096\"/>\n",
- "<text text-anchor=\"middle\" x=\"81.0396\" y=\"-174.68\" font-family=\"Times,serif\" font-size=\"14.00\">k5</text>\n",
- "</g>\n",
- "<!-- 3->1 -->\n",
- "<g id=\"edge18\" class=\"edge\"><title>3->1</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M27,-154.137C27,-135.157 27,-105.11 27,-82.9567\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"30.5001,-82.7983 27,-72.7983 23.5001,-82.7983 30.5001,-82.7983\"/>\n",
- "<text text-anchor=\"middle\" x=\"35\" y=\"-114.347\" font-family=\"Times,serif\" font-size=\"14.00\">k5</text>\n",
- "</g>\n",
- "<!-- 2->1 -->\n",
- "<g id=\"edge20\" class=\"edge\"><title>2->1</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M126.024,-190.719C106.385,-163.688 69.1556,-112.447 46.3626,-81.0746\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"49.0526,-78.8226 40.3432,-72.7896 43.3895,-82.9371 49.0526,-78.8226\"/>\n",
- "<text text-anchor=\"middle\" x=\"77.1931\" y=\"-138.697\" font-family=\"Times,serif\" font-size=\"14.00\">k5</text>\n",
- "</g>\n",
- "</g>\n",
- "</svg>"
- ],
- "text/plain": [
- "<Dot visualization: expr_as_graph [(\"k5\",{x,y|x:1..5 & y:1..5 & x>y})]>"
- ]
- },
- "execution_count": 8,
+ "execution_count": 84,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- ":dot expr_as_graph (\"k5\",{x,y|x:1..5 & y:1..5 & x>y})"
+ ":dot expr_as_graph (\"k5\",({x,y|x:1..5 & y:1..5 & x>y} ))"
]
},
{
@@ -674,7 +582,7 @@
},
{
"cell_type": "code",
- "execution_count": 9,
+ "execution_count": 58,
"metadata": {},
"outputs": [
{
@@ -683,7 +591,7 @@
"Loaded machine: Jupyter_LibraryRegex"
]
},
- "execution_count": 9,
+ "execution_count": 58,
"metadata": {},
"output_type": "execute_result"
}
@@ -712,7 +620,7 @@
},
{
"cell_type": "code",
- "execution_count": 10,
+ "execution_count": 59,
"metadata": {},
"outputs": [
{
@@ -724,7 +632,7 @@
"{(1↦\"234\"),(2↦\"567\")}"
]
},
- "execution_count": 10,
+ "execution_count": 59,
"metadata": {},
"output_type": "execute_result"
}
@@ -735,7 +643,7 @@
},
{
"cell_type": "code",
- "execution_count": 11,
+ "execution_count": 60,
"metadata": {},
"outputs": [
{
@@ -747,7 +655,7 @@
"[\"a\",\"b\",\"c\",\"ä\",\"é\",\"à\"]"
]
},
- "execution_count": 11,
+ "execution_count": 60,
"metadata": {},
"output_type": "execute_result"
}
@@ -770,20 +678,9 @@
},
{
"cell_type": "code",
- "execution_count": 12,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "Loaded machine: BaseTypes"
- ]
- },
- "execution_count": 12,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"::load\n",
"MACHINE BaseTypes\n",
@@ -808,23 +705,9 @@
},
{
"cell_type": "code",
- "execution_count": 13,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "$\\{(\\mathit{peter}\\mapsto \\mathit{red}),(\\mathit{peter}\\mapsto \\mathit{green}),(\\mathit{peter}\\mapsto \\mathit{blue}),(\\mathit{paul}\\mapsto \\mathit{red}),(\\mathit{paul}\\mapsto \\mathit{green}),(\\mathit{paul}\\mapsto \\mathit{blue}),(\\mathit{mary}\\mapsto \\mathit{red}),(\\mathit{mary}\\mapsto \\mathit{green}),(\\mathit{mary}\\mapsto \\mathit{blue})\\}$"
- ],
- "text/plain": [
- "{(peter↦red),(peter↦green),(peter↦blue),(paul↦red),(paul↦green),(paul↦blue),(mary↦red),(mary↦green),(mary↦blue)}"
- ]
- },
- "execution_count": 13,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"PERSONS × COLOURS"
]
@@ -842,23 +725,9 @@
},
{
"cell_type": "code",
- "execution_count": 14,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "$\\{(\\mathit{peter}\\mapsto \\mathit{green}),(\\mathit{peter}\\mapsto \\mathit{blue}),(\\mathit{mary}\\mapsto \\mathit{blue})\\}$"
- ],
- "text/plain": [
- "{(peter↦green),(peter↦blue),(mary↦blue)}"
- ]
- },
- "execution_count": 14,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"{peter|->green,peter|->blue,mary|->blue}"
]
@@ -876,111 +745,18 @@
},
{
"cell_type": "code",
- "execution_count": 15,
+ "execution_count": null,
"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=\"166pt\" height=\"208pt\"\n",
- " viewBox=\"0.00 0.00 166.00 208.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 204)\">\n",
- "<title>state</title>\n",
- "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-204 163,-204 163,5 -4,5\"/>\n",
- "<g id=\"graph2\" class=\"cluster\"><title>cluster_PERSONS</title>\n",
- "<polygon fill=\"lightgrey\" stroke=\"lightgrey\" points=\"8,-118 8,-192 150,-192 150,-118 8,-118\"/>\n",
- "<text text-anchor=\"middle\" x=\"79\" y=\"-177.2\" font-family=\"Times,serif\" font-size=\"12.00\">PERSONS</text>\n",
- "</g>\n",
- "<g id=\"graph3\" class=\"cluster\"><title>cluster_COLOURS</title>\n",
- "<polygon fill=\"lightgrey\" stroke=\"lightgrey\" points=\"8,-8 8,-82 150,-82 150,-8 8,-8\"/>\n",
- "<text text-anchor=\"middle\" x=\"79\" y=\"-67.2\" font-family=\"Times,serif\" font-size=\"12.00\">COLOURS</text>\n",
- "</g>\n",
- "<!-- mary -->\n",
- "<g id=\"node1\" class=\"node\"><title>mary</title>\n",
- "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-162 16,-162 16,-126 70,-126 70,-162\"/>\n",
- "<text text-anchor=\"middle\" x=\"43\" y=\"-139.8\" font-family=\"Times,serif\" font-size=\"14.00\">mary</text>\n",
- "</g>\n",
- "<!-- blue -->\n",
- "<g id=\"node3\" class=\"node\"><title>blue</title>\n",
- "<polygon fill=\"#bdef6b\" stroke=\"#bdef6b\" points=\"70,-52 16,-52 16,-16 70,-16 70,-52\"/>\n",
- "<text text-anchor=\"middle\" x=\"43\" y=\"-29.8\" font-family=\"Times,serif\" font-size=\"14.00\">blue</text>\n",
- "</g>\n",
- "<!-- mary->blue -->\n",
- "<g id=\"edge2\" class=\"edge\"><title>mary->blue</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M43,-125.648C43,-108.564 43,-82.215 43,-62.3195\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"46.5001,-62.309 43,-52.309 39.5001,-62.309 46.5001,-62.309\"/>\n",
- "<text text-anchor=\"middle\" x=\"48.8303\" y=\"-94.8\" font-family=\"Times,serif\" font-size=\"14.00\">r1</text>\n",
- "</g>\n",
- "<!-- peter -->\n",
- "<g id=\"node4\" class=\"node\"><title>peter</title>\n",
- "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"142,-162 88,-162 88,-126 142,-126 142,-162\"/>\n",
- "<text text-anchor=\"middle\" x=\"115\" y=\"-139.8\" font-family=\"Times,serif\" font-size=\"14.00\">peter</text>\n",
- "</g>\n",
- "<!-- peter->blue -->\n",
- "<g id=\"edge4\" class=\"edge\"><title>peter->blue</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M103.432,-125.648C91.728,-108.092 73.5006,-80.7508 60.1229,-60.6843\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"62.9986,-58.6881 54.5393,-52.309 57.1742,-62.571 62.9986,-58.6881\"/>\n",
- "<text text-anchor=\"middle\" x=\"95.8303\" y=\"-94.8\" font-family=\"Times,serif\" font-size=\"14.00\">r1</text>\n",
- "</g>\n",
- "<!-- green -->\n",
- "<g id=\"node7\" class=\"node\"><title>green</title>\n",
- "<polygon fill=\"#bdef6b\" stroke=\"#bdef6b\" points=\"142,-52 88,-52 88,-16 142,-16 142,-52\"/>\n",
- "<text text-anchor=\"middle\" x=\"115\" y=\"-29.8\" font-family=\"Times,serif\" font-size=\"14.00\">green</text>\n",
- "</g>\n",
- "<!-- peter->green -->\n",
- "<g id=\"edge6\" class=\"edge\"><title>peter->green</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M115,-125.648C115,-108.564 115,-82.215 115,-62.3195\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"118.5,-62.309 115,-52.309 111.5,-62.309 118.5,-62.309\"/>\n",
- "<text text-anchor=\"middle\" x=\"120.83\" y=\"-94.8\" font-family=\"Times,serif\" font-size=\"14.00\">r1</text>\n",
- "</g>\n",
- "</g>\n",
- "</svg>"
- ],
- "text/plain": [
- "<Dot visualization: expr_as_graph [(\"r1\",{(peter,green),(peter,blue),(mary,blue)})]>"
- ]
- },
- "execution_count": 15,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":dot expr_as_graph (\"r1\",{peter|->green,peter|->blue,mary|->blue})"
]
},
{
"cell_type": "code",
- "execution_count": 16,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "|prj1|prj2|\n",
- "|---|---|\n",
- "|$\\mathit{peter}$|$\\mathit{green}$|\n",
- "|$\\mathit{peter}$|$\\mathit{blue}$|\n",
- "|$\\mathit{mary}$|$\\mathit{blue}$|\n"
- ],
- "text/plain": [
- "prj1\tprj2\n",
- "peter\tgreen\n",
- "peter\tblue\n",
- "mary\tblue\n"
- ]
- },
- "execution_count": 16,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":table {peter|->green,peter|->blue,mary|->blue}"
]
@@ -999,46 +775,18 @@
},
{
"cell_type": "code",
- "execution_count": 17,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "$\\{(\\mathit{peter}\\mapsto \\mathit{green}),(\\mathit{peter}\\mapsto \\mathit{blue})\\}$"
- ],
- "text/plain": [
- "{(peter↦green),(peter↦blue)}"
- ]
- },
- "execution_count": 17,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"{peter|->green,peter|->blue,mary|->blue} - {mary|->blue}"
]
},
{
"cell_type": "code",
- "execution_count": 18,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "$\\{(\\mathit{mary}\\mapsto \\mathit{blue})\\}$"
- ],
- "text/plain": [
- "{(mary↦blue)}"
- ]
- },
- "execution_count": 18,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"{peter|->green,peter|->blue,mary|->blue} /\\ {mary}*COLOURS"
]
@@ -1099,7 +847,7 @@
},
{
"cell_type": "code",
- "execution_count": 20,
+ "execution_count": 3,
"metadata": {},
"outputs": [
{
@@ -1108,7 +856,7 @@
"Loaded machine: NFA_nach_DFA"
]
},
- "execution_count": 20,
+ "execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
@@ -1124,10 +872,10 @@
" S ⊆ Z ∧ F ⊆ Z ∧ δ ∈ (Z×Σ) → ℙ(Z) ∧\n",
"\n",
" /* Definition der erweiterten Übergangsfunktion */\n",
- " δs = λ(ZZ,s).(ZZ⊆Z | IF s=[] THEN ZZ ELSE UNION(z).(z∈ZZ|δs(δ(z,first(s)),tail(s))) END )\n",
+ " δs = λ(Z2,s).(Z2⊆Z | IF s=[] THEN Z2 ELSE UNION(z).(z∈Z2|δs(δ(z,first(s)),tail(s))) END )\n",
" ∧\n",
" /* die vom Automaten generierte Sprache */\n",
- " L = {s|s∈seq(Σ) ∧ δs(S,s) ∩ F ≠ ∅}\n",
+ " L = {ω|ω∈seq(Σ) ∧ δs(S,ω) ∩ F ≠ ∅}\n",
" ∧\n",
" /* Nun ein Beispiel-Automat von Folie 24 (Info 4) */\n",
" Σ = {0,1} ∧\n",
@@ -1141,7 +889,7 @@
},
{
"cell_type": "code",
- "execution_count": 21,
+ "execution_count": 62,
"metadata": {},
"outputs": [
{
@@ -1150,7 +898,7 @@
"Machine constants set up using operation 0: $setup_constants()"
]
},
- "execution_count": 21,
+ "execution_count": 62,
"metadata": {},
"output_type": "execute_result"
}
@@ -1161,7 +909,7 @@
},
{
"cell_type": "code",
- "execution_count": 22,
+ "execution_count": 63,
"metadata": {},
"outputs": [
{
@@ -1170,7 +918,7 @@
"Machine initialised using operation 1: $initialise_machine()"
]
},
- "execution_count": 22,
+ "execution_count": 63,
"metadata": {},
"output_type": "execute_result"
}
@@ -1192,7 +940,7 @@
},
{
"cell_type": "code",
- "execution_count": 23,
+ "execution_count": 64,
"metadata": {},
"outputs": [
{
@@ -1204,7 +952,7 @@
"{z0,z1}"
]
},
- "execution_count": 23,
+ "execution_count": 64,
"metadata": {},
"output_type": "execute_result"
}
@@ -1222,7 +970,7 @@
},
{
"cell_type": "code",
- "execution_count": 8,
+ "execution_count": 65,
"metadata": {},
"outputs": [
{
@@ -1234,7 +982,7 @@
"2"
]
},
- "execution_count": 8,
+ "execution_count": 65,
"metadata": {},
"output_type": "execute_result"
}
@@ -1259,7 +1007,7 @@
},
{
"cell_type": "code",
- "execution_count": 9,
+ "execution_count": 66,
"metadata": {},
"outputs": [
{
@@ -1288,7 +1036,7 @@
"z3\t1\t{z3}\n"
]
},
- "execution_count": 9,
+ "execution_count": 66,
"metadata": {},
"output_type": "execute_result"
}
@@ -1299,7 +1047,7 @@
},
{
"cell_type": "code",
- "execution_count": 10,
+ "execution_count": 67,
"metadata": {},
"outputs": [
{
@@ -1383,7 +1131,7 @@
"<Dot visualization: expr_as_graph [(\"0\",{x,y|x:Z & y:δ(x, 0)})]>"
]
},
- "execution_count": 10,
+ "execution_count": 67,
"metadata": {},
"output_type": "execute_result"
}
@@ -1406,7 +1154,7 @@
},
{
"cell_type": "code",
- "execution_count": 11,
+ "execution_count": 68,
"metadata": {},
"outputs": [
{
@@ -1418,7 +1166,7 @@
"{z0,z1,z2,z3}"
]
},
- "execution_count": 11,
+ "execution_count": 68,
"metadata": {},
"output_type": "execute_result"
}
@@ -1436,7 +1184,7 @@
},
{
"cell_type": "code",
- "execution_count": 12,
+ "execution_count": 69,
"metadata": {},
"outputs": [
{
@@ -1448,7 +1196,7 @@
"{z2}"
]
},
- "execution_count": 12,
+ "execution_count": 69,
"metadata": {},
"output_type": "execute_result"
}
@@ -1459,7 +1207,7 @@
},
{
"cell_type": "code",
- "execution_count": 13,
+ "execution_count": 70,
"metadata": {},
"outputs": [
{
@@ -1471,7 +1219,7 @@
"∅"
]
},
- "execution_count": 13,
+ "execution_count": 70,
"metadata": {},
"output_type": "execute_result"
}
@@ -1493,7 +1241,7 @@
},
{
"cell_type": "code",
- "execution_count": 136,
+ "execution_count": 71,
"metadata": {},
"outputs": [
{
@@ -1514,7 +1262,7 @@
"1\t1\t1\n"
]
},
- "execution_count": 136,
+ "execution_count": 71,
"metadata": {},
"output_type": "execute_result"
}
@@ -1532,7 +1280,7 @@
},
{
"cell_type": "code",
- "execution_count": 24,
+ "execution_count": 72,
"metadata": {},
"outputs": [
{
@@ -1553,7 +1301,7 @@
"1\t0\t1\n"
]
},
- "execution_count": 24,
+ "execution_count": 72,
"metadata": {},
"output_type": "execute_result"
}
@@ -1585,7 +1333,8 @@
"* Zustandsmenge von $M'$: die Potenzmenge $\\pow(Z)$ von $Z$,\n",
"* $\\delta'(Z' , a) = \\widehat{\\delta}(Z',a)$ für alle $Z' \\subseteq Z$ und $a \\in \\Sigma$,\n",
"* $z_0'=S$,\n",
- "* $F = \\{ Z' \\subseteq Z \\mid Z' \\cap E \\neq \\emptyset\\}$."
+ "* $F = \\{ Z' \\subseteq Z \\mid Z' \\cap E \\neq \\emptyset\\}$.\n",
+ "Offenbar sind M' und M äquivalent, denn für alle ...\n"
]
},
{
@@ -1598,7 +1347,7 @@
},
{
"cell_type": "code",
- "execution_count": 141,
+ "execution_count": 73,
"metadata": {},
"outputs": [
{
@@ -1610,7 +1359,7 @@
"{∅,{z0},{z0,z1},{z0,z2},{z0,z3},{z1},{z0,z1,z2},{z0,z1,z3},{z1,z2},{z1,z3},{z0,z1,z2,z3},{z2},{z0,z2,z3},{z1,z2,z3},{z2,z3},{z3}}"
]
},
- "execution_count": 141,
+ "execution_count": 73,
"metadata": {},
"output_type": "execute_result"
}
@@ -1632,7 +1381,7 @@
},
{
"cell_type": "code",
- "execution_count": 25,
+ "execution_count": 74,
"metadata": {},
"outputs": [
{
@@ -1709,7 +1458,7 @@
"{z3}\t1\t{z3}\n"
]
},
- "execution_count": 25,
+ "execution_count": 74,
"metadata": {},
"output_type": "execute_result"
}
@@ -1731,7 +1480,7 @@
},
{
"cell_type": "code",
- "execution_count": 17,
+ "execution_count": 75,
"metadata": {},
"outputs": [
{
@@ -1740,7 +1489,7 @@
"Preference changed: DOT_DECOMPOSE_NODES = FALSE\n"
]
},
- "execution_count": 17,
+ "execution_count": 75,
"metadata": {},
"output_type": "execute_result"
}
@@ -1751,7 +1500,7 @@
},
{
"cell_type": "code",
- "execution_count": 18,
+ "execution_count": 76,
"metadata": {},
"outputs": [
{
@@ -2101,7 +1850,7 @@
"<Dot visualization: expr_as_graph [(\"0\",{x,y|x:POW(Z) & δs(x, [0])=y})]>"
]
},
- "execution_count": 18,
+ "execution_count": 76,
"metadata": {},
"output_type": "execute_result"
}
@@ -2134,21 +1883,9 @@
},
{
"cell_type": "code",
- "execution_count": 19,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "ProB CLI: 1.9.0-nightly (6b5c5ef186e29710bc4c6a651339f67f972db657)\n",
- "ProB 2: 3.2.12-SNAPSHOT (16945773c7a5d9b44c1061db2a89cdd9e1da3cc3)"
- ]
- },
- "execution_count": 19,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":version"
]
@@ -2166,7 +1903,7 @@
},
{
"cell_type": "code",
- "execution_count": 26,
+ "execution_count": 77,
"metadata": {},
"outputs": [
{
@@ -2175,7 +1912,7 @@
"Loaded machine: ChemicalElements"
]
},
- "execution_count": 26,
+ "execution_count": 77,
"metadata": {},
"output_type": "execute_result"
}
@@ -2195,7 +1932,7 @@
},
{
"cell_type": "code",
- "execution_count": 27,
+ "execution_count": 78,
"metadata": {},
"outputs": [
{
@@ -2204,7 +1941,7 @@
"Machine constants set up using operation 0: $setup_constants()"
]
},
- "execution_count": 27,
+ "execution_count": 78,
"metadata": {},
"output_type": "execute_result"
}
@@ -2226,7 +1963,7 @@
},
{
"cell_type": "code",
- "execution_count": 33,
+ "execution_count": 79,
"metadata": {},
"outputs": [
{
@@ -2238,7 +1975,7 @@
"118"
]
},
- "execution_count": 33,
+ "execution_count": 79,
"metadata": {},
"output_type": "execute_result"
}
@@ -2249,7 +1986,7 @@
},
{
"cell_type": "code",
- "execution_count": 28,
+ "execution_count": 80,
"metadata": {},
"outputs": [
{
@@ -2498,7 +2235,7 @@
"\"Zirconium\"\t\"Zr\"\t40\t\"91.224\"\n"
]
},
- "execution_count": 28,
+ "execution_count": 80,
"metadata": {},
"output_type": "execute_result"
}
@@ -2520,7 +2257,7 @@
},
{
"cell_type": "code",
- "execution_count": 31,
+ "execution_count": 81,
"metadata": {},
"outputs": [
{
@@ -2553,7 +2290,7 @@
},
{
"cell_type": "code",
- "execution_count": 25,
+ "execution_count": 82,
"metadata": {},
"outputs": [
{
@@ -2578,7 +2315,7 @@
"\"Uranium\"\t\"238.0289\"\t\"Neptunium\"\t\"237.048\"\n"
]
},
- "execution_count": 25,
+ "execution_count": 82,
"metadata": {},
"output_type": "execute_result"
}
@@ -2654,7 +2391,6 @@
}
],
"metadata": {
- "celltoolbar": "Slideshow",
"kernelspec": {
"display_name": "ProB 2",
"language": "prob",