根据手册页，
进度标签用于定义正确性声明。进度标签规定了在任何无限系统执行中必须经常无限访问标记的全局状态的要求。验证者可以将任何违反此要求的行为报告为非进度循环。
和
Spin 有一个特殊的模式来证明不存在非进度循环。它使用预定义的 LTL 公式执行此操作：
(<>[] np_)它将非进度正式化为标准的 Buchi 接受属性。
但是让我们看一下非常原始的promela规范
bool initialised = 0;
init{
progress:
initialised++;
assert(initialised == 1);
}
据我了解，assert应该保持但验证失败，因为initialised++只执行一次，而progress标签声称应该可以任意频繁地执行它。
然而，即使使用上面的 LTL 公式，这在 ispin 中也可以很好地验证（见下文）。
如何正确测试是否可以经常任意执行语句（例如锁定方案）？
（Spin 版本 6.4.7——2017 年 8 月 19 日）
+ Partial Order Reduction完整的状态空间搜索：
never claim + (:np_:) assertion violations + (if within scope of claim) non-progress cycles + (fairness disabled) invalid end states - (disabled by never claim)状态向量 28 字节，深度达到 7，错误：0
6 states, stored (8 visited) 3 states, matched 11 transitions (= visited+matched) 0 atomic steps哈希冲突：0（已解决）
内存使用统计（以兆字节为单位）：
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在初始化中未达到
(0 of 3 states)pan：经过时间 0.001 秒
未发现错误——您是否验证了所有声明？
更新
仍然不知道如何使用这个......
bool initialised = 0;
init{
initialised = 1;
}
active [2] proctype reader()
{
assert(_pid >= 1);
(initialised == 1)
do
:: else ->
progress_reader:
assert(true);
od
}
active [2] proctype writer()
{
assert(_pid >= 1);
(initialised == 1)
do
:: else ->
(initialised == 0)
progress_writer:
assert(true);
od
}
让我们为非进展周期选择测试。然后 ispin 将其运行为
spin -a test.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DNP -DNOCLAIM -w -o pan pan.c
./pan -m10000 -l
验证无误。
因此，让我们尝试使用 ltl 属性...
/*pid: 0 = init, 1-2 = reader, 3-4 = writer*/
ltl progress_reader1{ []<> reader[1]@progress_reader }
ltl progress_reader2{ []<> reader[2]@progress_reader }
ltl progress_writer1{ []<> writer[3]@progress_writer }
ltl progress_writer2{ []<> writer[4]@progress_writer }
bool initialised = 0;
init{
initialised = 1;
}
active [2] proctype reader()
{
assert(_pid >= 1);
(initialised == 1)
do
:: else ->
progress_reader:
assert(true);
od
}
active [2] proctype writer()
{
assert(_pid >= 1);
(initialised == 1)
do
:: else ->
(initialised == 0)
progress_writer:
assert(true);
od
}
现在，首先，
the model contains 4 never claims: progress_writer2, progress_writer1, progress_reader2, progress_reader1
only one claim is used in a verification run
choose which one with ./pan -a -N name (defaults to -N progress_reader1)
or use e.g.: spin -search -ltl progress_reader1 test.pml
好吧，我不在乎，我只想让它最终运行，所以让我们继续progress_writer1担心以后如何将它们拼接在一起：
/*pid: 0 = init, 1-2 = reader, 3-4 = writer*/
/*ltl progress_reader1{ []<> reader[1]@progress_reader }*/
/*ltl progress_reader2{ []<> reader[2]@progress_reader }*/
ltl progress_writer1{ []<> writer[3]@progress_writer }
/*ltl progress_writer2{ []<> writer[4]@progress_writer }*/
bool initialised = 0;
init{
initialised = 1;
}
active [2] proctype reader()
{
assert(_pid >= 1);
(initialised == 1)
do
:: else ->
progress_reader:
assert(true);
od
}
active [2] proctype writer()
{
assert(_pid >= 1);
(initialised == 1)
do
:: else ->
(initialised == 0)
progress_writer:
assert(true);
od
}
ispin 运行这个
spin -a test.pml
ltl progress_writer1: [] (<> ((writer[3]@progress_writer)))
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -w -o pan pan.c
./pan -m10000
这不会产生错误，而是报告
unreached in claim progress_writer1
_spin_nvr.tmp:3, state 5, "(!((writer[3]._p==progress_writer)))"
_spin_nvr.tmp:3, state 5, "(1)"
_spin_nvr.tmp:8, state 10, "(!((writer[3]._p==progress_writer)))"
_spin_nvr.tmp:10, state 13, "-end-"
(3 of 13 states)
是的？灿烂！我完全不知道该怎么做。
我如何让它运行？