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

use greek Sigma in presentation

parent ddf16257
Branches
Tags
No related merge requests found
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Ein Jupyter-Kernel für Logik und Mengentheorie # Ein Jupyter-Kernel für Logik und Mengentheorie
### David Geleßus, Michael Leuschel ### David Geleßus, Michael Leuschel
### Bad Honnef, 2019 ### Bad Honnef, 2019
![ProB](./img/prob_logo.png) ![ProB](./img/prob_logo.png)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Einführung: Notebooks, Jupyter # Einführung: Notebooks, Jupyter
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Was ist ein Notebook? ## Was ist ein Notebook?
* Dokument mit Text und ausführbaren Code-Abschnitten * Dokument mit Text und ausführbaren Code-Abschnitten
* Code kann interaktiv ausgeführt werden * Code kann interaktiv ausgeführt werden
* Ergebnisse erscheinen im Notebook unter dem jeweiligem Code * Ergebnisse erscheinen im Notebook unter dem jeweiligem Code
* Ähnlich wie eine REPL (read-eval-print-loop), mit einigen Unterschieden: * Ähnlich wie eine REPL (read-eval-print-loop), mit einigen Unterschieden:
* Code-Abschnitte können "außer der Reihe" bearbeitet und ausgeführt werden * Code-Abschnitte können "außer der Reihe" bearbeitet und ausgeführt werden
* Ausgaben können formatierten Text und Grafiken enthalten * Ausgaben können formatierten Text und Grafiken enthalten
* Speicherbar als Datei * Speicherbar als Datei
* Code kann später neu ausgeführt werden * Code kann später neu ausgeführt werden
* Weitergabe an andere Nutzer möglich * Weitergabe an andere Nutzer möglich
* Implementierungen: Mathematica, Maple, Jupyter, u. a. * Implementierungen: Mathematica, Maple, Jupyter, u. a.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Jupyter Notebook ## Jupyter Notebook
* Browserbasierte Notebook-Oberfläche * Browserbasierte Notebook-Oberfläche
* Open Source und plattformübergreifend * Open Source und plattformübergreifend
* Stammt aus der Python-Community, in Python implementiert * Stammt aus der Python-Community, in Python implementiert
* Jupyter-Notebooks können aber verschiedene Programmiersprachen verwenden * Jupyter-Notebooks können aber verschiedene Programmiersprachen verwenden
* Dazu trennt Jupyter strikt zwischen Frontend und Kernel: * Dazu trennt Jupyter strikt zwischen Frontend und Kernel:
* Das allgemeine **Frontend** implementiert z. B. Benutzeroberfläche und Dateiformat * Das allgemeine **Frontend** implementiert z. B. Benutzeroberfläche und Dateiformat
* Ein sprachspezifischer **Kernel** stellt die Sprache dem Frontend zur Verfügung * Ein sprachspezifischer **Kernel** stellt die Sprache dem Frontend zur Verfügung
* Schnittstellen zwischen Frontend und Kernel sind sprachneutral * Schnittstellen zwischen Frontend und Kernel sind sprachneutral
* Kernel können in (fast) jeder Sprache implementiert werden, kein Python-Code nötig * Kernel können in (fast) jeder Sprache implementiert werden, kein Python-Code nötig
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## ProB (https://www3.hhu.de/stups/prob) ## ProB (https://www3.hhu.de/stups/prob)
* Werkzeug zur Animation, Verifikation und Visualisierung formeller Spezifikationen * Werkzeug zur Animation, Verifikation und Visualisierung formeller Spezifikationen
* Grundlage: Solver für Prädikatenlogik, Mengentheorie mit Relationen, Funktionen und Arithmetik. * Grundlage: Solver für Prädikatenlogik, Mengentheorie mit Relationen, Funktionen und Arithmetik.
* Unterstützt hauptsächlich B-Spezifikationen (klassisches B, Event-B) * Unterstützt hauptsächlich B-Spezifikationen (klassisches B, Event-B)
* Versteht auch andere Sprachen wie TLA<sup>+</sup> und CSP<sub>M</sub> * Versteht auch andere Sprachen wie TLA<sup>+</sup> und CSP<sub>M</sub>
* ProBs APIs sind für alle Sprachen gleich * ProBs APIs sind für alle Sprachen gleich
* Der ProB 2-Jupyter-Kernel unterstützt daher (fast) alle Sprachen, die ProB versteht * Der ProB 2-Jupyter-Kernel unterstützt daher (fast) alle Sprachen, die ProB versteht
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Einsatz von ProB in der Industrie ## Einsatz von ProB in der Industrie
* Datenvalidierung: Siemens (Paris Line 1, Barcelona, Alger, ...), Alstom (Amsterdam,...), Thales (Schweiz,...), RATP, SNCF, ... * Datenvalidierung: Siemens (Paris Line 1, Barcelona, Alger, ...), Alstom (Amsterdam,...), Thales (Schweiz,...), RATP, SNCF, ...
* Zertifizierung als T2 Werkzeug nach EN50128 * Zertifizierung als T2 Werkzeug nach EN50128
* Validierung von Systemmodellen: ClearSy (Octys, ...),... * Validierung von Systemmodellen: ClearSy (Octys, ...),...
* Ausführung formaler Modelle in Echtzeit * Ausführung formaler Modelle in Echtzeit
* SlotTool * SlotTool
* Hybrid Level 3 - ETCS (Thales, ProRail/Network Rail/DB), Video der Deutschen Bahn: https://www.youtube.com/watch?v=FjKnugbmrP4 * Hybrid Level 3 - ETCS (Thales, ProRail/Network Rail/DB), Video der Deutschen Bahn: https://www.youtube.com/watch?v=FjKnugbmrP4
![HL3](./img/HL3_screenshot.png) ![HL3](./img/HL3_screenshot.png)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Architektur von ProB ## Architektur von ProB
* **`probcli`:** Kern/Hauptteil von ProB * **`probcli`:** Kern/Hauptteil von ProB
* Implementiert in SICStus Prolog * Implementiert in SICStus Prolog
* Erlaubt Animation, Visualisierung, Verifikation von formellen Spezifikationen * Erlaubt Animation, Visualisierung, Verifikation von formellen Spezifikationen
* Unterstützt u. A. (klassisches) B, Event-B, TLA<sup>+</sup>, CSP<sub>M</sub> * Unterstützt u. A. (klassisches) B, Event-B, TLA<sup>+</sup>, CSP<sub>M</sub>
* Kommandozeilentool oder interaktive REPL * Kommandozeilentool oder interaktive REPL
* **ProB 2-Java-API:** (aka ProB 2-Kernel; ≠ ProB 2-Jupyter-Kernel!) * **ProB 2-Java-API:** (aka ProB 2-Kernel; ≠ ProB 2-Jupyter-Kernel!)
* Objektorientierte Java-Schnittstelle für ProB * Objektorientierte Java-Schnittstelle für ProB
* Verwaltet automatisch eine oder mehrere `probcli`-Instanzen * Verwaltet automatisch eine oder mehrere `probcli`-Instanzen
* **ProB 2-Jupyter-Kernel:** Jupyter-Kernel-Implementierung für ProB * **ProB 2-Jupyter-Kernel:** Jupyter-Kernel-Implementierung für ProB
* In Java implementiert * In Java implementiert
* Ansteuerung von ProB durch ProB 2-Java-API * Ansteuerung von ProB durch ProB 2-Java-API
* Kommunikation mit Jupyter durch Jupyter-JVM-BaseKernel * Kommunikation mit Jupyter durch Jupyter-JVM-BaseKernel
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Formeln auswerten ## Formeln auswerten
* B-Ausdrücke auswerten und Prädikate lösen wie in `probcli -repl` * B-Ausdrücke auswerten und Prädikate lösen wie in `probcli -repl`
Zum Beispiel, Primzahlen bis 50 ausgeben: Zum Beispiel, Primzahlen bis 50 ausgeben:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{x | x > 1 & x < 50 & not(#y.(y > 1 & y < x & x mod y = 0))} {x | x > 1 & x < 50 & not(#y.(y > 1 & y < x & x mod y = 0))}
``` ```
%% Output %% Output
$\{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\}$
{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}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:prettyprint x > 1 & x < 50 & not(#y.(y > 1 & y < x & x mod y = 0)) :prettyprint x > 1 & x < 50 & not(#y.(y > 1 & y < x & x mod y = 0))
``` ```
%% Output %% Output
$\mathit{x} > 1 \wedge \mathit{x} < 50 \wedge \neg (\exists \mathit{y}\cdot (\mathit{y} > 1 \wedge \mathit{y} < \mathit{x} \wedge \mathit{x} \mod \mathit{y} = 0))$ $\mathit{x} > 1 \wedge \mathit{x} < 50 \wedge \neg (\exists \mathit{y}\cdot (\mathit{y} > 1 \wedge \mathit{y} < \mathit{x} \wedge \mathit{x} \mod \mathit{y} = 0))$
x > 1 ∧ x < 50 ∧ ¬(∃y·(y > 1 ∧ y < x ∧ x mod y = 0)) x > 1 ∧ x < 50 ∧ ¬(∃y·(y > 1 ∧ y < x ∧ x mod y = 0))
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Eingabe als Unicode ist auch erlaubt: Eingabe als Unicode ist auch erlaubt:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{x | x>1 ∧ x<50 ∧ ¬(∃y.(y>1 ∧ y<x ∧ x mod y=0))} {x | x>1 ∧ x<50 ∧ ¬(∃y.(y>1 ∧ y<x ∧ x mod y=0))}
``` ```
%% Output %% Output
$\{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\}$
{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}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Mehrzeilige Eingabe ist möglich, es gibt Syntax-Highlighting und Code Completion. Mehrzeilige Eingabe ist möglich, es gibt Syntax-Highlighting und Code Completion.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{S, E, N, D, M, O, R, Y} <: 0..9 {S, E, N, D, M, O, R, Y} <: 0..9
& S > 0 & M > 0 & S > 0 & M > 0
& card({S, E, N, D, M, O, R, Y}) = 8 & card({S, E, N, D, M, O, R, Y}) = 8
& &
S*1000 + E*100 + N*10 + D S*1000 + E*100 + N*10 + D
+ M*1000 + O*100 + R*10 + E + M*1000 + O*100 + R*10 + E
= M*10000 + O*1000 + N*100 + E*10 + Y = M*10000 + O*1000 + N*100 + E*10 + Y
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{R} = 8$ * $\mathit{R} = 8$
* $\mathit{S} = 9$ * $\mathit{S} = 9$
* $\mathit{D} = 7$ * $\mathit{D} = 7$
* $\mathit{E} = 5$ * $\mathit{E} = 5$
* $\mathit{Y} = 2$ * $\mathit{Y} = 2$
* $\mathit{M} = 1$ * $\mathit{M} = 1$
* $\mathit{N} = 6$ * $\mathit{N} = 6$
* $\mathit{O} = 0$ * $\mathit{O} = 0$
TRUE TRUE
Solution: Solution:
R = 8 R = 8
S = 9 S = 9
D = 7 D = 7
E = 5 E = 5
Y = 2 Y = 2
M = 1 M = 1
N = 6 N = 6
O = 0 O = 0
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Mithilfe der Mengentheorie kann man alle Lösungen finden, und mit dem ```:table``` Kommando als Tabelle ausgeben. Mithilfe der Mengentheorie kann man alle Lösungen finden, und mit dem ```:table``` Kommando als Tabelle ausgeben.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table {S,E,N,D,M,O,R,Y | :table {S,E,N,D,M,O,R,Y |
{S, E, N, D, M, O, R, Y} <: 0..9 {S, E, N, D, M, O, R, Y} <: 0..9
& S > 0 & M > 0 // <-- & S > 0 & M > 0 // <--
& card({S, E, N, D, M, O, R, Y}) = 8 & card({S, E, N, D, M, O, R, Y}) = 8
& &
S*1000 + E*100 + N*10 + D S*1000 + E*100 + N*10 + D
+ M*1000 + O*100 + R*10 + E + M*1000 + O*100 + R*10 + E
= M*10000 + O*1000 + N*100 + E*10 + Y = M*10000 + O*1000 + N*100 + E*10 + Y
} }
``` ```
%% Output %% Output
|S|E|N|D|M|O|R|Y| |S|E|N|D|M|O|R|Y|
|---|---|---|---|---|---|---|---| |---|---|---|---|---|---|---|---|
|$9$|$5$|$6$|$7$|$1$|$0$|$8$|$2$| |$9$|$5$|$6$|$7$|$1$|$0$|$8$|$2$|
S E N D M O R Y S E N D M O R Y
9 5 6 7 1 0 8 2 9 5 6 7 1 0 8 2
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
In B sind Folgen auch Funktionen, Funktionen auch Relationen, Relationen auch Mengen. In B sind Folgen auch Funktionen, Funktionen auch Relationen, Relationen auch Mengen.
Relationen können in Jupyter auch grafisch dargestellt werden. Relationen können in Jupyter auch grafisch dargestellt werden.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
: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})
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [("k5",{x,y|x:1..5 & y:1..5 & x>y})]> <Dot visualization: expr_as_graph [("k5",{x,y|x:1..5 & y:1..5 & x>y})]>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:pref DOT_ENGINE=circo :pref DOT_ENGINE=circo
``` ```
%% Output %% Output
Preference changed: DOT_ENGINE = circo Preference changed: DOT_ENGINE = circo
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
: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})
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [("k5",{x,y|x:1..5 & y:1..5 & x>y})]> <Dot visualization: expr_as_graph [("k5",{x,y|x:1..5 & y:1..5 & x>y})]>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Anwendungsmöglichkeiten # Anwendungsmöglichkeiten
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Interaktive Nutzung als REPL ## Interaktive Nutzung als REPL
* Jupyter Notebook kann wie eine REPL benutzt werden * Jupyter Notebook kann wie eine REPL benutzt werden
* Vorteile: mehrzeilige Eingaben, formatierte Ausgaben, verbesserte Editor-Funktionen, speicherbar * Vorteile: mehrzeilige Eingaben, formatierte Ausgaben, verbesserte Editor-Funktionen, speicherbar
* Alternative: `jupyter console` ermöglicht Verwendung von Jupyter-Kerneln im Terminal * Alternative: `jupyter console` ermöglicht Verwendung von Jupyter-Kerneln im Terminal
* Verhält sich wie eine klassische REPL, arbeitet nicht mit Notebooks * Verhält sich wie eine klassische REPL, arbeitet nicht mit Notebooks
* Unterstützt trotzdem erweiterte Funktionen: Eingabeverlauf, Code-Vervollständigung * Unterstützt trotzdem erweiterte Funktionen: Eingabeverlauf, Code-Vervollständigung
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Interaktive Experimentierung ## Interaktive Experimentierung
* Beliebige Stellen im Notebook können bearbeitet und neu ausgeführt werden * Beliebige Stellen im Notebook können bearbeitet und neu ausgeführt werden
* Vereinfacht Testen von Änderungen am Code, z. B.: * Vereinfacht Testen von Änderungen am Code, z. B.:
* Andere Konstanten-/Präferenzwerte * Andere Konstanten-/Präferenzwerte
* Hinzufügen/Entfernen von Invarianten/Guards * Hinzufügen/Entfernen von Invarianten/Guards
* Ändern der Operationsfolge * Ändern der Operationsfolge
* Auch Notebooks von anderen Nutzern können ohne Weiteres bearbeitet werden * Auch Notebooks von anderen Nutzern können ohne Weiteres bearbeitet werden
* Notebook-Dateien sind nie "schreibgeschützt" * Notebook-Dateien sind nie "schreibgeschützt"
* Anzeige und Bearbeitung nutzen die gleiche Oberfläche * Anzeige und Bearbeitung nutzen die gleiche Oberfläche
* Anwendungen: * Anwendungen:
* ProB-Notebook als Dokumentation und Beispielcode zu einem B-Modell * ProB-Notebook als Dokumentation und Beispielcode zu einem B-Modell
* ProB-Notebook * ProB-Notebook
* Übungsblätter für Lehrveranstaltungen (B, Logik, Mengentheorie, theoretische Informatik) als Notebooks * Übungsblätter für Lehrveranstaltungen (B, Logik, Mengentheorie, theoretische Informatik) als Notebooks
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Anwendung als Dokumentation (Bibliothek von ProB) # Anwendung als Dokumentation (Bibliothek von ProB)
## LibraryRegex ## LibraryRegex
This library provides various facilities for pattern matching with regular expressions. This library provides various facilities for pattern matching with regular expressions.
You can obtain the definitions below by putting the following into your DEFINITIONS clause: You can obtain the definitions below by putting the following into your DEFINITIONS clause:
`DEFINITIONS "LibraryRegex.def"` `DEFINITIONS "LibraryRegex.def"`
The file `LibraryRegex.def` is also bundled with ProB and can be found in the `stdlib` folder (as of version 1.8.3-beta4). The file `LibraryRegex.def` is also bundled with ProB and can be found in the `stdlib` folder (as of version 1.8.3-beta4).
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE Jupyter_LibraryRegex MACHINE Jupyter_LibraryRegex
DEFINITIONS "LibraryRegex.def"; "LibraryStrings.def" DEFINITIONS "LibraryRegex.def"; "LibraryStrings.def"
END END
``` ```
%% Output %% Output
Loaded machine: Jupyter_LibraryRegex Loaded machine: Jupyter_LibraryRegex
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### REGEX_SEARCH_ALL ### REGEX_SEARCH_ALL
This external function searches for **all** occurences of a pattern in a string and returns the matched strings as a B sequence. This external function searches for **all** occurences of a pattern in a string and returns the matched strings as a B sequence.
It always starts to match at the beginning. It always starts to match at the beginning.
Type: $STRING \times STRING \rightarrow seq(STRING)$. Type: $STRING \times STRING \rightarrow seq(STRING)$.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
REGEX_SEARCH_ALL("abcdef000234daf567","([1-9])([0-9]*)") REGEX_SEARCH_ALL("abcdef000234daf567","([1-9])([0-9]*)")
``` ```
%% Output %% Output
$\{(1\mapsto\text{"234"}),(2\mapsto\text{"567"})\}$ $\{(1\mapsto\text{"234"}),(2\mapsto\text{"567"})\}$
{(1↦"234"),(2↦"567")} {(1↦"234"),(2↦"567")}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
REGEX_SEARCH_ALL("abc-äéà-123","[[:alpha:]]") REGEX_SEARCH_ALL("abc-äéà-123","[[:alpha:]]")
``` ```
%% Output %% Output
$[\text{"a"},\text{"b"},\text{"c"},\text{"ä"},\text{"é"},\text{"à"}]$ $[\text{"a"},\text{"b"},\text{"c"},\text{"ä"},\text{"é"},\text{"à"}]$
["a","b","c","ä","é","à"] ["a","b","c","ä","é","à"]
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Anwendung: Interaktive Skripte für Vorlesungen # Anwendung: Interaktive Skripte für Vorlesungen
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE BaseTypes MACHINE BaseTypes
SETS PERSONS = {peter,paul,mary}; COLOURS = {red,green,blue} SETS PERSONS = {peter,paul,mary}; COLOURS = {red,green,blue}
END END
``` ```
%% Output %% Output
Loaded machine: BaseTypes Loaded machine: BaseTypes
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
In mathematics a binary relation over the sets $A$ and $B$ is defined to be In mathematics a binary relation over the sets $A$ and $B$ is defined to be
a subset of $A\times B$. a subset of $A\times B$.
The Cartesian product $A \times B$ in turn is defined to be the set of pairs The Cartesian product $A \times B$ in turn is defined to be the set of pairs
$a \mapsto b$ such that $a\in A$ and $b\in B$. $a \mapsto b$ such that $a\in A$ and $b\in B$.
For example, we have: For example, we have:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
PERSONS × COLOURS PERSONS × COLOURS
``` ```
%% Output %% Output
$\{(\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})\}$ $\{(\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})\}$
{(peter↦red),(peter↦green),(peter↦blue),(paul↦red),(paul↦green),(paul↦blue),(mary↦red),(mary↦green),(mary↦blue)} {(peter↦red),(peter↦green),(peter↦blue),(paul↦red),(paul↦green),(paul↦blue),(mary↦red),(mary↦green),(mary↦blue)}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
A particular relation could be the following one, which is a subset of PERSONS × COLOURS: A particular relation could be the following one, which is a subset of PERSONS × COLOURS:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{peter|->green,peter|->blue,mary|->blue} {peter|->green,peter|->blue,mary|->blue}
``` ```
%% Output %% Output
$\{(\mathit{peter}\mapsto \mathit{green}),(\mathit{peter}\mapsto \mathit{blue}),(\mathit{mary}\mapsto \mathit{blue})\}$ $\{(\mathit{peter}\mapsto \mathit{green}),(\mathit{peter}\mapsto \mathit{blue}),(\mathit{mary}\mapsto \mathit{blue})\}$
{(peter↦green),(peter↦blue),(mary↦blue)} {(peter↦green),(peter↦blue),(mary↦blue)}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
We can visualize this relation graphically as follows: We can visualize this relation graphically as follows:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("r1",{peter|->green,peter|->blue,mary|->blue}) :dot expr_as_graph ("r1",{peter|->green,peter|->blue,mary|->blue})
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [("r1",{(peter,green),(peter,blue),(mary,blue)})]> <Dot visualization: expr_as_graph [("r1",{(peter,green),(peter,blue),(mary,blue)})]>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table {peter|->green,peter|->blue,mary|->blue} :table {peter|->green,peter|->blue,mary|->blue}
``` ```
%% Output %% Output
|prj1|prj2| |prj1|prj2|
|---|---| |---|---|
|$\mathit{peter}$|$\mathit{green}$| |$\mathit{peter}$|$\mathit{green}$|
|$\mathit{peter}$|$\mathit{blue}$| |$\mathit{peter}$|$\mathit{blue}$|
|$\mathit{mary}$|$\mathit{blue}$| |$\mathit{mary}$|$\mathit{blue}$|
prj1 prj2 prj1 prj2
peter green peter green
peter blue peter blue
mary blue mary blue
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
As in B a relation is a set of pairs, all set operators can be applied to relations. As in B a relation is a set of pairs, all set operators can be applied to relations.
For example, For example,
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{peter|->green,peter|->blue,mary|->blue} - {mary|->blue} {peter|->green,peter|->blue,mary|->blue} - {mary|->blue}
``` ```
%% Output %% Output
$\{(\mathit{peter}\mapsto \mathit{green}),(\mathit{peter}\mapsto \mathit{blue})\}$ $\{(\mathit{peter}\mapsto \mathit{green}),(\mathit{peter}\mapsto \mathit{blue})\}$
{(peter↦green),(peter↦blue)} {(peter↦green),(peter↦blue)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{peter|->green,peter|->blue,mary|->blue} /\ {mary}*COLOURS {peter|->green,peter|->blue,mary|->blue} /\ {mary}*COLOURS
``` ```
%% Output %% Output
$\{(\mathit{mary}\mapsto \mathit{blue})\}$ $\{(\mathit{mary}\mapsto \mathit{blue})\}$
{(mary↦blue)} {(mary↦blue)}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Anwendung: Skript für theoretische Informatik (NFA) # Anwendung: Skript für theoretische Informatik (NFA)
Es folgen Teile aus dem Skript von Informatik 4 (Hauptautor Jörg Rothe). Es folgen Teile aus dem Skript von Informatik 4 (Hauptautor Jörg Rothe).
Nun erweitern wir die Überführungsfunktion in der Definition eines DFA Nun erweitern wir die Überführungsfunktion in der Definition eines DFA
und bezeichnen die neuen Automaten als NFA. und bezeichnen die neuen Automaten als NFA.
#### DEFINITION 2.9 (NFA) #### DEFINITION 2.9 (NFA)
Ein nichtdeterministischer endlicher Automat Ein nichtdeterministischer endlicher Automat
(kurz NFA) ist ein Quintupel $M = (\Sigma, Z, \delta , S, F)$, wobei (kurz NFA) ist ein Quintupel $M = (\Sigma, Z, \delta , S, F)$, wobei
* $\Sigma$ ein Alphabet ist, * $\Sigma$ ein Alphabet ist,
* $Z$ eine endliche Menge von Zust"anden mit $\Sigma \cap Z = \emptyset$, * $Z$ eine endliche Menge von Zust"anden mit $\Sigma \cap Z = \emptyset$,
* $\delta : Z \times \Sigma \rightarrow \pow(Z)$ die * $\delta : Z \times \Sigma \rightarrow \pow(Z)$ die
Überführungsfunktion (hier: $\pow(Z)$ ist die Potenzmenge Überführungsfunktion (hier: $\pow(Z)$ ist die Potenzmenge
von $Z$, also die Menge aller Teilmengen von $Z$), von $Z$, also die Menge aller Teilmengen von $Z$),
* $S \subseteq Z$ die Menge der Startzustände und * $S \subseteq Z$ die Menge der Startzustände und
* $F \subseteq Z$ die Menge der Endzustände (Finalzustände). * $F \subseteq Z$ die Menge der Endzustände (Finalzustände).
#### DEFINITION 2.10 (Sprache eines NFA) #### DEFINITION 2.10 (Sprache eines NFA)
Die erweiterte Überführungsfunktion $\widehat{\delta} : Die erweiterte Überführungsfunktion $\widehat{\delta} :
\pow(Z) \times \Sigma^* \rightarrow \pow(Z)$ von $M$ ist \pow(Z) \times \Sigma^* \rightarrow \pow(Z)$ von $M$ ist
induktiv definiert: induktiv definiert:
* $\widehat{\delta}(Z', \lambda) = Z'$ * $\widehat{\delta}(Z', \lambda) = Z'$
* $\widehat{\delta}(Z', ax) = \bigcup_{z \in Z'} \widehat{\delta}(\delta(z,a), x)$ * $\widehat{\delta}(Z', ax) = \bigcup_{z \in Z'} \widehat{\delta}(\delta(z,a), x)$
für alle $Z' \subseteq Z$, $a \in \Sigma$ und $x \in \Sigma^*$. für alle $Z' \subseteq Z$, $a \in \Sigma$ und $x \in \Sigma^*$.
Die vom NFA $M$ akzeptierte Sprache ist definiert durch Die vom NFA $M$ akzeptierte Sprache ist definiert durch
* L(M) = $\{w \in \Sigma^* \mid \widehat{\delta}(S,w) \cap F \neq \emptyset\}$ * L(M) = $\{w \in \Sigma^* \mid \widehat{\delta}(S,w) \cap F \neq \emptyset\}$
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Wie laden nun ein B Modell welches diese Definitionen beinhaltet. Wie laden nun ein B Modell welches diese Definitionen beinhaltet.
Wörter werden dabei in der B Sprache mit eckigen Klammern und Kommas geschrieben; aus 101 wird [1,0,1]. Wörter werden dabei in der B Sprache mit eckigen Klammern und Kommas geschrieben; aus 101 wird [1,0,1].
Gewisse griechische Zeichen sind in der B Sprache als Schlüsselwörter reserviert, zB $\Sigma$. Gewisse griechische Zeichen sind in der B Sprache als Schlüsselwörter reserviert, zB $\lambda$.
Auch kann man leider weder ' noch $\hat$ in Bezeichnern verwenden. Auch kann man leider weder ' noch $\hat$ in Bezeichnern verwenden.
Deshalb wird aus Deshalb wird aus
* $\Sigma$ wird ```Sig``` * $\Sigma^*$ wird ```seq(Σ)```
* $\Sigma^*$ wird ```seq(Seq)```
* $\widehat{\delta}$ wird ```δs``` * $\widehat{\delta}$ wird ```δs```
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE NFA_nach_DFA MACHINE NFA_nach_DFA
SETS SETS
Z = {z0,z1,z2,z3} Z = {z0,z1,z2,z3}
DEFINITIONS Sig == {0,1}
ABSTRACT_CONSTANTS δs, L ABSTRACT_CONSTANTS δs, L
CONSTANTS S, F, δ CONSTANTS Σ, S, F, δ
PROPERTIES PROPERTIES
S ⊆ Z ∧ F ⊆ Z ∧ δ ∈ (Z×Sig) → ℙ(Z) ∧ S ⊆ Z ∧ F ⊆ Z ∧ δ ∈ (Z×Σ) → ℙ(Z) ∧
/* Definition der erweiterten Übergangsfunktion */ /* Definition der erweiterten Übergangsfunktion */
δs = λ(ZZ,s).(ZZ⊆Z | IF s=[] THEN ZZ ELSE UNION(z).(z∈ZZ|δs(δ(z,first(s)),tail(s))) END ) δs = λ(ZZ,s).(ZZ⊆Z | IF s=[] THEN ZZ ELSE UNION(z).(z∈ZZ|δs(δ(z,first(s)),tail(s))) END )
/* die vom Automaten generierte Sprache */ /* die vom Automaten generierte Sprache */
L = {s|s∈seq(Sig) ∧ δs(S,s) ∩ F ≠ ∅} L = {s|s∈seq(Σ) ∧ δs(S,s) ∩ F ≠ ∅}
/* Nun ein Beispiel-Automat von Folie 24 (Info 4) */ /* Nun ein Beispiel-Automat von Folie 24 (Info 4) */
Σ = {0,1} ∧
S = {z0} ∧ F={z2} ∧ S = {z0} ∧ F={z2} ∧
δ = { (z0,0)↦{z0}, (z0,1)↦{z0,z1}, δ = { (z0,0)↦{z0}, (z0,1)↦{z0,z1},
(z1,0)↦{z2}, (z1,1)↦{z2}, (z1,0)↦{z2}, (z1,1)↦{z2},
(z2,0)↦{z3}, (z2,1)↦{z3}, (z2,0)↦{z3}, (z2,1)↦{z3},
(z3,0)↦{z3}, (z3,1)↦{z3} } (z3,0)↦{z3}, (z3,1)↦{z3} }
END END
``` ```
%% Output %% Output
Loaded machine: NFA_nach_DFA Loaded machine: NFA_nach_DFA
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:constants :constants
``` ```
%% Output %% Output
Machine constants set up using operation 0: $setup_constants() Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:init :init
``` ```
%% Output %% Output
Machine initialised using operation 1: $initialise_machine() Machine initialised using operation 1: $initialise_machine()
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Die Übergangsfunktion $\delta$ gibt us für einen Zustand und ein Symbol die möglichen nächsten Zustande an: Die Übergangsfunktion $\delta$ gibt us für einen Zustand und ein Symbol die möglichen nächsten Zustande an:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
δ(z0,1) δ(z0,1)
``` ```
%% Output %% Output
$\{\mathit{z0},\mathit{z1}\}$ $\{\mathit{z0},\mathit{z1}\}$
{z0,z1} {z0,z1}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Der obige Automat ist nichtdeterministisch, da zum Beispiel: Der obige Automat ist nichtdeterministisch, da zum Beispiel:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card(δ(z0,1)) card(δ(z0,1))
``` ```
%% Output %% Output
$2$ $2$
2 2
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
``` ```
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Wir können die Übergangsfunktion $\delta$ des Automaten auch als Tabelle oder Graphen darstellen: Wir können die Übergangsfunktion $\delta$ des Automaten auch als Tabelle oder Graphen darstellen:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table δ :table δ
``` ```
%% Output %% Output
|prj11|prj12|prj2| |prj11|prj12|prj2|
|---|---|---| |---|---|---|
|$\mathit{z0}$|$0$|$\{\mathit{z0}\}$| |$\mathit{z0}$|$0$|$\{\mathit{z0}\}$|
|$\mathit{z0}$|$1$|$\{\mathit{z0},\mathit{z1}\}$| |$\mathit{z0}$|$1$|$\{\mathit{z0},\mathit{z1}\}$|
|$\mathit{z1}$|$0$|$\{\mathit{z2}\}$| |$\mathit{z1}$|$0$|$\{\mathit{z2}\}$|
|$\mathit{z1}$|$1$|$\{\mathit{z2}\}$| |$\mathit{z1}$|$1$|$\{\mathit{z2}\}$|
|$\mathit{z2}$|$0$|$\{\mathit{z3}\}$| |$\mathit{z2}$|$0$|$\{\mathit{z3}\}$|
|$\mathit{z2}$|$1$|$\{\mathit{z3}\}$| |$\mathit{z2}$|$1$|$\{\mathit{z3}\}$|
|$\mathit{z3}$|$0$|$\{\mathit{z3}\}$| |$\mathit{z3}$|$0$|$\{\mathit{z3}\}$|
|$\mathit{z3}$|$1$|$\{\mathit{z3}\}$| |$\mathit{z3}$|$1$|$\{\mathit{z3}\}$|
prj11 prj12 prj2 prj11 prj12 prj2
z0 0 {z0} z0 0 {z0}
z0 1 {z0,z1} z0 1 {z0,z1}
z1 0 {z2} z1 0 {z2}
z1 1 {z2} z1 1 {z2}
z2 0 {z3} z2 0 {z3}
z2 1 {z3} z2 1 {z3}
z3 0 {z3} z3 0 {z3}
z3 1 {z3} z3 1 {z3}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("0",{x,y| x∈Z & y:δ(x,0)}, :dot expr_as_graph ("0",{x,y| x∈Z & y:δ(x,0)},
"1",{x,y| x∈S & y∈δ(x,1)}) "1",{x,y| x∈S & y∈δ(x,1)})
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [("0",{x,y|x:Z & y:δ(x, 0)})]> <Dot visualization: expr_as_graph [("0",{x,y|x:Z & y:δ(x, 0)})]>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Die Funktion $\widehat{\delta}$ berechnet die möglichen Zustände nach dem Abarbeiten eines Wortes. Zum Beispiel, kann sich der Automat nach dem Abarbeiten des Präfixes 111 in folgenden Zuständen befinden: Die Funktion $\widehat{\delta}$ berechnet die möglichen Zustände nach dem Abarbeiten eines Wortes. Zum Beispiel, kann sich der Automat nach dem Abarbeiten des Präfixes 111 in folgenden Zuständen befinden:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
δs(S,[1,1,1]) δs(S,[1,1,1])
``` ```
%% Output %% Output
$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$ $\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$
{z0,z1,z2,z3} {z0,z1,z2,z3}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Der Automat akzeptiert zum Beispiel das Wort 111 und das Wort 101 nicht, da: Der Automat akzeptiert zum Beispiel das Wort 111 und das Wort 101 nicht, da:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
δs(S,[1,1,1]) ∩ F δs(S,[1,1,1]) ∩ F
``` ```
%% Output %% Output
$\{\mathit{z2}\}$ $\{\mathit{z2}\}$
{z2} {z2}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
δs(S,[1,0,1]) ∩ F δs(S,[1,0,1]) ∩ F
``` ```
%% Output %% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$ $\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Folgende Wörter der Länge 3 werden vom Automaten akzeptiert: Folgende Wörter der Länge 3 werden vom Automaten akzeptiert:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table {x,y,z| [x,y,z]∈L} :table {x,y,z| [x,y,z]∈L}
``` ```
%% Output %% Output
|x|y|z| |x|y|z|
|---|---|---| |---|---|---|
|$0$|$1$|$0$| |$0$|$1$|$0$|
|$0$|$1$|$1$| |$0$|$1$|$1$|
|$1$|$1$|$0$| |$1$|$1$|$0$|
|$1$|$1$|$1$| |$1$|$1$|$1$|
x y z x y z
0 1 0 0 1 0
0 1 1 0 1 1
1 1 0 1 1 0
1 1 1 1 1 1
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
und folgende werden nicht akzeptiert: und folgende werden nicht akzeptiert:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table {x,y,z| {x,y,z} ⊆ Sig & ¬([x,y,z]∈L)} :table {x,y,z| {x,y,z} ⊆ Σ & ¬([x,y,z]∈L)}
``` ```
%% Output %% Output
|x|y|z| |x|y|z|
|---|---|---| |---|---|---|
|$0$|$0$|$0$| |$0$|$0$|$0$|
|$0$|$0$|$1$| |$0$|$0$|$1$|
|$1$|$0$|$0$| |$1$|$0$|$0$|
|$1$|$0$|$1$| |$1$|$0$|$1$|
x y z x y z
0 0 0 0 0 0
0 0 1 0 0 1
1 0 0 1 0 0
1 0 1 1 0 1
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Es stellt sich die Frage, ob NFAs mächtiger sind als DFAs. Die Es stellt sich die Frage, ob NFAs mächtiger sind als DFAs. Die
Antwort lautet: Nein. Antwort lautet: Nein.
## Theorem (Rabin und Scott) ## Theorem (Rabin und Scott)
Jede von einem NFA akzeptierte Sprache kann auch von einem DFA akzeptiert Jede von einem NFA akzeptierte Sprache kann auch von einem DFA akzeptiert
werden. werden.
### Beweis ### Beweis
Sei $M = (\Sigma, Z, \delta , S, E)$ ein NFA. Sei $M = (\Sigma, Z, \delta , S, E)$ ein NFA.
Konstruiere einen zu Konstruiere einen zu
$M$ äquivalenten DFA $M$ äquivalenten DFA
$M' = (\Sigma, \pow(Z), \delta' ,z_0', F)$ wie folgt: $M' = (\Sigma, \pow(Z), \delta' ,z_0', F)$ wie folgt:
* Zustandsmenge von $M'$: die Potenzmenge $\pow(Z)$ von $Z$, * Zustandsmenge von $M'$: die Potenzmenge $\pow(Z)$ von $Z$,
* $\delta'(Z' , a) = \widehat{\delta}(Z',a)$ für alle $Z' \subseteq Z$ und $a \in \Sigma$, * $\delta'(Z' , a) = \widehat{\delta}(Z',a)$ für alle $Z' \subseteq Z$ und $a \in \Sigma$,
* $z_0'=S$, * $z_0'=S$,
* $F = \{ Z' \subseteq Z \mid Z' \cap E \neq \emptyset\}$. * $F = \{ Z' \subseteq Z \mid Z' \cap E \neq \emptyset\}$.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Für den oben geladen Automaten können wir diese Konstruktion illustrieren. Für den oben geladen Automaten können wir diese Konstruktion illustrieren.
Die Potenzmenge der Zustände ist: Die Potenzmenge der Zustände ist:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
ℙ(Z) ℙ(Z)
``` ```
%% Output %% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{\mathit{z0}\},\{\mathit{z0},\mathit{z1}\},\{\mathit{z0},\mathit{z2}\},\{\mathit{z0},\mathit{z3}\},\{\mathit{z1}\},\{\mathit{z0},\mathit{z1},\mathit{z2}\},\{\mathit{z0},\mathit{z1},\mathit{z3}\},\{\mathit{z1},\mathit{z2}\},\{\mathit{z1},\mathit{z3}\},\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\},\{\mathit{z2}\},\{\mathit{z0},\mathit{z2},\mathit{z3}\},\{\mathit{z1},\mathit{z2},\mathit{z3}\},\{\mathit{z2},\mathit{z3}\},\{\mathit{z3}\}\}$ $\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{\mathit{z0}\},\{\mathit{z0},\mathit{z1}\},\{\mathit{z0},\mathit{z2}\},\{\mathit{z0},\mathit{z3}\},\{\mathit{z1}\},\{\mathit{z0},\mathit{z1},\mathit{z2}\},\{\mathit{z0},\mathit{z1},\mathit{z3}\},\{\mathit{z1},\mathit{z2}\},\{\mathit{z1},\mathit{z3}\},\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\},\{\mathit{z2}\},\{\mathit{z0},\mathit{z2},\mathit{z3}\},\{\mathit{z1},\mathit{z2},\mathit{z3}\},\{\mathit{z2},\mathit{z3}\},\{\mathit{z3}\}\}$
{∅,{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}} {∅,{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}}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Tabellarisch k¨ønnen wir $\widehat{\delta}$ für $\pow(Z)$ wie folgt ausrechnen: Tabellarisch k¨ønnen wir $\widehat{\delta}$ für $\pow(Z)$ wie folgt ausrechnen:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table {x,a,y| a:Sig & x∈ℙ(Z) & y=δs(x,[a])} :table {x,a,y| a∈Σ & x∈ℙ(Z) & y=δs(x,[a])}
``` ```
%% Output %% Output
|x|a|y| |x|a|y|
|---|---|---| |---|---|---|
|$\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$|$0$|$\emptyset$| |$\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$|$0$|$\emptyset$|
|$\emptyset$|$1$|$\emptyset$| |$\emptyset$|$1$|$\emptyset$|
|$\{\mathit{z0}\}$|$0$|$\{\mathit{z0}\}$| |$\{\mathit{z0}\}$|$0$|$\{\mathit{z0}\}$|
|$\{\mathit{z0}\}$|$1$|$\{\mathit{z0},\mathit{z1}\}$| |$\{\mathit{z0}\}$|$1$|$\{\mathit{z0},\mathit{z1}\}$|
|$\{\mathit{z0},\mathit{z1}\}$|$0$|$\{\mathit{z0},\mathit{z2}\}$| |$\{\mathit{z0},\mathit{z1}\}$|$0$|$\{\mathit{z0},\mathit{z2}\}$|
|$\{\mathit{z0},\mathit{z1}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z2}\}$| |$\{\mathit{z0},\mathit{z1}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z2}\}$|
|$\{\mathit{z0},\mathit{z2}\}$|$0$|$\{\mathit{z0},\mathit{z3}\}$| |$\{\mathit{z0},\mathit{z2}\}$|$0$|$\{\mathit{z0},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z2}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$| |$\{\mathit{z0},\mathit{z2}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z3}\}$|$0$|$\{\mathit{z0},\mathit{z3}\}$| |$\{\mathit{z0},\mathit{z3}\}$|$0$|$\{\mathit{z0},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z3}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$| |$\{\mathit{z0},\mathit{z3}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$|
|$\{\mathit{z1}\}$|$0$|$\{\mathit{z2}\}$| |$\{\mathit{z1}\}$|$0$|$\{\mathit{z2}\}$|
|$\{\mathit{z1}\}$|$1$|$\{\mathit{z2}\}$| |$\{\mathit{z1}\}$|$1$|$\{\mathit{z2}\}$|
|$\{\mathit{z0},\mathit{z1},\mathit{z2}\}$|$0$|$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$| |$\{\mathit{z0},\mathit{z1},\mathit{z2}\}$|$0$|$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z1},\mathit{z2}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$| |$\{\mathit{z0},\mathit{z1},\mathit{z2}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$|$0$|$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$| |$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$|$0$|$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$| |$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z1},\mathit{z2}\}$|$0$|$\{\mathit{z2},\mathit{z3}\}$| |$\{\mathit{z1},\mathit{z2}\}$|$0$|$\{\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z1},\mathit{z2}\}$|$1$|$\{\mathit{z2},\mathit{z3}\}$| |$\{\mathit{z1},\mathit{z2}\}$|$1$|$\{\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z1},\mathit{z3}\}$|$0$|$\{\mathit{z2},\mathit{z3}\}$| |$\{\mathit{z1},\mathit{z3}\}$|$0$|$\{\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z1},\mathit{z3}\}$|$1$|$\{\mathit{z2},\mathit{z3}\}$| |$\{\mathit{z1},\mathit{z3}\}$|$1$|$\{\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$|$0$|$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$| |$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$|$0$|$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$| |$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z2}\}$|$0$|$\{\mathit{z3}\}$| |$\{\mathit{z2}\}$|$0$|$\{\mathit{z3}\}$|
|$\{\mathit{z2}\}$|$1$|$\{\mathit{z3}\}$| |$\{\mathit{z2}\}$|$1$|$\{\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$|$0$|$\{\mathit{z0},\mathit{z3}\}$| |$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$|$0$|$\{\mathit{z0},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$| |$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$|
|$\{\mathit{z1},\mathit{z2},\mathit{z3}\}$|$0$|$\{\mathit{z2},\mathit{z3}\}$| |$\{\mathit{z1},\mathit{z2},\mathit{z3}\}$|$0$|$\{\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z1},\mathit{z2},\mathit{z3}\}$|$1$|$\{\mathit{z2},\mathit{z3}\}$| |$\{\mathit{z1},\mathit{z2},\mathit{z3}\}$|$1$|$\{\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z2},\mathit{z3}\}$|$0$|$\{\mathit{z3}\}$| |$\{\mathit{z2},\mathit{z3}\}$|$0$|$\{\mathit{z3}\}$|
|$\{\mathit{z2},\mathit{z3}\}$|$1$|$\{\mathit{z3}\}$| |$\{\mathit{z2},\mathit{z3}\}$|$1$|$\{\mathit{z3}\}$|
|$\{\mathit{z3}\}$|$0$|$\{\mathit{z3}\}$| |$\{\mathit{z3}\}$|$0$|$\{\mathit{z3}\}$|
|$\{\mathit{z3}\}$|$1$|$\{\mathit{z3}\}$| |$\{\mathit{z3}\}$|$1$|$\{\mathit{z3}\}$|
x a y x a y
{} 0 {} {} 0 {}
{} 1 {} {} 1 {}
{z0} 0 {z0} {z0} 0 {z0}
{z0} 1 {z0,z1} {z0} 1 {z0,z1}
{z0,z1} 0 {z0,z2} {z0,z1} 0 {z0,z2}
{z0,z1} 1 {z0,z1,z2} {z0,z1} 1 {z0,z1,z2}
{z0,z2} 0 {z0,z3} {z0,z2} 0 {z0,z3}
{z0,z2} 1 {z0,z1,z3} {z0,z2} 1 {z0,z1,z3}
{z0,z3} 0 {z0,z3} {z0,z3} 0 {z0,z3}
{z0,z3} 1 {z0,z1,z3} {z0,z3} 1 {z0,z1,z3}
{z1} 0 {z2} {z1} 0 {z2}
{z1} 1 {z2} {z1} 1 {z2}
{z0,z1,z2} 0 {z0,z2,z3} {z0,z1,z2} 0 {z0,z2,z3}
{z0,z1,z2} 1 {z0,z1,z2,z3} {z0,z1,z2} 1 {z0,z1,z2,z3}
{z0,z1,z3} 0 {z0,z2,z3} {z0,z1,z3} 0 {z0,z2,z3}
{z0,z1,z3} 1 {z0,z1,z2,z3} {z0,z1,z3} 1 {z0,z1,z2,z3}
{z1,z2} 0 {z2,z3} {z1,z2} 0 {z2,z3}
{z1,z2} 1 {z2,z3} {z1,z2} 1 {z2,z3}
{z1,z3} 0 {z2,z3} {z1,z3} 0 {z2,z3}
{z1,z3} 1 {z2,z3} {z1,z3} 1 {z2,z3}
{z0,z1,z2,z3} 0 {z0,z2,z3} {z0,z1,z2,z3} 0 {z0,z2,z3}
{z0,z1,z2,z3} 1 {z0,z1,z2,z3} {z0,z1,z2,z3} 1 {z0,z1,z2,z3}
{z2} 0 {z3} {z2} 0 {z3}
{z2} 1 {z3} {z2} 1 {z3}
{z0,z2,z3} 0 {z0,z3} {z0,z2,z3} 0 {z0,z3}
{z0,z2,z3} 1 {z0,z1,z3} {z0,z2,z3} 1 {z0,z1,z3}
{z1,z2,z3} 0 {z2,z3} {z1,z2,z3} 0 {z2,z3}
{z1,z2,z3} 1 {z2,z3} {z1,z2,z3} 1 {z2,z3}
{z2,z3} 0 {z3} {z2,z3} 0 {z3}
{z2,z3} 1 {z3} {z2,z3} 1 {z3}
{z3} 0 {z3} {z3} 0 {z3}
{z3} 1 {z3} {z3} 1 {z3}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Graphisch lässt sich der Automat wie folgt darstellen; die Start und Endzustände sind noch nicht schön markiert. Graphisch lässt sich der Automat wie folgt darstellen; die Start und Endzustände sind noch nicht schön markiert.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:pref DOT_DECOMPOSE_NODES=FALSE :pref DOT_DECOMPOSE_NODES=FALSE
``` ```
%% Output %% Output
Preference changed: DOT_DECOMPOSE_NODES = FALSE Preference changed: DOT_DECOMPOSE_NODES = FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("0",{x,y| x∈ℙ(Z) & δs(x,[0]) = y}, :dot expr_as_graph ("0",{x,y| x∈ℙ(Z) & δs(x,[0]) = y},
"1",{x,y| x∈ℙ(Z) & δs(x,[1]) = y}, "1",{x,y| x∈ℙ(Z) & δs(x,[1]) = y},
"start", {x,y|x=y & x={z0}}, "start", {x,y|x=y & x={z0}},
"end", {x,y|x=y & x∩F ≠ ∅}) "end", {x,y|x=y & x∩F ≠ ∅})
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [("0",{x,y|x:POW(Z) & δs(x, [0])=y})]> <Dot visualization: expr_as_graph [("0",{x,y|x:POW(Z) & δs(x, [0])=y})]>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Anwendung: Prüfbericht # Anwendung: Prüfbericht
ProB wird zur Datenvalidierung benutzt. ProB wird zur Datenvalidierung benutzt.
Man kann mit Jupyter auch Prüfberichte erstellen, inklusive der Darstellung von Gegenbeispielen und Erklärungen. Man kann mit Jupyter auch Prüfberichte erstellen, inklusive der Darstellung von Gegenbeispielen und Erklärungen.
Als Beispiel werden hier keine Daten aus der Bahntechnik sondern Daten über chemische Elemente benutzt. Als Beispiel werden hier keine Daten aus der Bahntechnik sondern Daten über chemische Elemente benutzt.
## Validation Report: Chemical Elements ## Validation Report: Chemical Elements
This report was generated with the following version of ProB: This report was generated with the following version of ProB:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:version :version
``` ```
%% Output %% Output
ProB CLI: 1.9.0-nightly (6b5c5ef186e29710bc4c6a651339f67f972db657) ProB CLI: 1.9.0-nightly (6b5c5ef186e29710bc4c6a651339f67f972db657)
ProB 2: 3.2.12-SNAPSHOT (16945773c7a5d9b44c1061db2a89cdd9e1da3cc3) ProB 2: 3.2.12-SNAPSHOT (16945773c7a5d9b44c1061db2a89cdd9e1da3cc3)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
We read in a CSV data file containing the chemical elements: We read in a CSV data file containing the chemical elements:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE ChemicalElements MACHINE ChemicalElements
DEFINITIONS DEFINITIONS
"LibraryStrings.def"; "LibraryStrings.def";
"LibraryCSV.def" "LibraryCSV.def"
CONSTANTS eltable CONSTANTS eltable
PROPERTIES PROPERTIES
eltable : POW(STRING*STRING*INTEGER*STRING) & eltable : POW(STRING*STRING*INTEGER*STRING) &
eltable = READ_CSV("csv/elementdata.csv",TRUE,TRUE) // we skip line 1 and extra columns eltable = READ_CSV("csv/elementdata.csv",TRUE,TRUE) // we skip line 1 and extra columns
END END
``` ```
%% Output %% Output
Loaded machine: ChemicalElements Loaded machine: ChemicalElements
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:constants :constants
``` ```
%% Output %% Output
Machine constants set up using operation 0: $setup_constants() Machine constants set up using operation 0: $setup_constants()
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
We have read in the following number of elements: We have read in the following number of elements:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card(eltable) card(eltable)
``` ```
%% Output %% Output
$118$ $118$
118 118
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table eltable :table eltable
``` ```
%% Output %% Output
|prj111|prj112|prj12|prj2| |prj111|prj112|prj12|prj2|
|---|---|---|---| |---|---|---|---|
|$\text{"Actinium"}$|$\text{"Ac"}$|$89$|$\text{"227.0278"}$| |$\text{"Actinium"}$|$\text{"Ac"}$|$89$|$\text{"227.0278"}$|
|$\text{"Aluminum"}$|$\text{"Al"}$|$13$|$\text{"26.981539"}$| |$\text{"Aluminum"}$|$\text{"Al"}$|$13$|$\text{"26.981539"}$|
|$\text{"Americium"}$|$\text{"Am"}$|$95$|$\text{"243.0614"}$| |$\text{"Americium"}$|$\text{"Am"}$|$95$|$\text{"243.0614"}$|
|$\text{"Antimony"}$|$\text{"Sb"}$|$51$|$\text{"121.76"}$| |$\text{"Antimony"}$|$\text{"Sb"}$|$51$|$\text{"121.76"}$|
|$\text{"Argon"}$|$\text{"Ar"}$|$18$|$\text{"39.948"}$| |$\text{"Argon"}$|$\text{"Ar"}$|$18$|$\text{"39.948"}$|
|$\text{"Arsenic"}$|$\text{"As"}$|$33$|$\text{"74.92159"}$| |$\text{"Arsenic"}$|$\text{"As"}$|$33$|$\text{"74.92159"}$|
|$\text{"Astatine"}$|$\text{"At"}$|$85$|$\text{"209.9871"}$| |$\text{"Astatine"}$|$\text{"At"}$|$85$|$\text{"209.9871"}$|
|$\text{"Barium"}$|$\text{"Ba"}$|$56$|$\text{"137.327"}$| |$\text{"Barium"}$|$\text{"Ba"}$|$56$|$\text{"137.327"}$|
|$\text{"Berkelium"}$|$\text{"Bk"}$|$97$|$\text{"247.0703"}$| |$\text{"Berkelium"}$|$\text{"Bk"}$|$97$|$\text{"247.0703"}$|
|$\text{"Beryllium"}$|$\text{"Be"}$|$4$|$\text{"9.01218"}$| |$\text{"Beryllium"}$|$\text{"Be"}$|$4$|$\text{"9.01218"}$|
|$\text{"Bismuth"}$|$\text{"Bi"}$|$83$|$\text{"208.98037"}$| |$\text{"Bismuth"}$|$\text{"Bi"}$|$83$|$\text{"208.98037"}$|
|$\text{"Bohrium"}$|$\text{"Bh"}$|$107$|$\text{"[264]"}$| |$\text{"Bohrium"}$|$\text{"Bh"}$|$107$|$\text{"[264]"}$|
|$\text{"Boron"}$|$\text{"B"}$|$5$|$\text{"10.811"}$| |$\text{"Boron"}$|$\text{"B"}$|$5$|$\text{"10.811"}$|
|$\text{"Bromine"}$|$\text{"Br"}$|$35$|$\text{"79.904"}$| |$\text{"Bromine"}$|$\text{"Br"}$|$35$|$\text{"79.904"}$|
|$\text{"Cadmium"}$|$\text{"Cd"}$|$48$|$\text{"112.411"}$| |$\text{"Cadmium"}$|$\text{"Cd"}$|$48$|$\text{"112.411"}$|
|$\text{"Calcium"}$|$\text{"Ca"}$|$20$|$\text{"40.078"}$| |$\text{"Calcium"}$|$\text{"Ca"}$|$20$|$\text{"40.078"}$|
|$\text{"Californium"}$|$\text{"Cf"}$|$98$|$\text{"251.0796"}$| |$\text{"Californium"}$|$\text{"Cf"}$|$98$|$\text{"251.0796"}$|
|$\text{"Carbon"}$|$\text{"C"}$|$6$|$\text{"12.011"}$| |$\text{"Carbon"}$|$\text{"C"}$|$6$|$\text{"12.011"}$|
|$\text{"Cerium"}$|$\text{"Ce"}$|$58$|$\text{"140.115"}$| |$\text{"Cerium"}$|$\text{"Ce"}$|$58$|$\text{"140.115"}$|
|$\text{"Cesium"}$|$\text{"Cs"}$|$55$|$\text{"132.90543"}$| |$\text{"Cesium"}$|$\text{"Cs"}$|$55$|$\text{"132.90543"}$|
|$\text{"Chlorine"}$|$\text{"Cl"}$|$17$|$\text{"35.4527"}$| |$\text{"Chlorine"}$|$\text{"Cl"}$|$17$|$\text{"35.4527"}$|
|$\text{"Chromium"}$|$\text{"Cr"}$|$24$|$\text{"51.9961"}$| |$\text{"Chromium"}$|$\text{"Cr"}$|$24$|$\text{"51.9961"}$|
|$\text{"Cobalt"}$|$\text{"Co"}$|$27$|$\text{"58.9332"}$| |$\text{"Cobalt"}$|$\text{"Co"}$|$27$|$\text{"58.9332"}$|
|$\text{"Copper"}$|$\text{"Cu"}$|$29$|$\text{"63.546"}$| |$\text{"Copper"}$|$\text{"Cu"}$|$29$|$\text{"63.546"}$|
|$\text{"Curium"}$|$\text{"Cm"}$|$96$|$\text{"247.0703"}$| |$\text{"Curium"}$|$\text{"Cm"}$|$96$|$\text{"247.0703"}$|
|$\text{"Dubnium"}$|$\text{"Db"}$|$105$|$\text{"[262]"}$| |$\text{"Dubnium"}$|$\text{"Db"}$|$105$|$\text{"[262]"}$|
|$\text{"Dysprosium"}$|$\text{"Dy"}$|$66$|$\text{"162.5"}$| |$\text{"Dysprosium"}$|$\text{"Dy"}$|$66$|$\text{"162.5"}$|
|$\text{"Einsteinium"}$|$\text{"Es"}$|$99$|$\text{"252.083"}$| |$\text{"Einsteinium"}$|$\text{"Es"}$|$99$|$\text{"252.083"}$|
|$\text{"Erbium"}$|$\text{"Er"}$|$68$|$\text{"167.26"}$| |$\text{"Erbium"}$|$\text{"Er"}$|$68$|$\text{"167.26"}$|
|$\text{"Europium"}$|$\text{"Eu"}$|$63$|$\text{"151.965"}$| |$\text{"Europium"}$|$\text{"Eu"}$|$63$|$\text{"151.965"}$|
|$\text{"Fermium"}$|$\text{"Fm"}$|$100$|$\text{"257.0951"}$| |$\text{"Fermium"}$|$\text{"Fm"}$|$100$|$\text{"257.0951"}$|
|$\text{"Fluorine"}$|$\text{"F"}$|$9$|$\text{"18.998403"}$| |$\text{"Fluorine"}$|$\text{"F"}$|$9$|$\text{"18.998403"}$|
|$\text{"Francium"}$|$\text{"Fr"}$|$87$|$\text{"223.0197"}$| |$\text{"Francium"}$|$\text{"Fr"}$|$87$|$\text{"223.0197"}$|
|$\text{"Gadolinium"}$|$\text{"Gd"}$|$64$|$\text{"157.25"}$| |$\text{"Gadolinium"}$|$\text{"Gd"}$|$64$|$\text{"157.25"}$|
|$\text{"Gallium"}$|$\text{"Ga"}$|$31$|$\text{"69.723"}$| |$\text{"Gallium"}$|$\text{"Ga"}$|$31$|$\text{"69.723"}$|
|$\text{"Germanium"}$|$\text{"Ge"}$|$32$|$\text{"72.61"}$| |$\text{"Germanium"}$|$\text{"Ge"}$|$32$|$\text{"72.61"}$|
|$\text{"Gold"}$|$\text{"Au"}$|$79$|$\text{"196.96654"}$| |$\text{"Gold"}$|$\text{"Au"}$|$79$|$\text{"196.96654"}$|
|$\text{"Hafnium"}$|$\text{"Hf"}$|$72$|$\text{"178.49"}$| |$\text{"Hafnium"}$|$\text{"Hf"}$|$72$|$\text{"178.49"}$|
|$\text{"Hassium"}$|$\text{"Hs"}$|$108$|$\text{"[269]"}$| |$\text{"Hassium"}$|$\text{"Hs"}$|$108$|$\text{"[269]"}$|
|$\text{"Helium"}$|$\text{"He"}$|$2$|$\text{"4.002602"}$| |$\text{"Helium"}$|$\text{"He"}$|$2$|$\text{"4.002602"}$|
|$\text{"Holmium"}$|$\text{"Ho"}$|$67$|$\text{"164.93032"}$| |$\text{"Holmium"}$|$\text{"Ho"}$|$67$|$\text{"164.93032"}$|
|$\text{"Hydrogen"}$|$\text{"H"}$|$1$|$\text{"1.00794"}$| |$\text{"Hydrogen"}$|$\text{"H"}$|$1$|$\text{"1.00794"}$|
|$\text{"Indium"}$|$\text{"In"}$|$49$|$\text{"114.818"}$| |$\text{"Indium"}$|$\text{"In"}$|$49$|$\text{"114.818"}$|
|$\text{"Iodine"}$|$\text{"I"}$|$53$|$\text{"126.90447"}$| |$\text{"Iodine"}$|$\text{"I"}$|$53$|$\text{"126.90447"}$|
|$\text{"Iridium"}$|$\text{"Ir"}$|$77$|$\text{"192.22"}$| |$\text{"Iridium"}$|$\text{"Ir"}$|$77$|$\text{"192.22"}$|
|$\text{"Iron"}$|$\text{"Fe"}$|$26$|$\text{"55.847"}$| |$\text{"Iron"}$|$\text{"Fe"}$|$26$|$\text{"55.847"}$|
|$\text{"Krypton"}$|$\text{"Kr"}$|$36$|$\text{"83.8"}$| |$\text{"Krypton"}$|$\text{"Kr"}$|$36$|$\text{"83.8"}$|
|$\text{"Lanthanum"}$|$\text{"La"}$|$57$|$\text{"138.9055"}$| |$\text{"Lanthanum"}$|$\text{"La"}$|$57$|$\text{"138.9055"}$|
|$\text{"Lawrencium"}$|$\text{"Lr"}$|$103$|$\text{"262.11"}$| |$\text{"Lawrencium"}$|$\text{"Lr"}$|$103$|$\text{"262.11"}$|
|$\text{"Lead"}$|$\text{"Pb"}$|$82$|$\text{"207.2"}$| |$\text{"Lead"}$|$\text{"Pb"}$|$82$|$\text{"207.2"}$|
|$\text{"Lithium"}$|$\text{"Li"}$|$3$|$\text{"6.941"}$| |$\text{"Lithium"}$|$\text{"Li"}$|$3$|$\text{"6.941"}$|
|$\text{"Lutetium"}$|$\text{"Lu"}$|$71$|$\text{"174.967"}$| |$\text{"Lutetium"}$|$\text{"Lu"}$|$71$|$\text{"174.967"}$|
|$\text{"Magnesium"}$|$\text{"Mg"}$|$12$|$\text{"24.305"}$| |$\text{"Magnesium"}$|$\text{"Mg"}$|$12$|$\text{"24.305"}$|
|$\text{"Manganese"}$|$\text{"Mn"}$|$25$|$\text{"54.93805"}$| |$\text{"Manganese"}$|$\text{"Mn"}$|$25$|$\text{"54.93805"}$|
|$\text{"Meitnerium"}$|$\text{"Mt"}$|$109$|$\text{"[268]"}$| |$\text{"Meitnerium"}$|$\text{"Mt"}$|$109$|$\text{"[268]"}$|
|$\text{"Mendelevium"}$|$\text{"Md"}$|$101$|$\text{"258.1"}$| |$\text{"Mendelevium"}$|$\text{"Md"}$|$101$|$\text{"258.1"}$|
|$\text{"Mercury"}$|$\text{"Hg"}$|$80$|$\text{"200.59"}$| |$\text{"Mercury"}$|$\text{"Hg"}$|$80$|$\text{"200.59"}$|
|$\text{"Molybdenum"}$|$\text{"Mo"}$|$42$|$\text{"95.94"}$| |$\text{"Molybdenum"}$|$\text{"Mo"}$|$42$|$\text{"95.94"}$|
|$\text{"Neodymium"}$|$\text{"Nd"}$|$60$|$\text{"144.24"}$| |$\text{"Neodymium"}$|$\text{"Nd"}$|$60$|$\text{"144.24"}$|
|$\text{"Neon"}$|$\text{"Ne"}$|$10$|$\text{"20.1797"}$| |$\text{"Neon"}$|$\text{"Ne"}$|$10$|$\text{"20.1797"}$|
|$\text{"Neptunium"}$|$\text{"Np"}$|$93$|$\text{"237.048"}$| |$\text{"Neptunium"}$|$\text{"Np"}$|$93$|$\text{"237.048"}$|
|$\text{"Nickel"}$|$\text{"Ni"}$|$28$|$\text{"58.6934"}$| |$\text{"Nickel"}$|$\text{"Ni"}$|$28$|$\text{"58.6934"}$|
|$\text{"Niobium"}$|$\text{"Nb"}$|$41$|$\text{"92.90638"}$| |$\text{"Niobium"}$|$\text{"Nb"}$|$41$|$\text{"92.90638"}$|
|$\text{"Nitrogen"}$|$\text{"N"}$|$7$|$\text{"14.00674"}$| |$\text{"Nitrogen"}$|$\text{"N"}$|$7$|$\text{"14.00674"}$|
|$\text{"Nobelium"}$|$\text{"No"}$|$102$|$\text{"259.1009"}$| |$\text{"Nobelium"}$|$\text{"No"}$|$102$|$\text{"259.1009"}$|
|$\text{"Osmium"}$|$\text{"Os"}$|$76$|$\text{"190.23"}$| |$\text{"Osmium"}$|$\text{"Os"}$|$76$|$\text{"190.23"}$|
|$\text{"Oxygen"}$|$\text{"O"}$|$8$|$\text{"15.9994"}$| |$\text{"Oxygen"}$|$\text{"O"}$|$8$|$\text{"15.9994"}$|
|$\text{"Palladium"}$|$\text{"Pd"}$|$46$|$\text{"106.42"}$| |$\text{"Palladium"}$|$\text{"Pd"}$|$46$|$\text{"106.42"}$|
|$\text{"Phosphorus"}$|$\text{"P"}$|$15$|$\text{"30.973762"}$| |$\text{"Phosphorus"}$|$\text{"P"}$|$15$|$\text{"30.973762"}$|
|$\text{"Platinum"}$|$\text{"Pt"}$|$78$|$\text{"195.08"}$| |$\text{"Platinum"}$|$\text{"Pt"}$|$78$|$\text{"195.08"}$|
|$\text{"Plutonium"}$|$\text{"Pu"}$|$94$|$\text{"244.0642"}$| |$\text{"Plutonium"}$|$\text{"Pu"}$|$94$|$\text{"244.0642"}$|
|$\text{"Polonium"}$|$\text{"Po"}$|$84$|$\text{"208.9824"}$| |$\text{"Polonium"}$|$\text{"Po"}$|$84$|$\text{"208.9824"}$|
|$\text{"Potassium"}$|$\text{"K"}$|$19$|$\text{"39.0983"}$| |$\text{"Potassium"}$|$\text{"K"}$|$19$|$\text{"39.0983"}$|
|$\text{"Praseodymium"}$|$\text{"Pr"}$|$59$|$\text{"140.90765"}$| |$\text{"Praseodymium"}$|$\text{"Pr"}$|$59$|$\text{"140.90765"}$|
|$\text{"Promethium"}$|$\text{"Pm"}$|$61$|$\text{"144.9127"}$| |$\text{"Promethium"}$|$\text{"Pm"}$|$61$|$\text{"144.9127"}$|
|$\text{"Protactinium"}$|$\text{"Pa"}$|$91$|$\text{"231.03588"}$| |$\text{"Protactinium"}$|$\text{"Pa"}$|$91$|$\text{"231.03588"}$|
|$\text{"Radium"}$|$\text{"Ra"}$|$88$|$\text{"226.0254"}$| |$\text{"Radium"}$|$\text{"Ra"}$|$88$|$\text{"226.0254"}$|
|$\text{"Radon"}$|$\text{"Rn"}$|$86$|$\text{"222.0176"}$| |$\text{"Radon"}$|$\text{"Rn"}$|$86$|$\text{"222.0176"}$|
|$\text{"Rhenium"}$|$\text{"Re"}$|$75$|$\text{"186.207"}$| |$\text{"Rhenium"}$|$\text{"Re"}$|$75$|$\text{"186.207"}$|
|$\text{"Rhodium"}$|$\text{"Rh"}$|$45$|$\text{"102.9055"}$| |$\text{"Rhodium"}$|$\text{"Rh"}$|$45$|$\text{"102.9055"}$|
|$\text{"Rubidium"}$|$\text{"Rb"}$|$37$|$\text{"85.4678"}$| |$\text{"Rubidium"}$|$\text{"Rb"}$|$37$|$\text{"85.4678"}$|
|$\text{"Ruthenium"}$|$\text{"Ru"}$|$44$|$\text{"101.07"}$| |$\text{"Ruthenium"}$|$\text{"Ru"}$|$44$|$\text{"101.07"}$|
|$\text{"Rutherfordium"}$|$\text{"Rf"}$|$104$|$\text{"[261]"}$| |$\text{"Rutherfordium"}$|$\text{"Rf"}$|$104$|$\text{"[261]"}$|
|$\text{"Samarium"}$|$\text{"Sm"}$|$62$|$\text{"150.36"}$| |$\text{"Samarium"}$|$\text{"Sm"}$|$62$|$\text{"150.36"}$|
|$\text{"Scandium"}$|$\text{"Sc"}$|$21$|$\text{"44.95591"}$| |$\text{"Scandium"}$|$\text{"Sc"}$|$21$|$\text{"44.95591"}$|
|$\text{"Seaborgium"}$|$\text{"Sg"}$|$106$|$\text{"[266]"}$| |$\text{"Seaborgium"}$|$\text{"Sg"}$|$106$|$\text{"[266]"}$|
|$\text{"Selenium"}$|$\text{"Se"}$|$34$|$\text{"78.96"}$| |$\text{"Selenium"}$|$\text{"Se"}$|$34$|$\text{"78.96"}$|
|$\text{"Silicon"}$|$\text{"Si"}$|$14$|$\text{"28.0855"}$| |$\text{"Silicon"}$|$\text{"Si"}$|$14$|$\text{"28.0855"}$|
|$\text{"Silver"}$|$\text{"Ag"}$|$47$|$\text{"107.8682"}$| |$\text{"Silver"}$|$\text{"Ag"}$|$47$|$\text{"107.8682"}$|
|$\text{"Sodium"}$|$\text{"Na"}$|$11$|$\text{"22.989768"}$| |$\text{"Sodium"}$|$\text{"Na"}$|$11$|$\text{"22.989768"}$|
|$\text{"Strontium"}$|$\text{"Sr"}$|$38$|$\text{"87.62"}$| |$\text{"Strontium"}$|$\text{"Sr"}$|$38$|$\text{"87.62"}$|
|$\text{"Sulfur"}$|$\text{"S"}$|$16$|$\text{"32.066"}$| |$\text{"Sulfur"}$|$\text{"S"}$|$16$|$\text{"32.066"}$|
|$\text{"Tantalum"}$|$\text{"Ta"}$|$73$|$\text{"180.9479"}$| |$\text{"Tantalum"}$|$\text{"Ta"}$|$73$|$\text{"180.9479"}$|
|$\text{"Technetium"}$|$\text{"Tc"}$|$43$|$\text{"97.9072"}$| |$\text{"Technetium"}$|$\text{"Tc"}$|$43$|$\text{"97.9072"}$|
|$\text{"Tellurium"}$|$\text{"Te"}$|$52$|$\text{"127.6"}$| |$\text{"Tellurium"}$|$\text{"Te"}$|$52$|$\text{"127.6"}$|
|$\text{"Terbium"}$|$\text{"Tb"}$|$65$|$\text{"158.92534"}$| |$\text{"Terbium"}$|$\text{"Tb"}$|$65$|$\text{"158.92534"}$|
|$\text{"Thallium"}$|$\text{"Tl"}$|$81$|$\text{"204.3833"}$| |$\text{"Thallium"}$|$\text{"Tl"}$|$81$|$\text{"204.3833"}$|
|$\text{"Thorium"}$|$\text{"Th"}$|$90$|$\text{"232.0381"}$| |$\text{"Thorium"}$|$\text{"Th"}$|$90$|$\text{"232.0381"}$|
|$\text{"Thulium"}$|$\text{"Tm"}$|$69$|$\text{"168.93421"}$| |$\text{"Thulium"}$|$\text{"Tm"}$|$69$|$\text{"168.93421"}$|
|$\text{"Tin"}$|$\text{"Sn"}$|$50$|$\text{"118.71"}$| |$\text{"Tin"}$|$\text{"Sn"}$|$50$|$\text{"118.71"}$|
|$\text{"Titanium"}$|$\text{"Ti"}$|$22$|$\text{"47.88"}$| |$\text{"Titanium"}$|$\text{"Ti"}$|$22$|$\text{"47.88"}$|
|$\text{"Tungsten"}$|$\text{"W"}$|$74$|$\text{"183.84"}$| |$\text{"Tungsten"}$|$\text{"W"}$|$74$|$\text{"183.84"}$|
|$\text{"Ununbium"}$|$\text{"Uub"}$|$112$|$\text{"[277]"}$| |$\text{"Ununbium"}$|$\text{"Uub"}$|$112$|$\text{"[277]"}$|
|$\text{"Ununhexium"}$|$\text{"Uuh"}$|$116$|$\text{"-"}$| |$\text{"Ununhexium"}$|$\text{"Uuh"}$|$116$|$\text{"-"}$|
|$\text{"Ununnilium"}$|$\text{"Uun"}$|$110$|$\text{"[269]"}$| |$\text{"Ununnilium"}$|$\text{"Uun"}$|$110$|$\text{"[269]"}$|
|$\text{"Ununoctium"}$|$\text{"Uuo"}$|$118$|$\text{"-"}$| |$\text{"Ununoctium"}$|$\text{"Uuo"}$|$118$|$\text{"-"}$|
|$\text{"Ununpentium"}$|$\text{"Uup"}$|$115$|$\text{"-"}$| |$\text{"Ununpentium"}$|$\text{"Uup"}$|$115$|$\text{"-"}$|
|$\text{"Ununquadium"}$|$\text{"Uuq"}$|$114$|$\text{"[289]"}$| |$\text{"Ununquadium"}$|$\text{"Uuq"}$|$114$|$\text{"[289]"}$|
|$\text{"Ununseptium"}$|$\text{"Uus"}$|$117$|$\text{"-"}$| |$\text{"Ununseptium"}$|$\text{"Uus"}$|$117$|$\text{"-"}$|
|$\text{"Ununtrium"}$|$\text{"Uut"}$|$113$|$\text{"-"}$| |$\text{"Ununtrium"}$|$\text{"Uut"}$|$113$|$\text{"-"}$|
|$\text{"Unununium"}$|$\text{"Uuu"}$|$111$|$\text{"[272]"}$| |$\text{"Unununium"}$|$\text{"Uuu"}$|$111$|$\text{"[272]"}$|
|$\text{"Uranium"}$|$\text{"U"}$|$92$|$\text{"238.0289"}$| |$\text{"Uranium"}$|$\text{"U"}$|$92$|$\text{"238.0289"}$|
|$\text{"Vanadium"}$|$\text{"V"}$|$23$|$\text{"50.9415"}$| |$\text{"Vanadium"}$|$\text{"V"}$|$23$|$\text{"50.9415"}$|
|$\text{"Xenon"}$|$\text{"Xe"}$|$54$|$\text{"131.29"}$| |$\text{"Xenon"}$|$\text{"Xe"}$|$54$|$\text{"131.29"}$|
|$\text{"Ytterbium"}$|$\text{"Yb"}$|$70$|$\text{"173.04"}$| |$\text{"Ytterbium"}$|$\text{"Yb"}$|$70$|$\text{"173.04"}$|
|$\text{"Yttrium"}$|$\text{"Y"}$|$39$|$\text{"88.90585"}$| |$\text{"Yttrium"}$|$\text{"Y"}$|$39$|$\text{"88.90585"}$|
|$\text{"Zinc"}$|$\text{"Zn"}$|$30$|$\text{"65.39"}$| |$\text{"Zinc"}$|$\text{"Zn"}$|$30$|$\text{"65.39"}$|
|$\text{"Zirconium"}$|$\text{"Zr"}$|$40$|$\text{"91.224"}$| |$\text{"Zirconium"}$|$\text{"Zr"}$|$40$|$\text{"91.224"}$|
prj111 prj112 prj12 prj2 prj111 prj112 prj12 prj2
"Actinium" "Ac" 89 "227.0278" "Actinium" "Ac" 89 "227.0278"
"Aluminum" "Al" 13 "26.981539" "Aluminum" "Al" 13 "26.981539"
"Americium" "Am" 95 "243.0614" "Americium" "Am" 95 "243.0614"
"Antimony" "Sb" 51 "121.76" "Antimony" "Sb" 51 "121.76"
"Argon" "Ar" 18 "39.948" "Argon" "Ar" 18 "39.948"
"Arsenic" "As" 33 "74.92159" "Arsenic" "As" 33 "74.92159"
"Astatine" "At" 85 "209.9871" "Astatine" "At" 85 "209.9871"
"Barium" "Ba" 56 "137.327" "Barium" "Ba" 56 "137.327"
"Berkelium" "Bk" 97 "247.0703" "Berkelium" "Bk" 97 "247.0703"
"Beryllium" "Be" 4 "9.01218" "Beryllium" "Be" 4 "9.01218"
"Bismuth" "Bi" 83 "208.98037" "Bismuth" "Bi" 83 "208.98037"
"Bohrium" "Bh" 107 "[264]" "Bohrium" "Bh" 107 "[264]"
"Boron" "B" 5 "10.811" "Boron" "B" 5 "10.811"
"Bromine" "Br" 35 "79.904" "Bromine" "Br" 35 "79.904"
"Cadmium" "Cd" 48 "112.411" "Cadmium" "Cd" 48 "112.411"
"Calcium" "Ca" 20 "40.078" "Calcium" "Ca" 20 "40.078"
"Californium" "Cf" 98 "251.0796" "Californium" "Cf" 98 "251.0796"
"Carbon" "C" 6 "12.011" "Carbon" "C" 6 "12.011"
"Cerium" "Ce" 58 "140.115" "Cerium" "Ce" 58 "140.115"
"Cesium" "Cs" 55 "132.90543" "Cesium" "Cs" 55 "132.90543"
"Chlorine" "Cl" 17 "35.4527" "Chlorine" "Cl" 17 "35.4527"
"Chromium" "Cr" 24 "51.9961" "Chromium" "Cr" 24 "51.9961"
"Cobalt" "Co" 27 "58.9332" "Cobalt" "Co" 27 "58.9332"
"Copper" "Cu" 29 "63.546" "Copper" "Cu" 29 "63.546"
"Curium" "Cm" 96 "247.0703" "Curium" "Cm" 96 "247.0703"
"Dubnium" "Db" 105 "[262]" "Dubnium" "Db" 105 "[262]"
"Dysprosium" "Dy" 66 "162.5" "Dysprosium" "Dy" 66 "162.5"
"Einsteinium" "Es" 99 "252.083" "Einsteinium" "Es" 99 "252.083"
"Erbium" "Er" 68 "167.26" "Erbium" "Er" 68 "167.26"
"Europium" "Eu" 63 "151.965" "Europium" "Eu" 63 "151.965"
"Fermium" "Fm" 100 "257.0951" "Fermium" "Fm" 100 "257.0951"
"Fluorine" "F" 9 "18.998403" "Fluorine" "F" 9 "18.998403"
"Francium" "Fr" 87 "223.0197" "Francium" "Fr" 87 "223.0197"
"Gadolinium" "Gd" 64 "157.25" "Gadolinium" "Gd" 64 "157.25"
"Gallium" "Ga" 31 "69.723" "Gallium" "Ga" 31 "69.723"
"Germanium" "Ge" 32 "72.61" "Germanium" "Ge" 32 "72.61"
"Gold" "Au" 79 "196.96654" "Gold" "Au" 79 "196.96654"
"Hafnium" "Hf" 72 "178.49" "Hafnium" "Hf" 72 "178.49"
"Hassium" "Hs" 108 "[269]" "Hassium" "Hs" 108 "[269]"
"Helium" "He" 2 "4.002602" "Helium" "He" 2 "4.002602"
"Holmium" "Ho" 67 "164.93032" "Holmium" "Ho" 67 "164.93032"
"Hydrogen" "H" 1 "1.00794" "Hydrogen" "H" 1 "1.00794"
"Indium" "In" 49 "114.818" "Indium" "In" 49 "114.818"
"Iodine" "I" 53 "126.90447" "Iodine" "I" 53 "126.90447"
"Iridium" "Ir" 77 "192.22" "Iridium" "Ir" 77 "192.22"
"Iron" "Fe" 26 "55.847" "Iron" "Fe" 26 "55.847"
"Krypton" "Kr" 36 "83.8" "Krypton" "Kr" 36 "83.8"
"Lanthanum" "La" 57 "138.9055" "Lanthanum" "La" 57 "138.9055"
"Lawrencium" "Lr" 103 "262.11" "Lawrencium" "Lr" 103 "262.11"
"Lead" "Pb" 82 "207.2" "Lead" "Pb" 82 "207.2"
"Lithium" "Li" 3 "6.941" "Lithium" "Li" 3 "6.941"
"Lutetium" "Lu" 71 "174.967" "Lutetium" "Lu" 71 "174.967"
"Magnesium" "Mg" 12 "24.305" "Magnesium" "Mg" 12 "24.305"
"Manganese" "Mn" 25 "54.93805" "Manganese" "Mn" 25 "54.93805"
"Meitnerium" "Mt" 109 "[268]" "Meitnerium" "Mt" 109 "[268]"
"Mendelevium" "Md" 101 "258.1" "Mendelevium" "Md" 101 "258.1"
"Mercury" "Hg" 80 "200.59" "Mercury" "Hg" 80 "200.59"
"Molybdenum" "Mo" 42 "95.94" "Molybdenum" "Mo" 42 "95.94"
"Neodymium" "Nd" 60 "144.24" "Neodymium" "Nd" 60 "144.24"
"Neon" "Ne" 10 "20.1797" "Neon" "Ne" 10 "20.1797"
"Neptunium" "Np" 93 "237.048" "Neptunium" "Np" 93 "237.048"
"Nickel" "Ni" 28 "58.6934" "Nickel" "Ni" 28 "58.6934"
"Niobium" "Nb" 41 "92.90638" "Niobium" "Nb" 41 "92.90638"
"Nitrogen" "N" 7 "14.00674" "Nitrogen" "N" 7 "14.00674"
"Nobelium" "No" 102 "259.1009" "Nobelium" "No" 102 "259.1009"
"Osmium" "Os" 76 "190.23" "Osmium" "Os" 76 "190.23"
"Oxygen" "O" 8 "15.9994" "Oxygen" "O" 8 "15.9994"
"Palladium" "Pd" 46 "106.42" "Palladium" "Pd" 46 "106.42"
"Phosphorus" "P" 15 "30.973762" "Phosphorus" "P" 15 "30.973762"
"Platinum" "Pt" 78 "195.08" "Platinum" "Pt" 78 "195.08"
"Plutonium" "Pu" 94 "244.0642" "Plutonium" "Pu" 94 "244.0642"
"Polonium" "Po" 84 "208.9824" "Polonium" "Po" 84 "208.9824"
"Potassium" "K" 19 "39.0983" "Potassium" "K" 19 "39.0983"
"Praseodymium" "Pr" 59 "140.90765" "Praseodymium" "Pr" 59 "140.90765"
"Promethium" "Pm" 61 "144.9127" "Promethium" "Pm" 61 "144.9127"
"Protactinium" "Pa" 91 "231.03588" "Protactinium" "Pa" 91 "231.03588"
"Radium" "Ra" 88 "226.0254" "Radium" "Ra" 88 "226.0254"
"Radon" "Rn" 86 "222.0176" "Radon" "Rn" 86 "222.0176"
"Rhenium" "Re" 75 "186.207" "Rhenium" "Re" 75 "186.207"
"Rhodium" "Rh" 45 "102.9055" "Rhodium" "Rh" 45 "102.9055"
"Rubidium" "Rb" 37 "85.4678" "Rubidium" "Rb" 37 "85.4678"
"Ruthenium" "Ru" 44 "101.07" "Ruthenium" "Ru" 44 "101.07"
"Rutherfordium" "Rf" 104 "[261]" "Rutherfordium" "Rf" 104 "[261]"
"Samarium" "Sm" 62 "150.36" "Samarium" "Sm" 62 "150.36"
"Scandium" "Sc" 21 "44.95591" "Scandium" "Sc" 21 "44.95591"
"Seaborgium" "Sg" 106 "[266]" "Seaborgium" "Sg" 106 "[266]"
"Selenium" "Se" 34 "78.96" "Selenium" "Se" 34 "78.96"
"Silicon" "Si" 14 "28.0855" "Silicon" "Si" 14 "28.0855"
"Silver" "Ag" 47 "107.8682" "Silver" "Ag" 47 "107.8682"
"Sodium" "Na" 11 "22.989768" "Sodium" "Na" 11 "22.989768"
"Strontium" "Sr" 38 "87.62" "Strontium" "Sr" 38 "87.62"
"Sulfur" "S" 16 "32.066" "Sulfur" "S" 16 "32.066"
"Tantalum" "Ta" 73 "180.9479" "Tantalum" "Ta" 73 "180.9479"
"Technetium" "Tc" 43 "97.9072" "Technetium" "Tc" 43 "97.9072"
"Tellurium" "Te" 52 "127.6" "Tellurium" "Te" 52 "127.6"
"Terbium" "Tb" 65 "158.92534" "Terbium" "Tb" 65 "158.92534"
"Thallium" "Tl" 81 "204.3833" "Thallium" "Tl" 81 "204.3833"
"Thorium" "Th" 90 "232.0381" "Thorium" "Th" 90 "232.0381"
"Thulium" "Tm" 69 "168.93421" "Thulium" "Tm" 69 "168.93421"
"Tin" "Sn" 50 "118.71" "Tin" "Sn" 50 "118.71"
"Titanium" "Ti" 22 "47.88" "Titanium" "Ti" 22 "47.88"
"Tungsten" "W" 74 "183.84" "Tungsten" "W" 74 "183.84"
"Ununbium" "Uub" 112 "[277]" "Ununbium" "Uub" 112 "[277]"
"Ununhexium" "Uuh" 116 "-" "Ununhexium" "Uuh" 116 "-"
"Ununnilium" "Uun" 110 "[269]" "Ununnilium" "Uun" 110 "[269]"
"Ununoctium" "Uuo" 118 "-" "Ununoctium" "Uuo" 118 "-"
"Ununpentium" "Uup" 115 "-" "Ununpentium" "Uup" 115 "-"
"Ununquadium" "Uuq" 114 "[289]" "Ununquadium" "Uuq" 114 "[289]"
"Ununseptium" "Uus" 117 "-" "Ununseptium" "Uus" 117 "-"
"Ununtrium" "Uut" 113 "-" "Ununtrium" "Uut" 113 "-"
"Unununium" "Uuu" 111 "[272]" "Unununium" "Uuu" 111 "[272]"
"Uranium" "U" 92 "238.0289" "Uranium" "U" 92 "238.0289"
"Vanadium" "V" 23 "50.9415" "Vanadium" "V" 23 "50.9415"
"Xenon" "Xe" 54 "131.29" "Xenon" "Xe" 54 "131.29"
"Ytterbium" "Yb" 70 "173.04" "Ytterbium" "Yb" 70 "173.04"
"Yttrium" "Y" 39 "88.90585" "Yttrium" "Y" 39 "88.90585"
"Zinc" "Zn" 30 "65.39" "Zinc" "Zn" 30 "65.39"
"Zirconium" "Zr" 40 "91.224" "Zirconium" "Zr" 40 "91.224"
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
We now check the following property, that the atomic weights are not decreasing with increasing atomic number: We now check the following property, that the atomic weights are not decreasing with increasing atomic number:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:assert !(n1,n2,s1,s2,nr,aw1,aw2).( :assert !(n1,n2,s1,s2,nr,aw1,aw2).(
(n1,s1,nr,aw1):eltable & (n2,s2,nr+1,aw2):eltable (n1,s1,nr,aw1):eltable & (n2,s2,nr+1,aw2):eltable
=> =>
DEC_STRING_TO_INT(aw1,3) <= DEC_STRING_TO_INT(aw2,3) DEC_STRING_TO_INT(aw1,3) <= DEC_STRING_TO_INT(aw2,3)
) )
``` ```
%% Output %% Output
:assert: Assertion is not true: FALSE :assert: Assertion is not true: FALSE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
In case the property is false, we can extract a table with the counter examples to the rule: In case the property is false, we can extract a table with the counter examples to the rule:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table {n1,aw1,n2,aw2|#(s1,s2,nr).( :table {n1,aw1,n2,aw2|#(s1,s2,nr).(
(n1,s1,nr,aw1):eltable & STRING_IS_NUMBER(aw1) & (n1,s1,nr,aw1):eltable & STRING_IS_NUMBER(aw1) &
(n2,s2,nr+1,aw2):eltable & STRING_IS_NUMBER(aw2) & (n2,s2,nr+1,aw2):eltable & STRING_IS_NUMBER(aw2) &
DEC_STRING_TO_INT(aw1,3) > DEC_STRING_TO_INT(aw2,3))} DEC_STRING_TO_INT(aw1,3) > DEC_STRING_TO_INT(aw2,3))}
``` ```
%% Output %% Output
|n1|aw1|n2|aw2| |n1|aw1|n2|aw2|
|---|---|---|---| |---|---|---|---|
|$\text{"Argon"}$|$\text{"39.948"}$|$\text{"Potassium"}$|$\text{"39.0983"}$| |$\text{"Argon"}$|$\text{"39.948"}$|$\text{"Potassium"}$|$\text{"39.0983"}$|
|$\text{"Cobalt"}$|$\text{"58.9332"}$|$\text{"Nickel"}$|$\text{"58.6934"}$| |$\text{"Cobalt"}$|$\text{"58.9332"}$|$\text{"Nickel"}$|$\text{"58.6934"}$|
|$\text{"Plutonium"}$|$\text{"244.0642"}$|$\text{"Americium"}$|$\text{"243.0614"}$| |$\text{"Plutonium"}$|$\text{"244.0642"}$|$\text{"Americium"}$|$\text{"243.0614"}$|
|$\text{"Tellurium"}$|$\text{"127.6"}$|$\text{"Iodine"}$|$\text{"126.90447"}$| |$\text{"Tellurium"}$|$\text{"127.6"}$|$\text{"Iodine"}$|$\text{"126.90447"}$|
|$\text{"Thorium"}$|$\text{"232.0381"}$|$\text{"Protactinium"}$|$\text{"231.03588"}$| |$\text{"Thorium"}$|$\text{"232.0381"}$|$\text{"Protactinium"}$|$\text{"231.03588"}$|
|$\text{"Uranium"}$|$\text{"238.0289"}$|$\text{"Neptunium"}$|$\text{"237.048"}$| |$\text{"Uranium"}$|$\text{"238.0289"}$|$\text{"Neptunium"}$|$\text{"237.048"}$|
n1 aw1 n2 aw2 n1 aw1 n2 aw2
"Argon" "39.948" "Potassium" "39.0983" "Argon" "39.948" "Potassium" "39.0983"
"Cobalt" "58.9332" "Nickel" "58.6934" "Cobalt" "58.9332" "Nickel" "58.6934"
"Plutonium" "244.0642" "Americium" "243.0614" "Plutonium" "244.0642" "Americium" "243.0614"
"Tellurium" "127.6" "Iodine" "126.90447" "Tellurium" "127.6" "Iodine" "126.90447"
"Thorium" "232.0381" "Protactinium" "231.03588" "Thorium" "232.0381" "Protactinium" "231.03588"
"Uranium" "238.0289" "Neptunium" "237.048" "Uranium" "238.0289" "Neptunium" "237.048"
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Anwendung: Modelldokumentation, Beschreibung von Szenarien, Tests # Anwendung: Modelldokumentation, Beschreibung von Szenarien, Tests
Die ProB-Jupyter Kernel kann auch zur Erstellung von Dokumentation von B Modellen Die ProB-Jupyter Kernel kann auch zur Erstellung von Dokumentation von B Modellen
benutzt werden: benutzt werden:
- Beschreibung der Datenstrukturen und wie das Modell benutzt werden kann - Beschreibung der Datenstrukturen und wie das Modell benutzt werden kann
- Beschreibung von gewünschten oder unerwünschten Szenarien - Beschreibung von gewünschten oder unerwünschten Szenarien
### Beispiel: problematisches Szenario im AMASS Projekt: ### Beispiel: problematisches Szenario im AMASS Projekt:
![AMASS](./img/AMASS_screenshot.png) ![AMASS](./img/AMASS_screenshot.png)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Future Work # Future Work
* Mehr Kommandos: * Mehr Kommandos:
* Temporäre ("lokale") Variablen mit `:let` * Temporäre ("lokale") Variablen mit `:let`
* Verifikation (LTL, Model Checking) * Verifikation (LTL, Model Checking)
* Diagramme: Plotten von Werten im Verlauf des Traces * Diagramme: Plotten von Werten im Verlauf des Traces
* `In`/`Out`-Arrays um vorherige Eingaben/Ergebnisse abzurufen * `In`/`Out`-Arrays um vorherige Eingaben/Ergebnisse abzurufen
* Integration mit ProB 2-Trace-Dateien * Integration mit ProB 2-Trace-Dateien
* Konvertierung zwischen `.prob2trace` und `.ipynb` * Konvertierung zwischen `.prob2trace` und `.ipynb`
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Zusammenfassung # Zusammenfassung
* die B Sprache ist relativ nahe an der Mathematik die man in der Lehre der Informatik verwendet * die B Sprache ist relativ nahe an der Mathematik die man in der Lehre der Informatik verwendet
* die B Sprache erlaubt funktionale Programmierung, Constraint-Programmierung, logisches Schließen und Beweisen * die B Sprache erlaubt funktionale Programmierung, Constraint-Programmierung, logisches Schließen und Beweisen
* mit ProB kann man B (und TLA+ und Z) animieren, auswerten, grafisch darstellen * mit ProB kann man B (und TLA+ und Z) animieren, auswerten, grafisch darstellen
* mit dem neuen Jupyter Kernel kann man interaktive, ausführbare Dokumente erstellen. * mit dem neuen Jupyter Kernel kann man interaktive, ausführbare Dokumente erstellen.
* die Anwendungen sind hoffentlich vielfältig * die Anwendungen sind hoffentlich vielfältig
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
``` ```
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment