A forum for Spin users
You are not logged in.
Pages: 1
Ok, so with:
gcc -DSAFETY -DCOLLAPSE -DVECTORSZ=6144 -o pan pan.c
the results are:
Depth= 159 States= 1e+006 Transitions= 4.96e+006 Memory= 138.757 t= 179 R= 6e+003
Depth= 159 States= 2e+006 Transitions= 1e+007 Memory= 244.615 t= 363 R= 6e+003
pan: resizing hashtable to -w21.. done
gcc -DSAFETY -DMEMLIM=4096 -DVECTORSZ=6144 -o pan pan.c
the results are:
pan: out of memory
1.9353e+009 bytes used
600000 bytes more needed
4.29497e+009 bytes limit
with 0 errors
Finally with: gcc -DSAFETY -DBITSTATE -DVECTORSZ=6144 -o pan pan.c
each proctype is unreached.
Maybe there are other type of errors in my Promela code.
Hi! I read this interesting topic because I had a similar problem with VECTORSZ.
I use Win7. In command line I submitted : gcc -DSAFETY -DVECTORSZ=4096 -o pan pan.c
but JSpin always returns : pan:1: VECTORSZ is too small, edit pan.h (at depth 0) with 1 error
so I tried with : gcc -DSAFETY -DVECTORSZ=8192 -o pan pan.c
but it returns :
pan: out of memory
hint: to reduce memory, recompile with
-DCOLLAPSE # good, fast compression, or
-DMA=5916 # better/slower compression, or
-DHC # hash-compaction, approximation
-DBITSTATE # supertrace, approximation
(Spin Version 6.0.0 -- 5 December 2010)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 5916 byte, depth reached 159, errors: 0
359829 states, stored
1163880 states, matched
1523709 transitions (= stored+matched)
74554 atomic steps
hash conflicts: 135148 (resolved)
1935.594 memory usage (Mbyte)
pan: elapsed time 24.4 seconds
pan: rate 14724.762 states/second
How can I resolve this trouble?
Thanks!
Yes sure.
spin: promela_c.pml:61, Error: syntax error saw ''(' = 40'
59 proctype Copy_Init()
60 {
61 set_syntax(variable, -1, 1);
62 set_syntax(variable, -1, 3);
63 set_syntax(variable, -1, 4);
64 set_syntax(variable, -1, 5);
65 set_syntax(variable, -1, 8);
66 set_syntax(variable, -1, 10);
67 set_syntax(variable, -1, 14);
68 }spin: promela_c.pml:160, Error: syntax error saw ''(' = 40'
spin: promela_c.pml:160, Error: syntax error saw 'process name' near 'set_syntax'
spin: promela_c.pml:160, Error: syntax error saw 'an identifier' near 'X_obj'
158 s1:
159 if
160 ::flow[c_copy]?inn -> Copy_Init();Copy_Copy();Copy_getFileUtils();Copy_setToFile();Copy_setToDir();Copy_setToDir();Copy_createFilterSet();Copy_setPreserveLastModified();Copy_setVerbose();Copy_execute();Copy_getFilterSet();flow[c_run]!out;
161 goto s0;
162 fi;Hi! I'm new on SpinRoot.
When I try to check my Promela Code, Spin returns:
Error: syntax error saw ''(' = 40'
Error: syntax error saw ''(' = 40'
Error: syntax error saw 'process name' near 'set_syntax'
Error: syntax error saw 'an identifier' near 'X_obj'
Error: no runable process40 there isn't a symbol in my code, someone can help me? Thanks in advance.
-
sylvy
Pages: 1