问题描述
这个问题让我有点困惑,当我运行该程序时,我得到的结果大于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。