Spin unreached in proctype "-end-"

Question

I'm pretty new at spin model checking and wanted to know what this error means:

unreached in proctype P1
    ex2.pml:16, state 11, "-end-"
    (1 of 11 states)
unreached in proctype P2
    ex2.pml:29, state 11, "-end-"
    (1 of 11 states)

here is my code:

int y1, y2;
byte insideCritical;

active proctype P1(){
do
    ::true->
        y2 = y1 + 1;
        (y1 == 0 || y2 < y1);
        /* Entering critical section */
            insideCritical++;
            assert(insideCritical < 2);
            insideCritical--;
        /* Exiting critical section */
        y2 = 0;
od
}
active proctype P2(){
do
    ::true->
        y1 = y2 + 1;
        (y2 == 0 || y1 < y2);
        /* Entering critical section */
            insideCritical++;
            assert(insideCritical < 2);
            insideCritical--;
        /* Exiting critical section */
        y1 = 0;
od
}

It actually doesn't have to end, it is a mutual exclusion program that checks if the two processes aren't at the critical section together. Does the error means that the program doesn't end? Thanks!

Answer 1

Spin informs you that your proctypes never reach the "end" state, which is of course true since they consist of endless loops. If this was not intended behavior, it would be a useful information. In your case, however, you might just tell Spin that the program is allowed to end in the state corresponding to the do-loop by adding an end label to your code, e.g.:

active proctype P1(){
  endHere:
  do
  :: true->
    y2 = y1 + 1;
    (y1 == 0 || y2 < y1);
    /* Entering critical section */
        insideCritical++;
        assert(insideCritical < 2);
        insideCritical--;
    /* Exiting critical section */
    y2 = 0;
  od
}

An end label is any label starting with "end". If your proctype ends in a state marked in such a way, Spin will not show you those warnings.

Answer 2

The checked answer is a good one; it is good form to be explicit by adding an end label appropriately. However, it is not always possible to do that and thus you can quiet SPIN by running the pan verification with the -n flag:

-n : no listing of unreached states at the end of the run