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.

---

This documentation is relevant.

• accept labels
• end labels
• progress labels

An end label by itself may not solve this issue. If by chance you have an accept label prefix, you can still get mysterious verification messages. For example, a connection oriented protocol might naively use an accept label. These labels are special to the verification mode of spin (as are other features like trace, never, etc). In some ways, this is a little unfortunate as goto label; is a model or simulation property. The labels end, progress and accept are dual purpose for both simulation and verification of models.

So if you are new to spin, be aware that 'labels' should not use these prefixes (unless of course, you known and understand the verification implications). For a connection oriented interface, labels like open, active, and close (or other alternatives) should be used over open, accept and end.