输出是否总是大于0?PROMELA程序

Question

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

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

Answer 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 = %dn", 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可以是假的。