Спин, проверяющий свойства, связанные с каналами

Question

Я создал простую модель в Spin, в которой два процесса S отправляют сообщения другому процессу R. Процесс R затем отправляет ответы на оба процесса. Я хотел бы определить свойство «если процесс х отправляет сообщение, а затем обрабатывает его в конечном итоге», как показано ниже. Проблема в том, что, хотя симуляция работает, как ожидалось, проверка не выполняется. Свойство, которое я определил в строке 9, всегда проходит без ошибок, хотя я ввел ошибку в строку 17, которая должна сделать проверку неудачной. Я что-то упустил?

1 byte r1PId; 
2 byte s1PId; 
3 byte s2PId; 
4 
5 byte nextM = 1; 
6 
7 chan toS[2] = [2] of {byte}; 
8 
9 ltl p1 {[] ((s[s1PId]:m > 0) -> <>(s[s1PId]:m == r:m))} 
10 
11 proctype r(byte id; chan stoR) 
12 { 
13  do 
14  :: true 
15  byte c; byte m; byte m2; 
16  stoR?c, m2; 
17  m = 67; //should be m = m2 
18 
19  byte response = 50; 
20 
21  toS[c]!response; 
22  od 
23 } 
24 
25 proctype s(byte id; chan rtoS; chan stoR) 
26 { 
27  byte m; 
28  atomic 
29  { 
30   m = nextM; 
31   nextM = nextM+1; 
32  } 
33  stoR!id, m; 
34  byte response; 
35  rtoS?response; 
36 } 
37 
38 init{ 
39  chan toR = [10] of {byte, byte}; 
40  r1PId = run r(10, toR); 
41  s1PId = run s(0, toS[0], toR); 
42  s2PId = run s(1, toS[1], toR); 
43 } 

Answer 1

Похоже, проблема с объемом. Когда процесс s завершается, его локальные переменные будут недоступны. В этом случае ссылка s[s1PId]:m будет 0.

С другой стороны, в процессе r, переменная m объявляется внутри блока. Он инициализируется до 0 каждый раз перед stoR?c, m2. В результате ссылка r:m всегда будет 0 после получения сообщений дважды.

Таким образом, <>(s[s1PId]:m == r:m) всегда будет true.

Чтобы быстро исправить это, вы можете (i) переместить объявление byte m в r вне цикла; или (ii) добавить бесконечный цикл в s, чтобы предотвратить его завершение.