Installing jpf-prism

In case you were interested in running jpf-prism while it is under development, this blog post will tell you how to do that.

What you'll need: Eclipse (possibly with Mercurial and SVN), jpf-core, jpf-nhandler, jpf-probabilistic, PRISM (built from source), and of course jpf-prism.

First, if you need to install JPF, download and build jpf-core, which is available here via Mercurial:  http://babelfish.arc.nasa.gov/hg/jpf/jpf-core. If it asks for a version, take the "default" version (not v6), as the system is being developed for v7 which is default as of June 22nd (see here). Build the project, and then install the JPF Eclipse plugin and set up your site.properties file.

Second, download and build jpf-nhandler from the following Mercurial repository: https://bitbucket.org/nastaran/jpf-nhandler . Make sure that you modify your site.properties file to include it as described on the BitBucket page.

Third, download and build jpf-probabilistic from the following Mercurial repository: https://bitbucket.org/discoveri/jpf-probabilistic . Again, make sure that you modify your site.properties file to include it as described on the BitBucket page. (Note: since the interesting classes we're using in jpf-prism have been copied into jpf-prism, this might not actually be necessary, but I'm including it to be safe.)

Next, download the source for PRISM, build it (for the C/C++ parts), and set it up for Eclipse as described here (you can also get it from SVN). Then make a new a project in Eclipse and import the prism directory (as described in the last link) and build it again (for the Java files). Then add a variable, say prism-jpf, to your site.properties file pointing to the classes folder of the build, for example: prism-jpf = ${user.home}/GSoC2013 Workspace/prism-jpf/prism/classes/

Lastly, download and build jpf-prism, which is available  from the following Mercurial repository: https://bitbucket.org/jpfprism/jpf-prism . Add jpf-prism to the site.properties file, for example: jpf-prism = ${user.home}/GSoC2013 Workspace/jpf-prism (or wherever your jpf-prism project is located) and adding ${jpf-prism} to the extensions variable.

Now you should be ready to go! To test the installation, try using JPF to verify the BiasedDieTest.java by creating BiasedDieTest.jpf and putting the following in:
@using = jpf-nhandler
target=probabilistic.BiasedDieTest
classpath=${jpf-probabilistic}/build/jpf-probabilistic-examples.jar
native_classpath= ${prism-jpf}
listener=prism.listener.MarkovExporter

Then run JPF on the .jpf file. And that's it. If there are any concerns or comments, please feel free to contact me.