Verifizierung von claims

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

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]

Hallo,

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

[Nathan Wasser]

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

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

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]

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?

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

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