54
2 Spezifikation und Modellierung
Beispiel 2.8: Abb. 2.11 zeigt ein Beispiel für einen zeitgesteuerten Automaten. Der
Anrufbeantworter befindet sich normalerweise im links dargestellten Anfangszustand.
x <=9
ring
beep
record
beep
silent
start
play
text
dead
talk
wait
li ft -o ff
return hand-set
x
y
<=5
y
y
x
x
x
y
y
y
x
y
:=0
>=4
:=0
<=2
:=0
:=0
>=1
<=2
>=8
>=1
:=0
end
of text
Abb. 2.11 Bearbeitung ankommender Anrufe bei einem Anrufbeantworter
Wenn ein Anruf ankommt, wird die Uhr x auf 0 zurückgesetzt und der Automat
wechselt in den Wartezustand wait. Wenn der Angerufene den Anruf annimmt, kann
ein Gespräch stattfinden, bis der Hörer aufgelegt wird. Ansonsten kann ein Übergang
zum Zustand play text stattfinden, wenn die Zeit den Wert 4 erreicht hat.
Sobald der Übergang stattgefunden hat, wird eine aufgezeichnete Nachricht abgespielt und mit einem Piepton beendet. Die Uhr y garantiert, dass der Ton mindestens
eine Zeiteinheit lang ist. Danach wird die Uhr x wieder auf 0 zurückgesetzt und der
Anrufbeantworter beginnt mit der Aufnahme. Wenn die Zeit den Wert 8 erreicht
hat oder der Anrufer nichts sagt, kann der nächste Piepton abgespielt werden, der
auch wieder mindestens eine Zeiteinheit dauert. Danach findet ein Übergang in den
Schlusszustand statt. In diesem Beispiel werden Übergänge durch Eingaben (wie
lift-off ) oder durch Uhren-Einschränkungen (engl. clock constraints) ausgelöst. ∇
Zeitbedingungen beschreiben Übergänge, die stattfinden können, aber nicht müssen. Um sicherzustellen, dass ein Übergang wirklich stattfindet, können zusätzlich
Stelleninvarianten (engl. location invariants) definiert werden. Die Stelleninvarianten x ≤ 5, x ≤ 9 und y ≤ 2 werden im Beispiel verwendet, damit Transitionen
spätestens eine Zeiteinheit nach der sie auslösenden Bedingung aktiv werden. Im
Beispiel dienen zwei Uhren der Veranschaulichung, eine Uhr wäre ausreichend.
Formal lassen sich zeitgesteuerte Automaten wie folgt definieren [44]: Sei C
eine Menge reellwertiger, nicht negativer Variablen, die Uhren darstellen. Sei Σ ein
endliches Alphabet möglicher Eingaben.
Definition 2.7: Eine Zeitbedingung ist eine konjunktive Formel atomarer Bedingungen der Form x ◦ n oder (x − y) ◦ n mit x, y ∈ C, ◦ ∈ {≤, <, =, >, ≥} und n ∈ N.
Die verwendeten Konstanten n der Bedingungen müssen ganzzahlig sein, auch
wenn die Uhren reellwertig sind. Eine Erweiterung auf rationale Konstanten wäre
einfach, da diese sich einfach durch Multiplikation in ganze Zahlen wandeln lassen.
Sei B(C) die Menge an Zeitbedingungen.
2 Spezifikation und Modellierung
Beispiel 2.8: Abb. 2.11 zeigt ein Beispiel für einen zeitgesteuerten Automaten. Der
Anrufbeantworter befindet sich normalerweise im links dargestellten Anfangszustand.
x <=9
ring
beep
record
beep
silent
start
play
text
dead
talk
wait
li ft -o ff
return hand-set
x
y
<=5
y
y
x
x
x
y
y
y
x
y
:=0
>=4
:=0
<=2
:=0
:=0
>=1
<=2
>=8
>=1
:=0
end
of text
Abb. 2.11 Bearbeitung ankommender Anrufe bei einem Anrufbeantworter
Wenn ein Anruf ankommt, wird die Uhr x auf 0 zurückgesetzt und der Automat
wechselt in den Wartezustand wait. Wenn der Angerufene den Anruf annimmt, kann
ein Gespräch stattfinden, bis der Hörer aufgelegt wird. Ansonsten kann ein Übergang
zum Zustand play text stattfinden, wenn die Zeit den Wert 4 erreicht hat.
Sobald der Übergang stattgefunden hat, wird eine aufgezeichnete Nachricht abgespielt und mit einem Piepton beendet. Die Uhr y garantiert, dass der Ton mindestens
eine Zeiteinheit lang ist. Danach wird die Uhr x wieder auf 0 zurückgesetzt und der
Anrufbeantworter beginnt mit der Aufnahme. Wenn die Zeit den Wert 8 erreicht
hat oder der Anrufer nichts sagt, kann der nächste Piepton abgespielt werden, der
auch wieder mindestens eine Zeiteinheit dauert. Danach findet ein Übergang in den
Schlusszustand statt. In diesem Beispiel werden Übergänge durch Eingaben (wie
lift-off ) oder durch Uhren-Einschränkungen (engl. clock constraints) ausgelöst. ∇
Zeitbedingungen beschreiben Übergänge, die stattfinden können, aber nicht müssen. Um sicherzustellen, dass ein Übergang wirklich stattfindet, können zusätzlich
Stelleninvarianten (engl. location invariants) definiert werden. Die Stelleninvarianten x ≤ 5, x ≤ 9 und y ≤ 2 werden im Beispiel verwendet, damit Transitionen
spätestens eine Zeiteinheit nach der sie auslösenden Bedingung aktiv werden. Im
Beispiel dienen zwei Uhren der Veranschaulichung, eine Uhr wäre ausreichend.
Formal lassen sich zeitgesteuerte Automaten wie folgt definieren [44]: Sei C
eine Menge reellwertiger, nicht negativer Variablen, die Uhren darstellen. Sei Σ ein
endliches Alphabet möglicher Eingaben.
Definition 2.7: Eine Zeitbedingung ist eine konjunktive Formel atomarer Bedingungen der Form x ◦ n oder (x − y) ◦ n mit x, y ∈ C, ◦ ∈ {≤, <, =, >, ≥} und n ∈ N.
Die verwendeten Konstanten n der Bedingungen müssen ganzzahlig sein, auch
wenn die Uhren reellwertig sind. Eine Erweiterung auf rationale Konstanten wäre
einfach, da diese sich einfach durch Multiplikation in ganze Zahlen wandeln lassen.
Sei B(C) die Menge an Zeitbedingungen.