Promela (ispin) застревает в конце цикла

ну, у меня есть это (это часть кода):

20  proctype Main(byte myID) {
21    do
22    ::int J=0;
23      int K=0;
24    
25      atomic{
26        requestCS[myID]=true;
27        myNum[myID]=highestNum[myID]+1;
28    }
29  
30      do
31      :: J <= NPROCS-1 ->
32        if
33          :: J != myID -> ch[J] ! request, myID, myNum[myID];
34        fi;
35        J++;
36      :: else break;
37      od;//////////////////////////////////
38  
39    
40    do
41    :: K <= NPROCS-2 ->
42      ch[myID] ?? reply, _, _;
43      K++;
44    :: else break;
45    od;
46    
47    
48    cs: critical++;
49    assert (critical==1);
50    critical--;
51    requestCS[myID]=false;
52  
53    byte N;
54       do
55       :: empty(deferred[myID]) -> break;
56          deferred [myID] ? N -> ch[N] ! reply, 0, 0;
57       od;
58    od;
59  }

на ///////////// застревает (таймаут записи), и нет пути вперед, на шаг 40, например.

это часть алгоритма Рикарта-Агравала, вот он и др.:

1   #define  NPROCS 2
2   int critical = 0;
3   byte myNum[NPROCS];
4   byte highestNum[NPROCS];
5   bool requestCS[NPROCS];
6   chan deferred[NPROCS] = [NPROCS] of {byte};
7   mtype={request, reply};
8   chan ch[NPROCS]=[NPROCS] of {mtype, byte, byte};
9   
10  init {  
11    atomic {
12      int i;
13      for (i : 0 .. NPROCS-1){
14        run Main(i);
15        run Receive(i);
16      }
17    }
18  }
19  
20  proctype Main(byte myID) {
21    do
22    ::int J=0;
23      int K=0;
24    
25      atomic{
26        requestCS[myID]=true;
27        myNum[myID]=highestNum[myID]+1;
28    }
29  
30      do
31      :: J <= NPROCS-1 ->
32        if
33          :: J != myID -> ch[J] ! request, myID, myNum[myID];
34        fi;
35        J++;
36      :: else break;
37      od;
38  
39    
40    do
41    :: K <= NPROCS-2 ->
42      ch[myID] ?? reply, _, _;
43      K++;
44    :: else break;
45    od;
46    
47    
48    cs: critical++;
49    assert (critical==1);
50    critical--;
51    requestCS[myID]=false;
52  
53    byte N;
54       do
55       :: empty(deferred[myID]) -> break;
56          deferred [myID] ? N -> ch[N] ! reply, 0, 0;
57       od;
58    od;
59  }
60  
61  proctype Receive(byte myID){
62    byte reqNum, source;
63    do
64     :: ch[myID] ?? request, source, reqNum;
65  
66       highestNum[myID] = ((reqNum > highestNum[myID]) -> reqNum : highestNum[myID]);
67  
68       atomic {
69        if
70        :: requestCS[myID] && ((myNum[myID] < reqNum) || ((myNum[myID] == reqNum) && (myID < source))) -> deferred[myID] ! source
71        :: else -> ch[source] ! reply, 0, 0;
72        fi;
73    }
74    od;
75  }

что я делаю неправильно? Заранее спасибо

P.S. Critical - критическая секция "симулятор", потому что этот алгоритм для распределенных систем...