Liveness -> Warum wird das verifiziert?

[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]

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]

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

[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]

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]

Ok, danke für deine Hilfe!

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