Seite 1 von 1

trail in ispin

Verfasst: 24. Nov 2012 20:35
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.

Re: trail in ispin

Verfasst: 24. Nov 2012 20:46
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.