löse lightbot.de mit ProB und event-B
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
jochen@homeland e654974401 die maschine simple in simple9 und dann zurück auf simple umbenennen, hat mir die verlorenen POs aus der scheinbar kaputtgeglaubten simple.bpo wiederhergezaubert. 2 years ago
notizen fertig 2 years ago
.project klappt, aber max events erreicht 2 years ago
README.md fertig 2 years ago
README.pdf fertig 2 years ago
ctx0.bcc für alle drei level wird eine korrekte lösung via theorem verletzung gezeigt. 2 years ago
ctx0.bpr erster umbauversuch, um den contexten und später systemen je level eine strucktur zu geben 2 years ago
ctx0.buc für alle drei level wird eine korrekte lösung via theorem verletzung gezeigt. 2 years ago
ctxGame.bcc für alle drei level wird eine korrekte lösung via theorem verletzung gezeigt. 2 years ago
ctxGame.bpr erster umbauversuch, um den contexten und später systemen je level eine strucktur zu geben 2 years ago
ctxGame.buc erster umbauversuch, um den contexten und später systemen je level eine strucktur zu geben 2 years ago
ctxLevel.bcc für alle drei level wird eine korrekte lösung via theorem verletzung gezeigt. 2 years ago
ctxLevel.bpr erster umbauversuch, um den contexten und später systemen je level eine strucktur zu geben 2 years ago
ctxLevel.buc erster umbauversuch, um den contexten und später systemen je level eine strucktur zu geben 2 years ago
level11.bcc für alle drei level wird eine korrekte lösung via theorem verletzung gezeigt. 2 years ago
level11.bpo Doku ist fast fertig 2 years ago
level11.bpr level sind erweiterung von ctx 2 years ago
level11.bps Doku ist fast fertig 2 years ago
level11.buc erster umbauversuch, um den contexten und später systemen je level eine strucktur zu geben 2 years ago
level21.bcc für alle drei level wird eine korrekte lösung via theorem verletzung gezeigt. 2 years ago
level21.bpo Doku ist fast fertig 2 years ago
level21.bpr nutze any um x und y beim zMove in nur einem UP ab zu bilden. Aufteilung der Level in untersch. contexte 2 years ago
level21.bps Doku ist fast fertig 2 years ago
level21.buc für alle drei level wird eine korrekte lösung via theorem verletzung gezeigt. 2 years ago
level31.bcc für alle drei level wird eine korrekte lösung via theorem verletzung gezeigt. 2 years ago
level31.bpo Doku ist fast fertig 2 years ago
level31.bpr nutze any um x und y beim zMove in nur einem UP ab zu bilden. Aufteilung der Level in untersch. contexte 2 years ago
level31.bps nutze any um x und y beim zMove in nur einem UP ab zu bilden. Aufteilung der Level in untersch. contexte 2 years ago
level31.buc für alle drei level wird eine korrekte lösung via theorem verletzung gezeigt. 2 years ago
simple.bcm sieht gut aus. withness bzw glue von modus und filling hat nicht so geklappt, wie ich wollte. 2 years ago
simple.bpo die maschine simple in simple9 und dann zurück auf simple umbenennen, hat mir die verlorenen POs aus der scheinbar kaputtgeglaubten simple.bpo wiederhergezaubert. 2 years ago
simple.bpr die maschine simple in simple9 und dann zurück auf simple umbenennen, hat mir die verlorenen POs aus der scheinbar kaputtgeglaubten simple.bpo wiederhergezaubert. 2 years ago
simple.bps die maschine simple in simple9 und dann zurück auf simple umbenennen, hat mir die verlorenen POs aus der scheinbar kaputtgeglaubten simple.bpo wiederhergezaubert. 2 years ago
simple.bum krampf 2 years ago
system.bcm sieht gut aus. withness bzw glue von modus und filling hat nicht so geklappt, wie ich wollte. 2 years ago
system.bpo die maschine simple in simple9 und dann zurück auf simple umbenennen, hat mir die verlorenen POs aus der scheinbar kaputtgeglaubten simple.bpo wiederhergezaubert. 2 years ago
system.bpr krampf 2 years ago
system.bps die maschine simple in simple9 und dann zurück auf simple umbenennen, hat mir die verlorenen POs aus der scheinbar kaputtgeglaubten simple.bpo wiederhergezaubert. 2 years ago
system.bum sieht gut aus. withness bzw glue von modus und filling hat nicht so geklappt, wie ich wollte. 2 years ago
systemL11.bcm sieht gut aus. withness bzw glue von modus und filling hat nicht so geklappt, wie ich wollte. 2 years ago
systemL11.bpo die maschine simple in simple9 und dann zurück auf simple umbenennen, hat mir die verlorenen POs aus der scheinbar kaputtgeglaubten simple.bpo wiederhergezaubert. 2 years ago
systemL11.bpr für alle drei level wird eine korrekte lösung via theorem verletzung gezeigt. 2 years ago
systemL11.bps für alle drei level wird eine korrekte lösung via theorem verletzung gezeigt. 2 years ago
systemL11.bum sieht gut aus. withness bzw glue von modus und filling hat nicht so geklappt, wie ich wollte. 2 years ago
systemL21.bcm sieht gut aus. withness bzw glue von modus und filling hat nicht so geklappt, wie ich wollte. 2 years ago
systemL21.bpo die maschine simple in simple9 und dann zurück auf simple umbenennen, hat mir die verlorenen POs aus der scheinbar kaputtgeglaubten simple.bpo wiederhergezaubert. 2 years ago
systemL21.bpr für alle drei level wird eine korrekte lösung via theorem verletzung gezeigt. 2 years ago
systemL21.bps für alle drei level wird eine korrekte lösung via theorem verletzung gezeigt. 2 years ago
systemL21.bum sieht gut aus. withness bzw glue von modus und filling hat nicht so geklappt, wie ich wollte. 2 years ago
systemL31.bcm sieht gut aus. withness bzw glue von modus und filling hat nicht so geklappt, wie ich wollte. 2 years ago
systemL31.bpo die maschine simple in simple9 und dann zurück auf simple umbenennen, hat mir die verlorenen POs aus der scheinbar kaputtgeglaubten simple.bpo wiederhergezaubert. 2 years ago
systemL31.bpr für alle drei level wird eine korrekte lösung via theorem verletzung gezeigt. 2 years ago
systemL31.bps für alle drei level wird eine korrekte lösung via theorem verletzung gezeigt. 2 years ago
systemL31.bum sieht gut aus. withness bzw glue von modus und filling hat nicht so geklappt, wie ich wollte. 2 years ago

README.md

Einleitung

Ziel des Projekts ist, das System des Spiels lightbot in ProB nach zu bilden. Die Idee ist, mit diesen System die Level des Spiels zu lösen, in dem man durch ein Model-Checking eine Invarianten- oder Theorem-Verletzung sucht, welche einer Lösung des Spiels entspricht. Die Events, die zu dieser Verletzung führen, geben einen möglichen, gültigen Lösungsweg des Levels vor. Szenarien, die im Spiel unsinnig wären, müssen zu einem Deadlock führen. Beispiel: Im echten Spiel ließe sich ein Level auch lösen, in dem man einige Male gegen die ,,Grenzen” des Spielfelds läuft, und dann erst das Level löst.

Ein weiteres Ziel ist es, durch dieses Projekt die Zulassung zur Prüfung für das Modul ,,Sicherheitskritische Systeme” im WS16/17 bei Prof. Dr. Leuschel (Heinrich-Heine-Universität Düsseldorf) zu bekommen.

System

Das Projekt wurde von mir sehr pragmatisch umgesetzt. Ich habe mir zu Anfang Gedanken gemacht, wie sich die Anforderungen je Level das System durch Erweiterungen Stück für Stück ausbauen lässt. Als ich jedoch mit der Umsetzung der ersten Events begann, konzentrierte ich mich umgehend auf alle, für das endgültige System notwendige Datentypen. Das Ergebnis lässt jedoch erahnen, dass ein strukturierter Aufbau ein deutlich knapperes und übersichtlicheres System hätte schaffen können. Erkennbar wird dies an sehr vielen, extrem ähnlichen Guards und Aktionen in Events, die möglicherweise durch ein vereinfachtes System und Event hätte zusammengeführt werden können.

Equipment

Das System besteht aus folgenden beteiligten Objekten:

  • EQP-1 Level: eine Menge von Feldern
  • EQP-2 Feld: eine Position im Level, der eine Licht-Eigenschaft zugeordnet ist
  • EQP-3 Licht-Eigenschaft: Ein Feld kann ein oder ausgeschaltet sein oder auch diese Funktion nicht besitzen (unusable)
  • EQP-4 Lightbot: ein Objekt mit …
    • EQP-4.1 Orientierung (in oder gegen x-Richtung, in oder gegen y-Richtung)
    • EQP-4.2 Position (z, x,y)
  • EQP-5 eine Drag-Area mit einer Auswahl von Aktionen:
    • EQP-5.1 Links-Drehung
    • EQP-5.2 Rechts-Drehung
    • EQP-5.3 Vorwärts
    • EQP-5.4 Hüpfen (rauf/runter)
    • EQP-5.5 Licht (an/aus)
    • EQP-5.6 zu P1 wechseln
    • EQP-5.7 zu P2 wechseln
  • EQP-6 Drei Drop-Area (Stack)
    • EQP-6.1 Main
    • EQP-6.2 P1
    • EQP-6.3 P2

Funktionale-Anforderungen

Sichtbar

  • FUN-1 Darstellung des oben beschriebenen Equipments
  • FUN-2 Aktion einer Drop-Area (Stack) zufügen
  • FUN-3 ein PLAY Knopf

Versteckt

  • FUN-4 Durchlaufen der Aktionen in Main nach dem Klicken auf PLAY
  • FUN-5 Stack Fokus-Wechsel beim Aufruf der P1 oder P2 Aktion
  • FUN-6 Stack Fokus-Wechsel beim Ende des P1 oder P2 Stacks
  • FUN-7 Entscheidungsautomatik: rauf- oder runterhüpfen

Sicherheits-Anforderungen

SAF-1 : Im Solve Modus, oder wenn in der Maschine simple die Variable filling = TRUE ist, ist folgendes zu beachten:

  • SAF-1.1 Die Drop-Areas haben je Level ein Limit, welches bestimmt, wie viele Aktionen dort abgelegt werden können
  • SAF-1.2 Play geht nur, wenn mindestens eine Aktion in Main ist
  • SAF-1.3 Aktionen können nur nach P1 ge-droppt werden, wenn in den drei Drop-Areas (Stacks) p1 bereits als Aktion vorhanden ist
  • SAF-1.4 Aktionen können nur nach P2 ge-droppt werden, wenn in den drei Drop-Areas (Stacks) p2 bereits als Aktion vorhanden ist

SAF-2 : Im Play Modus wird die Gültigkeit der in den 3 Stacks abgelegten Actionen geprüft. Auf folgende Aspekte wird dabei geachtet:

  • SAF-2.1 Sinnlose Schleifen: ein Limit, um nicht zum Ziel führende Endlosschleifen zu verhindern
  • SAF-2.2 Auf einem Feld darf nur das Licht eingeschaltet werden, wenn es bereits ein- oder ausgeschaltet ist
  • SAF-2.3 Vorwärts geht nur, wenn passend zur Orientierung und Position des Lightbot ein nachfolgendes Feld im Level existiert
  • SAF-2.4 Hüpfen geht nur, wenn passend zur Orientierung und Position des Lightbot ein nachfolgendes Feld im Level existiert, welches um 1 in der Höhe verschieden ist

Das Herunterspringen von einem Turm ist somit nicht erlaubt, obwohl dies im richtigen Spiel geht. Das Verhindern von zu langen Schleifen weicht ebenfalls vom richtigen Lightbot Spiel ab und fehlt dort.

Das Rodin Projekt

Aufbau

Es gibt fünf Maschinen-Dateien (drei sind mit jeweils drei Context-Dateien verbunden, die die jeweiligen Level darstellen) und sechs Context-Dateien (auch hier: 3 Stück für die jeweiligen Level 1.1, 2.1 und 3.1).

  • ctx0 enthält die Beschreibungen zu Licht, Position, Feld und Level
  • ctxGame erweitert ctx0 und enthält alles, was das Spiel beschreibt. Dazu gehören Aktionen, Richtungen, Spielzüge, Spiel-Modus (solve/play) und die Stacks (Main, P1, P2)
  • ctxLevel erweitert den obigen Context um Konstanten und Typen, die für ein Level wichtig sind. Dies sind die Start-Position des Lightbots, seine Orientierung und eine Grenze für den Verarbeitungs-Stack. Letzteres soll verhindern, dass beim Model-Checking Endlosschleifen betrachtet werden.
  • level11,21,31 erweitern ctxLevel und enthalten konkrete Werte für das Level, die in ctxLevel nur allgemein angegeben sind.
  • systemL11, L21, L31 sind Erweiterungen von der Maschine system und binden nur jeweils einen unterschiedlichen Context je Level ein
  • system ist die Maschine, die die Stacks (Main, P1, P2) abarbeiten kann. Sie ist eine Erweiterung von simple und enthält ein Refinement des PLAY Events.
  • simple ist die Maschine, in der das Drag-and-Drop für die Stacks realisiert ist.

Besondere Details

Die lev Variable

Um meine Definition eines Levels besser zu verstehen, ist folgende Zeichnung hilfreich:

Level Positionsangabe

Proof Obligations

Ein paar Proof Obligations (POs) konnte ich sehr leicht mit Rodin lösen. Hierzu orientierte ich mich an den Tipps das Kapitels 2.9 vom Rodin-Handbuch. Ein paar sehr allgemein gehaltene Datentypen musste ich mit zwei kleinen C-Programm konkret erzeugen und hinterlegen. Dass hat Probleme beim Model-Checking (uneindeutige oder unbrauchbare Initialisierung) verhindert und half bei vielen POs. Leider konnte das automatische Prüfen und ich einige POs nicht zu einem positiven Ergebnis hin beweisen. Dies waren vor allen dingen Aktionen und Guards in Events, welche mit Mengen-Operationen auf Sequenzen arbeiteten und in denen z.B. card() in Kombination mit arithmetischen Operationen benutzt wurden.

Lösungssuche

Wie bereits in der Einleitung beschrieben, kann man das Model-Checking von ProB in Rodin nutzen, um zu einem Level eine Lösung zu suchen. Hierbei muss man ein System mit der entsprechenden Einbindung des Level-Context automatisch nach Theorem-Verletzungen checken lassen. Mein Theorem, was bei mir nach dem Lösen verletzt wird, sieht so aus (in der Maschine system):

theorem @inv100 Game /= Ziel

Zwar könnten nach dem Lösungsweg noch weitere Befehle folgen, die das Licht wieder aus machen, aber auch der richtige Lightbot sieht in dem Fall das Level als gelöst an.

Die Variable Game entspricht dem Spielfeld. Nach dem PLAY Event wird durch das Ablaufen der Stacks mit dem ITER Event und dem Auslösen der zu den Aktionen passenden play_ Events in Game das Licht auf den Feldern eingeschaltet. Die Variable Ziel entspricht dem Level in umgekehrter Form: Alle nicht unusable Felder sind auf on geschaltet. Das mache ich bei der Initialisierung so:

@act06 Ziel := ( lev |>> {off} ) \/ ( dom(lev(lev |>> {off})) ** {on} )

Die Variable lev ist hierbei das in einem der Context-Files definierte, konkrete Level.

Anmerkungen

Ich habe die Positionen (z,x,y) generiert. Die Höhe kann von 1 bis 3 gehen und die x und y Koordinaten von 1 bis 7. Hierzu und zu möglichen ,,unmöglichen” Leveln wollte ich folgende Axiome hinterlegen, die ich leider aufgrund von Problemen beim Model-Checking wieder verworfen habe:

Für ein z (Höhe) darf es im Level nur eine x-y Koordinate geben

!z1,z2,x,y. z1|->x|->y : Pos & z2|->x|->y : Pos => z1 = z2

Zusammenhang der möglichen Positionen und den Spielfeldgrenzen eines Levels

Pos <: 1..card(dom(dom(dom(lev)))) ** 1..card(ran(dom(dom(lev)))) ** 1..card(ran(dom(lev)))

Die Verwendung der Definition einer Sequenz als Menge von Mengen, die durch eine totale Funktion von den natürlichen Zahlen zusammengesetzt wird (Übungsblatt 3) hat bei mir ausschließlich zu Problemen geführt (Model-Checking startete nicht, Unmengen von POs blieben rot). Dies wollte ich für die Funktions-Stacks und später für die Abarbeitung der Stacks verwenden. Entweder lag dies daran, dass 1..5 bei den POs als INT angesehen wurde, oder weil ich durch die Definition von Grenzen mittels card() eben nicht mehr total bin. Ich habe mich gut 3 Tage damit auseinander gesetzt, und die Formulierung einer allg. Sequenz wie in Übungsblatt 3 war für mich leider nicht nutzbar.

Weiteres:

  • Ein Entfernen von Aktionen aus dem Drop-Stacks ist nicht implementiert
  • Es wurde von mir leider nicht bedacht, dass je Level nicht alle möglichen Aktionen zur Verfügung stehen.
  • Von den Leveln 1.1, 2.1 und 3.1 konnte ich 2.1 nur durch eine Reduzierung der möglichen freien Stellen im Main- und P1-Stack automatisch (ca 45 Min.) eine Lösung finden lassen.
  • ProB Problem: beim Öffnen des Model-Checkers wird ein Error angezeigt: ,,Translation incomplete due to a Bug in Rodin”
  • Bei den Maschinen simple und system wollte ich mit einer Withness arbeiten, die die Variable filling in system überflüssig macht und durch modus ersetzt. Das ist mir leider nicht mehr gelungen.