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