A forum for Spin users
You are not logged in.
I am trying to do a randomized search process using the -DT_RAND and -DP_RAND option. When I execute the code it runs fine for some seeds, but gets stuck for few others.
For example when I tried to run with -RS38 it worked fine.
But when I tried -RS59 it got stuck. In this case it gets stuck as soon as it find the first collision. When I do CTRL+C and come out, the result shows as follows
State-vector 35684 byte, depth reached 4647, errors: 0
2324 states, stored
1 states, matched
2325 transitions (= stored+matched)
0 atomic steps
I run it as follows
gcc -O2 -DVECTORSZ=64000 -DBITSTATE -DP_RAND -DT_RAND pan.c
./a.out -a -RS59 -w20
The updated model is put at at http://srp7.web.rice.edu/new_pe.pml
Thank you
Sriraj
Offline
Is there a time frame by which the SPIN 6.2.7 will be released?
Since the model is large, we get a hash factor as small as 2. We are relying on randomized search to get some more coverage.
Is there some way to get a patched version of SPIN that fixes this problem or is there some work around that we can try at our side?
We usually create the spin executable from the sources.
Thank you
Sriraj
Offline
I'm also very interested in it: we perform verification on very large models using a swarm approach based essentially on randomized searches. I noticed that sometimes the searches were not terminating, and remained stuck for days. I decided to write you to ask your opinion, but I'm lucky and I already get the answer. However it would be very nice if the bug will be fixed ASAP.
Thank you
Mara
Offline
Thank you very much. That will be very helpful.
Offline
Thank you. Now it is working with different random seeds.
Offline
Thank you very much!!
Offline