How to REALLY get the JPF eclipse plugin running on OSX

jpf_plugin_osx.txt

1) Install the plugin using the instructions from the wiki.

Ensure that you are running Eclipse >= 3.5 (Galileo)
In Eclipse go to Help -> Install New Software
In the new window selected "Add"
The name is up to you but, set "Location" to http://babelfish.arc.nasa.gov/trac/jpf/raw-attachment/wiki/install/eclipse-plugin/update/
From the "Work with:" drop down menu select the update site that you just entered from the previous step
Check the "Eclipse-JPF" check box, select "Next" and go through the install process.

2) Download the jpf core binary and extract it somewhere: http://babelfish.arc.nasa.gov/trac/jpf/attachment/wiki/projects/jpf-core/jpf-core-r615.zip

3) Create a site.properties file and save it somewhere. Mine looks like this.

# JPF site configuration
jpf-core = ${user.home}/Programming/jpf-core
extensions=${jpf-core}

Note that jpf-core points to where I extracted the zip archive in step 2.

4) In Eclipse, go to Eclipse-> Preferences -> JPF Preferences and set the path to site.properties to the file you created in step 3.

5) Create an Eclipse project with some classes in it.

6) Create a settings.jpf file in your eclipse project. Here's mine:
target = pset3.TestSequenceGenerator
classpath = ./bin/;${classpath}

pset3 is the package that TestSequenceGenerator is in.
classpath is the full path to the bin directory of the eclipse project.

7) Right click on your exmaple.jpf file inside eclipse and click "verify". If it's working you'll see output like this: 

Executing command: java -jar /Users/burt/Programming/jpf-core/build/RunJPF.jar +shell.port=4242 /Users/burt/Programming/workspace/TestingHW3/hw3.jpf 
JavaPathfinder v6.0 (rev 611+) - (C) RIACS/NASA Ames Research Center


====================================================== system under test
application: pset3/TestSequenceGenerator.java

====================================================== search started: 4/10/12 3:11 PM

====================================================== results
no errors detected

====================================================== statistics
elapsed time:       00:00:00
states:             new=1, visited=0, backtracked=0, end=1
search:             maxDepth=1, constraints hit=0
choice generators:  thread=1 (signal=0, lock=1, shared ref=0), data=0
heap:               new=665, released=29, max live=665, gc-cycles=1
instructions:       3881
max memory:         81MB
loaded code:        classes=95, methods=1210

====================================================== search finished: 4/10/12 3:11 PM