Use Java Path Finder from another java project

1.9k views Asked by At

I want to use JPF (Java Path Finder) from another java project.

Steps that i have done:

  1. I have created a new Java project

  2. Referenced the jpf-core in build path.

  3. Created a java class(Test.java) printing Hello world (in my new project).

  4. Created a .jpf file (Test.jpf) in that i have mentioned, target=Test.

  5. In the eclipse launch configuration i have mentioned

    project = jpf-core
    Main Class = gov.nasa.jpf.tool.RunJPF
    

My problem is If i place the same .java file and .jpf file in jpf-core/examples package in jpf-core project i am able to run the jpf file and get the results. But when i am trying to run the .jpf from another java project i am unable to do so. I am getting the following error

[SEVERE] can't find startup class: Test`
[SEVERE] error initializing startup classes (check 'classpath')

Please help me to resolve this.

Update:

Do i have to write any properties file mentioning the classpath of my Test class files? If i write so how do i link up them with jpf.properties?

2

There are 2 answers

1
Angel O'Sphere On

Your other project needs to reference the project that contains the Test class. Otherwise it is obviously not on the classpath. Check the Project tab under Build-Path.

0
bLaXjack On

I hope this is not too late. I am using Eclipse Plugin for JPF.
To run the JPF from another java project. I need to create a jpf.properties file to setup the config. With eclipse plugin and it can be auto-generated when creating a JPF project. Inside the jpf.properties file, the .classpath and .sourcepath config need to be set to your testing file (always from build\XXX as JPF is loading java bytecode). Then right click on the .jpf file and click "Verify" (eclipse plugin). Before hand, I need to tell the eclipse about the jpf-core directory. Just create a site.properties file and write "jpf-core = your JPFdirectory" will be done. Thank you.
As advised by the JPF authority, JPF is easier and faster with plug-in support.