Testing the LTL Model Using Spin and Promela Syntax

I am trying to reproduce the ALGOL 60 code written by Dijkstra in a document called "Sharing sequential processes", the code is the first attempt to solve the mutex problem, here is the syntax:

begin integer turn; turn:= 1;
      parbegin
      process 1: begin Ll: if turn = 2 then goto Ll;
                           critical section 1;
                           turn:= 2;
                           remainder of cycle 1; goto L1
                 end;
      process 2: begin L2: if turn = 1 then goto L2;
                           critical section 2;
                           turn:= 1;
                           remainder of cycle 2; goto L2
                  end
      parend
end 

So, I tried to reproduce the above code in Promela, and here is my code:

#define true    1
#define Aturn true
#define Bturn false

bool turn, status;

active proctype A()
{   
    L1: (turn == 1); 
    status = Aturn;
    goto L1;
    /* critical section */
    turn = 1;

}

active proctype B()
{   
    L2: (turn == 2); 
    status = Bturn;
    goto L2;
    /* critical section */
    turn = 2;
}

never{ /* ![]p */ 
    if
    :: (!status) -> skip
    fi;
}

init
{   turn = 1;
    run A(); run B();
}

What I'm trying to do is make sure that the property of justice will never be fulfilled, because the label L1 works endlessly.

The problem is that my block never claims to be an error, the result I get simply says that my statement was never reached.

here is the actual output of iSpin

spin -a  dekker.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -w -o pan pan.c
./pan -m10000 
Pid: 46025

(Spin Version 6.2.3 -- 24 October 2012)
    + Partial Order Reduction

Full statespace search for:
    never claim             - (not selected)
    assertion violations    +
    cycle checks        - (disabled by -DSAFETY)
    invalid end states  +

State-vector 44 byte, depth reached 8, errors: 0
       11 states, stored
        9 states, matched
       20 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.001   equivalent memory usage for states (stored*(State-vector + overhead))
    0.291   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 A
    dekker.pml:13, state 4, "turn = 1"
    dekker.pml:15, state 5, "-end-"
    (2 of 5 states)
unreached in proctype B
    dekker.pml:20, state 2, "status = 0"
    dekker.pml:23, state 4, "turn = 2"
    dekker.pml:24, state 5, "-end-"
    (3 of 5 states)
unreached in claim never_0
    dekker.pml:30, state 5, "-end-"
    (1 of 5 states)
unreached in init
    (0 of 4 states)

pan: elapsed time 0 seconds
No errors found -- did you verify all claims?

never{..}, ( ), ltl{..} (), , , init proctypes, - ?