Download TRACS Abschlussbericht - FB3 - Uni Bremen

KAPITEL 7. BESCHREIBUNG DER KOMPONENTEN
210
• AG p
Entlang aller Pfade im Transitionssystem ist p in allen zukünftigen Zuständen
erfüllt.
• EG p
Es existiert ein Pfad im Transitionssystem, in dem p in allen zukünftigen Zuständen erfüllt ist.
• AF p
Entlang alle Pfade im Transitionssystem wird irgendwann ein Zustand erreicht, in
dem p erfüllt ist.
• A[p U q]
Entlang aller Pfade im Transitionssystems ist p solange erfüllt, bis q erfüllt ist.
7.6.3.1.5 checkinvar declaration In der checkinvar declaration-Umgebung werden Invarianten spezifiziert. Dies sind Bedingungen, die in allen Zuständen des Systems
erfüllt sein müssen. Das Schlüsselwort INVARSPEC drückt aus, dass eine Invariante
folgt.
7.6.3.2
Beispiel
Es soll nun ein einfaches Beispiel angegeben werden. Das Beispiel dient dazu, das Grundprinzip von NuSMV zu verdeutlichen, bevor im nächsten Abschnitt die Modellierung das
eigentlichen Systems beschrieben wird.
Die Abbildung 7.46 zeigt eine einfache Kreuzung. Vor der Kreuzung befindet sich jeweils
ein Signal und hinter der Kreuzung ein Sensor.
Abbildung 7.46: Einfaches Gleisnetz