Before you start an experiment, you should complete steps 1 and 2:

1. Set the environment variable experiment_root to point to the parent
directory of the subject directory by typing
"setenv experiment_root <path>"

   For example, assume you have a subject directory "allocationvector"
and you locate it under /cs_machine/exp_group/experiments, then you
would set experiment_root by executing the command:

for csh/tcsh:
        setenv experiment_root /cs_machine/exp_group/experiments
for bash:
	export experiment_root=/cs_machine/exp_group/experiments

   The allocationvector subject uses the gov.nasa.jpf.jvm.Verify class
from the JPF library so step 2 below is mandatory.  Due to this
dependency you must use JDK 1.6 and set JAVA_HOME in your shell
environment to point at JDK 1.6.  If JAVA_HOME is set to a JDK < 1.6
you will receive the error:

bad class file: /home/wmotycka/JPF/lib/jpf.jar(gov/nasa/jpf/jvm/Verify.class)
class file has wrong version 50.0, should be 49.0

This error is the clue that your JDK is < 1.6.

2. If you plan to model check the account example using 
Java PathFinder (JPF), set the environment variable jpf_root to point
to the root directory of the JPF installation.

   For example, assuming you have installed JPF  at
/usr/tools/javapathfinder, then you would set jpf_root by executing
the command:

for csh/tcsh:
        setenv jpf_root /usr/tools/javapathfinder
for bash:
	export jpf_root=/usr/tools/javapathfinder

Notes
1. The version of JPF against which this example was tested requires
the use of JDK Version 1.6.
2. The runJPF shell script can be modified to use the expect tool to limit
the amount of time JPF will spend searching the state space. This is useful
for programs with a large statespace. Refer to the runJPF.sh script for
details (shown in the random run sections).
