與LTL公式

Question

考慮找到一個變量的所有可能的執行最小值操縱共享變量N兩個過程以下Promela型號：

byte N = 0; 

active [2] proctype P(){ 
    byte temp, i; 
    i = 1; 
    do 
     :: i < 10 -> 
      temp = N; 
      temp++; 
      N = temp; 
      i++; 
     :: else -> 
      break; 
    od 
} 

如何使用LTL formula找出最低當兩個進程都結束時，變量N可以具有的值？

Answer 1

一般，這是不可能的。一個LTL公式表示一個屬性，該屬性必須位於執行路徑上，而根據定義最小值，您希望在多個執行路徑上表示屬性。事實上Ñ被認爲最小僅當沒有其它執行跟蹤，其中它有一個較小值。

---

解決方法。然而，您可以通過在LTL公式上多次運行Spin來找到的最小值的N，其中N的值增加，並檢查輸出以確定正確的答案。

考慮這個例子：

byte N = 0; 

short cend = 0; 

active [2] proctype P(){ 
    byte temp, i; 
    i = 1; 
    do 
     :: i < 10 -> 
      temp = N; 
      temp++; 
      N = temp; 
      i++; 
     :: else -> 
      break; 
    od 

    cend++; 
} 

ltl p0 { [] ((cend == 2) -> 2 <= N) }; 
ltl p1 { [] ((cend == 2) -> 3 <= N) }; 

我們有兩個特性：

• p0狀態，這是全球真正，當這兩個進程終止N值至少2。這個公式是驗證：

  ~$ spin -a -search -bfs -ltl p0 m.pml 
  ... 
  Full statespace search for: 
      never claim    + (p0) 
      assertion violations + (if within scope of claim) 
      cycle checks   - (disabled by -DSAFETY) 
      invalid end states  - (disabled by never claim) 
  
  State-vector 36 byte, depth reached 98, errors: 0 
  ... 
  

• p1說，它是全球真，當這兩個進程終止的N值是至少3。這個公式是不驗證：

  ~$ spin -a -search -bfs -ltl p1 m.pml 
  ... 
  Full statespace search for: 
      never claim    + (p1) 
      assertion violations + (if within scope of claim) 
      cycle checks   - (disabled by -DSAFETY) 
      invalid end states  - (disabled by never claim) 
  
  State-vector 36 byte, depth reached 95, errors: 1 
  ... 
  

所以我們知道，N最小值等於2。

讓我們來看看反例：

~$ spin -l -g -p -t m.pml 
ltl p0: [] ((! ((cend==2))) || ((2<=N))) 
ltl p1: [] ((! ((cend==2))) || ((3<=N))) 
starting claim 2 
using statement merging 
    1: proc 1 (P:1) m.pml:7 (state 1) [i = 1] 
     P(1):i = 1 
    2: proc 1 (P:1) m.pml:9 (state 2) [((i<10))] 
    3: proc 0 (P:1) m.pml:7 (state 1) [i = 1] 
     P(0):i = 1 
    4: proc 0 (P:1) m.pml:9 (state 2) [((i<10))] 
    5: proc 1 (P:1) m.pml:10 (state 3) [temp = N] 
     P(1):temp = 0 
    6: proc 1 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(1):temp = 1 
    7: proc 0 (P:1) m.pml:10 (state 3) [temp = N] 
     P(0):temp = 0 
    8: proc 0 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(0):temp = 1 
    9: proc 1 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 1 
10: proc 1 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(1):i = 2 
11: proc 1 (P:1) m.pml:9 (state 2) [((i<10))] 
12: proc 1 (P:1) m.pml:10 (state 3) [temp = N] 
     P(1):temp = 1 
13: proc 1 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(1):temp = 2 
14: proc 1 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 2 
15: proc 1 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(1):i = 3 
16: proc 1 (P:1) m.pml:9 (state 2) [((i<10))] 
17: proc 1 (P:1) m.pml:10 (state 3) [temp = N] 
     P(1):temp = 2 
18: proc 1 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(1):temp = 3 
19: proc 1 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 3 
20: proc 1 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(1):i = 4 
21: proc 1 (P:1) m.pml:9 (state 2) [((i<10))] 
22: proc 1 (P:1) m.pml:10 (state 3) [temp = N] 
     P(1):temp = 3 
23: proc 1 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(1):temp = 4 
24: proc 1 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 4 
25: proc 1 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(1):i = 5 
26: proc 1 (P:1) m.pml:9 (state 2) [((i<10))] 
27: proc 1 (P:1) m.pml:10 (state 3) [temp = N] 
     P(1):temp = 4 
28: proc 1 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(1):temp = 5 
29: proc 1 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 5 
30: proc 1 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(1):i = 6 
31: proc 1 (P:1) m.pml:9 (state 2) [((i<10))] 
32: proc 1 (P:1) m.pml:10 (state 3) [temp = N] 
     P(1):temp = 5 
33: proc 1 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(1):temp = 6 
34: proc 1 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 6 
35: proc 1 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(1):i = 7 
36: proc 1 (P:1) m.pml:9 (state 2) [((i<10))] 
37: proc 1 (P:1) m.pml:10 (state 3) [temp = N] 
     P(1):temp = 6 
38: proc 1 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(1):temp = 7 
39: proc 1 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 7 
40: proc 1 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(1):i = 8 
41: proc 1 (P:1) m.pml:9 (state 2) [((i<10))] 
42: proc 1 (P:1) m.pml:10 (state 3) [temp = N] 
     P(1):temp = 7 
43: proc 1 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(1):temp = 8 
44: proc 1 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 8 
45: proc 1 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(1):i = 9 
46: proc 1 (P:1) m.pml:9 (state 2) [((i<10))] 
47: proc 0 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 1 
48: proc 0 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(0):i = 2 
49: proc 0 (P:1) m.pml:9 (state 2) [((i<10))] 
50: proc 1 (P:1) m.pml:10 (state 3) [temp = N] 
     P(1):temp = 1 
51: proc 1 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(1):temp = 2 
52: proc 0 (P:1) m.pml:10 (state 3) [temp = N] 
     P(0):temp = 1 
53: proc 0 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(0):temp = 2 
54: proc 0 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 2 
55: proc 0 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(0):i = 3 
56: proc 0 (P:1) m.pml:9 (state 2) [((i<10))] 
57: proc 0 (P:1) m.pml:10 (state 3) [temp = N] 
     P(0):temp = 2 
58: proc 0 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(0):temp = 3 
59: proc 0 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 3 
60: proc 0 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(0):i = 4 
61: proc 0 (P:1) m.pml:9 (state 2) [((i<10))] 
62: proc 0 (P:1) m.pml:10 (state 3) [temp = N] 
     P(0):temp = 3 
63: proc 0 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(0):temp = 4 
64: proc 0 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 4 
65: proc 0 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(0):i = 5 
66: proc 0 (P:1) m.pml:9 (state 2) [((i<10))] 
67: proc 0 (P:1) m.pml:10 (state 3) [temp = N] 
     P(0):temp = 4 
68: proc 0 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(0):temp = 5 
69: proc 0 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 5 
70: proc 0 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(0):i = 6 
71: proc 0 (P:1) m.pml:9 (state 2) [((i<10))] 
72: proc 0 (P:1) m.pml:10 (state 3) [temp = N] 
     P(0):temp = 5 
73: proc 0 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(0):temp = 6 
74: proc 0 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 6 
75: proc 0 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(0):i = 7 
76: proc 0 (P:1) m.pml:9 (state 2) [((i<10))] 
77: proc 0 (P:1) m.pml:10 (state 3) [temp = N] 
     P(0):temp = 6 
78: proc 0 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(0):temp = 7 
79: proc 0 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 7 
80: proc 0 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(0):i = 8 
81: proc 0 (P:1) m.pml:9 (state 2) [((i<10))] 
82: proc 0 (P:1) m.pml:10 (state 3) [temp = N] 
     P(0):temp = 7 
83: proc 0 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(0):temp = 8 
84: proc 0 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 8 
85: proc 0 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(0):i = 9 
86: proc 0 (P:1) m.pml:9 (state 2) [((i<10))] 
87: proc 0 (P:1) m.pml:10 (state 3) [temp = N] 
     P(0):temp = 8 
88: proc 0 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(0):temp = 9 
89: proc 0 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 9 
90: proc 0 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(0):i = 10 
91: proc 0 (P:1) m.pml:14 (state 7) [else] 
92: proc 1 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 2 
93: proc 1 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(1):i = 10 
94: proc 1 (P:1) m.pml:14 (state 7) [else] 
95: proc 0 (P:1) m.pml:17 (state 12) [cend = (cend+1)] 
     cend = 1 
96: proc 1 (P:1) m.pml:17 (state 12) [cend = (cend+1)] 
     cend = 2 
spin: trail ends after 96 steps 
#processes: 2 
     N = 2 
     cend = 2 
96: proc 1 (P:1) m.pml:18 (state 13) <valid end state> 
96: proc 0 (P:1) m.pml:18 (state 13) <valid end state> 
96: proc - (p1:1) _spin_nvr.tmp:11 (state 6) 
2 processes created 

正如你所看到的，反例對應於執行，其中：

• proc0存儲值N = 0爲temp和然後停止執行任何指令
• proc1遞增值N爲8倍
• proc0復位的N回1
• proc1拷貝N = 1在temp的值，然後停止執行任何指令
• proc0增量N高達9，然後終止
• proc1復位的值N回到2然後終止