86
2 Spezifikation und Modellierung
Wenn zwei Züge gleichzeitig den eingleisigen Abschnitt benutzen wollen (siehe
Abb. 2.48), kann nur einer der beiden in den Abschnitt eintreten.
nach rechts
Zug will nach rechts
Gleis verfügbar
Zug fährt
nach links
Zug fährt
Zug fährt nach rechts heraus
Zug fährt von links ein
Abb. 2.48 Konflikt um die Ressource „Gleisabschnitt“
∇
In solchen Situationen wird das nächste Ereignis nichtdeterministisch ausgewählt.
Netzanalysen müssen dabei alle möglichen Folgen von Ausführungen von Ereignissen berücksichtigen. Bei Petrinetzen modellieren wir absichtlich Nichtdeterminismus.
Ein wichtiger Vorteil von Petrinetzen liegt darin, dass sie als Grundlage für formale Beweise von Systemeigenschaften dienen können. Es existieren bereits einige Standardmethoden, um solche Beweise automatisch zu erzeugen. Um diese Beweise zu
ermöglichen, benötigen wir eine formalere Definition von Petrinetzen. Wir betrachten drei Klassen von Petrinetzen: Bedingungs/Ereignis-Netze, Stellen/TransitionsNetze und Prädikat/Ereignis-Netze.
2.6.2 Bedingungs/Ereignis-Netze
Als erste Klasse von Petrinetzen werden wir Bedingungs/Ereignis-Netze formal
definieren.
Definition 2.15: N = (C, E, F) heißt Netz, genau dann, wenn die folgenden Bedingungen erfüllt sind:
1. C und E sind disjunkte Mengen.
2. F ⊆ (E × C) ∪ (C × E) ist eine zweistellige Relation, genannt Flussrelation.
Die Menge C heißt die Menge der Bedingungen und die Menge E ist die Menge der
Ereignisse (auch Transitionen genannt).
Definition 2.16: Sei N ein Netz und sei x ∈ (C ∪ E). Dann heißt • x := {y|yF x, y ∈
(C ∪ E)} der Vorbereich von x. Wenn x ein Ereignis ist, dann heißt • x auch „Menge
der Vorbedingungen von x”.
2 Spezifikation und Modellierung
Wenn zwei Züge gleichzeitig den eingleisigen Abschnitt benutzen wollen (siehe
Abb. 2.48), kann nur einer der beiden in den Abschnitt eintreten.
nach rechts
Zug will nach rechts
Gleis verfügbar
Zug fährt
nach links
Zug fährt
Zug fährt nach rechts heraus
Zug fährt von links ein
Abb. 2.48 Konflikt um die Ressource „Gleisabschnitt“
∇
In solchen Situationen wird das nächste Ereignis nichtdeterministisch ausgewählt.
Netzanalysen müssen dabei alle möglichen Folgen von Ausführungen von Ereignissen berücksichtigen. Bei Petrinetzen modellieren wir absichtlich Nichtdeterminismus.
Ein wichtiger Vorteil von Petrinetzen liegt darin, dass sie als Grundlage für formale Beweise von Systemeigenschaften dienen können. Es existieren bereits einige Standardmethoden, um solche Beweise automatisch zu erzeugen. Um diese Beweise zu
ermöglichen, benötigen wir eine formalere Definition von Petrinetzen. Wir betrachten drei Klassen von Petrinetzen: Bedingungs/Ereignis-Netze, Stellen/TransitionsNetze und Prädikat/Ereignis-Netze.
2.6.2 Bedingungs/Ereignis-Netze
Als erste Klasse von Petrinetzen werden wir Bedingungs/Ereignis-Netze formal
definieren.
Definition 2.15: N = (C, E, F) heißt Netz, genau dann, wenn die folgenden Bedingungen erfüllt sind:
1. C und E sind disjunkte Mengen.
2. F ⊆ (E × C) ∪ (C × E) ist eine zweistellige Relation, genannt Flussrelation.
Die Menge C heißt die Menge der Bedingungen und die Menge E ist die Menge der
Ereignisse (auch Transitionen genannt).
Definition 2.16: Sei N ein Netz und sei x ∈ (C ∪ E). Dann heißt • x := {y|yF x, y ∈
(C ∪ E)} der Vorbereich von x. Wenn x ein Ereignis ist, dann heißt • x auch „Menge
der Vorbedingungen von x”.