Kurzanleitung zu NuSMV
shell-prompt> /proj/i11praktikum/nusmv/setup
shell-prompt> NuSMV –int Datei.smv
Installation:
Programmstart:
Befehle:
help
befehl –h
go
print_reachable_states
print_reachable_states –v
pick_state –i -a
simulate –i –a 10
show_traces
check_spec
quit
Liste aller Befehle anzeigen
Hilfe zu diesem Befehl anzeigen
Modell laden und vorbereiten
Anzahl der erreichbaren Zustände
Alle erreichbaren Zustände auflisten
Anfangszustand wählen
interaktiv 10 Schritte simulieren
Simulationsabfolge der Zustände anzeigen
Spezifikationen testen
NuSMV beenden
Beispiel:
-- Kommentar
-- Autor: ...
MODULE ampel (andereAmpel)
VAR
farbe : {rot, rot_gelb, gruen, gelb};
INIT
farbe = rot | andereAmpel.farbe = rot;
ASSIGN
next (farbe) :=
case
farbe = rot & next(andereAmpel.farbe) = rot: rot_gelb;
farbe = rot_gelb: gruen;
farbe = gruen: gelb;
farbe = gelb: rot;
1: farbe;
-- default-Fall
esac;
MODULE main
VAR
semaphore: boolean;
zahl: 1..5;
a: ampel (b);
b: ampel (a);
c: process ampel (a);
INIT
semaphore = FALSE & zahl = 1;
-- synchroner Prozess
-- synchroner Prozess
-- asynchroner Prozess
SPEC AG (a.farbe = rot | b.farbe = rot);
SPEC AG (zahl = 3 -> AF semaphore);
-- Spezifikationen
Spezifikation in CTL:
EG p
p gilt auf (mind.)
einem Pfad immer
.
.
.
.
.
.
. .
. .
. .
.
.
.
.
.
.
.
.
.
. .
. .
. .
.
.
.
AG p
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
. .
. .
. .
.
.
.
.
.
.
.
.
.
. .
. .
. .
.
.
.
p gilt in allen
nächsten Zuständen
.
.
.
. .
. .
. .
EF p
AX p
p gilt immer
.
.
.
EX p
p gilt in (mind.) einem p gilt irgendwann auf
nächsten Zustand
(mind.) einem Pfad
.
.
.
.
.
.
Software Engineering in der Praxis
Lehrstuhl für Software Engineering
. .
. .
. .
.
.
.
.
.
.
. .
. .
. .
.
.
.
.
.
.
.
.
.
. .
. .
. .
.
.
.
.
.
.
. .
. .
. .
.
.
.
.
.
.
.
.
.
. .
. .
. .
.
.
.
AF p
p gilt irgendwann auf
jedem Pfad
.
.
.
.
.
.
. .
. .
. .
.
.
.
.
.
.
.
.
.
. .
. .
. .
.
.
.
E [p U q]
p gilt auf (mind.)
einem Pfad bis q gilt
.
.
.
.
.
.
. .
. .
. .
.
.
.
.
.
.
.
.
.
. .
. .
. .
.
.
.
A [p U q]
p gilt auf jedem Pfad
bis q gilt
.
.
.
.
.
.
. .
. .
. .
.
.
.
.
.
.
.
.
.
. .
. .
. .
.
.
.
© Copyright 2024 ExpyDoc
