Download Endbericht

IV
INHALTSVERZEICHNIS
3.2
3.3
3.4
3.5
3.6
3.7
Automaten . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
3.2.1
Aufbau eines Automaten . . . . . . . . . . . . . . . . . . . . . . . . 105
3.2.2
Berechnung von Transitionen bei Automatenoperationen . . . . . . 122
3.2.3
Einleitung und Übersicht zur Weiterführung . . . . . . . . . . . . . 127
3.2.4
OBDDs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131
3.2.5
Büchiautomaten . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137
3.2.6
Kripkestruktur . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 144
Parser . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 147
3.3.1
Parser Infrastruktur . . . . . . . . . . . . . . . . . . . . . . . . . . 147
3.3.2
First-Generation (Presburger-Parser) . . . . . . . . . . . . . . . . . 150
3.3.3
Second-Generation (LTL, CTL, While) . . . . . . . . . . . . . . . . 153
3.3.4
Parser für reguläre und ω-reguläre Ausdrücke . . . . . . . . . . . . 157
Der Workspace - Stand Februar 2006 . . . . . . . . . . . . . . . . . . . . . 163
3.4.1
Planungsphase . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 163
3.4.2
Das Workspacekonzept . . . . . . . . . . . . . . . . . . . . . . . . . 166
3.4.3
Features der Implementation . . . . . . . . . . . . . . . . . . . . . . 167
Der Workspace - Stand Juli 2006 . . . . . . . . . . . . . . . . . . . . . . . 178
3.5.1
Planungsphase . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 178
3.5.2
Das Workspacekonzept . . . . . . . . . . . . . . . . . . . . . . . . . 179
3.5.3
Features der Implementierung . . . . . . . . . . . . . . . . . . . . . 181
3.5.4
Plugins . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 183
3.5.5
Die Klasse GenericOperationDriver . . . . . . . . . . . . . . . . . 183
Editor . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 196
3.6.1
Ziele . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 196
3.6.2
Das Paintable-Framework . . . . . . . . . . . . . . . . . . . . . . . 197
3.6.3
3.6.4
Das PaintableAutomaton“-Addon . . . . . . . . . . . . . . . . . . 201
”
Kripke-Modelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 209
3.6.5
OBDDs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 211
3.6.6
Layouting von Automaten . . . . . . . . . . . . . . . . . . . . . . . 212
Handbuch . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 218
3.7.1
Der Workspace-Überblick . . . . . . . . . . . . . . . . . . . . . . . 218
3.7.2
Starten von neuen Automatenanalysen . . . . . . . . . . . . . . . . 219
3.7.3
Umgang mit dem Navigator . . . . . . . . . . . . . . . . . . . . . . 220
3.7.4
Die Konsole . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 221
3.7.5
Laden . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 221
3.7.6
Speichern . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 222
3.7.7
Operationen und Analysen . . . . . . . . . . . . . . . . . . . . . . . 222
3.7.8
Automateneditor . . . . . . . . . . . . . . . . . . . . . . . . . . . . 222
3.7.9
Plugins . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 226