= 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 <method>: 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>: Method used to determine the gain of each mec.
   Possible values:
   * politer: Strategy iteration
   * valiter: Value iteration
 * -mcgbsysmethod <method>: 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 <method>: 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 <value>" 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 " <model> <properties>". 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