David,
Applied patch and got similar distribution (before, after):
0.05 403 335
0.1 0 52
0.15 0 0
0.2 0 0
0.25 193 184
0.3 0 0
0.35 0 0
0.4 0 0
0.45 0 0
0.5 391 413
The states changed but the sum of weights below 0.05 remained the same ~
0.234.
After applying the patch states at the moment of gathering data were:
0.5, 0.25, 0.0625, 0.03125, 0.03125, 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.00195312,
0.00195312, 0.00195312, 0.00195312, 0.00195312, 0.00195312, 0.00195312,
0.00195312, 0.000976562, 0.000976562, 0.000976562, 0.000488281, 0.000244141,
0.00012207, 6.10352e-05, 3.05176e-05, 1.52588e-05, 7.62939e-06, 3.8147e-06,
1.90735e-06, 1.91E-006
For transparency here is the description of the experiment:
run printf.bc (with --sym-args 0 2 4) under klee. Used *WeightedRandomSearcher
*with *Depth WeightType.*
In the call selectState the check on number of states in the DiscretePDF is
added -- when DiscretePDF contains more than 30 states start gathering data
(call choose with *theRNG*).
--Sincerely, Ayrat
On Tue, Feb 1, 2011 at 11:26 PM, David A. Ramos <daramos at stanford.edu>wrote:
> 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/20110202/7d8a2d28/attachment-0001.html
