verification - チャネルに関連するスピン検証プロパティ

Question

2 つのプロセス S が別のプロセス R にメッセージを送信する単純なモデルを Spin で作成しました。次に、プロセス R が両方のプロセスに応答を送信します。以下に示すように、「プロセス x がメッセージを送信した場合、プロセス y が最終的にそれを受信する」というプロパティを定義したいと思います。問題は、シミュレーションが期待どおりに機能しているにもかかわらず、検証がうまくいかないことです。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  }