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 markiert. In der nächsten Spalte färben sich einige Zellen gelb und rot.
- Alternativ könnte man die einen Schleifendurchlauf noch einmal hinten dran hängen, um den Benutzer zu entlasten.
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