A ping-pong linear temporal logic never claim in promela that fails to verify

ping_pong_ltl_claim

mtype = { PING , PONG , INFO } ;

typedef Node {
  chan inChan = [50] of {mtype } ;
  bool receivedInfo;
};
Node nodes[2];

active proctype Master()  {
  
  run Slave(0, nodes[1].inChan);
  run Slave(1, nodes[0].inChan);
  
  if
    :: nodes[0].inChan ! INFO
    :: nodes[1].inChan ! INFO
  fi
}  

proctype Slave(int me; chan other) {
  
  nodes[me].receivedInfo = false;
  bool waitingPong = false ;  
  
  do
    :: !waitingPong -> other ! PING ; waitingPong = true ;
    :: nodes[me].inChan ? PING ->     waitingPong = false ;
    :: nodes[me].inChan ? INFO ->     nodes[me].receivedInfo = true;
  od ;

} 

#define one_info_received ( nodes[0].receivedInfo + nodes[1].receivedInfo  == 1)

never  {    /* ! [] <> one_info_received */
T0_init:
  if
    :: (! ((one_info_received))) -> goto accept_S4
    :: (1) -> goto T0_init
  fi;
accept_S4:
  if
    :: (! ((one_info_received))) -> goto accept_S4
  fi;
}




///////////////////////////////////
// Output from verifying this never claim
///////////////////////////////////
/*
spin -a  demo2.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DNP -w -o pan pan.c
./pan -m10000  -l
Pid: 10793
pan:1: non-progress cycle (at depth 18)
pan: wrote demo2.pml.trail

(Spin Version 6.2.3 -- 24 October 2012)
Warning: Search not completed
  + Partial Order Reduction

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

State-vector 144 byte, depth reached 37, errors: 1
       19 states, stored
        0 states, matched
       19 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.003	equivalent memory usage for states (stored*(State-vector + overhead))
    0.290	actual memory usage for states
   64.000	memory used for hash table (-w24)
    0.343	memory used for DFS stack (-m10000)
   64.539	total actual memory usage
*/