diff --git a/sks/Interlocking.ipynb b/sks/Interlocking.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..7ba6e1c63b954f3575b2678791ba45b89ca52502
--- /dev/null
+++ b/sks/Interlocking.ipynb
@@ -0,0 +1,1107 @@
+{
+ "cells": [
+ {
+ "cell_type": "code",
+ "execution_count": 48,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: train_ctx0_beebook_ctx"
+ ]
+ },
+ "execution_count": 48,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":load models/train_ctx0_beebook_ctx.eventb"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 49,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants were not set up yet. Automatically set up constants using arbitrary transition: SETUP_CONSTANTS()\n",
+ "Executed operation: INITIALISATION()"
+ ]
+ },
+ "execution_count": 49,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Die Topologie wird durch diese Konstante definiert:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 50,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(\\mathit{R1}\\mapsto\\{(\\mathit{A}\\mapsto\\mathit{B}),(\\mathit{B}\\mapsto\\mathit{C}),(\\mathit{L}\\mapsto\\mathit{A})\\}),(\\mathit{R2}\\mapsto\\{(\\mathit{A}\\mapsto\\mathit{B}),(\\mathit{B}\\mapsto\\mathit{D}),(\\mathit{D}\\mapsto\\mathit{E}),(\\mathit{E}\\mapsto\\mathit{F}),(\\mathit{F}\\mapsto\\mathit{G}),(\\mathit{L}\\mapsto\\mathit{A})\\}),(\\mathit{R3}\\mapsto\\{(\\mathit{A}\\mapsto\\mathit{B}),(\\mathit{B}\\mapsto\\mathit{D}),(\\mathit{D}\\mapsto\\mathit{K}),(\\mathit{J}\\mapsto\\mathit{N}),(\\mathit{K}\\mapsto\\mathit{J}),(\\mathit{L}\\mapsto\\mathit{A})\\}),(\\mathit{R4}\\mapsto\\{(\\mathit{F}\\mapsto\\mathit{G}),(\\mathit{H}\\mapsto\\mathit{I}),(\\mathit{I}\\mapsto\\mathit{K}),(\\mathit{K}\\mapsto\\mathit{F}),(\\mathit{M}\\mapsto\\mathit{H})\\}),(\\mathit{R5}\\mapsto\\{(\\mathit{H}\\mapsto\\mathit{I}),(\\mathit{I}\\mapsto\\mathit{J}),(\\mathit{J}\\mapsto\\mathit{N}),(\\mathit{M}\\mapsto\\mathit{H})\\}),(\\mathit{R6}\\mapsto\\{(\\mathit{A}\\mapsto\\mathit{L}),(\\mathit{B}\\mapsto\\mathit{A}),(\\mathit{C}\\mapsto\\mathit{B})\\}),(\\mathit{R7}\\mapsto\\{(\\mathit{A}\\mapsto\\mathit{L}),(\\mathit{B}\\mapsto\\mathit{A}),(\\mathit{D}\\mapsto\\mathit{B}),(\\mathit{E}\\mapsto\\mathit{D}),(\\mathit{F}\\mapsto\\mathit{E}),(\\mathit{G}\\mapsto\\mathit{F})\\}),(\\mathit{R8}\\mapsto\\{(\\mathit{A}\\mapsto\\mathit{L}),(\\mathit{B}\\mapsto\\mathit{A}),(\\mathit{D}\\mapsto\\mathit{B}),(\\mathit{J}\\mapsto\\mathit{K}),(\\mathit{K}\\mapsto\\mathit{D}),(\\mathit{N}\\mapsto\\mathit{J})\\}),(\\mathit{R9}\\mapsto\\{(\\mathit{F}\\mapsto\\mathit{K}),(\\mathit{G}\\mapsto\\mathit{F}),(\\mathit{H}\\mapsto\\mathit{M}),(\\mathit{I}\\mapsto\\mathit{H}),(\\mathit{K}\\mapsto\\mathit{I})\\}),(\\mathit{R10}\\mapsto\\{(\\mathit{H}\\mapsto\\mathit{M}),(\\mathit{I}\\mapsto\\mathit{H}),(\\mathit{J}\\mapsto\\mathit{I}),(\\mathit{N}\\mapsto\\mathit{J})\\})\\}$"
+ ],
+ "text/plain": [
+ "{(R1↦{(A↦B),(B↦C),(L↦A)}),(R2↦{(A↦B),(B↦D),(D↦E),(E↦F),(F↦G),(L↦A)}),(R3↦{(A↦B),(B↦D),(D↦K),(J↦N),(K↦J),(L↦A)}),(R4↦{(F↦G),(H↦I),(I↦K),(K↦F),(M↦H)}),(R5↦{(H↦I),(I↦J),(J↦N),(M↦H)}),(R6↦{(A↦L),(B↦A),(C↦B)}),(R7↦{(A↦L),(B↦A),(D↦B),(E↦D),(F↦E),(G↦F)}),(R8↦{(A↦L),(B↦A),(D↦B),(J↦K),(K↦D),(N↦J)}),(R9↦{(F↦K),(G↦F),(H↦M),(I↦H),(K↦I)}),(R10↦{(H↦M),(I↦H),(J↦I),(N↦J)})}"
+ ]
+ },
+ "execution_count": 50,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "nxt"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Die Typisierung ist durch axm4 angegeben:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 51,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 51,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "nxt ∈ ROUTES → (BLOCKS ⤔ BLOCKS)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Eine einzelne Route bekommt man durch Funktionsanwendung:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 53,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(\\mathit{A}\\mapsto\\mathit{B}),(\\mathit{B}\\mapsto\\mathit{C}),(\\mathit{L}\\mapsto\\mathit{A})\\}$"
+ ],
+ "text/plain": [
+ "{(A↦B),(B↦C),(L↦A)}"
+ ]
+ },
+ "execution_count": 53,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "nxt(R1)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 54,
+ "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 6.0.1 (20220911.1526)\n",
+ " -->\n",
+ "<!-- Title: state Pages: 1 -->\n",
+ "<svg width=\"101pt\" height=\"358pt\"\n",
+ " viewBox=\"0.00 0.00 101.00 358.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 354)\">\n",
+ "<title>state</title>\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-354 97,-354 97,4 -4,4\"/>\n",
+ "<g id=\"clust2\" class=\"cluster\">\n",
+ "<title>cluster_BLOCKS</title>\n",
+ "<polygon fill=\"lightgrey\" stroke=\"lightgrey\" points=\"8,-8 8,-342 85,-342 85,-8 8,-8\"/>\n",
+ "<text text-anchor=\"middle\" x=\"46.5\" y=\"-328.4\" font-family=\"Times,serif\" font-size=\"12.00\">BLOCKS</text>\n",
+ "</g>\n",
+ "<!-- L -->\n",
+ "<g id=\"node1\" class=\"node\">\n",
+ "<title>L</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-313 16,-313 16,-277 70,-277 70,-313\"/>\n",
+ "<text text-anchor=\"middle\" x=\"43\" y=\"-291.3\" font-family=\"Times,serif\" font-size=\"14.00\">L</text>\n",
+ "</g>\n",
+ "<!-- A -->\n",
+ "<g id=\"node2\" class=\"node\">\n",
+ "<title>A</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-226 16,-226 16,-190 70,-190 70,-226\"/>\n",
+ "<text text-anchor=\"middle\" x=\"43\" y=\"-204.3\" font-family=\"Times,serif\" font-size=\"14.00\">A</text>\n",
+ "</g>\n",
+ "<!-- L->A -->\n",
+ "<g id=\"edge1\" class=\"edge\">\n",
+ "<title>L->A</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M43,-276.8C43,-265.16 43,-249.55 43,-236.24\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"46.5,-236.18 43,-226.18 39.5,-236.18 46.5,-236.18\"/>\n",
+ "<text text-anchor=\"middle\" x=\"64.5\" y=\"-247.8\" font-family=\"Times,serif\" font-size=\"14.00\">nxt(R1)</text>\n",
+ "</g>\n",
+ "<!-- B -->\n",
+ "<g id=\"node3\" class=\"node\">\n",
+ "<title>B</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\">B</text>\n",
+ "</g>\n",
+ "<!-- A->B -->\n",
+ "<g id=\"edge3\" class=\"edge\">\n",
+ "<title>A->B</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M43,-189.8C43,-178.16 43,-162.55 43,-149.24\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"46.5,-149.18 43,-139.18 39.5,-149.18 46.5,-149.18\"/>\n",
+ "<text text-anchor=\"middle\" x=\"64.5\" y=\"-160.8\" font-family=\"Times,serif\" font-size=\"14.00\">nxt(R1)</text>\n",
+ "</g>\n",
+ "<!-- C -->\n",
+ "<g id=\"node4\" class=\"node\">\n",
+ "<title>C</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\">C</text>\n",
+ "</g>\n",
+ "<!-- B->C -->\n",
+ "<g id=\"edge2\" class=\"edge\">\n",
+ "<title>B->C</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M43,-102.8C43,-91.16 43,-75.55 43,-62.24\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"46.5,-62.18 43,-52.18 39.5,-62.18 46.5,-62.18\"/>\n",
+ "<text text-anchor=\"middle\" x=\"64.5\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">nxt(R1)</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>\n"
+ ],
+ "text/plain": [
+ "<Dot visualization: expr_as_graph [nxt(R1)]>"
+ ]
+ },
+ "execution_count": 54,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot expr_as_graph nxt(R1)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Man kann die komplette Topologie so bestimmen:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 55,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{\\{(\\mathit{A}\\mapsto\\mathit{L}),(\\mathit{B}\\mapsto\\mathit{A}),(\\mathit{C}\\mapsto\\mathit{B})\\},\\{(\\mathit{A}\\mapsto\\mathit{B}),(\\mathit{B}\\mapsto\\mathit{C}),(\\mathit{L}\\mapsto\\mathit{A})\\},\\{(\\mathit{A}\\mapsto\\mathit{L}),(\\mathit{B}\\mapsto\\mathit{A}),(\\mathit{D}\\mapsto\\mathit{B}),(\\mathit{E}\\mapsto\\mathit{D}),(\\mathit{F}\\mapsto\\mathit{E}),(\\mathit{G}\\mapsto\\mathit{F})\\},\\{(\\mathit{A}\\mapsto\\mathit{L}),(\\mathit{B}\\mapsto\\mathit{A}),(\\mathit{D}\\mapsto\\mathit{B}),(\\mathit{J}\\mapsto\\mathit{K}),(\\mathit{K}\\mapsto\\mathit{D}),(\\mathit{N}\\mapsto\\mathit{J})\\},\\{(\\mathit{A}\\mapsto\\mathit{B}),(\\mathit{B}\\mapsto\\mathit{D}),(\\mathit{D}\\mapsto\\mathit{E}),(\\mathit{E}\\mapsto\\mathit{F}),(\\mathit{F}\\mapsto\\mathit{G}),(\\mathit{L}\\mapsto\\mathit{A})\\},\\{(\\mathit{A}\\mapsto\\mathit{B}),(\\mathit{B}\\mapsto\\mathit{D}),(\\mathit{D}\\mapsto\\mathit{K}),(\\mathit{J}\\mapsto\\mathit{N}),(\\mathit{K}\\mapsto\\mathit{J}),(\\mathit{L}\\mapsto\\mathit{A})\\},\\{(\\mathit{F}\\mapsto\\mathit{K}),(\\mathit{G}\\mapsto\\mathit{F}),(\\mathit{H}\\mapsto\\mathit{M}),(\\mathit{I}\\mapsto\\mathit{H}),(\\mathit{K}\\mapsto\\mathit{I})\\},\\{(\\mathit{H}\\mapsto\\mathit{M}),(\\mathit{I}\\mapsto\\mathit{H}),(\\mathit{J}\\mapsto\\mathit{I}),(\\mathit{N}\\mapsto\\mathit{J})\\},\\{(\\mathit{H}\\mapsto\\mathit{I}),(\\mathit{I}\\mapsto\\mathit{J}),(\\mathit{J}\\mapsto\\mathit{N}),(\\mathit{M}\\mapsto\\mathit{H})\\},\\{(\\mathit{F}\\mapsto\\mathit{G}),(\\mathit{H}\\mapsto\\mathit{I}),(\\mathit{I}\\mapsto\\mathit{K}),(\\mathit{K}\\mapsto\\mathit{F}),(\\mathit{M}\\mapsto\\mathit{H})\\}\\}$"
+ ],
+ "text/plain": [
+ "{{(A↦L),(B↦A),(C↦B)},{(A↦B),(B↦C),(L↦A)},{(A↦L),(B↦A),(D↦B),(E↦D),(F↦E),(G↦F)},{(A↦L),(B↦A),(D↦B),(J↦K),(K↦D),(N↦J)},{(A↦B),(B↦D),(D↦E),(E↦F),(F↦G),(L↦A)},{(A↦B),(B↦D),(D↦K),(J↦N),(K↦J),(L↦A)},{(F↦K),(G↦F),(H↦M),(I↦H),(K↦I)},{(H↦M),(I↦H),(J↦I),(N↦J)},{(H↦I),(I↦J),(J↦N),(M↦H)},{(F↦G),(H↦I),(I↦K),(K↦F),(M↦H)}}"
+ ]
+ },
+ "execution_count": 55,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "ran(nxt)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 56,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(\\mathit{A}\\mapsto\\mathit{B}),(\\mathit{A}\\mapsto\\mathit{L}),(\\mathit{B}\\mapsto\\mathit{A}),(\\mathit{B}\\mapsto\\mathit{C}),(\\mathit{B}\\mapsto\\mathit{D}),(\\mathit{C}\\mapsto\\mathit{B}),(\\mathit{D}\\mapsto\\mathit{B}),(\\mathit{D}\\mapsto\\mathit{E}),(\\mathit{D}\\mapsto\\mathit{K}),(\\mathit{E}\\mapsto\\mathit{D}),(\\mathit{E}\\mapsto\\mathit{F}),(\\mathit{F}\\mapsto\\mathit{E}),(\\mathit{F}\\mapsto\\mathit{G}),(\\mathit{F}\\mapsto\\mathit{K}),(\\mathit{G}\\mapsto\\mathit{F}),(\\mathit{H}\\mapsto\\mathit{I}),(\\mathit{H}\\mapsto\\mathit{M}),(\\mathit{I}\\mapsto\\mathit{H}),(\\mathit{I}\\mapsto\\mathit{J}),(\\mathit{I}\\mapsto\\mathit{K}),(\\mathit{J}\\mapsto\\mathit{I}),(\\mathit{J}\\mapsto\\mathit{K}),(\\mathit{J}\\mapsto\\mathit{N}),(\\mathit{K}\\mapsto\\mathit{D}),(\\mathit{K}\\mapsto\\mathit{F}),(\\mathit{K}\\mapsto\\mathit{I}),(\\mathit{K}\\mapsto\\mathit{J}),(\\mathit{L}\\mapsto\\mathit{A}),(\\mathit{M}\\mapsto\\mathit{H}),(\\mathit{N}\\mapsto\\mathit{J})\\}$"
+ ],
+ "text/plain": [
+ "{(A↦B),(A↦L),(B↦A),(B↦C),(B↦D),(C↦B),(D↦B),(D↦E),(D↦K),(E↦D),(E↦F),(F↦E),(F↦G),(F↦K),(G↦F),(H↦I),(H↦M),(I↦H),(I↦J),(I↦K),(J↦I),(J↦K),(J↦N),(K↦D),(K↦F),(K↦I),(K↦J),(L↦A),(M↦H),(N↦J)}"
+ ]
+ },
+ "execution_count": 56,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "union(ran(nxt))"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 57,
+ "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 6.0.1 (20220911.1526)\n",
+ " -->\n",
+ "<!-- Title: state Pages: 1 -->\n",
+ "<svg width=\"691pt\" height=\"706pt\"\n",
+ " viewBox=\"0.00 0.00 691.00 706.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 702)\">\n",
+ "<title>state</title>\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-702 687,-702 687,4 -4,4\"/>\n",
+ "<g id=\"clust2\" class=\"cluster\">\n",
+ "<title>cluster_BLOCKS</title>\n",
+ "<polygon fill=\"lightgrey\" stroke=\"lightgrey\" points=\"8,-8 8,-690 675,-690 675,-8 8,-8\"/>\n",
+ "<text text-anchor=\"middle\" x=\"341.5\" y=\"-676.4\" font-family=\"Times,serif\" font-size=\"12.00\">BLOCKS</text>\n",
+ "</g>\n",
+ "<!-- N -->\n",
+ "<g id=\"node1\" class=\"node\">\n",
+ "<title>N</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"227,-661 173,-661 173,-625 227,-625 227,-661\"/>\n",
+ "<text text-anchor=\"middle\" x=\"200\" y=\"-639.3\" font-family=\"Times,serif\" font-size=\"14.00\">N</text>\n",
+ "</g>\n",
+ "<!-- J -->\n",
+ "<g id=\"node2\" class=\"node\">\n",
+ "<title>J</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"228,-574 174,-574 174,-538 228,-538 228,-574\"/>\n",
+ "<text text-anchor=\"middle\" x=\"201\" y=\"-552.3\" font-family=\"Times,serif\" font-size=\"14.00\">J</text>\n",
+ "</g>\n",
+ "<!-- N->J -->\n",
+ "<g id=\"edge1\" class=\"edge\">\n",
+ "<title>N->J</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M172.88,-630.21C156.26,-621.14 139.63,-607.55 148,-592 151.97,-584.63 158.24,-578.55 165.11,-573.64\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"167.4,-576.34 174,-568.05 163.67,-570.42 167.4,-576.34\"/>\n",
+ "<text text-anchor=\"middle\" x=\"190\" y=\"-595.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- J->N -->\n",
+ "<g id=\"edge8\" class=\"edge\">\n",
+ "<title>J->N</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M221.3,-574.21C229.68,-583.48 236.51,-595.38 232,-607 230.64,-610.51 228.74,-613.88 226.55,-617.05\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"223.75,-614.94 220.2,-624.93 229.2,-619.33 223.75,-614.94\"/>\n",
+ "<text text-anchor=\"middle\" x=\"275\" y=\"-595.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- K -->\n",
+ "<g id=\"node7\" class=\"node\">\n",
+ "<title>K</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"228,-400 174,-400 174,-364 228,-364 228,-400\"/>\n",
+ "<text text-anchor=\"middle\" x=\"201\" y=\"-378.3\" font-family=\"Times,serif\" font-size=\"14.00\">K</text>\n",
+ "</g>\n",
+ "<!-- J->K -->\n",
+ "<g id=\"edge9\" class=\"edge\">\n",
+ "<title>J->K</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M173.64,-543.36C151.7,-532.37 122.42,-513.6 109,-487 101.79,-472.71 101.79,-465.29 109,-451 120.63,-427.93 144.2,-410.75 164.57,-399.43\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"166.43,-402.4 173.64,-394.64 163.17,-396.21 166.43,-402.4\"/>\n",
+ "<text text-anchor=\"middle\" x=\"151\" y=\"-465.3\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- I -->\n",
+ "<g id=\"node8\" class=\"node\">\n",
+ "<title>I</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"347,-487 293,-487 293,-451 347,-451 347,-487\"/>\n",
+ "<text text-anchor=\"middle\" x=\"320\" y=\"-465.3\" font-family=\"Times,serif\" font-size=\"14.00\">I</text>\n",
+ "</g>\n",
+ "<!-- J->I -->\n",
+ "<g id=\"edge10\" class=\"edge\">\n",
+ "<title>J->I</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M201.32,-537.62C202.44,-526.9 205.6,-513.6 214,-505 234.34,-484.16 249.43,-496.36 277,-487 279.1,-486.29 281.25,-485.53 283.41,-484.75\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"284.72,-487.99 292.85,-481.2 282.26,-481.44 284.72,-487.99\"/>\n",
+ "<text text-anchor=\"middle\" x=\"256\" y=\"-508.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- M -->\n",
+ "<g id=\"node3\" class=\"node\">\n",
+ "<title>M</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"513,-313 459,-313 459,-277 513,-277 513,-313\"/>\n",
+ "<text text-anchor=\"middle\" x=\"486\" y=\"-291.3\" font-family=\"Times,serif\" font-size=\"14.00\">M</text>\n",
+ "</g>\n",
+ "<!-- H -->\n",
+ "<g id=\"node4\" class=\"node\">\n",
+ "<title>H</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"466,-400 412,-400 412,-364 466,-364 466,-400\"/>\n",
+ "<text text-anchor=\"middle\" x=\"439\" y=\"-378.3\" font-family=\"Times,serif\" font-size=\"14.00\">H</text>\n",
+ "</g>\n",
+ "<!-- M->H -->\n",
+ "<g id=\"edge2\" class=\"edge\">\n",
+ "<title>M->H</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M507.85,-313.17C517.44,-322.83 525.08,-335.12 518,-346 508.67,-360.34 491.98,-368.85 476.34,-373.87\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"474.97,-370.62 466.29,-376.7 476.87,-377.36 474.97,-370.62\"/>\n",
+ "<text text-anchor=\"middle\" x=\"562\" y=\"-334.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- H->M -->\n",
+ "<g id=\"edge14\" class=\"edge\">\n",
+ "<title>H->M</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M430.57,-363.87C426.85,-353.77 424.44,-341.03 430,-331 434.61,-322.68 442.12,-316.07 450.16,-310.95\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"452,-313.93 458.98,-305.96 448.55,-307.84 452,-313.93\"/>\n",
+ "<text text-anchor=\"middle\" x=\"472\" y=\"-334.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- H->I -->\n",
+ "<g id=\"edge15\" class=\"edge\">\n",
+ "<title>H->I</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M466.31,-392.81C487.86,-402.06 512.27,-416.88 499,-433 481.41,-454.36 404.4,-462.87 357.31,-466.12\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"356.93,-462.63 347.17,-466.77 357.38,-469.62 356.93,-462.63\"/>\n",
+ "<text text-anchor=\"middle\" x=\"544\" y=\"-421.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- L -->\n",
+ "<g id=\"node5\" class=\"node\">\n",
+ "<title>L</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"338,-52 284,-52 284,-16 338,-16 338,-52\"/>\n",
+ "<text text-anchor=\"middle\" x=\"311\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">L</text>\n",
+ "</g>\n",
+ "<!-- A -->\n",
+ "<g id=\"node6\" class=\"node\">\n",
+ "<title>A</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"340,-139 286,-139 286,-103 340,-103 340,-139\"/>\n",
+ "<text text-anchor=\"middle\" x=\"313\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">A</text>\n",
+ "</g>\n",
+ "<!-- L->A -->\n",
+ "<g id=\"edge3\" class=\"edge\">\n",
+ "<title>L->A</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M331.2,-52.07C335.99,-57.28 340.44,-63.4 343,-70 346.21,-78.28 343.7,-86.75 339.02,-94.31\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"335.92,-92.61 332.73,-102.71 341.53,-96.8 335.92,-92.61\"/>\n",
+ "<text text-anchor=\"middle\" x=\"386\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- A->L -->\n",
+ "<g id=\"edge29\" class=\"edge\">\n",
+ "<title>A->L</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M285.95,-110.71C274.24,-105.18 261.71,-96.88 255,-85 247.18,-71.15 259.54,-59.14 274.62,-50.36\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"276.48,-53.35 283.69,-45.58 273.21,-47.15 276.48,-53.35\"/>\n",
+ "<text text-anchor=\"middle\" x=\"297\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- B -->\n",
+ "<g id=\"node13\" class=\"node\">\n",
+ "<title>B</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"496,-226 442,-226 442,-190 496,-190 496,-226\"/>\n",
+ "<text text-anchor=\"middle\" x=\"469\" y=\"-204.3\" font-family=\"Times,serif\" font-size=\"14.00\">B</text>\n",
+ "</g>\n",
+ "<!-- A->B -->\n",
+ "<g id=\"edge30\" class=\"edge\">\n",
+ "<title>A->B</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M332.51,-139.08C345.15,-149.54 362.31,-162.67 379,-172 395.76,-181.37 415.54,-189.36 432.28,-195.33\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"431.14,-198.64 441.74,-198.61 433.43,-192.02 431.14,-198.64\"/>\n",
+ "<text text-anchor=\"middle\" x=\"421\" y=\"-160.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- K->J -->\n",
+ "<g id=\"edge4\" class=\"edge\">\n",
+ "<title>K->J</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M199.24,-400.07C198.73,-405.77 198.25,-412.15 198,-418 196.38,-455.98 197.95,-499.92 199.36,-527.59\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"195.87,-527.89 199.9,-537.69 202.86,-527.52 195.87,-527.89\"/>\n",
+ "<text text-anchor=\"middle\" x=\"239\" y=\"-465.3\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- K->I -->\n",
+ "<g id=\"edge5\" class=\"edge\">\n",
+ "<title>K->I</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M228.32,-386.86C249.64,-391.16 278.77,-400.04 298,-418 304.68,-424.23 309.44,-432.86 312.79,-441.18\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"309.5,-442.38 316.1,-450.67 316.11,-440.07 309.5,-442.38\"/>\n",
+ "<text text-anchor=\"middle\" x=\"350\" y=\"-421.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- F -->\n",
+ "<g id=\"node9\" class=\"node\">\n",
+ "<title>F</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"73,-139 19,-139 19,-103 73,-103 73,-139\"/>\n",
+ "<text text-anchor=\"middle\" x=\"46\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">F</text>\n",
+ "</g>\n",
+ "<!-- K->F -->\n",
+ "<g id=\"edge6\" class=\"edge\">\n",
+ "<title>K->F</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M192.97,-363.86C179.8,-336.76 151.77,-283.08 119,-244 87.62,-206.58 56.27,-216.43 36,-172 32.73,-164.83 32.94,-156.61 34.61,-148.92\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"37.98,-149.85 37.47,-139.27 31.27,-147.86 37.98,-149.85\"/>\n",
+ "<text text-anchor=\"middle\" x=\"172\" y=\"-247.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- D -->\n",
+ "<g id=\"node10\" class=\"node\">\n",
+ "<title>D</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"370,-313 316,-313 316,-277 370,-277 370,-313\"/>\n",
+ "<text text-anchor=\"middle\" x=\"343\" y=\"-291.3\" font-family=\"Times,serif\" font-size=\"14.00\">D</text>\n",
+ "</g>\n",
+ "<!-- K->D -->\n",
+ "<g id=\"edge7\" class=\"edge\">\n",
+ "<title>K->D</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M228.36,-376.22C250.35,-371.36 281.22,-362.19 304,-346 313.02,-339.59 320.97,-330.51 327.29,-321.84\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"330.3,-323.65 333.06,-313.42 324.52,-319.69 330.3,-323.65\"/>\n",
+ "<text text-anchor=\"middle\" x=\"361\" y=\"-334.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- I->J -->\n",
+ "<g id=\"edge12\" class=\"edge\">\n",
+ "<title>I->J</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M316.1,-487.33C312.88,-498.03 307.29,-511.33 298,-520 281.62,-535.3 258.07,-544 238.27,-548.91\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"237.31,-545.53 228.32,-551.14 238.84,-552.36 237.31,-545.53\"/>\n",
+ "<text text-anchor=\"middle\" x=\"350\" y=\"-508.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- I->H -->\n",
+ "<g id=\"edge13\" class=\"edge\">\n",
+ "<title>I->H</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M347.22,-458.76C362.45,-452.81 381.27,-444.11 396,-433 405.14,-426.11 413.71,-416.96 420.75,-408.39\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"423.58,-410.45 427,-400.42 418.07,-406.13 423.58,-410.45\"/>\n",
+ "<text text-anchor=\"middle\" x=\"453\" y=\"-421.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- I->K -->\n",
+ "<g id=\"edge11\" class=\"edge\">\n",
+ "<title>I->K</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M292.87,-456.73C287.65,-454.72 282.18,-452.71 277,-451 247.73,-441.32 230.86,-455.7 210,-433 204.38,-426.88 201.67,-418.49 200.5,-410.34\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"203.99,-410.02 199.73,-400.31 197.01,-410.55 203.99,-410.02\"/>\n",
+ "<text text-anchor=\"middle\" x=\"252\" y=\"-421.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- F->K -->\n",
+ "<g id=\"edge17\" class=\"edge\">\n",
+ "<title>F->K</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M36.32,-139.29C33.74,-144.78 31.31,-150.99 30,-157 20.35,-201.3 10.07,-218.79 31,-259 59.18,-313.15 123.61,-348.77 164.56,-366.86\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"163.35,-370.15 173.92,-370.88 166.11,-363.72 163.35,-370.15\"/>\n",
+ "<text text-anchor=\"middle\" x=\"73\" y=\"-247.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- G -->\n",
+ "<g id=\"node11\" class=\"node\">\n",
+ "<title>G</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"122,-52 68,-52 68,-16 122,-16 122,-52\"/>\n",
+ "<text text-anchor=\"middle\" x=\"95\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">G</text>\n",
+ "</g>\n",
+ "<!-- F->G -->\n",
+ "<g id=\"edge18\" class=\"edge\">\n",
+ "<title>F->G</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M37.51,-102.84C33.77,-92.72 31.36,-79.98 37,-70 41.98,-61.18 50.17,-54.34 58.85,-49.14\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"60.76,-52.08 67.95,-44.29 57.48,-45.9 60.76,-52.08\"/>\n",
+ "<text text-anchor=\"middle\" x=\"79\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- E -->\n",
+ "<g id=\"node12\" class=\"node\">\n",
+ "<title>E</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"213,-226 159,-226 159,-190 213,-190 213,-226\"/>\n",
+ "<text text-anchor=\"middle\" x=\"186\" y=\"-204.3\" font-family=\"Times,serif\" font-size=\"14.00\">E</text>\n",
+ "</g>\n",
+ "<!-- F->E -->\n",
+ "<g id=\"edge19\" class=\"edge\">\n",
+ "<title>F->E</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M73.13,-129.99C90.96,-135.93 114.35,-145.06 133,-157 144.15,-164.14 155.05,-173.8 164.03,-182.73\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"161.61,-185.26 171.09,-189.98 166.62,-180.37 161.61,-185.26\"/>\n",
+ "<text text-anchor=\"middle\" x=\"194\" y=\"-160.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- D->K -->\n",
+ "<g id=\"edge22\" class=\"edge\">\n",
+ "<title>D->K</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M315.97,-296.15C287.4,-297.79 242.82,-304.78 216,-331 209.89,-336.97 206.25,-345.32 204.09,-353.48\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"200.6,-353.05 202.06,-363.54 207.46,-354.43 200.6,-353.05\"/>\n",
+ "<text text-anchor=\"middle\" x=\"258\" y=\"-334.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- D->E -->\n",
+ "<g id=\"edge23\" class=\"edge\">\n",
+ "<title>D->E</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M343.96,-276.57C343.59,-265.84 341.23,-252.54 333,-244 318.06,-228.51 261.89,-218.5 223.47,-213.31\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"223.52,-209.78 213.16,-211.97 222.62,-216.72 223.52,-209.78\"/>\n",
+ "<text text-anchor=\"middle\" x=\"382\" y=\"-247.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- D->B -->\n",
+ "<g id=\"edge24\" class=\"edge\">\n",
+ "<title>D->B</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M370.29,-289.55C425.54,-280.51 545.57,-260.69 547,-259 562.56,-240.54 533.07,-226.54 506.01,-218.12\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"506.81,-214.71 496.23,-215.27 504.85,-221.43 506.81,-214.71\"/>\n",
+ "<text text-anchor=\"middle\" x=\"593\" y=\"-247.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- G->F -->\n",
+ "<g id=\"edge16\" class=\"edge\">\n",
+ "<title>G->F</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M115.73,-52.32C124.8,-62.03 131.96,-74.31 125,-85 115.67,-99.34 98.98,-107.85 83.34,-112.87\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"81.97,-109.62 73.29,-115.7 83.87,-116.36 81.97,-109.62\"/>\n",
+ "<text text-anchor=\"middle\" x=\"169\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- E->F -->\n",
+ "<g id=\"edge20\" class=\"edge\">\n",
+ "<title>E->F</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M158.69,-200.44C117.95,-190.63 45.89,-173.14 45,-172 40.09,-165.72 38.83,-157.52 39.23,-149.58\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"42.73,-149.84 40.55,-139.47 35.79,-148.94 42.73,-149.84\"/>\n",
+ "<text text-anchor=\"middle\" x=\"87\" y=\"-160.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- E->D -->\n",
+ "<g id=\"edge21\" class=\"edge\">\n",
+ "<title>E->D</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M204.45,-226.22C216.45,-236.74 232.82,-249.87 249,-259 266.75,-269.01 287.92,-277.19 305.67,-283.11\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"305.08,-286.6 315.67,-286.33 307.22,-279.93 305.08,-286.6\"/>\n",
+ "<text text-anchor=\"middle\" x=\"291\" y=\"-247.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- B->A -->\n",
+ "<g id=\"edge28\" class=\"edge\">\n",
+ "<title>B->A</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M441.82,-206.54C391.2,-205.06 285.59,-198.75 263,-172 253.62,-160.89 263.62,-149.36 277.07,-140.18\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"279.11,-143.03 285.75,-134.79 275.41,-137.09 279.11,-143.03\"/>\n",
+ "<text text-anchor=\"middle\" x=\"305\" y=\"-160.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- B->D -->\n",
+ "<g id=\"edge26\" class=\"edge\">\n",
+ "<title>B->D</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M462.55,-226.37C457.78,-237.09 450.32,-250.38 440,-259 422.91,-273.27 399.55,-281.93 380.03,-287.07\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"379.12,-283.69 370.22,-289.45 380.77,-290.49 379.12,-283.69\"/>\n",
+ "<text text-anchor=\"middle\" x=\"494\" y=\"-247.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- C -->\n",
+ "<g id=\"node14\" class=\"node\">\n",
+ "<title>C</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"556,-139 502,-139 502,-103 556,-103 556,-139\"/>\n",
+ "<text text-anchor=\"middle\" x=\"529\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">C</text>\n",
+ "</g>\n",
+ "<!-- B->C -->\n",
+ "<g id=\"edge27\" class=\"edge\">\n",
+ "<title>B->C</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M466.68,-189.62C466.18,-179.42 467.12,-166.67 473,-157 477.8,-149.1 485.14,-142.7 492.93,-137.65\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"494.92,-140.54 501.81,-132.5 491.41,-134.48 494.92,-140.54\"/>\n",
+ "<text text-anchor=\"middle\" x=\"515\" y=\"-160.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "<!-- C->B -->\n",
+ "<g id=\"edge25\" class=\"edge\">\n",
+ "<title>C->B</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M551.08,-139.32C560.73,-149.03 568.37,-161.31 561,-172 548.69,-189.85 525.98,-198.6 506.21,-202.89\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"505.4,-199.48 496.21,-204.75 506.68,-206.37 505.4,-199.48\"/>\n",
+ "<text text-anchor=\"middle\" x=\"605\" y=\"-160.8\" font-family=\"Times,serif\" font-size=\"14.00\">union(ran(nxt))</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>\n"
+ ],
+ "text/plain": [
+ "<Dot visualization: expr_as_graph [union(ran(nxt))]>"
+ ]
+ },
+ "execution_count": 57,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot expr_as_graph union(ran(nxt))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Für jede Route gibt es einen ersten (fst) und letzten (lst) Block:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 59,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{r3} = \\{(\\mathit{A}\\mapsto\\mathit{B}),(\\mathit{B}\\mapsto\\mathit{C}),(\\mathit{L}\\mapsto\\mathit{A})\\}$\n",
+ "* $\\mathit{last} = \\mathit{N}$\n",
+ "* $\\mathit{first} = \\mathit{L}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tr3 = {(A↦B),(B↦C),(L↦A)}\n",
+ "\tlast = N\n",
+ "\tfirst = L"
+ ]
+ },
+ "execution_count": 59,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "r3 = nxt(R1) & first=fst(R3) & last=lst(R3)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Mit der Routing Table rtbl kann man einfach die Blöcke einer Route berechnen:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 60,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(\\mathit{A}\\mapsto\\mathit{R1}),(\\mathit{A}\\mapsto\\mathit{R2}),(\\mathit{A}\\mapsto\\mathit{R3}),(\\mathit{A}\\mapsto\\mathit{R6}),(\\mathit{A}\\mapsto\\mathit{R7}),(\\mathit{A}\\mapsto\\mathit{R8}),(\\mathit{B}\\mapsto\\mathit{R1}),(\\mathit{B}\\mapsto\\mathit{R2}),(\\mathit{B}\\mapsto\\mathit{R3}),(\\mathit{B}\\mapsto\\mathit{R6}),(\\mathit{B}\\mapsto\\mathit{R7}),(\\mathit{B}\\mapsto\\mathit{R8}),(\\mathit{C}\\mapsto\\mathit{R1}),(\\mathit{C}\\mapsto\\mathit{R6}),(\\mathit{D}\\mapsto\\mathit{R2}),(\\mathit{D}\\mapsto\\mathit{R3}),(\\mathit{D}\\mapsto\\mathit{R7}),(\\mathit{D}\\mapsto\\mathit{R8}),(\\mathit{E}\\mapsto\\mathit{R2}),(\\mathit{E}\\mapsto\\mathit{R7}),(\\mathit{F}\\mapsto\\mathit{R2}),(\\mathit{F}\\mapsto\\mathit{R4}),(\\mathit{F}\\mapsto\\mathit{R7}),(\\mathit{F}\\mapsto\\mathit{R9}),(\\mathit{G}\\mapsto\\mathit{R2}),(\\mathit{G}\\mapsto\\mathit{R4}),(\\mathit{G}\\mapsto\\mathit{R7}),(\\mathit{G}\\mapsto\\mathit{R9}),(\\mathit{H}\\mapsto\\mathit{R4}),(\\mathit{H}\\mapsto\\mathit{R5}),(\\mathit{H}\\mapsto\\mathit{R9}),(\\mathit{H}\\mapsto\\mathit{R10}),(\\mathit{I}\\mapsto\\mathit{R4}),(\\mathit{I}\\mapsto\\mathit{R5}),(\\mathit{I}\\mapsto\\mathit{R9}),(\\mathit{I}\\mapsto\\mathit{R10}),(\\mathit{J}\\mapsto\\mathit{R3}),(\\mathit{J}\\mapsto\\mathit{R5}),(\\mathit{J}\\mapsto\\mathit{R8}),(\\mathit{J}\\mapsto\\mathit{R10}),(\\mathit{K}\\mapsto\\mathit{R3}),(\\mathit{K}\\mapsto\\mathit{R4}),(\\mathit{K}\\mapsto\\mathit{R8}),(\\mathit{K}\\mapsto\\mathit{R9}),(\\mathit{L}\\mapsto\\mathit{R1}),(\\mathit{L}\\mapsto\\mathit{R2}),(\\mathit{L}\\mapsto\\mathit{R3}),(\\mathit{L}\\mapsto\\mathit{R6}),(\\mathit{L}\\mapsto\\mathit{R7}),(\\mathit{L}\\mapsto\\mathit{R8}),(\\mathit{M}\\mapsto\\mathit{R4}),(\\mathit{M}\\mapsto\\mathit{R5}),(\\mathit{M}\\mapsto\\mathit{R9}),(\\mathit{M}\\mapsto\\mathit{R10}),(\\mathit{N}\\mapsto\\mathit{R3}),(\\mathit{N}\\mapsto\\mathit{R5}),(\\mathit{N}\\mapsto\\mathit{R8}),(\\mathit{N}\\mapsto\\mathit{R10})\\}$"
+ ],
+ "text/plain": [
+ "{(A↦R1),(A↦R2),(A↦R3),(A↦R6),(A↦R7),(A↦R8),(B↦R1),(B↦R2),(B↦R3),(B↦R6),(B↦R7),(B↦R8),(C↦R1),(C↦R6),(D↦R2),(D↦R3),(D↦R7),(D↦R8),(E↦R2),(E↦R7),(F↦R2),(F↦R4),(F↦R7),(F↦R9),(G↦R2),(G↦R4),(G↦R7),(G↦R9),(H↦R4),(H↦R5),(H↦R9),(H↦R10),(I↦R4),(I↦R5),(I↦R9),(I↦R10),(J↦R3),(J↦R5),(J↦R8),(J↦R10),(K↦R3),(K↦R4),(K↦R8),(K↦R9),(L↦R1),(L↦R2),(L↦R3),(L↦R6),(L↦R7),(L↦R8),(M↦R4),(M↦R5),(M↦R9),(M↦R10),(N↦R3),(N↦R5),(N↦R8),(N↦R10)}"
+ ]
+ },
+ "execution_count": 60,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "rtbl"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 62,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{\\mathit{A},\\mathit{B},\\mathit{C},\\mathit{L}\\}$"
+ ],
+ "text/plain": [
+ "{A,B,C,L}"
+ ]
+ },
+ "execution_count": 62,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "rtbl∼[{R1}]"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 63,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{\\mathit{A},\\mathit{B},\\mathit{C},\\mathit{L}\\}$"
+ ],
+ "text/plain": [
+ "{A,B,C,L}"
+ ]
+ },
+ "execution_count": 63,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "dom(nxt(R1)) \\/ ran(nxt(R1))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Wie kann man prüfen ob diese Routen korrekt sind?"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Der erste und letzte Block muss unterschiedlich sein:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 64,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 64,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "∀r·r∈ROUTES ⇒ fst(r)≠lst(r)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 65,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 65,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "∀r.(r:ROUTES ⇒ (fst(r):dom(nxt(r)) & fst(r) /: ran(nxt(r))))"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 66,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 66,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "∀r.(r:ROUTES ⇒ (lst(r)/:dom(nxt(r)) & lst(r) : ran(nxt(r))))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Jeder Block taucht nur einmal auf; dies wurde schon in der Typisierung festgesetzt:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 67,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 67,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "∀r.(r:ROUTES ⇒ nxt(r): (BLOCKS ⤔ BLOCKS))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Alle Blöcke ausser fst/lst tauchen sowohl in dom als auch ran auf:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 68,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 68,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "∀r.(r:ROUTES ⇒ !b.(b:dom(nxt(r)) & b ≠ fst(r) => b:ran(nxt(r))))"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 69,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 69,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "∀r.(r:ROUTES ⇒ !b.(b:ran(nxt(r)) & b ≠ lst(r) => b:dom(nxt(r))))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Axiom 9 ist dies:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "∀r·r∈ROUTES ⇒ nxt(r) ∈ rtbl∼[{r}]∖{lst(r)} ⤖ rtbl∼[{r}]∖{fst(r)}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "rtbl∼[{R3}]"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Axiom 12 modelliert: first block cannot be in middle of other route"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "∀r,s·r∈ROUTES ∧ s∈ROUTES ∧ r≠s ⇒ fst(r)∉rtbl∼[{s}]∖{fst(s),lst(s)}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Axiom 13 modelliert: last block cannot be in middle of other route"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "∀r,s·r∈ROUTES ∧ s∈ROUTES ∧ r≠s ⇒ lst(r)∉rtbl∼[{s}]∖{fst(s),lst(s)}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Wie kann man die Abwesenheit von Zyklen prüfen?\n",
+ "\n",
+ "Folgende Route R0 würde die Eigenschaften oben erfüllen"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 70,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{last} = \\mathit{C}$\n",
+ "* $\\mathit{R0} = \\{(\\mathit{A}\\mapsto\\mathit{C}),(\\mathit{D}\\mapsto\\mathit{D}),(\\mathit{L}\\mapsto\\mathit{A})\\}$\n",
+ "* $\\mathit{first} = \\mathit{L}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tlast = C\n",
+ "\tR0 = {(A↦C),(D↦D),(L↦A)}\n",
+ "\tfirst = L"
+ ]
+ },
+ "execution_count": 70,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "R0 = {L |-> A, A|->C, D|->D} & first=L & last=C &\n",
+ "R0 : (BLOCKS ⤔ BLOCKS) &\n",
+ "R0 : {L,A,D} >->> {A,C,D}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 71,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{FALSE}$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 71,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "R0 = {L |-> A, A|->C, D|->D} &\n",
+ "(∀S·S⊆BLOCKS ∧ S⊆R0[S] ⇒ S=∅)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 72,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{S} = \\{\\mathit{D}\\}$\n",
+ "* $\\mathit{R0} = \\{(\\mathit{A}\\mapsto\\mathit{C}),(\\mathit{D}\\mapsto\\mathit{D}),(\\mathit{L}\\mapsto\\mathit{A})\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tS = {D}\n",
+ "\tR0 = {(A↦C),(D↦D),(L↦A)}"
+ ]
+ },
+ "execution_count": 72,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "R0 = {L |-> A, A|->C, D|->D} &\n",
+ "not(S⊆BLOCKS ∧ S⊆R0[S] ⇒ S=∅)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "So ist die Modellierung in axm10 im Modell:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 73,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 73,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "∀r·r∈ROUTES ⇒ (∀S·S⊆BLOCKS ∧ S⊆nxt(r)[S] ⇒ S=∅)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "∀r·r∈ROUTES ⇒ (∀S·S⊆ran(nxt(r)) ∧ S⊆nxt(r)[S] ⇒ S=∅)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": []
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "ProB 2",
+ "language": "prob",
+ "name": "prob2"
+ },
+ "language_info": {
+ "codemirror_mode": "prob2_jupyter_repl",
+ "file_extension": ".prob",
+ "mimetype": "text/x-prob2-jupyter-repl",
+ "name": "prob"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}