Spin:错误,生成此 pan.c 的 spin 版本采用了不同的字长 (4 is 8)
Spin: error, the version of spin that generated this pan.c assumed a different wordsize (4 iso 8)
我正在使用 Windows O.S,在 Cygwin 中我输入:wish -f ispin.tcl
打开 ispin 界面。
我打开一个文件 test.pml
,其中包含:
byte state = 2;
proctype A()
{ (state == 1) -> state = 3
}
proctype B()
{ state = state - 1
}
init
{ run A(); run B()
}
在那之后,我 运行 它使用种子 = 123 的随机方式。结果打印在输出中没有问题:
0: proc - (:root:) creates proc 0 (:init:)
Starting A with pid 1
1: proc 0 (:init::1) creates proc 1 (A)
1: proc 0 (:init::1) test.pml:12 (state 1) [(run A())]
Starting B with pid 2
2: proc 0 (:init::1) creates proc 2 (B)
2: proc 0 (:init::1) test.pml:12 (state 2) [(run B())]
3: proc 2 (B:1) test.pml:8 (state 1) [state = (state-1)]
4: proc 1 (A:1) test.pml:4 (state 1) [((state==1))]
4: proc 2 (B:1) terminates
5: proc 1 (A:1) test.pml:4 (state 2) [state = 3]
5: proc 1 (A:1) terminates
5: proc 0 (:init::1) terminates
3 processes created
验证此模型时出现问题。验证结果为:
verification result:
spin -a test.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -w -o pan pan.c
./pan -m10000
Pid: 3952
spin: error, the version of spin that generated this pan.c assumed a different wordsize (4 iso 8)
我该如何解决这个问题?我在 Internet 上搜索但找不到可以帮助我的东西。
注意:我没有更改任何验证属性:
上述错误的解决方案是安装 Cygwin for 32-bit versions of Windows even if my laptop is 64-bit. This is because the executable of spin exist only for Windows 32-bit,因此它们必须按照我的理解进行匹配。
Cygwin安装完成后(gcc
、cpp
、make
),我们移动spin
、ispin
和test
文件到新的 Cygwin 文件夹 (C:\cygwin\
)。
当我们尝试 运行 并再次验证模型时,无需任何其他修改,我们可以看到没有错误的正确输出:
verification result:
spin -a test.promela
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -w -o pan pan.c
./pan -m10000
Pid: 6304
pan:1: assertion violated 0 (at depth 6)
pan: wrote test.promela.trail
(Spin Version 6.4.5 -- 1 January 2016)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim - (not selected)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 20 byte, depth reached 6, errors: 1
7 states, stored
0 states, matched
7 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.000 equivalent memory usage for states (stored*(State-vector + overhead))
0.292 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
pan: elapsed time 0.002 seconds
To replay the error-trail, goto Simulate/Replay and select "Run"
我正在使用 Windows O.S,在 Cygwin 中我输入:wish -f ispin.tcl
打开 ispin 界面。
我打开一个文件 test.pml
,其中包含:
byte state = 2;
proctype A()
{ (state == 1) -> state = 3
}
proctype B()
{ state = state - 1
}
init
{ run A(); run B()
}
在那之后,我 运行 它使用种子 = 123 的随机方式。结果打印在输出中没有问题:
0: proc - (:root:) creates proc 0 (:init:)
Starting A with pid 1
1: proc 0 (:init::1) creates proc 1 (A)
1: proc 0 (:init::1) test.pml:12 (state 1) [(run A())]
Starting B with pid 2
2: proc 0 (:init::1) creates proc 2 (B)
2: proc 0 (:init::1) test.pml:12 (state 2) [(run B())]
3: proc 2 (B:1) test.pml:8 (state 1) [state = (state-1)]
4: proc 1 (A:1) test.pml:4 (state 1) [((state==1))]
4: proc 2 (B:1) terminates
5: proc 1 (A:1) test.pml:4 (state 2) [state = 3]
5: proc 1 (A:1) terminates
5: proc 0 (:init::1) terminates
3 processes created
验证此模型时出现问题。验证结果为:
verification result:
spin -a test.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -w -o pan pan.c
./pan -m10000
Pid: 3952
spin: error, the version of spin that generated this pan.c assumed a different wordsize (4 iso 8)
我该如何解决这个问题?我在 Internet 上搜索但找不到可以帮助我的东西。
注意:我没有更改任何验证属性:
上述错误的解决方案是安装 Cygwin for 32-bit versions of Windows even if my laptop is 64-bit. This is because the executable of spin exist only for Windows 32-bit,因此它们必须按照我的理解进行匹配。
Cygwin安装完成后(gcc
、cpp
、make
),我们移动spin
、ispin
和test
文件到新的 Cygwin 文件夹 (C:\cygwin\
)。
当我们尝试 运行 并再次验证模型时,无需任何其他修改,我们可以看到没有错误的正确输出:
verification result:
spin -a test.promela
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -w -o pan pan.c
./pan -m10000
Pid: 6304
pan:1: assertion violated 0 (at depth 6)
pan: wrote test.promela.trail
(Spin Version 6.4.5 -- 1 January 2016)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim - (not selected)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 20 byte, depth reached 6, errors: 1
7 states, stored
0 states, matched
7 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.000 equivalent memory usage for states (stored*(State-vector + overhead))
0.292 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
pan: elapsed time 0.002 seconds
To replay the error-trail, goto Simulate/Replay and select "Run"