I have created a rather large Promela model (2362 states, with a total of 29592 transitions among them) and I wish to verify an LTL property of the underlying system. The model is all defined in one process as follows:
int state=1;
bool p1a=true, p3=false, p1b=false;
active proctype model()
{
do
:: atomic{ state==1 -> state=1; p1a=true; p3=false; p1b=false }
:: atomic{ state==1 -> state=4; p1a=false; p3=false; p1b=false }
:: atomic{ state==1 -> state=5; p1a=false; p3=false; p1b=false }
:: atomic{ state==1 -> state=6; p1a=false; p3=false; p1b=false }
:: atomic{ state==1 -> state=133; p1a=true; p3=false; p1b=false }
:: atomic{ state==1 -> state=134; p1a=false; p3=false; p1b=false }
:: atomic{ state==1 -> state=136; p1a=false; p3=false; p1b=false }
:: atomic{ state==1 -> state=137; p1a=false; p3=false; p1b=false }
:: atomic{ state==1 -> state=138; p1a=false; p3=false; p1b=false }
:: atomic{ state==1 -> state=265; p1a=true; p3=false; p1b=false }
:: atomic{ state==1 -> state=266; p1a=false; p3=false; p1b=false }
:: atomic{ state==1 -> state=267; p1a=false; p3=false; p1b=false }
:: atomic{ state==1 -> state=268; p1a=false; p3=false; p1b=false }
:: atomic{ state==1 -> state=269; p1a=false; p3=false; p1b=false }
:: atomic{ state==1 -> state=270; p1a=false; p3=false; p1b=false }
:: atomic{ state==4 -> state=13; p1a=true; p3=false; p1b=false }
:: atomic{ state==4 -> state=14; p1a=false; p3=false; p1b=false }
.
. /* continues similarly */
.
:: atomic{ state==2376 -> state=1825; p1a=true; p3=true; p1b=false }
:: atomic{ state==2376 -> state=1837; p1a=true; p3=true; p1b=false }
od
}
ltl F {[]((p1a && p3) -> (<> p1b))}
You can find the whole file here: https://github.com/alevizada/bioFSA/blob/master/spin_files/abs_file_1.pml
When I run:
spin -a filename.pml
I get the following:
spin: filename.pml:19980, Error: memory exhausted saw 'operator: ='
spin: filename.pml:19980, Error: no runable process saw 'operator: ='
Checking the .pml file, this is equivalent to having stored 19974 state-transition pairs.
I have tried this both on my computer, and on a server, so I guess system memory is not the problem.
Is there a maximum number of such pairs spin can store? If yes, how can I resolve this and proceed with verification?
Many thanks!
EDIT: It seems that it is a parser spin is using (yacc) that's causing this problem. yacc allocates a stack with predefined/limited memory. I have found this reference on how to change it, but I'm not sure where the file these variables are defined should be. I suspect it is y.tab.c though.
Any help?
Thanks!
Edit the following line in spin.y:
#define YYMAXDEPTH 20000
to a larger number, and reinstall spin. It should work :)
Edit the following line in spin.y:
#define YYMAXDEPTH 20000
to a larger number, and reinstall spin. It should work :)