This README demonstrates how to build and run the model checker under Linux OS. It is tested only on 16.04 LTS, 64bits.
This project focuses on the model checking problem of PAMC. This tool EPMC-PAMC is implemented as a plugin in ePMC. We only integrate the checking function for pamc here, and omit the other unrelevant functional plugins. For more usage of ePMC, please visit EPMC - (An Extendible Probabilistic Model Checker, previously known as IscasMC).
1. Obtain source code of EPMC-PAMC
source code
2. Set dependencies: JDK 8.0+, Maven.
For Maven, you can simply use apt to install maven: sudo apt-get install maven
3. Build EPMC-PAMC distributions
Enter to the root <epmc-pamc>, run ./build.sh
Congratulations! You have packaged the tool in an ALL-IN-ONE jar file epmc-pamc.jar.
Now run java -jar epmc-pamc help, you’ll find out a command-help-list. Note that the model-checker EPMC-PAMC currently only support explicit model checking.
To perform PAMC model checking, please set the following options into your commands:
--prism-flatten false
--model-input-type scgs
--property-input-type pamc
This tool also supports epistemic operators (extended from Chen Fu's work). So you need to prepare 3 files totally: one for the model, one for equivalence relations and one for pamc properties. Here is an example on how to run in command line:
java -jar epmc-pamc.jar check --prism-flatten false --model-input-files path/to/your_model.prism path/to/your_equivalence_relations.equiv --property-input-files path/to/your_property.pamc --model-input-type scgs --property-input-type pamc
The model should be in the PRISM language with mdp as its system type. The composition of the modules is defined in Chen Fu’s work). Note that you need to define every possible transitions explicitly for each local action in each local agent.
This part is totally same to ePMC’s set up steps in Eclipse.
Now suppose you want to run the pbn example in our respository, you need to provide the directories of plugins by adding the followings into running arguments:
check
--prism-flatten
false
--model-input-files
path/to/epmc-pamc/experiments/pbn/pbn1.prism
path/to/epmc-pamc/experiments/pbn/pbn1.equiv
--property-input-files
path/to/epmc-pamc/experiments/pbn/pbn1.pamc
--model-input-type
scgs
--property-input-type
pamc
--plugin
path/to/epmc-pamc/plugins/util/target/classes,
path/to/epmc-pamc/plugins/value-basic/target/classes,
path/to/epmc-pamc/plugins/dd/target/classes,
path/to/epmc-pamc/plugins/expression-basic/target/classes,
path/to/epmc-pamc/plugins/graph/target/classes,
path/to/epmc-pamc/plugins/algorithm/target/classes,
path/to/epmc-pamc/plugins/graphsolver/target/classes,
path/to/epmc-pamc/plugins/graphsolver-iterative/target/classes,
path/to/epmc-pamc/plugins/jani-model/target/classes,
path/to/epmc-pamc/plugins/jani-interaction/target/classes,
path/to/epmc-pamc/plugins/automata/target/classes,
path/to/epmc-pamc/plugins/prism-format/target/classes,
path/to/epmc-pamc/plugins/command-check/target/classes,
path/to/epmc-pamc/plugins/command-help/target/classes,
path/to/epmc-pamc/plugins/propertysolver-propositional/target/classes,
path/to/epmc-pamc/plugins/propertysolver-operator/target/classes,
path/to/epmc-pamc/plugins/propertysolver-pctl/target/classes,
path/to/epmc-pamc/plugins/propertysolver-pamc/target/classes
From ePMC:
Note that you may get some error message during iteration phase, you have to build project “epmc-graphsolver-iterative” manually. The reason is that currently Eclipse is not able to automatically build C or C++ codes in those projects.
ShanghaiTech University
Open Source License
Copyright © 2019-2020 ShanghaiTech University
All rights reserved.
Developed by S3L lab at ShanghaiTech University (http://s3l.shanghaitech.edu.cn, Email: songfu@shanghaitech.edu.cn).
EPMC-PAMC is free for academic usage only. Any other use requires a license. As academic usage, we consider only work performed by researchers or students at institutions delivering academic degrees. In addition, the work or the worker may not be contracted by any non-academic institution.