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, <[email protected]> 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.
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
