自旋验证，验证变量达到一定的数值​​

Question

这是我在Stack Exchange上的第一个问题，所以如果有任何违规指标，请告诉我。

我有一个用Promela编写的大学OS和并发系统课程。有两个进程正在运行，增加一个变量n。我们的任务是编写这些流程，然后使用Spin中的验证工具来证明n有可能获得值4.我已经通读了所有的命令行参数，但是没有任何结果对我来说，“插入这个修饰符后跟一个变量名来检查所有可能的值。”

byte n; 

proctype p() 
{ 
    byte countp = 0; 
    byte temp; 
    do 
    :: countp != 2 -> temp = n; temp = temp + 1; n = temp; countp = countp + 1; 
    :: countp >= 2 -> break; 
    od 
} 

proctype q() 
{ 

    byte countq = 0; 

    do 
    :: countq != 2 -> n = n + 1; countq = countq + 1; 
    :: countq >= 2 -> break; 
    od 
} 

init 
{ 
    run p(); 
    run q(); 
} 

Answer 1

有几种方式做到这一点，但作为一名教师，我宁愿基于一个零担，因为至少它表明你了解如何使用它。

---

监视过程。

这是迄今为止最简单的概念：您只需添加一个过程，随时声明n != 4，然后检查这个断言是否最终会失败。

byte n; 

active proctype p() 
{ 
    byte countp = 0; 
    byte temp; 
    do 
    :: countp != 2 -> temp = n; temp = temp + 1; n = temp; countp = countp + 1; 
    :: countp >= 2 -> break; 
    od 
} 

active proctype q() 
{ 

    byte countq = 0; 

    do 
    :: countq != 2 -> n = n + 1; countq = countq + 1; 
    :: countq >= 2 -> break; 
    od 
} 

active proctype monitor() 
{ 
    do 
     :: true -> assert(n != 4); 
    od; 
} 

注：在监控过程中的循环是完全不必要的，但它使得它的目的更加清晰初学者。

您可以用下面的衬板验证此程序：

~$ spin -search -bfs buggy_01.pml 

自旋发现在零时间一个反例：

Depth=10 States=56 Transitions=84 Memory=128.195  
pan:1: assertion violated (n!=4) (at depth 19) 
pan: wrote buggy_01.pml.trail 

(Spin Version 6.4.3 -- 16 December 2014) 
Warning: Search not completed 
    + Breadth-First Search 
    + Partial Order Reduction 

Full statespace search for: 
    never claim    - (none specified) 
    assertion violations + 
    cycle checks   - (disabled by -DSAFETY) 
    invalid end states  + 

State-vector 28 byte, depth reached 19, errors: 1 
     215 states, stored 
      215 nominal states (stored-atomic) 
     181 states, matched 
     396 transitions (= stored+matched) 
     0 atomic steps 
hash conflicts:   0 (resolved) 

Stats on memory usage (in Megabytes): 
    0.011  equivalent memory usage for states (stored*(State-vector + overhead)) 
    0.290  actual memory usage for states 
    128.000  memory used for hash table (-w24) 
    128.195  total actual memory usage 

pan: elapsed time 0 seconds 

实际上，你可以检查执行跟踪这违反了以下断言：

~$ spin -t -p -g -l buggy_01.pml 

个

的选项具有以下含义：

• -t：重播通过旋
• -p产生的.trail反例：打印所有报表
• -g：打印所有的全局变量
• -l：打印所有局部变量

这是输出：

using statement merging 
    1: proc 2 (monitor:1) buggy_01.pml:27 (state 1) [(1)] 
    2: proc 1 (q:1) buggy_01.pml:19 (state 1) [((countq!=2))] 
    3: proc 0 (p:1) buggy_01.pml:8 (state 1) [((countp!=2))] 
    4: proc 1 (q:1) buggy_01.pml:19 (state 2) [n = (n+1)] 
     n = 1 
    5: proc 1 (q:1) buggy_01.pml:19 (state 3) [countq = (countq+1)] 
     q(1):countq = 1 
    6: proc 1 (q:1) buggy_01.pml:19 (state 1) [((countq!=2))] 
    7: proc 1 (q:1) buggy_01.pml:19 (state 2) [n = (n+1)] 
     n = 2 
    8: proc 1 (q:1) buggy_01.pml:19 (state 3) [countq = (countq+1)] 
     q(1):countq = 2 
    9: proc 1 (q:1) buggy_01.pml:20 (state 4) [((countq>=2))] 
10: proc 0 (p:1) buggy_01.pml:8 (state 2) [temp = n] 
     p(0):temp = 2 
11: proc 0 (p:1) buggy_01.pml:8 (state 3) [temp = (temp+1)] 
     p(0):temp = 3 
12: proc 0 (p:1) buggy_01.pml:8 (state 4) [n = temp] 
     n = 3 
13: proc 0 (p:1) buggy_01.pml:8 (state 5) [countp = (countp+1)] 
     p(0):countp = 1 
14: proc 0 (p:1) buggy_01.pml:8 (state 1) [((countp!=2))] 
15: proc 0 (p:1) buggy_01.pml:8 (state 2) [temp = n] 
     p(0):temp = 3 
16: proc 0 (p:1) buggy_01.pml:8 (state 3) [temp = (temp+1)] 
     p(0):temp = 4 
17: proc 0 (p:1) buggy_01.pml:8 (state 4) [n = temp] 
     n = 4 
18: proc 0 (p:1) buggy_01.pml:8 (state 5) [countp = (countp+1)] 
     p(0):countp = 2 
19: proc 0 (p:1) buggy_01.pml:9 (state 6) [((countp>=2))] 
spin: buggy_01.pml:27, Error: assertion violated 
spin: text of failed assertion: assert((n!=4)) 
20: proc 2 (monitor:1) buggy_01.pml:27 (state 2) [assert((n!=4))] 
spin: trail ends after 20 steps 
#processes: 3 
     n = 4 
20: proc 2 (monitor:1) buggy_01.pml:26 (state 3) 
20: proc 1 (q:1) buggy_01.pml:22 (state 9) <valid end state> 
20: proc 0 (p:1) buggy_01.pml:11 (state 11) <valid end state> 
3 processes created 

如您所见，它报告（一）导致断言违规的可能执行痕迹。

---

LTL。

人能想到几个LTL性质，可以帮助验证n是否最终会等于4。一种这样的性质，是[] (n != 4)，其内容为：

从初始状态开始，在每个可到达状态沿着所有外出路径它始终是true即n是从4不同。

新的模式是这样的：

byte n; 

active proctype p() 
{ 
    byte countp = 0; 
    byte temp; 
    do 
    :: countp != 2 -> temp = n; temp = temp + 1; n = temp; countp = countp + 1; 
    :: countp >= 2 -> break; 
    od 
} 

active proctype q() 
{ 

    byte countq = 0; 

    do 
    :: countq != 2 -> n = n + 1; countq = countq + 1; 
    :: countq >= 2 -> break; 
    od 
} 

ltl p0 { [] (n != 4) } 

你，你会这样的断言几乎以同样的方式验证该属性。为了保持这个答案总之，我不会复制和粘贴在这里，整个输出，只是列出所用的命令：

~$ spin -search -bfs buggy_02.pml 
ltl p0: [] ((n!=4)) 
Depth=10 States=40 Transitions=40 Memory=128.195  
pan:1: assertion violated !(!((n!=4))) (at depth 15) 
pan: wrote buggy_02.pml.trail 

... 

Full statespace search for: 
    never claim    + (p0) 
    ... 
State-vector 28 byte, depth reached 15, errors: 1 
... 

~$ spin -t -p -g -l buggy_02.pml 
... 

---

如果你想保证n总是最终等于4 ，那么您应该查看一些互斥方法来保护您的关键部分或者替代地检查documentation的d_step {}。