时间戳

首页 > 解决方案 > 输出总是大于 0 吗？PROMELA 计划

model-checking - 输出总是大于 0 吗？PROMELA 计划

问题描述

我对这个问题有点困惑，当我运行这个程序时，我得到的结果大于 0，但我不确定是否总是这样，因为程序可以首先执行 x++ 或 x-- 在理论上。我怎样才能明确地确认结果总是大于 0 ？

proctype testcount(byte x)
{
do
:: (x != 0 ) ->
if
:: x ++
:: x --
:: break
fi
:: else -> break
od;
printf("counter = %d\n", x);
}
init {run testcount(1)}

标签： model-checkingpromelaspin

解决方案

这可以通过使用您要验证的属性扩展模型来轻松验证：

ltl larger_or_equal { [] (testcount[1]:x >= 0) };
ltl strictly_larger { [] (testcount[1]:x > 0) };

larger_or_equal: ``总是如此x >= 0''

strictly_larger: ``总是如此x > 0''

完整型号：

proctype testcount(byte x)
{
    do
        :: (x != 0 ) ->
            if
                :: x ++
                :: x --
                :: break
            fi
        :: else -> break
    od;
    printf("counter = %d\n", x);
}

init {
    run testcount(1)
}

ltl larger_or_equal { [] (testcount[1]:x >= 0) };
ltl strictly_larger { [] (testcount[1]:x > 0) };

生成一个验证器，并运行它：

~$ spin -a test.pml 
~$ gcc pan.c -o run
~$ ./run -a -N larger_or_equal
pan: ltl formula larger_or_equal

...

Full statespace search for:
    never claim             + (larger_or_equal)
    assertion violations    + (if within scope of claim)
    acceptance   cycles     + (fairness disabled)
    invalid end states  - (disabled by never claim)

State-vector 28 byte, depth reached 1031, errors: 0
...

~$ ./run -a -N strictly_larger
pan: ltl formula strictly_larger
pan:1: assertion violated  !( !((testcount[0].x>0))) (at depth 1)
pan: wrote test.pml.trail

...

Full statespace search for:
    never claim             + (strictly_larger)
    assertion violations    + (if within scope of claim)
    acceptance   cycles     + (fairness disabled)
    invalid end states  - (disabled by never claim)

State-vector 20 byte, depth reached 1, errors: 1
...

正如上述验证的结果所证明的那样，属性larger_or_equal始终为真，而属性strictly_larger可能为假。

推荐阅读