[Javapathfinder-user] Running JPF

[Martijn H. <mar...@cs...>]

Hi,

I am new to JPF and I am trying to modelcheck the HelloWorld app in the 
example directory. I just cannot get it to work:

javapathfinder > bin/jpf examples/HelloWorld.class
Java Pathfinder Model Checker v3.1.2 - (C) 1999-2004 RIACS/NASA Ames 
Research Center
JPF exception, terminating: could not load class examples.HelloWorld.class

examples > ../bin/jpf HelloWorld.class
Java Pathfinder Model Checker v3.1.2 - (C) 1999-2004 RIACS/NASA Ames 
Research Center
error during VM runtime initialization: wrong model classes (check 
vm.[boot]classpath)

and i tried a lot more... I probably need to set some paths, but I can't 
figure what to do exactly.

The "ant run-tests" works fine: no errors are reported (I am using 
j2sdk1.4.2_08 on Linux).

It would be great if someone could help me with this.

Thanks!

Martijn Hendriks