[klee-dev] WeightedRandomSearcher and DiscretePDF

[David A. Ramos]

Ayrat,

Can you tell me if this patch changes your results at all? If not, could you send us the complete code for the experiment you're using to evaluate DiscretePDF?

Daniel/Cristi: It seems like after a rotation, we should be setting the sums of the child before the parent, which relies on the child.

Thanks,
-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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20110131/113823c2/attachment.html 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: discretePDF.patch
Type: application/octet-stream
Size: 392 bytes
Desc: not available
Url : http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20110131/113823c2/attachment.obj 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20110131/113823c2/attachment-0001.html