92
2 Spezifikation und Modellierung
Tabelle 2.3 N T für das Thalys-Beispiel
p 1 p 2 p 3 p 4 p 5 p 6 p 7 p 8 p 9 p 10 p 11 p 12 p 13
t 1 1 -1
-1
1
t 2
1 -1
t 3
1 -1
t 4
1 -1
1
t 5
1 -1 -1
1
t 6 -1
1
t 7
1 -1
t 8
1
-1
t 9
1 -1
t 10
1 -1
-1
In diesem Beispiel ist in Zeile 2 dargestellt, dass das Schalten von t 2 die Anzahl der
Marken bei p 2 um eine erhöht und die Anzahl der Marken bei p 3 um eine vermindert.
Unter Einsatz von Methoden der linearen Algebra können wir zeigen, dass die
folgenden vier Vektoren Lösungen dieses linearen Gleichungssystems darstellen:
c R,1 = (1,1,1,1,1,1,0,0,0,0,0,0,0)
c R,2 = (1,0,0,0,1,1,0,0,1,1,1,0,0)
c R,3 = (0,0,0,0,0,0,0,0,1,1,0,0,1)
c R,4 = (0,0,0,0,0,0,1,1,0,0,0,1,0)
Diese Vektoren entsprechen den Orten entlang der Gleise für Züge aus Köln
und Amsterdam sowie den Orten entlang des Weges für Lokführer von Zügen aus
Amsterdam und den Orten entlang der Gleise innerhalb von Paris. Damit können
wir zeigen, dass die Anzahl von Zügen und Lokführern entlang der Gleise konstant
ist (was wir natürlich erwartet haben). Dieses Beispiel zeigt, dass S-Invarianten
als Standardtechnik eingesetzt werden können, um Eigenschaften von Systemen zu
beweisen.
∇
2.6.4 Prädikat/Transitions-Netze
Sowohl Bedingungs/Ereignis-Netze als auch Stellen/Transitions-Netze können für
größere Beispiele schnell sehr groß und unübersichtlich werden. Eine Verringerung
der Größe ist häufig durch den Einsatz von Prädikat/Transitions-Netzen möglich.
Beispiel 2.25: Wir werden dies am Beispiel der „dinierenden Philosophen“ demonstrieren. Das Problem geht von einer Anzahl von Philosophen aus, die an einem runden
Tisch essen. Vor jedem Philosophen steht ein Teller mit Spaghetti (siehe Abb. 2.53).
Zwischen den Tellern befindet sich jeweils nur eine Gabel. Jeder Philosoph ist entweder mit Essen oder mit Nachdenken beschäftigt. Essende Philosophen benötigen
dafür die beiden Gabeln, die neben ihrem Teller liegen. Folglich kann ein Philosoph
nur dann essen, wenn seine beiden Nachbarn gerade nicht essen.
2 Spezifikation und Modellierung
Tabelle 2.3 N T für das Thalys-Beispiel
p 1 p 2 p 3 p 4 p 5 p 6 p 7 p 8 p 9 p 10 p 11 p 12 p 13
t 1 1 -1
-1
1
t 2
1 -1
t 3
1 -1
t 4
1 -1
1
t 5
1 -1 -1
1
t 6 -1
1
t 7
1 -1
t 8
1
-1
t 9
1 -1
t 10
1 -1
-1
In diesem Beispiel ist in Zeile 2 dargestellt, dass das Schalten von t 2 die Anzahl der
Marken bei p 2 um eine erhöht und die Anzahl der Marken bei p 3 um eine vermindert.
Unter Einsatz von Methoden der linearen Algebra können wir zeigen, dass die
folgenden vier Vektoren Lösungen dieses linearen Gleichungssystems darstellen:
c R,1 = (1,1,1,1,1,1,0,0,0,0,0,0,0)
c R,2 = (1,0,0,0,1,1,0,0,1,1,1,0,0)
c R,3 = (0,0,0,0,0,0,0,0,1,1,0,0,1)
c R,4 = (0,0,0,0,0,0,1,1,0,0,0,1,0)
Diese Vektoren entsprechen den Orten entlang der Gleise für Züge aus Köln
und Amsterdam sowie den Orten entlang des Weges für Lokführer von Zügen aus
Amsterdam und den Orten entlang der Gleise innerhalb von Paris. Damit können
wir zeigen, dass die Anzahl von Zügen und Lokführern entlang der Gleise konstant
ist (was wir natürlich erwartet haben). Dieses Beispiel zeigt, dass S-Invarianten
als Standardtechnik eingesetzt werden können, um Eigenschaften von Systemen zu
beweisen.
∇
2.6.4 Prädikat/Transitions-Netze
Sowohl Bedingungs/Ereignis-Netze als auch Stellen/Transitions-Netze können für
größere Beispiele schnell sehr groß und unübersichtlich werden. Eine Verringerung
der Größe ist häufig durch den Einsatz von Prädikat/Transitions-Netzen möglich.
Beispiel 2.25: Wir werden dies am Beispiel der „dinierenden Philosophen“ demonstrieren. Das Problem geht von einer Anzahl von Philosophen aus, die an einem runden
Tisch essen. Vor jedem Philosophen steht ein Teller mit Spaghetti (siehe Abb. 2.53).
Zwischen den Tellern befindet sich jeweils nur eine Gabel. Jeder Philosoph ist entweder mit Essen oder mit Nachdenken beschäftigt. Essende Philosophen benötigen
dafür die beiden Gabeln, die neben ihrem Teller liegen. Folglich kann ein Philosoph
nur dann essen, wenn seine beiden Nachbarn gerade nicht essen.