+++README+++

---Before the Experiments---
Make sure that your docker deamon creates container with enough RAM Access in order
to finish the computations. A minimum of 8Gb are recommended.

---Starting the VM---
First, load the image into docker:

  docker load -i <file>

Once the image is loaded, you can start the VM using

  docker run -it artifact

Some additional flags before the "artifact" keyword give further uses. The ones
to mention are:
  "-v $(pwd):/home/artifact/share"  saves the generated logs and graphss into the current directory of the host
  "-d" starts the container detached in the background
  "-v /tmp/.X11-unix:/tmp/.X11-unix -e DISPLAY=unix$DISPLAY" in order to pass the x11 content outside the container.
                                                              Allows the usage of xprism (the graphical overlay of prism)
For more information, Read the docker reference under
https://docs.docker.com/engine/reference/commandline/run/

---Using the artifact---

Once in the command line interface of the VM, you can use the run.py Python
script to start the experiments. In order to run the same Experiments as presented
in the paper, use

  python3 run.py All

Replacing the "All" keyword allows you to start only parts of the experiment set:
  - Strategies          Figure 2
  - Noise               Figure 3
  - Analysis-Horizon    Figure 4
  - Monitoring          Figure 5
  - Combined            Figure 6

Flags can be used to further adapt the experiment set and performance
  -j num, --jobs num      Allows the experiments to make num simulations in parallel. Increases
                          the proceedings significantly, but needs more processing power and RAM.
                          Default: 2
  -s num, --samples num   Number of samples gathered in simulation. Higher numbers mean a larger
                          sample size for probability and expectation results, but need more time
                          Default: 3000
  -m Xg, --memory Xg      Limits the amount of RAM, one simulation process may use. Actual used memory
                          can double, since both java(heap) and cudd memory usage get the same value.
                          Default: 2g
  -e str, --engine str    What model checking engine to use for preprocessing. See more in the Prism
                          documentation at https://www.prismmodelchecker.org/
                          Default: sparse
  --scope                 Options for the experiment set used. Possible options are:
                            - asInPaper: uses the same configurations and environments
                                         as shown in Paper. This is the default.
                            - extended: Uses all 110 environments and includes the budget
                                        based strategies in all experiments. Massively
                                        increases the time and memory needed to finish the
                                        experiments.
                            - reduced: Only uses the synthetic environments for experiments,
                                       and deactivates all budget based strategies. Reduces
                                       time needed to finish experiments significantly.
  -c, --create_graphs     Options for the generation of graphs out of experiment results:
                            - current: generates graphs for current experiment after computation.
                                       This is the default.
                            - all: generates graphs for all experiments with logs available
                                   after computation.
                            - only: as in "all", but does not start experiments,
                                    only creates graphs from already existing logs
                            - none: does not create graphs
  --help                  Prints this help text.

---Necessary Resources---

This image has been tested to work with a minimum of 2 CPUs and 8g RAM under default conditions.
Lower amounts of RAM may lead to processes being killed.

Please have it noted that the Experiments are incredibly computational expensive, and that even with
bigger CPU and RAM allotment, running all experiments as in the paper will take weeks.

Using this image on other chipsets than specified may lead to significant performance
loss due to emulation.

---Example---

To better understand the process of these experiments, the directory Demo contains one fully
working instance in our experiments (consisting of one environment with varying noise, full lookahead
and a decision every turn), that has been commented. To better understand its functionality, please
read Demo/README.txt