Skip to content
Snippets Groups Projects
Commit 6d085e2f authored by Michael Leuschel's avatar Michael Leuschel
Browse files

add interlocking notebook for SKS 


Signed-off-by: default avatarMichael Leuschel <leuschel@uni-duesseldorf.de>
parent 98f692d9
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Showing
with 1107 additions and 0 deletions
sks/Interlocking.ipynb 0 → 100644
+ 1107
− 0
View file @ 6d085e2f
%% Cell type:code id: tags:
``` prob
:load models/train_ctx0_beebook_ctx.eventb
```
%% Output
Loaded machine: train_ctx0_beebook_ctx
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
Machine constants were not set up yet. Automatically set up constants using arbitrary transition: SETUP_CONSTANTS()
Executed operation: INITIALISATION()
%% Cell type:markdown id: tags:
Die Topologie wird durch diese Konstante definiert:
%% Cell type:code id: tags:
``` prob
nxt
```
%% Output
$\{(\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})\})\}$
{(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)})}
%% Cell type:markdown id: tags:
Die Typisierung ist durch axm4 angegeben:
%% Cell type:code id: tags:
``` prob
nxt ∈ ROUTES → (BLOCKS ⤔ BLOCKS)
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:markdown id: tags:
Eine einzelne Route bekommt man durch Funktionsanwendung:
%% Cell type:code id: tags:
``` prob
nxt(R1)
```
%% Output
$\{(\mathit{A}\mapsto\mathit{B}),(\mathit{B}\mapsto\mathit{C}),(\mathit{L}\mapsto\mathit{A})\}$
{(A↦B),(B↦C),(L↦A)}
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph nxt(R1)
```
%% Output
<Dot visualization: expr_as_graph [nxt(R1)]>
%% Cell type:markdown id: tags:
Man kann die komplette Topologie so bestimmen:
%% Cell type:code id: tags:
``` prob
ran(nxt)
```
%% Output
$\{\{(\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})\}\}$
{{(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)}}
%% Cell type:code id: tags:
``` prob
union(ran(nxt))
```
%% Output
$\{(\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})\}$
{(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)}
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph union(ran(nxt))
```
%% Output
<Dot visualization: expr_as_graph [union(ran(nxt))]>
%% Cell type:markdown id: tags:
Für jede Route gibt es einen ersten (fst) und letzten (lst) Block:
%% Cell type:code id: tags:
``` prob
r3 = nxt(R1) & first=fst(R3) & last=lst(R3)
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{r3} = \{(\mathit{A}\mapsto\mathit{B}),(\mathit{B}\mapsto\mathit{C}),(\mathit{L}\mapsto\mathit{A})\}$
* $\mathit{last} = \mathit{N}$
* $\mathit{first} = \mathit{L}$
TRUE
Solution:
r3 = {(A↦B),(B↦C),(L↦A)}
last = N
first = L
%% Cell type:markdown id: tags:
Mit der Routing Table rtbl kann man einfach die Blöcke einer Route berechnen:
%% Cell type:code id: tags:
``` prob
rtbl
```
%% Output
$\{(\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})\}$
{(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)}
%% Cell type:code id: tags:
``` prob
rtbl∼[{R1}]
```
%% Output
$\{\mathit{A},\mathit{B},\mathit{C},\mathit{L}\}$
{A,B,C,L}
%% Cell type:code id: tags:
``` prob
dom(nxt(R1)) \/ ran(nxt(R1))
```
%% Output
$\{\mathit{A},\mathit{B},\mathit{C},\mathit{L}\}$
{A,B,C,L}
%% Cell type:markdown id: tags:
Wie kann man prüfen ob diese Routen korrekt sind?
%% Cell type:markdown id: tags:
Der erste und letzte Block muss unterschiedlich sein:
%% Cell type:code id: tags:
``` prob
∀r·r∈ROUTES ⇒ fst(r)≠lst(r)
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
∀r.(r:ROUTES ⇒ (fst(r):dom(nxt(r)) & fst(r) /: ran(nxt(r))))
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
∀r.(r:ROUTES ⇒ (lst(r)/:dom(nxt(r)) & lst(r) : ran(nxt(r))))
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:markdown id: tags:
Jeder Block taucht nur einmal auf; dies wurde schon in der Typisierung festgesetzt:
%% Cell type:code id: tags:
``` prob
∀r.(r:ROUTES ⇒ nxt(r): (BLOCKS ⤔ BLOCKS))
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:markdown id: tags:
Alle Blöcke ausser fst/lst tauchen sowohl in dom als auch ran auf:
%% Cell type:code id: tags:
``` prob
∀r.(r:ROUTES ⇒ !b.(b:dom(nxt(r)) & b ≠ fst(r) => b:ran(nxt(r))))
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
∀r.(r:ROUTES ⇒ !b.(b:ran(nxt(r)) & b ≠ lst(r) => b:dom(nxt(r))))
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:markdown id: tags:
Axiom 9 ist dies:
%% Cell type:code id: tags:
``` prob
∀r·r∈ROUTES ⇒ nxt(r) ∈ rtbl∼[{r}]∖{lst(r)} ⤖ rtbl∼[{r}]∖{fst(r)}
```
%% Cell type:code id: tags:
``` prob
rtbl∼[{R3}]
```
%% Cell type:markdown id: tags:
Axiom 12 modelliert: first block cannot be in middle of other route
%% Cell type:code id: tags:
``` prob
∀r,s·r∈ROUTES ∧ s∈ROUTES ∧ r≠s ⇒ fst(r)∉rtbl∼[{s}]∖{fst(s),lst(s)}
```
%% Cell type:markdown id: tags:
Axiom 13 modelliert: last block cannot be in middle of other route
%% Cell type:code id: tags:
``` prob
∀r,s·r∈ROUTES ∧ s∈ROUTES ∧ r≠s ⇒ lst(r)∉rtbl∼[{s}]∖{fst(s),lst(s)}
```
%% Cell type:markdown id: tags:
Wie kann man die Abwesenheit von Zyklen prüfen?
Folgende Route R0 würde die Eigenschaften oben erfüllen
%% Cell type:code id: tags:
``` prob
R0 = {L |-> A, A|->C, D|->D} & first=L & last=C &
R0 : (BLOCKS ⤔ BLOCKS) &
R0 : {L,A,D} >->> {A,C,D}
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{last} = \mathit{C}$
* $\mathit{R0} = \{(\mathit{A}\mapsto\mathit{C}),(\mathit{D}\mapsto\mathit{D}),(\mathit{L}\mapsto\mathit{A})\}$
* $\mathit{first} = \mathit{L}$
TRUE
Solution:
last = C
R0 = {(A↦C),(D↦D),(L↦A)}
first = L
%% Cell type:code id: tags:
``` prob
R0 = {L |-> A, A|->C, D|->D} &
(∀S·S⊆BLOCKS ∧ S⊆R0[S] ⇒ S=∅)
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:code id: tags:
``` prob
R0 = {L |-> A, A|->C, D|->D} &
not(S⊆BLOCKS ∧ S⊆R0[S] ⇒ S=∅)
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{S} = \{\mathit{D}\}$
* $\mathit{R0} = \{(\mathit{A}\mapsto\mathit{C}),(\mathit{D}\mapsto\mathit{D}),(\mathit{L}\mapsto\mathit{A})\}$
TRUE
Solution:
S = {D}
R0 = {(A↦C),(D↦D),(L↦A)}
%% Cell type:markdown id: tags:
So ist die Modellierung in axm10 im Modell:
%% Cell type:code id: tags:
``` prob
∀r·r∈ROUTES ⇒ (∀S·S⊆BLOCKS ∧ S⊆nxt(r)[S] ⇒ S=∅)
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
∀r·r∈ROUTES ⇒ (∀S·S⊆ran(nxt(r)) ∧ S⊆nxt(r)[S] ⇒ S=∅)
```
%% Cell type:code id: tags:
``` prob
```
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment