C Informelle Semantik
Die Programme stellen kommunizierende, parallele Prozesse dar. Der
Abschnitt beschreibt informell die Bedeutung der Mist-Programme. Die
Semantik ist nur für gecheckte Programme definiert (s.
Abschnitt 7); nicht-gecheckte Programme sind bedeutungslos.
Insbesondere können der Simulator und der Model-Checker
(Abschnitt 6 und 8), die die Semantik
realisieren, von gecheckter Syntax ausgehen.
C.1 Zustände
Der globale Zustand eines Programmes ist festgelegt aus den lokalen
Zuständen der Prozesse des Programmes: der globale Zustand ist also
das Produkt der lokalen Zustände. Ein lokaler Zustand eines
Prozesses besteht aus dem state, in dem sich der Prozeß befindet
und der Variablenbelegung, d.h., der Werte aller seiner lokalen
Variable. Es gibt keine globalen Variablen.
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.2 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).3 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