--- /dev/null
+# Building, Testing, and Running #
+
+If you downloaded binary snapshots, you don't have anything to build (except of creating/updating you [site.properties](./site-properties) file).
+
+## Building JPF ##
+
+If you have cloned the project repositories you are interested in (which at least includes [jpf-core](../jpf-core/index)), you can build and test each of them by means of their included [Ant](http://ant.apache.org) `build.xml` scripts. Note that you have to install Ant and JUnit separately, e.g. following directions [here](../install/requirements).
+
+
+### Using the command line ###
+
+~~~~~~~~ {.bash}
+> cd jpf-core
+> ant test
+
+... lots of output, at the end you should see something like:
+BUILD SUCCESSFUL
+Total time: 2 minutes 31 seconds
+~~~~~~~~
+
+### Within NetBeans ###
+
+ 1. run **File/Open Project..** from the application menu, entering the JPF project you just downloaded (e.g. "jpf-core")
+ 1. select the project that appears in our project pane (e.g. "jpf-core")
+ 1. run **Build** from the project context menu
+
+### Within Eclipse ###
+
+* Ensure that the `JAVA_HOME` environment variable points to the jdk1.6xxx directory. If it is empty or points to a JRE then errors such as **javac not found** maybe seen. If you do not want the system Java settings to point to jdk1.6xxx, you can also set project specific settings in eclipse.
+
+* If you eclipse settings are set to **Build Automatically** then the project after being cloned will be built.
+
+* To build a particular project in the Project menu select **Build Project**. All the dependencies for the project will be built automatically.
+
+#### Project Specific JDK settings within Eclipse ####
+1. In Eclipse go to **Project** -> **Properties**
+
+2. Select **Builders**
+
+3. Pick **Ant_Builder** -> click **Edit**
+
+4. Click on the **JRE** tab
+
+5. Select **Separate JRE** -> **Installed JREs**
+
+6. On Windows and Unix-based systems pick JDK1.6xxx. If it is not listed under the installed JREs, click on **Add**, browse your file system to where JDK1.6xxx resides and select. On OSx systems pick the JVM 1.6.0.
+
+
+## Running JPF ##
+
+### Using the command line ###
+
+
+~~~~~~~~ {.bash}
+> cd jpf-core
+> java -jar build/RunJPF.jar src/examples/Racer.jpf
+JavaPathfinder v5.0 - (C) 1999-2007 RIACS/NASA Ames Research Center
+.....
+====================================================== statistics
+elapsed time: 0:00:00
+states: new=9, visited=1, backtracked=4, end=2
+search: maxDepth=5, constraints=0
+choice generators: thread=8, data=0
+heap: gc=8, new=291, free=32
+instructions: 3112
+max memory: 79MB
+loaded code: classes=73, methods=1010
+
+====================================================== search finished: 1/12/10 2:30 PM
+~~~~~~~~
+
+### Using eclipse plugin ###
+
+ 1. Right click on a .jpf file. Examples can be found in the src\examples directory in jpf-core
+ 1. If the eclipse plugin is correctly installed, a Verify option will appear.
+ 1. Select the Verify option and the verification process of the system specified in the .jpf file begins
+
+Note that the Application.jpf file essentially replaces previous uses of eclipse launch configurations. The required element of a .jpf file is the `target=MAIN_CLASS` where `MAIN_CLASS` is the class containing main method of the system under test. Any other configurations that need to be specified can be added here. for example `listener=gov.nasa.jpf.tools.SearchMonitor`.
+
+Specify `classpath=PATH_TO_BIN_DIRECTORY` to add the class files for the program under test to JPF's class path. Windows users will need to use the double-backslash notation in specifying paths in the .jpf file. An example .jpf file for the Windows platform is included below for convenience:
+
+~~~~~~~~ {.bash}
+target=mutex.DekkerTestMain
+report.console.property_violation=error,trace,snapshot
+listener=gov.nasa.jpf.listener.EndlessLoopDetector
+classpath=C:\\Users\\fred\\Documents\\ch02-mutex\\bin
+sourcepath=C:\\Users\\fred\\Documents\\ch02-mutex\\src,C:\\Users\\Fred\\Documents\\ch02-mutex\\src-test
+~~~~~~~~
+
+The .jpf file not only indicates the `target` and `classpath`, but it also turns on error reporting with trace generation (`report.console.property_violation`) and configures the source path (`sourcepath`). Note that multiple source directories are specified using the comma separator.
+
+### Using eclipse Run Configuration ###
+
+ 1. Select a .jpf file by clicking on it in the Package Explorer
+ 1. Click **Run** -> **Run Configurations** -> **run-JPF-core**. It is important the correct .jpf file is selected when the configuration is run.
+
+#### Windows users ####
+After a fresh install of jpf-core you may see the following when trying to use the Eclipse Run-jpf-core configuration:
+
+~~~~~~~~
+java.lang.NoClassDefFoundError: gov/nasa/jpf/Main
+Caused by: java.lang.ClassNotFoundException: gov.nasa.jpf.Main
+ at java.net.URLClassLoader$1.run(Unknown Source)
+ at java.security.AccessController.doPrivileged(Native Method)
+ at java.net.URLClassLoader.findClass(Unknown Source)
+ at java.lang.ClassLoader.loadClass(Unknown Source)
+ at sun.misc.Launcher$AppClassLoader.loadClass(Unknown Source)
+ at java.lang.ClassLoader.loadClass(Unknown Source)
+Exception in thread "main"
+~~~~~~~~
+
+In this particular case, the error was generated after the initial build after the clone had completed. To resolve the issue, **refresh the Eclipse workspace** (F5 or right click Refresh). After the refresh, the Run-jpf-core configuration should work as described above.
projects / jpf-core.git / blobdiff