[klee-dev] Whats the difference between RandomSearcher and RandomPathSearcher?

[Zaman, Tarannum]

Thanks a lot Sean!

On Mon, Oct 12, 2015 at 5:14 PM, Sean Bartell <sean at yotann.org> 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.
>
-------------- next part --------------
HTML attachment scrubbed and removed