Posts by Laurapanizo

Laurapanizo · General

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

Laurapanizo · General

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

Laurapanizo · General

Hello everybody,
I would like to know if partial order reduction and statement merging are applied when there are embedded C code in the model.
I have read in "SPIN primer and reference manual" that statement mergin can be applied when there are code that only uses local data.
Does it holds when the local data is defined in c_state?
In addition I have seen that the examples in chapeter 17, the verification of the examples uses partial order reduction but I am not sure
If it is possible to reduce states when there are c_code that modify the value of PROMELA variables or C variables that are tracked.
There is any paper about partial order reduction and embed C code?

Thanks,
Laura

Spinroot

#1 Re: General » Exploration behaviour with unbounded counter » 2013-07-05 09:25:12

#2 General » Exploration behaviour with unbounded counter » 2013-07-04 09:10:14

#3 General » Embedded C code and partial order reduction » 2011-07-20 08:36:15

Board footer