Home

HOW TO GET STARTED WITH TIE

Download and Install Eclipse IDE version 3.5 (Galileo) or Later

1. http://www.eclipse.org/

Download and Install TortoiseHg and Mercurial ( I think the All-in-One Installer should do fine)

1. http://mercurial.selenic.com/wiki/Download

Install the MercurialEclipse plugin

1. Ensure that you are running Eclipse >= 3.5 (Galileo)
2. In Eclipse go to Help -> Install New Software
3. In the new window selected "Add"
4. The name is up to you but, set "Location" to http://cbes.javaforge.com/update
5. From the "Work with:" drop down menu select the update site that you just entered from the previous step
6. Check the "MercurialEclipse" check box, select "Next" and go through the install process.

Add JPF respository to the Eclipse IDE

1. Open up the Eclipse IDE and go to File->Import

2. Open the Mercurial Folder and chose "Clone Existing Mercurial Repository"

3. set URL, under Repository Location, to: "http://babelfish.arc.nasa.gov/hg/jpf/jpf-core"

4. Press Next and Eclipse Should start Cloning the repository

5. Select the default Working directory revision (Just press Next)

6. Once that is done, just click Finish

7. It should complete and start to Build

8. Most likely it should fail because you need to create a "site.properties" file under "<user.home>/.jpf/"

9. For more information on site.properties files go here: http://babelfish.arc.nasa.gov/trac/jpf/wiki/install/site-properties

10. My Eclipse project I created for JPF and TIE is under "C:/Tie" and therefore this is how my site.properties file looks

11. If there are still some Build failures, this link should help fix that: http://babelfish.arc.nasa.gov/trac/jpf/wiki/install/build

    #JPF site configuration
    
    jpf-core = C:/TIE/jpf-core
    
    # numeric extension
    # jpf-numeric = ${user.home}/projects/jpf/jpf-numeric
    
    # annotation-based program properties extension
    # jpf-aprop = ${user.home}/projects/jpf/jpf-aprop
    
    # extensions=${jpf-core},${jpf-aprop}
    
    #... and all your other installed project
    

Install the Eclipse JPF plugin (Using Eclipse >= 3.5 )

Using the Update Site (Simplest Method)

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

Running JPF using plugin

1. Right click on the a .jpf file. Examples can be found in the src\examples directory in jpf-core
2. If the eclipse plugin is correctly installed, a Verify option will appear.
3. Select the Verify option and the verification process of the system specified in the .jpf file begins

Adding Tie Source Code and Example Files to jpf-core

1. From Eclipse, open jpf-core and then src/main
2. You will see several packages with names all starting with "jpf.nasa.jpf"
3. Create a new package called "jpf.nasa.jpf.gVisualizer" under src/main
4. Extract all source files into this new package
5. Now navigate to back up to jpf-core and then to src/examples
6. The source code to the example files can be put into default package where the other source codes are
7. The ".jpf" file for the source codes can be placed into the src/examples folder
8. In order to run TIE on any concurrent program, open up its respective ".jpf" file and add the line "listener=gov.nasa.jpf.gVisualizer.JPFVisualization"
9. If a "listener=" line is already there, just add a comma and then add the gVisualizer line

Example: "listener=gov.nasa.jpf.listener.PreciseRaceDetector,gov.nasa.jpf.gVisualizer.JPFVisualization"

Running JPF using Eclipse plugin

1. As long as there is a ".jpf" file created for the program being tested, you can right click on the a .jpf file
2. If the eclipse plugin is correctly installed, a Verify option will appear.
3. Select the Verify option and the verification process of the system specified in the .jpf file begins
4. Examples can be found in the src\examples directory in jpf-core