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).

• 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.