Promela SPIN unreached in proctype error

Question

I'm pretty new to SPIN and Promela and I came across this error when I'm trying to verify the liveness property in my models.

Error code:

unreached in proctype P
        (0 of 29 states)
unreached in proctype monitor
        mutex_assert.pml:39, state 1, "assert(!((mutex>1)))"
        mutex_assert.pml:42, state 2, "-end-"
        (2 of 2 states)
unreached in init
        (0 of 3 states)
unreached in claim ltl_0
        _spin_nvr.tmp:10, state 13, "-end-"
        (1 of 13 states)

pan: elapsed time 0 seconds

The code is basically an implementation of Peterson's algorithm and I checked for safety and it seems to be valid. But whenever I try to validate the liveness property using the ltl {[]((wait -> <> (cs)))}, it comes up with the above errors. I'm not sure what they mean so I don't know how to proceed...

My code is as follows:

#define N 3
#define wait   (P[1]@WAIT)
#define cs     (P[1]@CRITICAL)

int pos[N]; 
int step[N]; 
int enter;
byte mutex;
ltl {[]((wait -> <> (cs)))}

proctype P(int i) {
  int t;
  int k;
  WAIT:
  for (t : 1 .. (N-1)){
  pos[i] = t
  step[t] = i
  k = 0;
  do
  ::  atomic {(k != i && k < N && (pos[k] < t|| step[t] != i)) -> k++}
  ::  atomic {k == i -> k++}
  ::  atomic {k == N -> break}
  od;
  }

CRITICAL:
  atomic {mutex++;
  printf("MSC: P(%d) HAS ENTERED THE CRITICAL SECTION.\n", i);
  mutex--;}
  pos[i] = 0;
}

init {
  atomic { run P(0); }
}

Answer 1

General Answer

This is a warning telling you that some states are unreachable due to transitions that are never taken.

In general, this is not an error, but it is a good practice to take a close look to the unreachable states for every routine that you modelled, and check that you expect none of them to be reachable. i.e. in the case the model is not correct wrt. the intended behaviour.

Note. You can use the label end: in front of a particular line of code to mark valid terminating states, so to get rid of those warnings, e.g. when your procedure does not terminate. More info here.

---

Specific Answer

I can not reproduce your output. In particular, by running

~$ spin -a file.pml
~$ gcc pan.c
~$ ./a.out -a

I get the following output, which is different from yours:

(Spin Version 6.4.3 -- 16 December 2014)
    + Partial Order Reduction

Full statespace search for:
    never claim             + (ltl_0)
    assertion violations    + (if within scope of claim)
    acceptance   cycles     + (fairness disabled)
    invalid end states  - (disabled by never claim)

State-vector 64 byte, depth reached 47, errors: 0
       41 states, stored (58 visited)
       18 states, matched
       76 transitions (= visited+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.004   equivalent memory usage for states (stored*(State-vector + overhead))
    0.288   actual memory usage for states
  128.000   memory used for hash table (-w24)
    0.534   memory used for DFS stack (-m10000)
  128.730   total actual memory usage


unreached in proctype P
    (0 of 29 states)
unreached in init
    (0 of 3 states)
unreached in claim ltl_0
    _spin_nvr.tmp:10, state 13, "-end-"
    (1 of 13 states)

pan: elapsed time 0 seconds

In particular, I lack the warnings about the unreached states in the monitor process. As far as I am concerned, juding from the source code, none of the warnings I obtained is problematic.

Either you are using a different version of Spin than me, or you did not include the full source code in your question. In the latter case, could you edit your question and add the code? I'll update my answer afterwards.

---

EDIT: in the comments, you ask what does the following message mean: "unreached in claim ltl_0 _spin_nvr.tmp:10, state 13, "-end-"".

If you open the file _spin_nvr.tmp, you can see the following piece of Promela code, which corresponds to a Büchi automaton that accepts all and only the execution which violate your ltl property []((wait -> <> (cs))).

never ltl_0 {    /* !([] ((! ((P[1]@WAIT))) || (<> ((P[1]@CRITICAL))))) */
T0_init:
    do
    :: (! ((! ((P[1]@WAIT)))) && ! (((P[1]@CRITICAL)))) -> goto accept_S4
    :: (1) -> goto T0_init
    od;
accept_S4:
    do
    :: (! (((P[1]@CRITICAL)))) -> goto accept_S4
    od;
}

The message simply warns you that the execution of this code will never reach the last closing bracket } (state "-end-"), meaning that the procedure does never terminate.