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
