我正在尝试习惯 iSpin/Promela。我在用:
Spin 版本 6.4.3——2014 年 12 月 16 日,iSpin 版本 1.1.4——2014 年 11 月 27 日,TclTk 版本 8.6/8.6,Windows 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?