Plan LTL Visualisation - Revision history

Daniel Plagge at 10:38, 6 April 2011

2011-04-06T10:38:52Z

← Older revision		Revision as of 10:38, 6 April 2011
Line 39:		Line 39:
	* Den LTL-Button in der Event-View und den LTL-Dialog entfernen und die Eingabe der Formeln komplett in der LTL-View erledigen.		* 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.		* Atomare Aussagen sollten in der StateView analysierbar werden, z.B. mittels Kontextmenü. Analog zum "grünen Plus" in der StateView. Ideal wäre DnD.

			=Interaktion mit anderen ProB-Komponenten=
			Bisher ist man als Benutzer noch relativ verloren, wenn man das Gegenbeispiel mit dem ursprünglichen Modell in Verbindung bringen will. Die bestehenden Anzeigen sollten mit benutzt werden, um den Benutzer zu helfen.

			Wenn in der LTL-View ein Zustand angewählt wird (oder explizit mittels Doppelklick oder so ähnlich), sollte der aktuelle Zustand und History auf
			den Zustand gesetzt werden:
			* In der State-View wird der aktuelle Zustand angezeigt und auswertbar gemacht.
			* In der History-View wird das komplette LTL-Gegenbeispiel angezeigt
			* In der Event-View werden alle möglichen Events angezeigt werden. Der Benutzer kann dann mit den vor-zurück-Buttons durch das Gegenbeispiel navigieren. Wählt er ein Event explizit, bekommt er eine neue History (wie bisher auch)
			* Atomare Aussagen sollten als Formeln in die State-View anzuzeigen sein.

			Umgekehrt sollte es möglich sein, die aktuelle Historie auf eine LTL-Formel hin zu überprüfen. Was machen wir in dem Fall mit dem Beispiels-Ende (also Deadlock, abgeschnitten oder Schleife?)

Daniel Plagge: /* Ideen zu GUI */

2011-02-03T12:41:28Z

Ideen zu GUI

← Older revision		Revision as of 12:41, 3 February 2011
Line 38:		Line 38:
	* 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.		* 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.		* 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ü.		* Atomare Aussagen sollten in der StateView analysierbar werden, z.B. mittels Kontextmenü. Analog zum "grünen Plus" in der StateView. Ideal wäre DnD.

Daniel Plagge: /* Ideen zu GUI */

2011-02-03T12:39:27Z

Ideen zu GUI

← Older revision		Revision as of 12:39, 3 February 2011
Line 38:		Line 38:
	* 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.		* 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.		* 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ü.

Daniel Plagge: /* Anzeige */

2011-01-19T13:47:28Z

← Older revision		Revision as of 13:47, 19 January 2011
Line 13:		Line 13:

	== Anzeige ==		== Anzeige ==
	* Wie kann ~~man~~ die Schleife erkennen, bzw. Unterschied zwischen Deadlock und gekürztem Pfad?		* 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:		* Formeln sollten evtl. durch den Rodin-UTF8-Konverter geschickt werden:
	RodinKeyboardPlugin.getDefault().translate(...)		RodinKeyboardPlugin.getDefault().translate(...)

Daniel Plagge: /* Wichtige Punkte */

2011-01-19T13:29:57Z

Wichtige Punkte

← Older revision		Revision as of 13:29, 19 January 2011
Line 25:		Line 25:
	* Alternativ könnte man die einen Schleifendurchlauf noch einmal hinten dran hängen, um den Benutzer zu entlasten.		* 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)		* 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 =		= Ideen zu GUI =

Daniel Plagge: /* Ideen zu GUI */

2011-01-19T13:08:49Z

Ideen zu GUI

← Older revision		Revision as of 13:08, 19 January 2011
Line 31:		Line 31:
	* Gleichzeitig in mehreren Reitern verschiedene Pfade speichern		* 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.		* 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.

Daniel Plagge: /* Anzeige */

2011-01-19T13:06:58Z

← Older revision		Revision as of 13:06, 19 January 2011
Line 16:		Line 16:
	* Formeln sollten evtl. durch den Rodin-UTF8-Konverter geschickt werden:		* Formeln sollten evtl. durch den Rodin-UTF8-Konverter geschickt werden:
	RodinKeyboardPlugin.getDefault().translate(...)		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.		* Bei Auswahl einer Zelle sollte mittels Farben (oder was besseres?) angezeigt werden, wie es zu dem Wert gekommen ist.

Daniel Plagge: /* Anzeige */

2011-01-19T13:06:07Z

← Older revision		Revision as of 13:06, 19 January 2011
Line 14:		Line 14:
	== Anzeige ==		== Anzeige ==
	* Wie kann man die Schleife erkennen, bzw. Unterschied zwischen Deadlock und gekürztem Pfad?		* Wie kann man die Schleife erkennen, bzw. Unterschied zwischen Deadlock und gekürztem Pfad?
	* Formeln sollten evtl. durch den Rodin-UTF8-Konverter geschickt werden.		* Formeln sollten evtl. durch den Rodin-UTF8-Konverter geschickt werden:
			RodinKeyboardPlugin.getDefault().translate(...)
	* Bei Auswahl einer Zelle sollte mittels Farben (oder was besseres?) angezeigt werden, wie es zu dem Wert gekommen ist.		* Bei Auswahl einer Zelle sollte mittels Farben (oder was besseres?) angezeigt werden, wie es zu dem Wert gekommen ist.

Daniel Plagge: /* Ideen zu GUI */

2011-01-19T13:02:53Z

Ideen zu GUI

← Older revision		Revision as of 13:02, 19 January 2011
Line 28:		Line 28:
	* 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.		* 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		* 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.

Daniel Plagge: /* Anzeige */

2011-01-19T12:59:31Z

← Older revision		Revision as of 12:59, 19 January 2011
Line 18:		Line 18:


	Beispiel: Hier wird die blau hinterlegte Zelle 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).		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).
	[[File:ltl1.png\|600px\|center]]		[[File:ltl1.png\|600px\|center]]