Spinroot

Laurapanizo

Member

Registered: 2011-07-19

Posts: 3

Exploration behaviour with unbounded counter

Hello,

We are having a strange problem with a simple model, and we are not sure if it's a problem with Spin or if we are failing to understand Spin's behaviour.

Let there be this simple Promela model:

// global.pml
bool flag;
int count;

active proctype infinity() {
    flag = true;
    count = 0;
    do
    :: flag -> atomic {flag = false; count++}
    :: !flag -> flag = true
    od
}

As you can see, the loop goes on forever and variable count keeps growing every other iteration. An exhaustive verification should loop for a while, before reaching the maximum exploration depth. However, it does not:

$ spin625 -a -O global.pml && gcc -o pan pan.c && ./pan
...
Full statespace search for:
    never claim             - (none specified)
    assertion violations    +
    acceptance   cycles     - (not selected)
    invalid end states    +

State-vector 20 byte, depth reached 5, errors: 0
        6 states, stored
        1 states, matched
        7 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)
...

However, if the count variable is turned into a local variable:

// local.pml
bool flag;

active proctype infinity() {
    flag = true;
    int count = 0;
    do
    :: flag -> atomic {flag = false; count++}
    :: !flag -> flag = true
    od
}

Then the verification does reach the maximum depth search, because the count variable keeps growing:

$ spin625 -a -O local.pml && gcc -o pan pan.c && ./pan
error: max search depth too small
...
Full statespace search for:
    never claim             - (none specified)
    assertion violations    +
    acceptance   cycles     - (not selected)
    invalid end states    +

State-vector 24 byte, depth reached 9999, errors: 0
    10000 states, stored
        1 states, matched
    10001 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)
...

Is this the expected behavior? If so, why?

Thanks in advance,
Laura & Alberto

spinroot

forum

Registered: 2010-11-18

Posts: 695

Website

Re: Exploration behaviour with unbounded counter

Spin can recognize in some contexts that a variable is used as a "write-only" variable.
This is what causes it to not consider count as a state variable in the first example.
It is interesting that it doesn't see this in the second case, but it errs on the side of caution here...

Laurapanizo

Member

Registered: 2011-07-19

Posts: 3

Re: Exploration behaviour with unbounded counter

Thank you for your answer. We have noticed that using the -o2 option does indeed produce the same results with local and global variables.