Spin model checker - Error: memory exhausted because of yacc stack size

Question

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!

---

SOLUTION

Edit the following line in spin.y:

#define YYMAXDEPTH      20000

to a larger number, and reinstall spin. It should work :)

Answer 1

Edit the following line in spin.y:

#define YYMAXDEPTH      20000

to a larger number, and reinstall spin. It should work :)