Thanks a lot Sean! On Mon, Oct 12, 2015 at 5:14 PM, Sean Bartell <[email protected]> wrote:
> Zaman, Tarannum on 2015-10-12: > > What I have understand that RandomSearcher selects next state randomly. > But what actually the RandomPathSearcher in Klee is doing? How it selects > its next state and what is the difference between this two searcher? > > Suppose KLEE has 3 states: one where the path is False (at first branch), > one where the path is True (at first branch), False (at second branch), and > one where the path is True (at first branch), True (at second branch). > > RandomSearcher gives each state a 1/3 probability, but there are two > states starting with True and only one state starting with False, so > there's a 2/3 probability of choosing a state that starts with True. So > it's fair between the states, but it's unfair between the paths in some > sense. > > RandomPathSearcher starts at the root and chooses a random direction at > each branch with equal probability. It keeps going until it finds a state. > So it has a 0.5 probability of choosing False and selecting the False > state; if it chooses True, it makes another random choice for the second > branch, so in total it has a 0.25 probability of choosing the True, False > state and the same for the True, True state. So RandomPathSearcher is > unfair between the states, but it's fair between the paths. >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
