= README =
Last updated: 06.06.2017
== Download ==
The sources are available at
https://www7.in.tum.de/~meggendo/artifacts/2017/atva_si.txz
The archive has a SHA1 checksum of
bb9efd3fd382ce2ad6ecb168b61565140234e9cc
We recommend verifying the integrity of the archive.
== Installation ==
In order to compile, simply cd into the prism subdirectory and run make.
This should create a runnable script in prism/bin. For further details, see
http://www.prismmodelchecker.org/manual/InstallingPRISM/Instructions
== Usage ==
We added several command line switches to prism as outlined below. Example
usages can be found further down.
* -mecdec: This enables the general purpose MEC-decomposition approach
* -mecreach : Solution method to use for the reachability query on
the weighted MEC quotient. Possible values:
* interval: Interval iteration (eps-precise)
* valiter: Value iteration (potentially imprecise)
* politer: Strategy iteration (precise)
* -mecmpsoln : Method used to determine the gain of each mec.
Possible values:
* politer: Strategy iteration
* valiter: Value iteration
* -mcgbsysmethod : Gain/bias equation type / method for Markov
Chains. Possible values:
* full: Solve the standard linear equation system
* compress: Solve the BSCC compressed equation system
* scc: Use the SCC decomposition approach
* -mdppimethod : Strategy iteration update type. Possible values:
* full: Standard update
* interleaved: Do bias update for all states which are gain-optimal
* heuristics: Use gain heuristics before updating
* attractor: Update all states to the best BSCC (only works on
communicating models or together with MEC decomposition)
* hybrid: Use hybrid between value iteration and policy iteration (only
works on communicating models or together with MEC decomposition)
Furthermore "-epsilon " is used as stopping criterion for all eps-
precise methods, "-politer" specifies usage of startegy iteration.
== Examples ==
In the following, we present some examples of the command line arguments.
To run the method on a particular model, add " ". We
included some sample models in the examples folder.
# Value iteration + interval reachability with total error of 10^-12.
-mecdec -mecreach interval -mecmpsoln valiter -epsilon 1e-12
# Standard strategy iteration
-politer -mcgbsysmethod full -mdppimethod full -epsilon 1e-12
# Standard strategy iteration with interleaved update
-politer -mcgbsysmethod full -mdppimethod interleaved -epsilon 1e-12
# Strategy iteration with BSCC compression
-politer -mcgbsysmethod compress -mdppimethod full -epsilon 1e-12
# Strategy iteration with SCC decomposition
-politer -mcgbsysmethod scc -mdppimethod full -epsilon 1e-12
# Strategy iteration with SCC decomposition and gain approximation
-politer -mcgbsysmethod scc -mdppimethod heuristics -epsilon 1e-12
# MEC decomposition + strategy iteration + interval reachability
-mecdec -mecreach interval -mecmpsoln politer -mcgbsysmethod full -mdppimethod full -epsilon 1e-12
# MEC decomposition + strategy iteration + strategy iteration reachability + interval reachability
-mecdec -mecreach politer -mecmpsoln politer -mcgbsysmethod full -mdppimethod full -epsilon 1e-12
# MEC decomposition + strategy iteration with interleaved update + interval reachability
-mecdec -mecreach interval -mecmpsoln politer -mcgbsysmethod full -mdppimethod interleaved -epsilon 1e-12
# MEC decomposition + strategy iteration with attractor update + interval reachability
-mecdec -mecreach interval -mecmpsoln politer -mcgbsysmethod full -mdppimethod attractor -epsilon 1e-12
# MEC decomposition + strategy iteration with gain approximation improvement + interval reachability
-mecdec -mecreach interval -mecmpsoln politer -mcgbsysmethod full -mdppimethod heuristics -epsilon 1e-12
# MEC decomposition + strategy iteration with BSCC compression + interval reachability
-mecdec -mecreach interval -mecmpsoln politer -mcgbsysmethod compress -mdppimethod full -epsilon 1e-12
# MEC decomposition + strategy iteration with SCC decomposition + strategy iteration reachability
-mecdec -mecreach interval -mecmpsoln politer -mcgbsysmethod scc -mdppimethod full -epsilon 1e-12