自旋验证与通道相关的属性

Question

我在 Spin 中创建了一个简单的模型，其中两个进程 S 向另一个进程 R 发送消息。然后进程 R 向两个进程发送响应。我想定义属性 "if process x sends a message, then process y eventually receives it"，如下所示。问题在于，尽管模拟按预期工作，但验证并非如此。我在第 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被声明在内部块中。每次在stoR?c, m2之前初始化为0。因此，引用 r:m 将在收到两次消息后始终为 0。

所以，<>(s[s1PId]:m == r:m) 将永远是 true。

要快速修复此问题，您可以 (i) 将 r 中的声明 byte m 移到循环外；或 (ii) 在 s 中添加一个无限循环以防止其终止。

自旋验证与通道相关的属性

Spin verifying properties related to channels

verification

spin