Spinroot

Thiago_Tuxi

Member

Registered: 2019-12-22

Posts: 1

SPIN does not generate an answer in huge models

I'm performing a verification of a huge model in spin, actually it is a benchmark model, and I'm comparing the results with different model checking tools.

Spin is just stopping the search without giving me any results when the model is very big, I tried several times but the search always stop at the same point.

The computer where I'm performing the test is WINDOWS 10 64 bit with 64Gb of RAM, so memory is not an issue since the verification stops when it uses only 6557.176 Mb

This is the command that I'm using:
spin -search -bitstate -w35 -m100000000 PLC8_F2.pml

The verification stops at this point:
Depth= 22593301 States= 4.57e+008 Transitions= 6.72e+009 Memory=  6557.176      t= 2.24e+003 R=  2e+005

Is there a limitation on the memory that SPIN can use?

Also, I got the following warning from the GCC compiler:

pan.c:24:25: warning: cast from pointer to integer of different size [-Wpointer-to-int-cast]
#define Offsetof(X, Y) ((ulong)(&(((X *)0)->Y)))
                         ^
pan.h:248:28: note: in expansion of macro 'Offsetof'
#define Air0 (sizeof(P0) - Offsetof(P0, pn53) - 1*sizeof(uchar))
                            ^~~~~~~~
pan.c:677:26: note: in expansion of macro 'Air0'
short Air[] = {  (short) Air0, (short) Air1, (short) Air2 };

Best Regards,

Last edited by Thiago_Tuxi (2021-04-21 15:44:06)

spinroot

forum

Registered: 2010-11-18

Posts: 695

Website

Re: SPIN does not generate an answer in huge models

sorry if this has gone unanswered for so long.
there's really not enough information to see what the issue is
it could be that the search stack is too deep -- can you try with half that size (the -m argument)
and see if that gets further?
it can't be a 32-bit vs 64-bit thing since you're already using over 4GB in this run, but there shouldn't be any other limit than what's available on your system.  does Windows impose a limit per process?
i don't think the gcc warning is an issue here