Why SPIN cannot detect non-progress loop here?

Consider this Promela code:

byte x=2;
active proctype A() {
  do  
  :: x = 3-x
  od  
}
active proctype B() {
  do  
  :: x = 3-x 
  od                                                                                                                          
}

being compiled as gcc -DNP -o my pan.c and run as ./my -l sure SPIN reports non-progress loop. If I change the process A to:

active proctype A() {
  do  
  :: x = 3-x; progress: skip
  od  
}

when I run it in mode ./my -l -f (-f for fair distribution of CPU ticks), sure non-progress loop disappears - at least one process will progress (during fair scheduling) and non-progress loop will be detected in ./my -l mode. OK.

But now I change only A process to:

active proctype A() {
progress:
  do  
  :: x = 3-x
  od  
}

and now both run modes: ./my -l and ./my -l -f don't detect any non-progress loops! This is my question - why?

I have only 2 suggestions:

1. either it's bug in SPIN
2. or both processes share common FSM (and a state) and I marked WHOLE this common state of the common FSM as always-in-progress

BTW, the FSM diagram is (generated with ./my -D):

digraph p_A {
size="8,10";
  GT [shape=box,style=dotted,label="A"];
  GT -> S2;
        S2 -> S2  [color=black,style=bold,label="x = (3-x)"];
  S2 [color=green,style=bold];
digraph p_B {
size="8,10";
  GT [shape=box,style=dotted,label="B"];
  GT -> S2;
        S2 -> S2  [color=black,style=bold,label="x = (3-x)"];

where I see only one state - S2.

There's only one state in process A, with a self-loop for the transition. That one state is part of the global system state, which now marks all executions as progress. Therefore, there will be no non-progress cycles.