Plan LTL Visualisation

Wichtige Punkte

Diese Teile müssen bei der Implementation / Beschreibung in der Arbeit beachtet werden.

Schleifen, Deadlocks, und gekürzte Gegenbeispiele

Der Modelchecker liefert drei Arten von Gegenbeispielen:

  • Schleifen, der Einstiegspunkt wird mitgeliefert. Eine Schleife repräsentiert einen unendlichen Pfad.
  • Pfade, die im Deadlock enden. Beispiele: Im letzten Zustand des Gegenbeispiels ist X(f) immer falsch, unabhängig von f. G(f) ist im letzten Zustand war, wenn f dort wahr ist.
  • Gekürzte Pfade. Als Gegenbeispiel reicht ein Teil der ursprünglich berechneten Schleife aus. Beispiele: X(f) ist im letzten Zustand nicht ermittelbar. Auch G(f) nicht, wenn f dort wahr ist.

Verwaltung von LTL-Formeln

  • Speichern von zuvor eingegebener Formeln (Model-abhängig?)
  • Evtl. mehrere Reiter für verschiedene Formeln

Anzeige

  • Wie kann der Benutzer die Schleife erkennen, bzw. den Unterschied zwischen Deadlock und gekürztem Pfad?
  • Formeln sollten evtl. durch den Rodin-UTF8-Konverter geschickt werden:
RodinKeyboardPlugin.getDefault().translate(...)

Dann muss allerdings der Rodin-Font verwendet werden.

  • Bei Auswahl einer Zelle sollte mittels Farben (oder was besseres?) angezeigt werden, wie es zu dem Wert gekommen ist.


Beispiel: Hier wird die blau hinterlegte Zelle vom Benutzer markiert. In der nächsten Spalte färben sich einige Zellen gelb und rot. "G(not q)" ist in 7 unwahr wegen der Folge 7(not q: true), 8(not q: true), 9(not q:false).

Ltl1.png
  • Alternativ könnte man die einen Schleifendurchlauf noch einmal hinten dran hängen, um den Benutzer zu entlasten.
  • Die Anzeige der Zustandsnummern bringt dem Benutzer nicht wirklich etwas (wird sonst nirgendwo anders verwendet)

Semantik vom Release-Operator

(pi,i) |= fRg genau dann wenn

  • ein j>=i existiert mit (pi,j) |= f&g und für alle k mit i<=k<j (pi,k) |= g gilt
  • oder (pi,j) |= g für alle j>=i gilt

Ideen zu GUI

  • Interaktion mit der aktuellen Historie: Evtl. sollte das Gegenbeispiel auch in die aktuelle Historie geladen werden und der aktuell ausgewählte Zustand dort auch angezeigt werden.
  • Gleichzeitig in mehreren Reitern verschiedene Pfade speichern
  • Evtl. könnte der Benutzer einen Knopf gebrauchen, mit dem er den Einstiegs-Zustand der Schleife (wenn eine existiert) wieder hinten anhängen kann. Dann verschiebt sich der Einstiegspunkt um 1.
  • Den LTL-Button in der Event-View und den LTL-Dialog entfernen und die Eingabe der Formeln komplett in der LTL-View erledigen.
  • Atomare Aussagen sollten in der StateView analysierbar werden, z.B. mittels Kontextmenü. Analog zum "grünen Plus" in der StateView. Ideal wäre DnD.