输出将始终大于0吗？ PROMELA计划

如何解决输出将始终大于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)}

解决方法

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

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始终为true，而属性strictly_larger可以为false。