Ayrat, Thanks for the clarification. Good to know DiscretePDF is working as intended.
-David On Feb 3, 2011, at 10:16 PM, Ayrat Khalimov wrote: > David, >> If the patch didn't trigger any assertions, then I don't see how DiscretePDF >> could be returning the distribution you reported earlier... > Your patch calculates correctness using node weights. > But the distribution I sent earlier counts state weights - not the node > weights and: > state->weight != states->getWeight (that return node->weight). > If call update then node->weight becomes equal to the state->weight. > > Here is a comparative table of state weights and corresponding node weights > at the moment of taking the statistics: > (The differences happen for states that has been branched) > state->weight discretePDF::getWeight(state) > 0.5 0.5 > 0.25 0.25 > 0.0625 0.0625 > 0.03125 0.125 > 0.03125 0.03125 > 0.015625 0.03125 > 0.015625 0.015625 > 0.0078125 0.0078125 > 0.0078125 0.03125 > 0.0078125 0.0078125 > 0.0078125 0.0078125 > 0.0078125 0.0078125 > 0.0078125 0.0078125 > 0.00390625 0.015625 > 0.00390625 0.00390625 > 0.00390625 0.00390625 > 0.00390625 0.00390625 > 0.00390625 0.00390625 > 0.00195312 0.00195312 > 0.00195312 0.0625 > 0.00195312 0.00195312 > 0.00195312 0.00195312 > 0.000976562 0.000976562 > 0.000976562 0.015625 > 0.000976562 0.000976562 > 0.000488281 0.000488281 > 0.000244141 0.000244141 > 0.00012207 0.00012207 > 6.10352e-05 6.10352e-05 > 3.05176e-05 3.05176e-05 > 1.52588e-05 1.52588e-05 > 7.62939e-06 7.62939e-06 > 3.8147e-06 3.8147e-06 > 1.90735e-06 0.015625 > 1.90735e-06 1.90735e-06 > > > -- > Sincerely, Ayrat > > > > > On Fri, Feb 4, 2011 at 12:43 AM, David A. Ramos <daramos at stanford.edu> > wrote: > Ayrat, > > At a branch, the original state takes one target of the branch, and a new > state (copying the original state) takes the other target. You're correct > that ExecutionState::branch() halves the weights of both resulting states. > Whether to update the weight inside the searcher depends on your definition > of "depth." These are all just heuristics (and this one may not be > particularly effective in either case). > > If the patch didn't trigger any assertions, then I don't see how DiscretePDF > could be returning the distribution you reported earlier... > > -David > > On Feb 3, 2011, at 1:07 PM, Ayrat Khalimov wrote: > >> David, >> thanks for the patch - I applied it and it didn't reveal any bugs in >> DiscretePDF. >> >> The depth of a state is a static measurement, so there's no need to update >> the weight of a state over time. Other metrics, like distance to uncovered >> instructions, do change over time. >> OK. In this case updateStates should be false. >> >> Could you please answer the following question: >> What happens with ExecutionState in klee after it has been branched? (After >> the call to ExecutionState::branch()) >> This call changes state weight: >> ExecutionState.cpp:99: >> weight *= .5; >> >> Is this state removed? >> Or it continues living? >> >> I am working on Cloud9 version of klee and here we have branched states that >> continue its living after branch happened. And weights are changing >> (state.weight != node.weight). >> >> >> >> -- >> Best regards, >> Ayrat >> >
