[klee-dev] Different between DFS Searcher and Random Searcher

[Loi Luu]

Hi,

Thank you for your answer, it makes sense to me :). After looking back at
the source  code, I realize that the DFS seacher add new states to the end
and get state from that direction also. Hence it will go deeper at any
branch. That's pretty clear now. Hence, I think that for BFS searcher, we
will insert the new states at the front of the vector and get state from
the end, right?

Best regards,


On Sun, Apr 14, 2013 at 4:58 PM, <gwpublic at wp.pl> wrote:

> Hi,
>
> > Random one. As I see from the source code (klee/lib/Core/Searcher.cpp),
> they are different in only the selectState() method, that makes me in
> doubt. I think that there must be other different point, but I couldnt
> figure it out.
>
> It makes perfectly sense, why would you need sth more to change order?
>
> > By the way, I still dont understand why we call it DFS based on the
> source code, it does not clear to me. So can you give me any hint/ point?
>
> Sorry, AFK responding from Tablet :-) .
>
> Hint might be that you can implement DFS.BFS etc in many many different
> ways and still they will be same algorithm.
> To point in code I would need to sit at PC from laptop.
>
> Best regards,
> Grzegorz Wierzowiecki
>



-- 
Loi, Luu The (Mr.)
University of  Engineering and Technology, Vietnam National University,
Hanoi.
-------------- next part --------------
HTML attachment scrubbed and removed