Iterative

[pazz]

This branch contains an implementation of the "dumb" alternative, namely a semi-decision procedure that iteratively constructs and solves an n-fold product MDP as long as the value remains 1.

This is not to be merged into the main branch (for now) and this PR is only meant to discuss this branch.

find the new binary called "schaeppert":

schaeppert -h
Usage: schaeppert [OPTIONS] <AUTOMATON_FILE> <TMP_DIR>

Arguments:
  <AUTOMATON_FILE>  Path to the input
  <TMP_DIR>         directory where to store the prism files

Options:
  -f, --from <INPUT_FORMAT>    The input format [default: tikz] [possible values: dot, tikz]
  -v, --verbose...             Increase verbosity level
  -l, --log-output <LOG_FILE>  Optional path to the log file. Defaults to stdout if not specified.
  -h, --help                   Print help
  -V, --version                Print version

It takes the same input /input type as shepherd and a path to some (empty) directory. It will create prism files called model-1.pm there, call prism and parse the output.

(prism cannot read from stdin so these files have to be written to disk).

mkdir tmp

./target/debug/schaeppert -f dot examples/fig6-butterfly.dot tmp/
n=1 -> 1.000
n=2 -> 1.000
n=3 -> 1.000
n=4 -> 1.000
n=5 -> 1.000
n=6 -> 1.000
n=7 -> 1.000
n=8 -> 1.000
n=9 -> 1.000
^C

 ./target/debug/schaeppert -f tikz examples/bottleneck-2.tikz tmp/
n=1 -> 1.000
n=2 -> 1.000
n=3 -> 0.778
The value is less than 1.0, stopping the search.

[pazz]

So I've been testing the iterative thing vs shepherd on a silly family of linear bottlenecks and something happens at n=7 that is funky.

The bottlenecks can be found in examples/guess-empty-n, which includes two scripts: one to generate the parameter-n model and one to benchmark the two solvers against each other.

Here is the result, where the x-axes is the parameter and y-axes is time to solve.

log_shepherd_7.txt
log_prism_7.txt
log_shepherd_6.txt
log_prism_6.txt
log_shepherd_5.txt
log_prism_5.txt

This uses the binaries as built with the --release flag and makes shephert's output verbose (-vv) so that you can try and debug what happens at n=6.
The commands used are these:

CMD1=schaeppert -vv -f dot bottleneck-N.dot iterate tmp/
CMD2=shepherd -vv -f dot bottleneck-N.dot

Basically, shepherd dies from n=8 onwards but up until n=5 it grows slower than prism does.

According to its logs, prism actually spends most of its time reading the input and then generating the internal model.

Possible variations / experiments to run:

• force prism to not use BDDs
• count the time it takes to turn our input into the product in prism lang
• enable the optimization in shepherd that tries to compute the winning strategy