trail in ispin

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

trail in ispin

Beitrag von StOl »

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 found -- did you verify all claims?

Was bedeutet unreached (1 of 23)? Kann ich das ignorieren oder ist es ein Fehler?

Vielen Dank schonmal.

dschneid
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 271
Registriert: 14. Dez 2009 00:56

Re: trail in ispin

Beitrag von dschneid »

Das bedeutet, dass der Endzustand im Prozess phil nie erreicht werden kann. Da die Philosophen aber in einer Endlosschleife essen und denken, ist das ja nur logisch.

Antworten

Zurück zu „Archiv“