考虑以下Promela两个操纵共享变量的进程的模型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 公式表示必须在执行路径上保持的属性，而根据 minimum 的定义，您希望在多个执行路径上表示属性。事实上，只有在没有其他执行跟踪的情况下，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) };
我们有两个属性：
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增加Nfor8次的值proc0将值重置N回1proc1复制然后停止执行任何N = 1指令tempproc0递增N到9然后终止proc1将值重置N回2然后终止