Promela共有変数を操作する次の 2 つのプロセスのモデルを考えてみましょうN。
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
一般に、それは不可能です。LTL 数式は、実行パスにわたって保持する必要があるプロパティを表しますが、最小の定義により、複数の実行パスにわたってプロパティを表現する必要があります。実際、 Nは、それより小さい値を持つ実行トレースが他にない場合にのみ、最小と見なされます。
回避策。ただし、 の値を増加させながら式を複数回実行することで の最小値を見つけ、出力を調べて正しい答えを決定することができます。NSpinLTLN
次の例を検討してください。
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) };
2 つのプロパティがあります。
p0は、両方のプロセスが終了したときに の値が少なくともであることがグローバルに真であると述べています。この式が検証されます。N2
~$ 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は、両方のプロセスが終了したときに の値が少なくともであることがグローバルに真であると述べています。この式は検証されていません:N3
~$ 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
ご覧のとおり、反例は次の実行に対応しています。
proc0N = 0値を格納し、temp命令の実行を停止しますproc1Nfor8回の値をインクリメントしますproc0の値をリセットしNます1proc1コピーN = 1してtempから、命令の実行を停止しますproc0まで増加Nし9、その後終了しますproc1の値を にリセットしてNから2終了します