====== Java PathFinder ======

A lot of information about JPF can be found
[[http://javapathfinder.sourceforge.net/|here]].

More information can be found
[[http://www.cse.yorku.ca/~sergey/jpf/|here]].

Although it describes an old version of JPF, 
[[http://www.havelund.com/Publications/jpf-manual.ps|this]]
manual may be useful.

Please do //not// run jpf on indigo, but instead use, for example, navy.

To configure JPF, you may want to use a 
jpf.properties file containing
<code>
search.class = gov.nasa.jpf.search.heuristic.BFSHeuristic
</code>
to use a breadth-first traversal of the state space (rather than a depth-first traversal which is the default).  To check for
race conditions, you may want to add\\
<code>
jpf.listener = gov.nasa.jpf.tools.PreciseRaceDetector
</code>
to your jpf.properties file.

To check some properties of our solution to the
readers-writers problem by means of JPF, we
modified our solution as follows (the attribute writers
and assertions have been added).

<code java>
/**
 * This class represents a database.  There are many competing
 * threads wishing to read and write.  It is acceptable to have
 * multiple processes reading at the same time, but if one thread
 * is writing then no other process may either read or write.
 */
public class Database
{
  private int readers; // number of active readers
  private int writers; // number of active writers

  /**
     Initializes this database.
  */
  public Database()
  {
    this.readers = 0;
  }

  /**
     Read from this database.

     @param number Number of the reader.
  */
  public void read(int number)
  {
    synchronized(this)
    {
      this.readers++;
    }

    assert((this.writers == 1 && this.readers == 0) || this.writers == 0);

    synchronized(this)
    {
      this.readers--;
      if (this.readers == 0)
      {
        this.notifyAll();
      }
    }
  }

  /**
     Writes to this database.

     @param number Number of the writer.
  */
  public synchronized void write(int number)
  {
    while (this.readers != 0)
    {
      try
      {
        this.wait();
      }
      catch (InterruptedException e) {}
    }
    this.writers++;

    assert((this.writers == 1 && this.readers == 0) || this.writers == 0);

    this.writers--;
    this.notifyAll();
  }
}
</code>