How to use VJP

For instructions on installing VJP see: Download, Lists, Bugs etc.

Verifing a program usually requires three steps:

  1. Create a Mode-Property File
  2. Configure the Mode Property File
  3. Launch the Mode Property File

What is a Mode Property File?

A Mode Property File contains a list of properties of values that JPF uses to perform the state model check. Properties like the target class , arguments and classpath are all defined in a Mode Property File. A Mode Property File is just a regular java property file that has the *.jpf extension. It can be edited by your favorite text editor or VJP can do the dirty work. VJP's only requirement is that the file be contained in an open Eclipse Project.

Creating a Mode Property File

There are many different ways to do this. If you want to create a file from scratch you can simply create a blank text file, set the target property to your main class (ex: 'target=Main') and then save it with the *.jpf extenstion within a Java project folder for eclipse. No matter where the file is placed in the project folder VJP will then automatically dectect it.
It should be noted that the 'target' property MUST be defined in your *.jpf file.

Another option is to click on VJP button next to the debug and run buttons on the top toolbar for eclipse. From the dialog press the 'New' button and then save the *.jpf file somewhere within the project folder of choice.

Yet another, and possibly the simplest option, is to right click on the class file from the package view and select 'Verify...'. VJP will then create a Mode Property File in that folder with that class as the target. The file can then be moved anywhere within the project if wanted. (Note: this will also cause the verification to be run)

Editing a Mode Property File

The 'VJP' approved way of editing a Mode Property File is to click on the VJP button at the top and then select the property file that you want to edit. An editor will appear that will allow you to add, remove and edit properties.

There are two tabs: Custom Properties and Default Properties.
Default Properties are the properties inherited from and These files are stored within VJP and shouldn't be edited. Instead if any of these settings need to be changed, uncheck 'Use Default' and edit at as needed.
The Custom Properties are any properties that need to be defined, but are not already defined in either or The most common examples of custom properties are 'target' and 'target_args'.

As always if needed, the property files can also be opened with a text editor and edited as needed. Comments can also be stored (and are encouraged!), VJP does not flatten or re-organize configuration files.

Running a State Mode Check.

Verification can be run from clicking on the VJP button, highlighting the Mode Property Configuration of choice then selecting either 'Step Verify' or 'Run Verify'. A simpler method is instead to right click on a .jpf file from either the 'Package Explorer' or 'Navigator' view and selecting 'Verify...'. This will automatically launch a verification.

By default VJP will only give the results of the run in a view. If you wish to step through the traces then add 'vjp.tracelistener=true' to your mode-property file.

The difference between 'Step Verify' and 'Run Verify'

The difference between Step and Run Verify is simple. With a 'Step Verify', JPF pauses after every state advancement or backtrack