A forum for Spin users
You are not logged in.
Pages: 1
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
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?
Pages: 1