Creating a New JPF Module

So what do you have to do to create a new JPF module? For a quick shortcut to setting up most things, use the create_project script of the jpf-template module.

However, jpf-template cannot do everything for you, so see below for more information on how to finish setting up your new project.

Several steps are involved:

1. get familiar with the JPF configuration

You need to understand how your project will be looked up and initialized during JPF startup, and the place to learn that is the JPF configuration page. Once you know what site properties and project properties are, you can proceed.

2. get familiar with the standard JPF project layout

Although this is mostly convention, and you can deviate if you really need to, please try hard not to.

You can get the details from the JPF Runtime Modules page, but the essence is that each project has two (possible) major build artifacts:

jpf-<module>.jar - executed by the host (platform) VM (contains main classes and peers)
jpf-<module>-classes.jar - executed by JPF (contains modeled classes)

Consequently, your sources are kept in src/main, src/peers, src/classes, src/annotations, src/tests and src/examples. You might only have some of these, but please provide regression tests so that people can check if your project works as expected.

All 3rd party code that is required at runtime goes into a lib directory.

We keep potential annotations separate (and provide additional jpf-<module>-annotations.jar) so that external projects (systems under test) can use them without relying on all JPF classes to be in their classpath. The idea is that this jar does not contain any code which could alter the system under test behavior if you execute it outside of JPF.

3. create a jpf.properties file

Within the root directory of each JPF module a project properties file is needed which is named jpf.properties. It contains the path settings the host VM and JPF need to know about at runtime. It looks like this:

# standard header
<module-name> = ${config_path}

# classpath elements for the host VM (java)
<module-name>.native_classpath = build/<module-name>.jar;lib/...

# classpath elements for JPF
<module-name>.classpath = build/<module-name>-classes.jar;...

# sources JPF should know about when creating traces etc.
<module-name>.sourcepath = src/classes;...

You can add other JPF properties, but be aware of that this is always processed during JPF startup if you add your module to the extensions list in your site.properties, and might conflict with other JPF modules. For this reason you should only add your module to extensions if you know it will always be used.

4. create your build.gradle

Our build process is Gradle based, hence we need a build.gradle file. The standard tasks are

clean
build (compiles and creates the jars)
test (run JUnit regression tests, depends on build)

If you stick to the general layout, you can use jpf-core’s build.gradle as a template. Gradle automatically handles dependencies and classpath configuration for JPF components you depend on (at least jpf-core).

5. add your module to your site.properties

This is optional, you only need to do this if you want to be able to run your JPF module outside its own directory. If so, add an entry to your site properties file that looks like this:

...
<module-name> = <path to your JPF extension module>
...

6. publish your repository

You can publish this wherever you want (github, bitbucket, or gitlab are suitable free hosting services), or ask us to host it on the JPF server. If you decide to use a 3rd party hosting service, please let us/the JPF community know about it (e.g. by posting on our Discord server).