Die Suche ergab 7 Treffer

von StOl
11. Dez 2012 23:19
Forum: Archiv
Thema: Counterexample angeben
Antworten: 1
Zugriffe: 236

Counterexample angeben

Hallo,

in der Aufgabenstellung 3 steht, dass man ein Gegenbeispiel angeben soll mithilfe von SPIN.
Wie funktioniert das genau?
von StOl
11. Dez 2012 22:54
Forum: Archiv
Thema: Verifizierung von claims
Antworten: 8
Zugriffe: 971

Re: Verifizierung von claims

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...
von StOl
11. Dez 2012 15:00
Forum: Archiv
Thema: Verifizierung von claims
Antworten: 8
Zugriffe: 971

Re: Verifizierung von claims

Hallo,

ich habe einen ltl Ausdruck unter den Code geschrieben, habe aber einen Äquivalenzpfeil benutzt.
von StOl
10. Dez 2012 10:50
Forum: Archiv
Thema: Verifizierung von claims
Antworten: 8
Zugriffe: 971

Verifizierung von claims

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,...
von StOl
30. Nov 2012 23:31
Forum: Archiv
Thema: hash conflicts
Antworten: 1
Zugriffe: 197

hash conflicts

Hallo,

nach der Verifikation gibt ispin folgendes aus:
hash conflicts: 23 (resolved)

Weiter unten steht das keine Fehler gefunden wurden.
Kann ich die hash conflicts ignorieren?

Vielen Dank schonmal.
von StOl
24. Nov 2012 20:35
Forum: Archiv
Thema: trail in ispin
Antworten: 1
Zugriffe: 250

trail in ispin

Hallo, ich habe eine Frage zum trail den mir (i)spin ausgibt. Ich habe das Programm verifiziert. Hier ist ein kleiner Auschnitt aus dem trail: unreached in proctype phil DiningDeadlock.pml:80, state 23, "-end-" (1 of 23 states) unreached in init (0 of 9 states) pan: elapsed time 0 seconds No errors ...
von StOl
27. Okt 2012 16:19
Forum: Archiv
Thema: SPIN
Antworten: 8
Zugriffe: 1007

Re: SPIN

Hallo, ich habe folgende Schritte getätigt: Ich habe die Datei heruntergeladen und in C: entpackt. Anschließend habe ich die Umgebungsvariable angelegt. Brauche ich weitere Dateien oder weitere Einstellugen um Spin zu laufen zu bringen? Und wie starte ich spin ohne gui überhaupt? vielen dank schonma...

Zur erweiterten Suche