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