How to install jpf-concurrent module

JPF is tool for static code analysis. I tried to use it for proving that code is thread safe. In multiple thread environment is problem with JVM 'state explosion'. When JPF try to examine all possible JVM states in multiple thread environment number of possible states grow exorbitantly. As documentation say this problem could be solved with module jpf-concurrent.

Because I didn't find guide how to install it here is simple guide.

Prerequisites

• linux/unix system, in my case it's Mac OSX
• Installed mercurial SCM
• Installed Apache ANT
• Installed jpf-core

Installation steps

• Go to directory where is jpf-core installed. In my case it's directory '/Users/jan/projects/jpf/'
• Checkout project

  hg clone http://babelfish.arc.nasa.gov/hg/jpf/jpf-concurrent

• Build jpf-concurrent project

  ant

• Edit your site property file. In my case is at '/Users/jan/.jpf/site.properties'. Add there following section:

  # concurrent extension
  jpf-concurrent = ${jpf.home}/jpf-concurrent
  extensions+=,${jpf-concurrent}
  

Ant it's done. Good luck.

[EDIT] - After some time of using jpf-concurrent project I had following problem:

gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
java.lang.IllegalMonitorStateException
at java.util.concurrent.locks.ReentrantLock.unlock(gov.nasa.jpf.concurrent.peers.JPF_java_util_concurrent_locks_ReentrantLock)
at com.coroptis.jblinktree.NodeLocks.unlockNode(NodeLocks.java:96)
at com.coroptis.jblinktree.NodeStoreImpl.unlockNode(NodeStoreImpl.java:59)

I contacted Nastaran Shafiei via google group, he is creator of jpf-concurrent. He told me, that jpf-concurrent module is outdated and no longer supported. So I removed jpf-concurrent module and path finder start work fine.

So, do NOT install jpf-concurrent module.