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