C Informelle Semantik
Dieser
Abschnitt beschreibt informell die Bedeutung der Snot-Programme. Die
Semantik ist nur für gecheckte SFC's definiert (s.
Abschnitt 8); nicht-gecheckte Programme sind bedeutungslos.
Insbesondere können der Simulator und der Model-Checker
(Abschnitt 9 und 11), die die Semantik
realisieren, von gecheckter Syntax ausgehen.
C.1 Zustände
Der globale Zustand eines Programmes ist gegeben durch die Variablenbelegungen
und die Menge der aktiven Steps.
C.2 Kommunikationsmodell und Schritte
Die Bedeutung der Konstrukte wie Wertzuweisung, Anfangszustand etc., sollte
unstrittig sein. Interpretationsspielraum gibt es für die
Kommunikationskonstrukte und das Wesen der Parallelität.
Aufgrund der informellen Diskussion haben wir uns auf folgendes Modell
geeinigt:
-
Interleaving-Parallelität
- zwei-Weg Kommnuikation (kein Broadcast)
- synchroner Nachrichtenaustausch
Das heißt genauer folgendes: Der Zustand des Programmes ändert sich in
den Transitionen. Es gibt 4 Arten davon
-
interne Aktionen (``tau'')
- Zuweisung
- Input
- Output
Die ersten beiden Aktionen werden von einem einzigen Prozeß alleine
ausgeführt, d.h., wir haben eine
Interleaving-Interpretation.3 Die t-Aktion läßt die Variablenbelegung unverändert,
die Verwertzuweisung ändert sie. Daneben wechselt der Betroffene Prozess
von einem state und einen Nachfolgezustand entsprechend der
Transition.
Daneben gibt es zwei Arten von Kommunikationstransitionen (input und
output) die immer komplementär und gleichzeitig ausgeführt werden
(synchones Modell) und bei der immer genau zwei Partner beteiligt sind
(zwei-Wege Kommunikation).4 Eine Kommunikation zwischen zwei Prozessen kann dann
stattfinden, wenn sich beide in einem Zustand befinden, bei dem der eine
eine Eingabe-, der andere eine Ausgabeaktion durchführen können (d.h.
auch, ihre Guards evaluieren zu true). Falls daß der Fall ist,
wechseln beide synchron in ihren Nachfolge-state, wobei der
Empfängerprozeß auch noch seine Variablenbelegung durch den empfangenen
Wert ändert.
Die Transitionen können mit einem Guard ausgestattet sein, einem
booleschen Ausdruck. Eine Transition kann nur genommen werden,
falls der Guard sich zu true evaluiert.
©Public License