为什么无限循环不会导致使用 Promela 和 Spin 进行模型检查时出错？
Why an infinite loop doesn't result in an error in model checking with Promela and Spin?
如果我在 Promela 中编写以下代码并 运行 在 Spin 中以验证器模式编写它，它以 0 个错误结束。它确实报告 toogle 和 init 有未达到的状态，但那些似乎只是警告。
byte x = 0; byte y = 0;
active proctype toggle() {
do
:: x == 1 -> x = 0
:: x == 0 -> x = 1
od
}
init {
(y == 1);
}
我对此感到困惑，因为我认为这会给我一个 'invalid end state' 错误。如果我用一个简单的 skip 语句更改 toogle proctype 的主体，它会按我预期的那样出错。
这是为什么？有没有办法强制模拟器将无限循环报告为错误？
关于 'unreached in proctype' 消息，将 end 标签添加到 do 循环似乎没有任何作用。
我正在 运行ning spin 6.5.0 和 运行 以下命令：
spin.exe -a test.pml
gcc -o pan pan.c
pan.exe
这些是输出结果，供参考。
使用 do 循环：
pan.exe
(Spin Version 6.5.0 -- 1 July 2019)
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
invalid end states +
State-vector 20 byte, depth reached 3, errors: 0
4 states, stored
1 states, matched
5 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
unreached in proctype toggle
..\test2.pml:7, state 8, "-end-"
(1 of 8 states)
unreached in init
..\test2.pml:10, state 2, "-end-"
(1 of 2 states)
pan: elapsed time 0.013 seconds
pan: rate 307.69231 states/second
与skip:
pan.exe
pan:1: invalid end state (at depth 0)
pan: wrote ..\test2.pml.trail
(Spin Version 6.5.0 -- 1 July 2019)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
invalid end states +
State-vector 20 byte, depth reached 1, errors: 1
2 states, stored
0 states, matched
2 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.293 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.015 seconds
pan: rate 133.33333 states/second
在这个例子中
byte x = 0; byte y = 0;
active proctype toggle() {
do
:: x == 1 -> x = 0
:: x == 0 -> x = 1
od
}
init {
(y == 1);
}
init 进程永远被阻塞（因为 y == 1 总是 false），但是 toggle 进程总是可以执行 something。因此，存在无无效结束状态错误.
相反，在这个例子中
byte x = 0; byte y = 0;
active proctype toggle() {
skip;
}
init {
(y == 1);
}
init 进程仍然永远阻塞，但是 toggle 进程可以执行它唯一的指令 skip; 然后终止。此时，剩余进程中的 none（即只有 init）有任何它可以执行的指令，因此 Spin 以 无效结束状态终止 错误。
~$ spin -a -search test.pml
pan:1: invalid end state (at depth 0)
pan: wrote test.pml.trail
(Spin Version 6.5.0 -- 17 July 2019)
...
State-vector 20 byte, depth reached 1, errors: 1
...
Is there a way to force the simulator to report the infinite loop as an error?
是的。其实有多种方式。
最简单的方法是使用 Spin:
的选项 -l
~$ spin --help
...
-l: search for non-progress cycles
...
使用此选项，Spin 会报告任何 无限循环 ，其中不包含带有 progress 标签的任何状态。
这是您原始问题的输出：
~$ spin -search -l test.pml
pan:1: non-progress cycle (at depth 2)
pan: wrote test.pml.trail
(Spin Version 6.5.0 -- 17 July 2019)
...
State-vector 28 byte, depth reached 9, errors: 1
...
~$ spin -t test.pml
spin: couldn't find claim 2 (ignored)
<<<<<START OF CYCLE>>>>>
spin: trail ends after 10 steps
#processes: 2
x = 0
y = 0
10: proc 1 (:init::1) test.pml:10 (state 1)
10: proc 0 (toggle:1) test.pml:5 (state 4)
2 processes created
另一种方法是使用 LTL 模型检查。例如，您可以声明在某些时候进程的数量（参见 _nr_pr) that are in execution becomes equal to 0 (or more, if you admit some infinite loops), or check that a particular process terminates correctly using remote references.
两种情况都包含在以下示例中：
byte x = 0; byte y = 0;
active proctype toggle() {
do
:: x == 1 -> x = 0
:: x == 0 -> x = 1
od;
end:
}
init {
(y == 1);
}
// sooner or later, the process toggle
// with _pid == 0 will reach the end
// state
ltl p1 { <> toggle[0]@end };
// sooner or later, the number of processes
// that are currently running becomes 0,
// (hence, there can be no infinite loops)
ltl p2 { <> (_nr_pr == 0) };
都是第一个
~$ spin -a -search -ltl p1 test.pml
~$ spin -t test.pml
ltl p1: <> ((toggle[0]@end))
ltl p2: <> ((_nr_pr==0))
<<<<<START OF CYCLE>>>>>
Never claim moves to line 4 [(!((toggle[0]._p==end)))]
spin: trail ends after 8 steps
#processes: 2
x = 0
y = 0
end = 0
8: proc 1 (:init::1) test.pml:10 (state 1)
8: proc 0 (toggle:1) test.pml:3 (state 5)
8: proc - (p1:1) _spin_nvr.tmp:3 (state 3)
2 processes created
和第二个
~$ spin -a -search -ltl p2 test.pml
~$ spin -t test.pml
ltl p1: <> ((toggle[0]@end))
ltl p2: <> ((_nr_pr==0))
<<<<<START OF CYCLE>>>>>
Never claim moves to line 11 [(!((_nr_pr==0)))]
spin: trail ends after 8 steps
#processes: 2
x = 0
y = 0
end = 0
8: proc 1 (:init::1) test.pml:10 (state 1)
8: proc 0 (toggle:1) test.pml:3 (state 5)
8: proc - (p2:1) _spin_nvr.tmp:10 (state 3)
2 processes created
发现 LTL 属性是假的。
Regarding the 'unreached in proctype' messages, adding an end label to the do loop doesn't seem to do anything.
end 标签用于删除 "invalid end state" error 否则会被发现。
例如修改你之前的例子如下：
byte x = 0; byte y = 0;
active proctype toggle() {
skip;
}
init {
end:
(y == 1);
}
消除错误：
~$ spin -a -search test.pml
(Spin Version 6.5.0 -- 17 July 2019)
...
State-vector 20 byte, depth reached 1, errors: 0
...
只有当一个人愿意保证一个进程被卡在没有可执行指令的情况下不是意外死锁的症状时，才应该使用end标签情况。
如果我在 Promela 中编写以下代码并 运行 在 Spin 中以验证器模式编写它，它以 0 个错误结束。它确实报告 toogle 和 init 有未达到的状态，但那些似乎只是警告。
byte x = 0; byte y = 0;
active proctype toggle() {
do
:: x == 1 -> x = 0
:: x == 0 -> x = 1
od
}
init {
(y == 1);
}
我对此感到困惑，因为我认为这会给我一个 'invalid end state' 错误。如果我用一个简单的 skip 语句更改 toogle proctype 的主体，它会按我预期的那样出错。
这是为什么？有没有办法强制模拟器将无限循环报告为错误？
关于 'unreached in proctype' 消息，将 end 标签添加到 do 循环似乎没有任何作用。
我正在 运行ning spin 6.5.0 和 运行 以下命令：
spin.exe -a test.pml
gcc -o pan pan.c
pan.exe
这些是输出结果，供参考。
使用 do 循环：
pan.exe
(Spin Version 6.5.0 -- 1 July 2019)
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
invalid end states +
State-vector 20 byte, depth reached 3, errors: 0
4 states, stored
1 states, matched
5 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
unreached in proctype toggle
..\test2.pml:7, state 8, "-end-"
(1 of 8 states)
unreached in init
..\test2.pml:10, state 2, "-end-"
(1 of 2 states)
pan: elapsed time 0.013 seconds
pan: rate 307.69231 states/second
与skip:
pan.exe
pan:1: invalid end state (at depth 0)
pan: wrote ..\test2.pml.trail
(Spin Version 6.5.0 -- 1 July 2019)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
invalid end states +
State-vector 20 byte, depth reached 1, errors: 1
2 states, stored
0 states, matched
2 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.293 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.015 seconds
pan: rate 133.33333 states/second
在这个例子中
byte x = 0; byte y = 0;
active proctype toggle() {
do
:: x == 1 -> x = 0
:: x == 0 -> x = 1
od
}
init {
(y == 1);
}
init 进程永远被阻塞（因为 y == 1 总是 false），但是 toggle 进程总是可以执行 something。因此，存在无无效结束状态错误.
相反，在这个例子中
byte x = 0; byte y = 0;
active proctype toggle() {
skip;
}
init {
(y == 1);
}
init 进程仍然永远阻塞，但是 toggle 进程可以执行它唯一的指令 skip; 然后终止。此时，剩余进程中的 none（即只有 init）有任何它可以执行的指令，因此 Spin 以 无效结束状态终止 错误。
~$ spin -a -search test.pml
pan:1: invalid end state (at depth 0)
pan: wrote test.pml.trail
(Spin Version 6.5.0 -- 17 July 2019)
...
State-vector 20 byte, depth reached 1, errors: 1
...
Is there a way to force the simulator to report the infinite loop as an error?
是的。其实有多种方式。
最简单的方法是使用 Spin:
的选项-l
~$ spin --help
...
-l: search for non-progress cycles
...
使用此选项，Spin 会报告任何 无限循环 ，其中不包含带有 progress 标签的任何状态。
这是您原始问题的输出：
~$ spin -search -l test.pml
pan:1: non-progress cycle (at depth 2)
pan: wrote test.pml.trail
(Spin Version 6.5.0 -- 17 July 2019)
...
State-vector 28 byte, depth reached 9, errors: 1
...
~$ spin -t test.pml
spin: couldn't find claim 2 (ignored)
<<<<<START OF CYCLE>>>>>
spin: trail ends after 10 steps
#processes: 2
x = 0
y = 0
10: proc 1 (:init::1) test.pml:10 (state 1)
10: proc 0 (toggle:1) test.pml:5 (state 4)
2 processes created
另一种方法是使用 LTL 模型检查。例如，您可以声明在某些时候进程的数量（参见 _nr_pr) that are in execution becomes equal to 0 (or more, if you admit some infinite loops), or check that a particular process terminates correctly using remote references.
两种情况都包含在以下示例中：
byte x = 0; byte y = 0;
active proctype toggle() {
do
:: x == 1 -> x = 0
:: x == 0 -> x = 1
od;
end:
}
init {
(y == 1);
}
// sooner or later, the process toggle
// with _pid == 0 will reach the end
// state
ltl p1 { <> toggle[0]@end };
// sooner or later, the number of processes
// that are currently running becomes 0,
// (hence, there can be no infinite loops)
ltl p2 { <> (_nr_pr == 0) };
都是第一个
~$ spin -a -search -ltl p1 test.pml
~$ spin -t test.pml
ltl p1: <> ((toggle[0]@end))
ltl p2: <> ((_nr_pr==0))
<<<<<START OF CYCLE>>>>>
Never claim moves to line 4 [(!((toggle[0]._p==end)))]
spin: trail ends after 8 steps
#processes: 2
x = 0
y = 0
end = 0
8: proc 1 (:init::1) test.pml:10 (state 1)
8: proc 0 (toggle:1) test.pml:3 (state 5)
8: proc - (p1:1) _spin_nvr.tmp:3 (state 3)
2 processes created
和第二个
~$ spin -a -search -ltl p2 test.pml
~$ spin -t test.pml
ltl p1: <> ((toggle[0]@end))
ltl p2: <> ((_nr_pr==0))
<<<<<START OF CYCLE>>>>>
Never claim moves to line 11 [(!((_nr_pr==0)))]
spin: trail ends after 8 steps
#processes: 2
x = 0
y = 0
end = 0
8: proc 1 (:init::1) test.pml:10 (state 1)
8: proc 0 (toggle:1) test.pml:3 (state 5)
8: proc - (p2:1) _spin_nvr.tmp:10 (state 3)
2 processes created
发现 LTL 属性是假的。
Regarding the 'unreached in proctype' messages, adding an end label to the do loop doesn't seem to do anything.
end 标签用于删除 "invalid end state" error 否则会被发现。
例如修改你之前的例子如下：
byte x = 0; byte y = 0;
active proctype toggle() {
skip;
}
init {
end:
(y == 1);
}
消除错误：
~$ spin -a -search test.pml
(Spin Version 6.5.0 -- 17 July 2019)
...
State-vector 20 byte, depth reached 1, errors: 0
...
只有当一个人愿意保证一个进程被卡在没有可执行指令的情况下不是意外死锁的症状时，才应该使用end标签情况。