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
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...
]]>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?
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.
]]>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