Set up EPMC in Eclipse

This tutorial has been tested on the following distributions:

• Ubuntu 16.04 LTS, 64-bits

Prerequisites

• Java Development Kit (currently only JDK 13.0+ works)
• Eclipse IDE
• Javacc plugin in Eclipse
• SPOT (check whether ltl2tgba and autfilt work correctly after installation)

Set up ePMC in Eclipse

Note that please do not put ePMC directly into the workspace directory of the Eclipse otherwise Eclipse may not be able to find the epmc project.

1. Import ePMC -> General -> Existing Projects to Workspace
2. Check Option Seach nested projects -> Uncheck epmc (path/to/ePMC/main)

Then select epmc project and choose to run it as Java application, then select "EPMC - epmc.main" as main class. The created configuration needs to be configured, as follows: choose "Run configurations..." from the menu, choose the newly created EPMC configuration, and fix the following settings:

3. Arguments tab -> working directory -> workspace -> choose "epmc/main/target/classes"
4. Dependencies tab -> Classpath entries -> add jars -> choose all jar files in "epmc/lib"
5. Dependencies tab -> Classpath entries -> advanced -> add folders -> choose "epmc/main/target/classes" and then apply the changes.

Now if you run the configuration EPMC, you should get no errors but just an empty output.

In the following tutorial, the epmc project is used as the main project.

Print help message in Eclipse

1. Run configurations -> duplicate "EPMC" to be Java application "EPMC-help" -> set main class as "epmc.main.EPMC"
2. Run configurations -> Java application EPMC-help -> add the following content in "Program arguments" and run:

help --plugin path/to/ePMC/plugins/util/target/classes,
path/to/ePMC/plugins/value-basic/target/classes,
path/to/ePMC/plugins/dd/target/classes,
path/to/ePMC/plugins/expression-basic/target/classes,
path/to/ePMC/plugins/graph/target/classes,
path/to/ePMC/plugins/algorithm/target/classes,
path/to/ePMC/plugins/graphsolver/target/classes,
path/to/ePMC/plugins/graphsolver-iterative/target/classes,
path/to/ePMC/plugins/jani-model/target/classes,
path/to/ePMC/plugins/jani-interaction/target/classes,
path/to/ePMC/plugins/automata/target/classes,
path/to/ePMC/plugins/prism-format/target/classes,
path/to/ePMC/plugins/command-help/target/classes,
path/to/ePMC/plugins/command-check/target/classes,
path/to/ePMC/plugins/command-explore/target/classes,
path/to/ePMC/plugins/constraintsolver/target/classes,
path/to/ePMC/plugins/constraintsolver-lp-solve/target/classes,
path/to/ePMC/plugins/propertysolver-propositional/target/classes,
path/to/ePMC/plugins/propertysolver-operator/target/classes,
path/to/ePMC/plugins/propertysolver-reward/target/classes,
path/to/ePMC/plugins/propertysolver-filter/target/classes,
path/to/ePMC/plugins/propertysolver-pctl/target/classes,
path/to/ePMC/plugins/propertysolver-multiobjective/target/classes,
path/to/ePMC/plugins/propertysolver-ltl-lazy/target/classes,
path/to/ePMC/plugins/dd-cudd/target/classes,
path/to/ePMC/plugins/dd-cudd-mtbdd/target/classes,
path/to/ePMC/plugins/automaton-determinisation/target/classes,
path/to/ePMC/plugins/graphsolver-lp/target/classes

You will see the following output after pressing the run button.

EPMC: Extensible Probabilistic Model Checker

Usage: <epmc> <command> [program-options]

Available commands:
  help .. Show program usage description

Available program options:
...

Run ePMC in Eclipse

Now if you want to check the Dice program with ePMC in Eclipse. Suppose the model and property files are dice.prism and dice.pctl respectively. Then we first need to duplicate Java application "EPMC-help" to be Java application "EPMC-check" in Eclipse.

In order to allow epmc project to find all required plugins, you have to provide the directories of plugins by adding following to running Arguments:

check
--model-input-files 
path/to/dice.prism
--property-input-files
path/to/dice.pctl 
--model-input-type 
prism
--property-input-type
prism
--plugin
path/to/ePMC/plugins/util/target/classes,
path/to/ePMC/plugins/value-basic/target/classes,
path/to/ePMC/plugins/dd/target/classes,
path/to/ePMC/plugins/expression-basic/target/classes,
path/to/ePMC/plugins/graph/target/classes,
path/to/ePMC/plugins/algorithm/target/classes,
path/to/ePMC/plugins/graphsolver/target/classes,
path/to/ePMC/plugins/graphsolver-iterative/target/classes,
path/to/ePMC/plugins/jani-model/target/classes,
path/to/ePMC/plugins/jani-interaction/target/classes,
path/to/ePMC/plugins/automata/target/classes,
path/to/ePMC/plugins/prism-format/target/classes,
path/to/ePMC/plugins/command-help/target/classes,
path/to/ePMC/plugins/command-check/target/classes,
path/to/ePMC/plugins/command-explore/target/classes,
path/to/ePMC/plugins/constraintsolver/target/classes,
path/to/ePMC/plugins/constraintsolver-lp-solve/target/classes,
path/to/ePMC/plugins/propertysolver-propositional/target/classes,
path/to/ePMC/plugins/propertysolver-operator/target/classes,
path/to/ePMC/plugins/propertysolver-reward/target/classes,
path/to/ePMC/plugins/propertysolver-filter/target/classes,
path/to/ePMC/plugins/propertysolver-pctl/target/classes,
path/to/ePMC/plugins/propertysolver-multiobjective/target/classes,
path/to/ePMC/plugins/propertysolver-ltl-lazy/target/classes,
path/to/ePMC/plugins/dd-cudd/target/classes,
path/to/ePMC/plugins/dd-cudd-mtbdd/target/classes,
path/to/ePMC/plugins/automaton-determinisation/target/classes,
path/to/ePMC/plugins/graphsolver-lp/target/classes

Note that you may get some error message during iteration phase, you have to build project "epmc-graphsolver-iterative" manually. You may also have to build epmc-dd-buddy, epmc-dd-cacbdd, epmc-dd-cudd, epmc-dd-cudd-mtbdd, epmc-dd-sylvan and epmc-dd-sylvan-mtbdd the first time you want to use symbolic data structures in model checking. The reason is that currently Eclipse is not able to automatically build C or C++ codes in those projects.