Home

Welcome to the java-with-jpf-example wiki!

Before you attempt to compile this project you should run configuration script which can be found in another repository: JPF configuration script

When your configuration of JPF is done you can try to compile this project. The easiest way to do so is to import project to InteliJ IDEA as a gradle project. Then one can open View->Tool Windows->Gradle and in the menu on the right choose Tasks->verification->test to run tests. Another way to run the project without IDE is to run gradle wrapper (it downloads gradle itself so there is no need to install it before) by: ./gradlew test it again run the very same gradle task test.

Currently there are:

• one dummy test of AppTest which does nothing interesting (to be removed)
• one dining philosophers test which runs two variations of Dining Philosopher Problem to find a deadlock and an example of reaching that deadlock (the test passes because it found a deadlock changing verifyDeadlock() to verifyNoPropertyViolation() in the if statement will make it other way round)
• one racer test which runs two threads that try to concurrently modify int value (the test fails with counterexample of concurrent READ and WRITE in different threads)