error JPF configuration , please help !!

[naouar...@gmail.com]

hi all ,

i'm trying to run jpf from command , for example to check DiningPhil class  contained in JPFModels.jar
the jpf batch is like this :

SET CLASSPATH=C:\JPF\lib\bcel.jar;C:\JPF\lib\jpf-marco.jar;C:\JPF\lib\JPFModels.jar;C:\JPF\lib\JPFMetaH.jar;C:\JPF\lib\sACO.jar
SET JAVAEXEC="C:\Program Files\Java\jdk1.6.0_19\bin\java"

%JAVAEXEC% -cp %CLASSPATH% -Xmx1024M -Xms1024M gov.nasa.jpf.JPF -c %1 %2 %3 %4 %5

i'm  using  a 32bits machine .

when i execute this line of code : c:\JPF\bin\jpf-exec -c dfs.conf DiningPhil 4    the following error appears :
[WARNING] no defaults.properties found
JPF configuration error: no classname entry for :" vm.class"

could someone please tell me what's failing ??

Thank you.

[Peter Mehlitz]

jpf.jar is not in the host VM classpath, but that is most likely not your only problem since you don't set JPF's 'classpath', i.e. JPF wouldn't find your system under test. Please note that running JPF requires setting two classpaths - one for the host VM to find all the classes (including extensions) that constitute JPF itself ('native_classpath'), and one for the classes that have to be loaded/executed by JPF ('classpath' - your system under test). While you can set this up manually, JPF has a lot of infrastructure to construct these paths from its configuration files (Config, RunJPF etc.). Please see http://babelfish.arc.nasa.gov/trac/jpf/wiki/user/config for details.

P.S. JPF does not need bcel, make sure you have a recent JPF version

-- Peter

[naouar...@gmail.com]

Hi Peter ,

Thanks for ansewring.
Yes, i'm not using the latest jpf version . But it worked some time , and now i don't really understand why i have this error!! i have to say that i'm using a machine of 32bit , do you think that could be the problem?

Thnk you for your help.

Noa

[Peter Mehlitz]

it depends on how old your JPF version is - really old versions didn't differentiate between the classpaths and just used the host VM setting (CLASSPATH environment var). If you did update and rebuild JPF these configs wouldn't work anymore.

jpf-core itself is pure Java doesn't depend on 32 or 64 bit

-- Peter