Verifing a program usually requires three steps:
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.
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)
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 default.properties
and jpf.properties. 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 default.properties or jpf.properties.
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.
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 and Run Verify is simple. With a 'Step Verify', JPF pauses after every state advancement or backtrack