Download Endbericht

Abbildungsverzeichnis
2.1
Automat A für Schnitt . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2.2
Automat B für Schnitt . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2.3
Ergebnis-Automat für Schnitt . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.4
Ursprungsautomat für Degeneralisierung . . . . . . . . . . . . . . . . . . . 15
2.5
Ergebnis der Degeneralisierung
2.6
Funktionsweise der Y-Konstruktion . . . . . . . . . . . . . . . . . . . . . . 34
2.7
Beispiel für die Y-Konstruktion . . . . . . . . . . . . . . . . . . . . . . . . 34
2.8
BDD-basierende Repräsentation eines Automaten . . . . . . . . . . . . . . 55
2.9
Logik-schichten in MOSEL . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
. . . . . . . . . . . . . . . . . . . . . . . . 16
2.10 Überblick über das Eclipse Project (siehe auch [?]) . . . . . . . . . . . . . 68
2.11 Beispiel eines mit GEF realisierten Editors . . . . . . . . . . . . . . . . . . 72
3.1
Transformation einer Presburger-Formel in einen Automaten . . . . . . . . 81
3.2
If zu Programmgraph . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93
3.3
Pipeline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94
3.4
Aufbau eines einfachen While-Programms . . . . . . . . . . . . . . . . . . 98
3.5
Schalenmodell . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
3.6
Ablauf . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100
3.7
If Ausführung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101
3.8
Die abstrakte Klasse Converter . . . . . . . . . . . . . . . . . . . . . . . . 120
3.9
Diagramm zu dem endgültigen Automatenkern . . . . . . . . . . . . . . . . 123
3.10 Objektdiagramm zur beispielhaften Konstruktion in 3.2.1.5 . . . . . . . . . 124
3.11 Situation bei der Potenzmengenkonstruktion . . . . . . . . . . . . . . . . . 125
3.12 Ein OBDD für die Funktion f = (x2 ∧ x7 ∧ x10 ) ∨ (x5 ∧ (x3 ∨ x7 )) . . . . . 132
3.13 eine einfache Grammatik (BNF) . . . . . . . . . . . . . . . . . . . . . . . . 150
3.14 Presburger (BNF) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 151
3.15 Infix CTL (PEG) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 154
3.16 Prefix CTL (PEG) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 154
3.17 Infix LTL (PEG) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155
3.18 Prefix LTL (PEG) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155
VII