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.
null