Verifizierung von claims

StOl
Neuling
Neuling
Beiträge: 7
Registriert: 16. Okt 2011 17:48

Verifizierung von claims

Beitrag von StOl »

Hallo,

nach der Verifizierung der ersten Eigenschaft wurde mir folgendes ausgegeben:
unreached in proctype Alice
(0 of 15 states)
unreached in proctype Bob
(0 of 14 states)
unreached in proctype Intruder
Alice.pml:146, state 38, "-end-"
(1 of 38 states)
unreached in claim a
_spin_nvr.tmp:8, state 9, "(((!(statusB)&&statusA)||(!(statusA)&&statusB)))"
_spin_nvr.tmp:10, state 11, "-end-"
(2 of 11 states)

Bedeutet, dass das der Claim erfüllt worden ist bzw. der never claim nicht erfüllt worden ist.
Danke im Voraus

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Verifizierung von claims

Beitrag von Nathan Wasser »

Das bedeutet erstmal nur, dass bestimmte Zustände nicht erreicht worden sind. Das kann in Ordnung sein, kann auch auf Fehler hinweisen. Schau im Code nach, ob es in Ordnung ist, das dieser Zustand nie erreicht wird.
unreached in claim a
_spin_nvr.tmp:8, state 9, "(((!(statusB)&&statusA)||(!(statusA)&&statusB)))"
Das aber sieht etwas suspekt aus. Benutzt du ltl Blöcke? Ich vermute nicht, da hier sehr wahrscheinlich ein "->" als Trennung zweier Statements gelesen wird, statt als Implikation. Sonst ergibt diese Warnung wegen einem unerreichten Zustand wenig Sinn.

StOl
Neuling
Neuling
Beiträge: 7
Registriert: 16. Okt 2011 17:48

Re: Verifizierung von claims

Beitrag von StOl »

Hallo,

ich habe einen ltl Ausdruck unter den Code geschrieben, habe aber einen Äquivalenzpfeil benutzt.

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Verifizierung von claims

Beitrag von Nathan Wasser »

Suche eventuell einen Tutor in seiner Sprechstunde auf. Ich kann mit deinen Angaben von der Ferne nicht wirklich viel anfangen.

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

Re: Verifizierung von claims

Beitrag von yourmaninamsterdam »

Kann es sein, dass spin ltl-Blöcke erst in Never-Claims umschreibt, die dann auch in eventuellen Fehlermeldungen auftauchen (und nicht die LTLs). Sieht hier aber tatsächlich so aus, als sei irgendwas in deiner LTL generell unzutreffend (daher "unreached"). Prüf mal die Semantik von Programm und LTL, insbesondere die Übereinstimmung von Modell mit zu beweisender Eigenschaft.

StOl
Neuling
Neuling
Beiträge: 7
Registriert: 16. Okt 2011 17:48

Re: Verifizierung von claims

Beitrag von StOl »

yourmaninamsterdam hat geschrieben:Kann es sein, dass spin ltl-Blöcke erst in Never-Claims umschreibt, die dann auch in eventuellen Fehlermeldungen auftauchen (und nicht die LTLs). Sieht hier aber tatsächlich so aus, als sei irgendwas in deiner LTL generell unzutreffend (daher "unreached"). Prüf mal die Semantik von Programm und LTL, insbesondere die Übereinstimmung von Modell mit zu beweisender Eigenschaft.

Hallo,

danke für die Antwort. Ich habe den claim überarbeitet.
Die temporallogische Formel ist nun nicht mehr zu sehen.
Allerdings gibt es nach wie vor folgende Meldung:

unreached in proctype Alice
(0 of 16 states)
unreached in proctype Bob
(0 of 13 states)
unreached in claim a
_spin_nvr.tmp:10, state 11, "-end-"
(1 of 11 states)

Hatte jemand hier bereits so eine Meldung?

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

Re: Verifizierung von claims

Beitrag von yourmaninamsterdam »

Ich habe den Verdacht, dass das okay und normal ist, dass der Endzustand im Claim nicht erreicht wird. Kann irgendwer das bestätigen oder widerlegen?

Benutzeravatar
slashafk
Erstie
Erstie
Beiträge: 19
Registriert: 7. Mär 2011 13:18

Re: Verifizierung von claims

Beitrag von slashafk »

Never claim translated into special Promela process with accept labels
If one of these reached infinitely often, the claim is disproved
Ich glaube, es ist ok so. NC Prozess bleibt quasi hängen, Label wird nicht unendlichoft erreicht, also stimmt die Aussage.
So hab ichs mir zumindest zusammengereimt.

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Verifizierung von claims

Beitrag von Nathan Wasser »

Unreached end states wird in iSpin bei never claims prinzipiell ausgeschaltet, dafür gibt es vermutlich einen Grund. :)

Antworten

Zurück zu „Archiv“