Running JPF

Executing JPF from the command line is easy - the jpf script (residing in the jpf/bin directory) acts as a drop in replacement for the normal 'java' executable. In case you don't have specific initialization needs (see [sec:Lots-of-Options]), all you need to do is to call the bin/jpf script with the class name of the main application class to check, and append any arguments the application is expecting. The formal syntax is:

> bin/jpf [-c config-file] {+key=value ..} app-class {app-args ..}

  -c config-file     optionally specifies the java.util.Properties file
                     that should be used for JPF configuration
                     (default is '')
  +key=value         is a convenient way to override configuration properties
                     via the commandline

Please note that the old -show option has been superceeded by the new reporting subsystem (e.g. the property) and is not supported anymore

A pure Java replacement for that shell script is available as the class RunJPF in the Java PathFinder install root. Simply replace "bin/jpf" above with "java RunJPF" to use this alternative. More information is available by running "java RunJPF" with no arguments.

RunJPF does not, however, tweak the host VM settings, as VM_ARGS does in the bin/jpf script. Thus, when directly starting your host VM (the "java" command) from the command line, it is wise to increase the maximum heap size with the -Xmx VM argument (e.g. -Xmx1024m).

One can also set up the required classpaths oneself and directly invoke gov.nasa.jpf.JPF as the Java main:

> java {vm-args..} gov.nasa.jpf.JPF jpf-args

To setup the classpath, make sure the following code is reachable, either by setting the CLASSPATH environment variable, or by using the -classpath VM command line argument

JPF can also be used embedded (e.g. an IDE), i.e. called from another Java application. The jpf/src/gov/nasa/jpf/tools/ directory contains various examples, e.g. the ExecTracker application that logs various aspects of JPF execution. A basic code sequence to start JPF looks like this:

import gov.nasa.jpf.JPF;
import gov.nasa.jpf.Config;
import gov.nasa.jpf.SearchListener;
import gov.nasa.jpf.VMListener;

void runJPF (String[] args) {
   MyListener listener = new MyListener(..);
   listener.filterArgs( args);  // 'null' any consumed args not to be JPF-processed
   Config config = JPF.createConfig( args);
   // set special config key/value pairs here..

   JPF jpf = new JPF( config);
   jpf.addVMListener( listener); // or addSearchListener;

If you run JPF from outside it's directory structure, e.g. from within a different project, there is one preferred way to tell it where to look for its default configuration file(s) - the jpf.basedir property. Assume you run JPF from within project MyProject, which happens to be a sibling directory of where JPF is located:

      jpf               --- shell script to run JPF
      jpf/              --- where the JPF core classfiles are 
      env/jvm/          --- where the MJI models are
      ..  --- the default configuration file
  MyProject/   --- the mode/application property file(s)

Then you want to run JPF by either giving it the jpf.basedir setting from the commandline:

> export CLASSPATH=<your-jpf-dir>/build/jpf:\
> cd MyProject
> java gov.nasa.jpf.JPF +jpf.basedir=../<your-jpf-dir> ...

or specify it in a mode/application property file (e.g. If you use the provided <your-jpf-dir>/bin/jpf script to start JPF, you don't have to set the CLASSPATH explicitly.

The same applies to Eclipse launch configurations: