Wie man eine Katze mit TLA + fängt

Viele Programmierer haben Schwierigkeiten, formale Methoden zu verwenden, um Probleme in ihren Programmen zu lösen, da diese Methoden zwar effektiv, aber unangemessen komplex sein können. Um zu verstehen, warum dies geschieht, verwenden wir die Modellprüfmethode , um ein relativ einfaches Rätsel zu lösen:

Bedingungen

Sie befinden sich in einem Flur mit sieben Türen auf einer Seite, die zu sieben Räumen führen. In einem dieser Räume versteckt sich eine Katze. Ihre Aufgabe ist es, die Katze zu fangen. Das Öffnen einer Tür dauert einen Schritt. Wenn Sie die richtige Tür erraten, fangen Sie die Katze. Wenn Sie die richtige Tür nicht erraten, rennt die Katze zum nächsten Raum.

TLA + und zeitliche Logik

Einige Tools können solche Probleme lösen. Beispielsweise verwenden SMT-Löser , die in diesen Fällen häufig verwendet werden, Prädikatenlogik, um das Problem zu lösen. Dies erfordert jedoch die Verwendung eines Arrays, was für Programmierer unpraktisch ist und häufig zu einer unnötig komplexen Abfolge von Aktionen führt. TLA + verwendet andererseits eine zeitliche Logik, die es einem Programm ermöglicht, den Status des Systems sowohl beim aktuellen als auch beim nächsten Schritt in einer Anweisung zu verwenden.

CatDistr' = CatDistr \ {n} 

Diese Bedingung besagt, dass nach der Überprüfung hinter Tür N die Anzahl der Türen, an denen sich die Katze befinden kann, mit der Anzahl der Räume übereinstimmt, aus denen N entnommen wurde. (Wenn die Katze hinter Tür N war, wurde sie natürlich gefasst.)

In einer imperativen Programmiersprache wird dadurch eine neue Variable erstellt, die aus der alten berechnet wird.

Über Sets

Die Position der Katze wird durch eine Variable innerhalb der Menge aller möglichen Räume bestimmt und nicht durch einen bestimmten Raum wie in einem Simulationsmodellierungssystem. Formale Programmiermethoden berücksichtigen die Vielzahl möglicher Werte anstelle des aktuellen Werts. Dies ist für Anfänger oft zu komplex. Eine Vereinfachung dieses Systems würde diesen Entwicklern helfen, schneller zu arbeiten.

Programmstruktur in TLA +

Das Programm besteht aus Deklarationen und Aussagen (Prädiktoren), die beschreiben:

• Der Ausgangszustand
• Die Verbindung zwischen tatsächlichen Zuständen
• Der nächste Zustand
• Eine Invariante, die in allen verfügbaren Zuständen ausgeführt wird.

Es können auch Hilfsprädikate (z. B. Parameter) beteiligt sein.

 ---- MODULE cat ------------------------------------------------------------- EXTENDS Integers CONSTANTS Doors VARIABLES CatDistr, LastDoor Init == /\ CatDistr = 0..Doors /\ LastDoor = -1 OpenDoor(n) == /\ CatDistr' = 0..Doors \intersect UNION { {x-1, x+1} : x \in CatDistr \ {n} } /\ LastDoor' = n Next == \E door \in 0..Doors : OpenDoor(door) CatWalk == CatDistr /= {} ============================================================================= 

In diesem Beispiel:

• In der ersten und letzten Zeile wird angegeben, dass dies ein Quellmodul ist.
• == bedeutet "per Definition gleichermaßen".
• = bedeutet, dass die berechneten Ausdruckswerte gleich sind
• Doors ist eine Konstante, die in der Konfigurationsdatei festgelegt ist.
• CatDistr bestimmt den Raum, in dem sich die Katze befindet.
• Die LastDoor- Variable, die den zuletzt überprüften Raum darstellt, liest bequem die Ausgabe des Programms. Bei großen Modellen können solche Variablen den Programmworkflow verlangsamen und die Anzahl der zu analysierenden Zustände erhöhen. In diesem Modell enthält der Staat jedoch jetzt die Geschichte, welche Türen geöffnet wurden. Somit sind gleiche Zustände, die auf unterschiedliche Weise erzeugt wurden, jetzt unterschiedlich.
• Der Init- Prädiktor beschreibt den Anfangszustand des Programms - in diesem Fall wurden noch keine Türen geöffnet.
• OpenDoor (n) beschreibt, was passiert, wenn Tür n geöffnet wird - entweder Sie haben die Katze gefangen oder Sie haben es nicht getan.
• Der Next- Prädiktor existiert, weil TLA + nicht weiß, in welchen Raum wir als nächstes eintreten könnten. Daher wird geprüft, ob die Invarianten jeweils korrekt sind.
  
  Hier ist eine klarere Variante:
  
  

   Next == OpenDoor(0) \/ OpenDoor(1) \/ ... \/ OpenDoor(Doors) 

  
  In diesem Fall arbeitet der Code mit einer festen Anzahl von Räumen, wodurch der Code parametrisiert wird.
• Schließlich bestimmt die CatWalk- Invariante, wo sich die Katze versteckt. Eine unveränderliche Verletzung bedeutet, dass die Katze überall dort gefangen wurde, wo sie sich versteckte. Bei der Überprüfung einer Spezifikation ist ein unveränderlicher Verstoß ein Fehler. Da wir das Tool jedoch nicht für den vorgesehenen Zweck verwenden, bedeutet das Erhalten eines Fehlers in diesem Fall die Lösung des Problems.

Modellkonfiguration

 CONSTANTS Doors = 6 INIT Init NEXT Next INVARIANT CatWalk 

Diese Konfiguration umfasst den Anfangszustand, die Anzahl der Räume, die Bedingungen für eine Zustandsänderung und einen überprüfbaren Test.

Sie können dieses Modell mit diesem Befehl über die Befehlszeile ausführen:
tlc2 -config cat.cfg cat.tla .

TLA + verfügt über eine erweiterte Benutzeroberfläche und wird mit dem Befehl tla-toolbox gestartet. Leider versteht es keine .cfg- Dateien, daher müssen die Modellparameter über das Menü konfiguriert werden.

Fazit

Das Erstellen dieses speziellen Programms war ziemlich einfach, aber in vielen Fällen erfordert die Anwendung formaler Methoden viel größere Modelle und die Verwendung verschiedener Sprachkonstruktionen. Wir hoffen, dass das Lösen einfacherer Rätsel wie dieses eine einfache und interessante Möglichkeit bietet, formale Methoden für die Arbeitsprojekte anzuwenden.

• Ein einfaches Programm zur interaktiven Lösungsüberprüfung finden Sie hier .
• Erfahren Sie hier mehr über TLA +.