CODEWITHSUNDEEP
verificationmodel-checkingspinpromela
K. Huber
K. Huber

Reputation: 33

Never claim does not work in promela model

Consider this simple PROMELA model:

#define p (x!=4)

int x = 0;

init {
    do
    :: x < 10 ->
        x++;
    od
}

I wanted to verify this model with this simple claim, which was generated by using spin -f:

never {    /* []p */
accept_init:
T0_init:
    do
    :: ((p)) -> goto T0_init
    od;
}

However, the verification using

spin -a model.pml
cc -o pan pan.c
./pan

yields no result. Trying the -a option also does not deliver results. Any random simulation shows, that obviously p is false at some point, so why does the never claim not work, despite I generated it with spin?

Am I missing something fundamental?

Upvotes: 2

Views: 1210

Answers (2)

d8d0d65b3f7cf42
d8d0d65b3f7cf42

Reputation: 2653

put the claim in the source code (say, check.pml)

int x = 0;

init {
    do
    :: x < 10 ->
        x++;
    od
}

ltl  { [] (x != 4) }

then

spin -a check.pml
cc     pan.c   -o pan
./pan -a

this gives

pan:1: assertion violated  !( !((x!=4))) (at depth 16)
pan: wrote check.pml.trail

you can watch the trail with

./pan -r -v

IMHO, using an extra tool to construct the automaton from the claim is terribly inconvenient and often confusing.

Upvotes: 1

dejvuth
dejvuth

Reputation: 7136

If you want to check []p, you will need to construct a never claim for ![]p.

From the reference:

To translate an LTL formula into a never claim, we have to consider first whether the formula expresses a positive or a negative property. A positive property expresses a good behavior that we would like our system to have. A negative property expresses a bad behavior that we claim the system does not have. A never claim is normally only used to formalize negative properties (behaviors that should never happen), which means that positive properties must be negated before they are translated into a claim.

Upvotes: 1

Related Questions