[klee-dev] WeightedRandomSearcher and DiscretePDF

[David A. Ramos]

Hey Ayrat,

DiscretePDF::choose() is supposed to return nodes uniformly distributed over the sum of the weights of all the nodes. That is, a node with weight 2N is twice as likely to be chosen as a node with weight N. It's supposed to be uniform, however, so the results you report are worrisome.

The class maintains the sum of the weights of the left/right subtrees at each node, and choose() uses the random value to guide its traversal of the tree.

Daniel, Christi, et. al, if there is a bug in DiscretePDF, it could explain the coverage problems we've been discussing. As I've indicated, I think the problem is in the searchers somewhere.

-David

On Jan 31, 2011, at 12:42 PM, Ayrat Khalimov wrote:

> Hi, All, 
> During testing different path exploration strategies (WeightedRandomSearcher with Depth WeightType)
> I have encountered an interesting class - DiscretePDF.
> What is its purpose?
> Ok, the first purpose is clear - it is an associative set (looks like red-black tree).
> But what about its choose method?
> Does it choose states according to some probability distribution of values? If yes - then what distribution does it use? The more weight the greater/less probability? How it take into account states' depth (or states' weight) ?
> (I found no known to me distribution of chosen values during experiments.. please correct if this is wrong)
> 
> Also what is strange is that the location of the node in the DiscretePDF internal tree depends on memory address of inserted value. 
> And child-parent connection depends on these memory addresses. And doesn't depend on weights.
> But the result of choose method depends on the total weight of the node (with kids weights) and hence on the structure of the internal tree. And hence the result of choose method depends on memory addresses of ExecutionState objects..
> 
> I've made an experiment. When tree size reach 30 states, 10000 samples are chosen:
> if(nodesCount > 30) {
>     for(int i = 0; i < 10000; ++i) {
>       ExecutionState* state = states->choose(theRNG.getDoubleL());
>       std::cerr << state->weight << "\t" << states->getFamilyWeight(state) << std::endl;
>     }
> }
> 
> Results:
> here is two distributions of chosen values:
> 1. own node weight (range of own weight, the number of values chosen in this range)
> 0.05    4003
> 0.1     0
> 0.15    0
> 0.2     0
> 0.25    1993
> 0.3     0
> 0.35    0
> 0.4     0
> 0.5     3880
> 
> 2. sum node weight (weight of node + weights of its children):
> 0.1     1784
> 0.2     554
> 0.3     1986
> 0.4     0
> 0.5     0
> 0.6     0
> 0.7     0
> 0.8     4157
> 1.3     1519
> 
> As you can see - quite a strange distribution.
> (Also checked the random generator - it is ok - random distributed).
> 
> Please comment on these questions.
> 
> Thanks!
> 
> --
> Sincerely, 
> Ayrat Khalimov,
> Russia, Uljanovsk
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev