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.

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