我正在努力适应 iSpin/Promela。我在用:
Spin 版本 6.4.3 -- 2014 年 12 月 16 日，
iSpin 版本 1.1.4 -- 2014 年 11 月 27 日，
TclTk 版本 8.6/8.6，
视窗 8.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 属性，因此我禁用所有安全属性并激活“使用声明”。声明名称是“alwaysten”。
但是，如果我激活“断言违规”，似乎只是评估 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 。)
关于spin - 仅使用激活的 "assertion violations"进行 iSpin LTL 属性评估？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/30918162/