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 man die Schleife erkennen, bzw. Unterschied zwischen Deadlock und gekürztem Pfad?
• Formeln sollten evtl. durch den Rodin-UTF8-Konverter geschickt 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)

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