Liveness -> Warum wird das verifiziert?

null
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 168
Registriert: 21. Apr 2012 14:58

Liveness -> Warum wird das verifiziert?

Beitrag von null »

Hallo zusammen,

warum verifziert das folgende Programm? Die Schleife sollte blockieren und der Prozess sollte nie das Labeln "liven" erreichen. Dennoch meckert Spin nicht rum. Warum?

Code: Alles auswählen

bool flag = false;

active proctype P() {
endX: //Deadlock legalisieren
        do
                :: flag;
                   printf("flag == true\n");
                   break;
        od;
liven: //Hier sollte P niemals hinkommen, weil er aus der Schleife nicht mehr rauskommt. 
        skip;
}
ltl liveness{<> P@liven} //wird verifiziert.
Danke und viele Grüße
null

yourmaninamsterdam
Nerd
Nerd
Beiträge: 681
Registriert: 26. Okt 2006 14:04
Kontaktdaten:

Re: Liveness -> Warum wird das verifiziert?

Beitrag von yourmaninamsterdam »

Die Frage ist: Was verifizierst du denn? Das Programm verstößt ja beispielsweise auch nicht gegen Assertions (mangels Assertions) und der Deadlock ist dank des end-Labels zulässig.

null
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 168
Registriert: 21. Apr 2012 14:58

Re: Liveness -> Warum wird das verifiziert?

Beitrag von null »

mmhh,....ich dachte eigentlich die LTL Formel :D.

null
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 168
Registriert: 21. Apr 2012 14:58

Re: Liveness -> Warum wird das verifiziert?

Beitrag von null »

Die Verifikation mache ich so:

spin -a ltlverification.pml
gcc -o pan pan.c
./pan -N liveness


Es werden keine Fehler gefunden, doch meiner Ansicht, dürfte P niemals terminieren und so nie das Label 'liven' erreichen.


2.) Auch ist mir folgendes komisches Verhalten von Spin bei Übung 3.6.b aufgefallen.

ltl positiv {[] ((count > 0) -> ((count > 0)U(mode > 1)))} --> Diese Eigenschaft erzeugt einen Fehler (error:1)
ltl positiv {[] (count > 0 -> ((count > 0)U(mode > 1)))} //Diese Eigenschaft wird verifiziert.

Wie kann es sein, dass redundante Klammern das Verifikationsergebnis beeinflussen. Für mich sind beide Ausdrücke äquivalent.

Kann mir das jemand erklären?
Danke

yourmaninamsterdam
Nerd
Nerd
Beiträge: 681
Registriert: 26. Okt 2006 14:04
Kontaktdaten:

Re: Liveness -> Warum wird das verifiziert?

Beitrag von yourmaninamsterdam »

null hat geschrieben: spin -a ltlverification.pml
gcc -o pan pan.c
./pan -N liveness
Du musst bei der Verifikation "acceptance cycles" aktivieren, um die Liveness-Eigenschaft zu prüfen:

Code: Alles auswählen

./pan -a

null
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 168
Registriert: 21. Apr 2012 14:58

Re: Liveness -> Warum wird das verifiziert?

Beitrag von null »

Ok, danke für deine Hilfe!

edit: Du musst aber auch noch -f anfügen!

Antworten

Zurück zu „Archiv“