Seite 1 von 1

Verifizierung von claims

Verfasst: 10. Dez 2012 10:50
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

Re: Verifizierung von claims

Verfasst: 11. Dez 2012 12:36
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.

Re: Verifizierung von claims

Verfasst: 11. Dez 2012 15:00
von StOl
Hallo,

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

Re: Verifizierung von claims

Verfasst: 11. Dez 2012 16:13
von Nathan Wasser
Suche eventuell einen Tutor in seiner Sprechstunde auf. Ich kann mit deinen Angaben von der Ferne nicht wirklich viel anfangen.

Re: Verifizierung von claims

Verfasst: 11. Dez 2012 16:39
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.

Re: Verifizierung von claims

Verfasst: 11. Dez 2012 22:54
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?

Re: Verifizierung von claims

Verfasst: 12. Dez 2012 14:54
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?

Re: Verifizierung von claims

Verfasst: 12. Dez 2012 16:45
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.

Re: Verifizierung von claims

Verfasst: 12. Dez 2012 17:14
von Nathan Wasser
Unreached end states wird in iSpin bei never claims prinzipiell ausgeschaltet, dafür gibt es vermutlich einen Grund. :)