Will the output always be greater than 0 ? PROMELA program

Question

I'm a bit boggled by this question, when I ran this program I got results greater than 0 but I'm not sure if that would always be the case since the program could execute x++ or x-- first in theory. How can I definitively confirm that the results will always be bigger than 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)}

Patrick Trentin Patrick Trentin · Accepted Answer · 2020-09-03T08:48:42

This can be easily verified by extending the model with the property you want to verify:

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

larger_or_equal: ``It is always the case that x >= 0''

strictly_larger: ``It is always the case that x > 0''

Complete Model:

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) };

Generate a verifier, and run it:

~$ 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
...

As witnessed by the result of the above verification, property larger_or_equal is always true whereas property strictly_larger can be false.

Will the output always be greater than 0 ? PROMELA program

1 Answers