iSpin LTL 属性 仅在激活后评估 "assertion violations"？
iSpin LTL property evaluation only with activated "assertion violations"?
我正在努力适应 iSpin/Promela。我正在使用：
旋转版本 6.4.3 -- 2014 年 12 月 16 日，
iSpin 1.1.4 版——2014 年 11 月 27 日，
TclTk 版本 8.6/8.6，
Windows8.1.
这是我尝试使用 LTL 的示例。如果 for 循环中的两个步骤是非原子的，那么 LTL 属性 的验证应该会产生错误：
1 #define ten ((n !=10) && (finished == 2))
2
3 int n = 0;
4 int finished = 0;
5 active [2] proctype P() {
6 //assert(_pid == 0 || _pid == 1);
7
8 int t = 0;
9 byte j;
10 for (j : 1 .. 5) {
11 atomic {
12 t = n;
13 n = t+1;
14 }
15 }
16 finished = finished+1;
17 }
18
19 ltl alwaysten {[] ! ten }
在验证点击中我只想测试 LTL 属性，所以我禁用所有安全属性并激活 "use claim"。声明名称是 "alwaysten".
但是如果我激活 "assertion violations"，LTL 属性 似乎只是被评估了。为什么？同事正在使用 iSpin v1.1.0，他不需要激活它吗？我究竟做错了什么？我想独立证明断言和 LTL 属性...
这是痕迹：
pan: elapsed time 0.002 seconds
To replay the error-trail, goto Simulate/Replay and select "Run"
spin -a 1_2_ConcurrentCounters_8.pml
ltl alwaysten: [] (! (((n!=10)) && ((finished==2))))
C:/cygwin/bin/gcc -DMEMLIM=1024 -O2 -DXUSAFE -w -o pan pan.c
./pan -m10000 -E -a -N alwaysten
Pid: 6980
warning: only one claim defined, -N ignored
(Spin Version 6.4.3 -- 16 December 2014)
+ Partial Order Reduction
Full statespace search for:
never claim + (alwaysten)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by -E flag)
State-vector 36 byte, depth reached 57, errors: 0
475 states, stored
162 states, matched
637 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.024 equivalent memory usage for states (stored*(State-vector + overhead))
0.291 actual memory usage for states
64.000 memory used for hash table (-w24)
0.343 memory used for DFS stack (-m10000)
64.539 total actual memory usage
unreached in proctype P
(0 of 13 states)
unreached in claim alwaysten
_spin_nvr.tmp:8, state 10, "-end-"
(1 of 10 states)
pan: elapsed time 0.001 seconds
No errors found -- did you verify all claims?
这是因为您的 LTL 被翻译成带有 assert 声明的索赔。请参阅以下自动机。
因此，如果不检查断言违规，就不会发现任何错误。
（对不同行为的可能解释：以前版本的 Spin 可能对此有不同的解释，可能使用 accept 而不是 assert。）
我正在努力适应 iSpin/Promela。我正在使用：
旋转版本 6.4.3 -- 2014 年 12 月 16 日， iSpin 1.1.4 版——2014 年 11 月 27 日， TclTk 版本 8.6/8.6， Windows8.1.
这是我尝试使用 LTL 的示例。如果 for 循环中的两个步骤是非原子的，那么 LTL 属性 的验证应该会产生错误：
1 #define ten ((n !=10) && (finished == 2))
2
3 int n = 0;
4 int finished = 0;
5 active [2] proctype P() {
6 //assert(_pid == 0 || _pid == 1);
7
8 int t = 0;
9 byte j;
10 for (j : 1 .. 5) {
11 atomic {
12 t = n;
13 n = t+1;
14 }
15 }
16 finished = finished+1;
17 }
18
19 ltl alwaysten {[] ! ten }
在验证点击中我只想测试 LTL 属性，所以我禁用所有安全属性并激活 "use claim"。声明名称是 "alwaysten".
但是如果我激活 "assertion violations"，LTL 属性 似乎只是被评估了。为什么？同事正在使用 iSpin v1.1.0，他不需要激活它吗？我究竟做错了什么？我想独立证明断言和 LTL 属性...
这是痕迹：
pan: elapsed time 0.002 seconds
To replay the error-trail, goto Simulate/Replay and select "Run"
spin -a 1_2_ConcurrentCounters_8.pml
ltl alwaysten: [] (! (((n!=10)) && ((finished==2))))
C:/cygwin/bin/gcc -DMEMLIM=1024 -O2 -DXUSAFE -w -o pan pan.c
./pan -m10000 -E -a -N alwaysten
Pid: 6980
warning: only one claim defined, -N ignored
(Spin Version 6.4.3 -- 16 December 2014)
+ Partial Order Reduction
Full statespace search for:
never claim + (alwaysten)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by -E flag)
State-vector 36 byte, depth reached 57, errors: 0
475 states, stored
162 states, matched
637 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.024 equivalent memory usage for states (stored*(State-vector + overhead))
0.291 actual memory usage for states
64.000 memory used for hash table (-w24)
0.343 memory used for DFS stack (-m10000)
64.539 total actual memory usage
unreached in proctype P
(0 of 13 states)
unreached in claim alwaysten
_spin_nvr.tmp:8, state 10, "-end-"
(1 of 10 states)
pan: elapsed time 0.001 seconds
No errors found -- did you verify all claims?
这是因为您的 LTL 被翻译成带有 assert 声明的索赔。请参阅以下自动机。
因此，如果不检查断言违规，就不会发现任何错误。
（对不同行为的可能解释：以前版本的 Spin 可能对此有不同的解释，可能使用 accept 而不是 assert。）