Ayrat,
Thanks for the clarification. In that case, some of the results do seem valid.
At first glance, the single 0.5 state was chosen twice as often as the 0.25
state.
The bucket size for weights <= 0.05 is a little deceptive since it includes
states with much smaller weights. In reality, what matters is the sum of the
weights of all the states in that bucket. With the data you gave, that's a sum
of 0.234 for the 29 "smaller" states. Now, if DiscretePDF is working correctly,
it should have chosen states from this bucket about as often as it chose the
single state with weight 0.25.
However, it chose these smaller states twice as often, which is wrong (assuming
the RNG is working correctly). Disproportionately choosing states with smaller
weights could certainly be one source of low coverage.
Can you try applying the patch I sent out and see how that affects these
results?
Thanks for your help,
-David
On Feb 1, 2011, at 12:03 PM, Ayrat Khalimov wrote:
> David, thanks,
> 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
>
> Looked again at my experiment. There is definitely a weak point:
> initial distribution of weights of states is not a uniform distribution -
> there are lots of states with small weights and very little states with large
> weights:
> 0.5, 0.25, 0.03125, 0.03125, 0.03125, 0.015625, 0.015625, 0.015625, 0.015625,
> 0.0078125, 0.0078125, 0.0078125, 0.00390625, 0.00390625, 0.00390625,
> 0.00390625, 0.00390625, 0.00390625, 0.00390625, 0.00390625, 0.00390625,
> 0.00390625, 0.00195312, 0.00195312, 0.00195312, 0.00195312, 0.00195312,
> 0.00195312, 0.00195312, 0.000976562, 0.000976562
>
> Well, in this case I think it is OK to have described earlier distribution:
> 0.05 402
> 0.1 0
> 0.15 0
> 0.2 0
> 0.25 198
> 0.3 0
> 0.35 0
> 0.4 0
> 0.45 0
> 0.5 400
>
> What do u think?
>
>
> --
> Best regards,
> Ayrat
>
>
>
> On Tue, Feb 1, 2011 at 5:24 AM, David A. Ramos <daramos at stanford.edu>
> wrote:
> 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/20110201/8499a6e3/attachment.html
