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
