Spinroot

A forum for Spin users

You are not logged in.

#1 2012-04-26 11:20:35

EdwardBear
Member
Registered: 2012-04-26
Posts: 2

Referencing Multi-Dimensional Arrays in an LTL formula

My real model is more complicated that what I'm about to write, but I've found the same problem occurs in simpler examples as well.  I have an array called arr.  arr[0] is 10, arr[1] is 20 and arr[2] is 30.  I also have a proctype called sender, which contains a variable localVar which is initialized to 0.

    proctype sender(){
        int localVar;
        localVar = 0;
    }

init consists of filling the array and then initialising sender:

    init{
        arr[0]=10;
        arr[1]=20;
        arr[2]=30;
        run sender();
    }

The LTL formula consists of:
ltl b {[] (arr[sender[1]:_3_localVar]==10)}

This should be very simple.  sender[1]:_3_localVar is always 0 and the contents of arr[0] will always be 10.  I wouldn't mind if I've made a mistake and this condition isn't always true but I cannot get as far as evaluating the LTL.  Whenever I run a syntax check I'm told:

ltl b: [] ((arr[sender[1]._3_localVar]==10))
spin: _spin_nvr.tmp:3, Error: syntax error    saw ''.' = 46'
spin: practice.pml:9, Error: proctype b not found
child process exited abnormally

This only happens when I refer to array using the process variables.  ltl b {[] (arr[0]==10)} and ltl b {[] (sender[1]:_3_localVar==0)} are fine.  Is there a way to use process variables to refer to array indexes in LTL?

Offline

#2 2012-04-26 15:14:48

feng_lei_76
Member
Registered: 2011-05-13
Posts: 43

Re: Referencing Multi-Dimensional Arrays in an LTL formula

There seems to be a syntactic error in your LTL statement "ltl b: [] ((arr[sender[1]._3_localVar]==10))". When you refer to a local variable in a process, you use ":" rather than "."

By the way, I don't understand why you write "sender[1]:_3_localVar". Why do you write "_3_"? Is the correct writing "sender[1]:localVar"?

Moreover, LTL statement "[](arr[0] == 10)" should be wrong because arr[0] is zero at the initial state of the model.

Offline

#3 2012-04-26 15:37:19

feng_lei_76
Member
Registered: 2011-05-13
Posts: 43

Re: Referencing Multi-Dimensional Arrays in an LTL formula

I encountered the same problem as EdwardBear.

When I type "arr[sender[1] : _1_localVar]" in my editor, the SPIN parser always replace it to "arr[sender[1]._1_localVar]". The ":" is always mistaken as "."

This might be a bug of Spin.

Offline

#4 2012-04-26 18:07:35

EdwardBear
Member
Registered: 2012-04-26
Posts: 2

Re: Referencing Multi-Dimensional Arrays in an LTL formula

Sometimes when you use remote referencing you need to add the _3_ (or another number) before the variable as for whatever reason those characters are added to the variable name in the pan.h file and you need to incorporate them into the ltl (see the last paragraph of http://spinroot.com/spin/Man/remoterefs.html).
I don't mind if the LTL condition evaluates to false or not (although thanks for pointing out that "[](arr[0] == 10)" will evaluate to false), I just want to get to the stage where the LTL formula shown above can be evaluated

Offline

#5 2012-05-04 04:36:45

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Referencing Multi-Dimensional Arrays in an LTL formula

found the cause of this bug -- it will be fixed in the next release of Spin
which will be Spin Version 6.2.0 -- hopefully available within the next two weeks.

the bug only happens in one very specific case: when you index an array
with a remote variable reference inside an inline ltl formula

excellent bug report -- thanks!

Offline

#6 2012-05-11 00:26:55

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Referencing Multi-Dimensional Arrays in an LTL formula

6.2.0 is now available

Offline

Board footer

Powered by FluxBB