Beide Tore der Schleuse offen
Eine Invariante ist eine Aussage, die in jedem Zustand eines Systems wahr sein muss. TLA+ ist eine Sprache, in der man ein System aus Zuständen und Schritten beschreibt, und TLC ist das Programm, das alle Zustände durchprobiert.
Eine Schiffsschleuse hat ein Außentor und ein Innentor. Beide zugleich zu öffnen, lässt das Wasser durchlaufen. TLC findet den kürzesten Weg dorthin.
Am Ende dieser Lektion
Notiz
Ich kann eine Invariante schreiben und das Gegenbeispiel von TLC lesen.
Schlüsselwörter
| Begriff | Was er bedeutet | Beispiel |
|---|---|---|
| Zustand | die Werte aller Variablen zu einem Zeitpunkt | |
| Schritt | ein Übergang von einem Zustand zum nächsten | |
| Invariante | eine Aussage, die in jedem Zustand wahr ist | ~(aussen /\ innen) |
| TLA+ | eine Sprache, um Systeme aus Zuständen und Schritten zu beschreiben | |
| TLC | das Programm, das alle Zustände eines TLA+-Modells prüft | |
| Gegenbeispiel | der Weg von Zustand zu Zustand bis zur verletzten Invariante |
Die Zellen, die Lernende ausfüllen, bleiben in dieser Vorschau leer.
Ein System ist eine Folge von Zuständen
Die Schleuse hat zwei Variablen: aussen und innen, jede wahr, wenn das Tor offen ist. Ein Zustand gibt beiden einen Wert. Am Anfang sind beide Tore zu.
Ein Schritt ändert den Zustand: ein Tor öffnen oder beide schließen. Eine Invariante verbietet Zustände. Hier lautet sie: nie beide Tore offen.
Das Modell der Schleuse in TLA+
---- MODULE Schleuse ----
VARIABLES aussen, innen
vars == <<aussen, innen>>
Init == aussen = FALSE /\ innen = FALSE
OeffneAussen == aussen = FALSE /\ aussen' = TRUE /\ UNCHANGED innen
OeffneInnen == innen = FALSE /\ innen' = TRUE /\ UNCHANGED aussen
Schliesse == (aussen \/ innen) /\ aussen' = FALSE /\ innen' = FALSE
Next == OeffneAussen \/ OeffneInnen \/ Schliesse
Spec == Init /\ [][Next]_vars
NieBeide == ~(aussen /\ innen)
AussenImmerZu == ~aussen
====
So ändert sich der Zustand bei jedem Schritt
| Schritt | Wirkung | aussen danach | innen danach |
|---|---|---|---|
| Start | beide Tore zu | FALSE | FALSE |
| OeffneAussen | Außentor auf | TRUE | unverändert |
| OeffneInnen | Innentor auf | unverändert | TRUE |
| Schliesse | beide Tore zu | FALSE | FALSE |
Die Zellen, die Lernende ausfüllen, bleiben in dieser Vorschau leer.
Das Modell schreiben und von TLC prüfen lassen
Die Datei braucht zwei Teile: das Modell Schleuse.tla und die Einstellungen Schleuse.cfg. Darin steht, welche Aussage TLC prüfen soll.
Die zwei ersten Befehle schreiben das Modell, der dritte die Einstellungen. Der vierte lässt TLC alle Zustände prüfen und zeigt nur die Zeilen mit dem Ergebnis und den Zuständen.
Einen Ordner anlegen
mkdir -p ~/schleuseHier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Den Anfang des Modells schreiben
printf '%s\n' "---- MODULE Schleuse ----" "VARIABLES aussen, innen" "vars == <<aussen, innen>>" "Init == aussen = FALSE /\ innen = FALSE" > ~/schleuse/Schleuse.tlaHier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Die Schritte und Invarianten anhängen
printf '%s\n' "OeffneAussen == aussen = FALSE /\ aussen' = TRUE /\ UNCHANGED innen" "OeffneInnen == innen = FALSE /\ innen' = TRUE /\ UNCHANGED aussen" "Schliesse == (aussen \/ innen) /\ aussen' = FALSE /\ innen' = FALSE" "Next == OeffneAussen \/ OeffneInnen \/ Schliesse" "Spec == Init /\ [][Next]_vars" "NieBeide == ~(aussen /\ innen)" "AussenImmerZu == ~aussen" "====" >> ~/schleuse/Schleuse.tlaHier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Die Einstellungen für zwei Modelle schreiben
printf '%s\n' "SPECIFICATION Spec" "INVARIANT NieBeide" | tee ~/schleuse/Schleuse.cfg > ~/schleuse/Schleuse2.cfgHier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Hält die Invariante NieBeide?
tlc ~/schleuse/Schleuse | grep -E "violated|^State"Hier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Das Gegenbeispiel ist der kürzeste Weg zum Fehler
TLC meldet, dass NieBeide verletzt ist, und nennt drei Zustände: den Start, das Öffnen des Außentors und das Öffnen des Innentors. Dahinter stehen Zeile und Spalte des Schritts in Ihrer Datei.
TLC sucht Zustand für Zustand, erst alle mit einem Schritt, dann mit zwei. Das erste Gegenbeispiel ist darum das kürzeste.
Ein häufiger Fehler
Warnung
Viele denken: Eine Invariante, die TLC nicht verletzt findet, beweist, dass das System sicher ist. Das stimmt nur für die Aussage, die dasteht. Die Invariante TRUE ist immer wahr und sagt nichts. Schreiben Sie die Aussage, die wirklich gelten soll.
Eine Reparatur ist eine zusätzliche Bedingung
Die Tore dürfen sich nur öffnen, wenn das andere Tor zu ist. Dafür bekommt jeder Öffnungsschritt eine Bedingung dazu. Der Befehl macht mit sed aus dem Modell ein zweites, Schleuse2, mit diesen beiden Bedingungen.
Danach prüft TLC dieselbe Invariante. Diesmal findet es keinen Fehler.
Das reparierte Modell schreiben
sed -e 's/Schleuse ----/Schleuse2 ----/' -e 's/^OeffneAussen == aussen = FALSE/& \/\\ innen = FALSE/' -e 's/^OeffneInnen == innen = FALSE/& \/\\ aussen = FALSE/' ~/schleuse/Schleuse.tla > ~/schleuse/Schleuse2.tlaHier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Hält NieBeide im reparierten Modell?
tlc ~/schleuse/Schleuse2 | grep -E "No error|violated|^State"Hier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Auch ein richtiges System verletzt manche Invariante
Die zweite Invariante, AussenImmerZu, behauptet, das Außentor sei nie offen. Das ist für eine Schleuse Unsinn, denn sie muss sich öffnen können.
TLC prüft sie trotzdem, wenn Sie ihren Namen hinter den Modellnamen schreiben. Das Gegenbeispiel zeigt dann: Das Tor lässt sich öffnen. Das beweist, dass die Schleuse nicht erstarrt ist.
Prüfen, ob das Außentor nie offen ist
tlc ~/schleuse/Schleuse2 AussenImmerZu | grep -E "No error|violated|^State"Hier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.