A forum for Spin users
You are not logged in.
Pages: 1
Can anyone please tell me the proper way of removing this warning both in ispin and using command line
warning: never claim + accept labels requires -a flag to fully verify
pan: out of memory
error: max search depth too small
Last edited by MuhammadIsmail (2012-10-19 17:48:16)
Offline
To remove the warning, you'll need to enable a search for acceptance cycles.
From the command line you do that by adding runtime flag -a to ./pan
To resolve the out of memory problem you can try to compile with -DHC4
To avoid hitting the search depth limit, just specify a larger search depth with -m
For instance:
./pan -a -m100000
Offline
Depth= 15771 States= 5.3e+07 Transitions= 2.48e+08 Memory= 1723.618 t= 2.15e+03 R= 2e+04
Depth= 15771 States= 5.4e+07 Transitions= 2.54e+08 Memory= 1750.512 t= 2.2e+03 R= 2e+04
What about t and R in the above lines of verification result?
State-vector 1772 byte, depth reached 15771, errors: 0
58341410 states, stored
2.17569e+08 states, matched
2.7591041e+08 transitions (= stored+matched)
35 atomic steps
hash conflicts: 1.0721985e+08 (resolved)
What things are included in State-vector?
There are alot of hash conflicts? Why is this such a great number? Has it any effect on verification? I am new one. so please briefly explain.
Can you please tell me some way by which no memory limit is imposed during verification. Also tell me about pan: out of memory. If all memory is consumed and this error happens, then can we say that the property is completely verified.
Last edited by MuhammadIsmail (2012-10-31 15:11:41)
Offline
t is the time that has elapsed since the start of the run
R is the rate of verification: the number of new states explored per second
The number of hash conflicts is high, but that does not affect the correctness of the verification, just the speed
(more conflicts = slower, because they need to be resolved in the hash-table)
you can reduce the number by picking a larger value for the -w parameter
when the run runs out of memory, and it has not found errors up to that point, there is no guarantee that there will be no errors if the search could continue up till the end; so in that case the search remains incomplete
there are a number of strategies that you can explore in that case to reduce memory use.
for instance, try compiling with -DCOLLAPSE, or -DHC4, or -DBITSTATE
Offline
How can we increase -w parameter in ispin. I am a new one. tell me
Offline
use ./pan -w28
(every increment in the value of -w will double the size of the hash-table.
if you pick a value that is too large, ./pan will fail because it will not be able to allocate the required memory.
if you pick a value that is too small, you incur more hash collisions)
Offline
Two questions are still pending. Kindly answer.
Q. What things are included in State-vector?
Q. Can you please tell me some way by which no memory limit is imposed during verification. Also tell me about pan: out of memory. If all memory is consumed and this error happens, then can we say that the property is completely verified.
Offline
The memory limit is ultimately imposed by the machine you are using: it only has a finite amount of RAM memory and that sets the memory limit...
I've answered the other question earlier: when the verification stops when you are out of memory, the verification is not complete, and therefore the model is also not completely verified.
The state vector defines the complete state of the system.
Offline
Another thing i need to know
I have tried -DHC4 -DBITSTATE and the physical memory available value as 10000 Mbytes. Even in these cases it gives error "pan: out of memory" after a lot of time. What can be done in this case. Kindly guide me on these guidelines. I am getting bored and tired now.
I can send you promela model if required for suggestions. Will be thankful for your cooperation. I have also tried -BITSTATE. Following are some of the lines of verification result.
pan: out of memory
hint: to reduce memory, recompile with -DBITSTATE # supertrace, approximation
pan. elapsed time 1.92e+03 seconds
No errors found -- did you verify all claims?
Last edited by MuhammadIsmail (2012-11-01 18:33:43)
Offline
if you add both HC4 *and* BITSTATE, I'm not sure which of these is going to win, or if pan.c will compile at all.
you'll have to choose one or the other, but you cannot use both simultaneously...
BITSTATE will never run out of memory
HC4 can, but only for very large problem sizes
if you still see an out of memory error then you'll have to reduce the complexity of the model -- use abstraction etc.
If you want to learn how to use the model checker well your best bet is to read one of the books that teach you how to do that, or to read through the tutorials that are online...
Offline
There is another question. I am not feeling well by questioning again and again. Kindly answer.
Q. In ispin is it possible to verify multiple LTL properties simultaneously. From the warning I have mentioned below, I think that may be this is possible.
warning: only one claim defined, -N ignored
Q. This is a short part of verification result. The depth doesn't increase, can you tell me the reason. Why it happens like this.
Depth= 301 States= 4e+06 Transitions= 1.35e+07 Memory= 21.150 t= 324 R= 1e+04
Depth= 301 States= 5e+06 Transitions= 1.67e+07 Memory= 21.150 t= 403 R= 1e+04
Depth= 301 States= 6e+06 Transitions= 1.93e+07 Memory= 21.150 t= 467 R= 1e+04
Depth= 301 States= 7e+06 Transitions= 2.28e+07 Memory= 21.150 t= 559 R= 1e+04
Depth= 301 States= 8e+06 Transitions= 2.6e+07 Memory= 21.150 t= 635 R= 1e+04
Depth= 301 States= 9e+06 Transitions= 2.95e+07 Memory= 21.150 t= 795 R= 1e+04
Depth= 301 States= 1e+07 Transitions= 3.23e+07 Memory= 21.150 t= 893 R= 1e+04
Depth= 301 States= 1.1e+07 Transitions= 3.51e+07 Memory= 21.150 t= 977 R= 1e+04
Depth= 301 States= 1.2e+07 Transitions= 3.84e+07 Memory= 21.150 t= 1.07e+03 R= 1e+04
Last edited by MuhammadIsmail (2012-11-02 06:07:04)
Offline
you can convert multiple claims into one, but that is almost never a smart thing to do.
spin only verifies one claim at a time
you can select which one with the -N parameter -- and if there's just one claims, that's the one you get of course
Offline
what abt my second question
Offline
I don't know whether i am right or wrong but if it reaches the maximum depth first time (doesn't change throughout verification) then why its verification is continued for 50 min or 60 min. Clarify me I dont know.
Offline
Thanks alot for your cooperation and prompt reply. Grateful to you.
Offline
Pages: 1