A forum for Spin users

You are not logged in.

#1 2012-10-19 10:30:53

Registered: 2012-05-30
Posts: 24

Depth of a verification and measure of the explored tree

Hi to all!
I'm running the verification of my model, that use 53 byte variables and has 34 different instructions, executable or not depending on the value (of one or more) of the variables.
I'm searching for all the execution trails in which a simple assertion is not verified at timeout (i.e. I've got two processes running, the one with my instructions and another one with the timeout->assert() instruction). The assertion takes into account the value of a single variable being < predefined number.

Obviously the execution tree is huge, and since I need all the traces (i.e. all the counterexamples) in which my assert is not valid, I have a lot of issues with memory usage.
Hence I tried the minimal automaton representation compiling Pan with -DMA option.
My verification is still running after a day, and the verbose output reports:

Depth=     382 States=    1e+06 Transitions=  5.4e+06 Nodes=    9902 Memory=     0.929    t=     21.2 R=   5e+04
Depth=     446 States= 3.08e+09 Transitions= 2.32e+10 Nodes=  753462 Memory=    46.340    t= 8.67e+04 R=   4e+04

Now the questions:
1) the Depth of the search is always increasing? Or eventually in the future this value will decrease when backtracking? This will be a very loose indication of the time I should wait for the verification of the longest branches of the tree...

2) It is possible to "measure" the extent of the explored portion of the execution tree from the information on Depth, Transitions, and Nodes? It will be interesting knowing how much it has been exhaustively explored and what is the extent of the remaining part. It will be for me a "degree of confidence" on the obtained counterexamples.

Thanks in advance for your attention,



#2 2012-10-21 05:32:00

Registered: 2010-11-18
Posts: 694

Re: Depth of a verification and measure of the explored tree

Re 1) The depth reported is the max reached, so it will never decrease during a run.
Re 2) nope, since it cannot be known how large the stte space is without first completing an exhaustive run...


Board footer

Powered by FluxBB