[klee-dev] Whats the difference between RandomSearcher and RandomPathSearcher?
Sean Bartell
sean at yotann.org
Mon Oct 12 22:14:23 BST 2015
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
More information about the klee-dev
mailing list