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 'jpf.properties')
  +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 +jpf.report.console.start=...:config 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 classes (either explicitly from the jpf/build/jpf/ directory, or implicitly via jpf.jar)
• library abstractions to use by JPF (per default in the jpf/build/env/jvm/ directory, or in jpf.jar)
• BCEL (the Bytecode Engineering Library from http://jakarta.apache.org/bcel/, usually in bcel.jar)
• optionally - your additional JPF extension classes (listeners, properties etc.)

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
   jpf.run();
   ..
}

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:

  ..
  <your-jpf-dir>/
    bin/
      jpf               --- shell script to run JPF
    build/
      jpf/              --- where the JPF core classfiles are 
      env/jvm/          --- where the MJI models are
      ..
    default.properties  --- the default configuration file
  ..
  MyProject/
    my-jpf.properties   --- 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:\
                   <your-jpf-dir>/build/env/jvm:\
                   <your-jpf-dir>/lib/bcel.jar
                 ...
> cd MyProject
> java gov.nasa.jpf.JPF +jpf.basedir=../<your-jpf-dir> ...

or specify it in a mode/application property file (e.g. my-jpf.properties). 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:

• add the JPF project as a "required project" to the "Java Build Path/Projects" tab in the MyProject "Properties" dialog
• specify gov.nasa.jpf.JPF as the main class in the "Run" dialog
• add a +jpf.basedir=../<your-jpf-dir> to the "Arguments" tab of the "Run" dialog