Re: [Javapathfinder-user] Problem with newer versions of JPF???

[Peter C. M. <Pet...@na...>]

must be a bug in HeuristicSearch, I'll have a look. It works well with  
DFSearch.

BTW - don't use vm.por=false. This is going to be dropped, and can be  
considered non-functional at this point

-- Peter



On Jun 23, 2008, at 2:51 PM, Marco Ferreira wrote:

> Hi,
>
> I'm facing a problem with the latest versions of JPF. I tried to use  
> BFS to search for the deadlock in the DiningPhilosophers problem  
> with only 2 philosophers (so it should be rather quick to find the  
> deadlock). However, after some steps, JPF seems to loop in an  
> infinite cycle in the executeStep() method. Any ideas about what's  
> going on? I've executed JPF on Windows with Java 1.6 using the  
> following command line:
>
> java -cp .\build\jpf;.\lib\bcel.jar;.\build\env\jvm;.\build\examples  
> -Xmx512M -Xms512M gov.nasa.jpf.JPF +vm.por=false  
> +search.class=gov.nasa.jpf.search.heuristic.HeuristicSearch  
> +search.heuristic.class=gov.nasa.jpf.search.heuristic.BFSHeuristic  
> DiningPhilosophers.DiningPhilosophers
>
> This worked quite well in older versions...
>
> Marco Ferreira