=== Artifact for CAV'17 Paper #156 === Last changed 23.04.2017. Download https://www7.in.tum.de/~meggendo/artifacts/2017/cav_156.txt for an up-to-date version. == SUMMARY FOR EVALUATION == = Download and startup = Please download the OVA image from https://www7.in.tum.de/~meggendo/artifacts/2017/cav_156.ova and verify the downloaded file by comparing its SHA1 checksum with 649d6b4a5db92cb77ebab9f6eaa5a33d3c41da39 also found at https://www7.in.tum.de/~meggendo/artifacts/2017/cav_156.ova.sha by invoking sha1sum and comparing the output. Then, simply import the OVA image in VirtualBox. Note that in order to reduce size of the image we did not include a GUI. The username and password is "cav", the user has sudo rights. = Usage and evaluation = For ease of use, we included a simple script "eval.sh" in the home directory. "eval.sh" replicates the results we found for table 1 and table 2. To use, simply call "./eval.sh 1" or "./eval.sh 2" to run the respective tests. Furthermore, we set the timeout to 1 minute instead 1 hour to quicken the evaluation process. The default can be overriden by specifying a second argument, e.g. "./eval.sh 1 1h". = Results = All methods listed are named as in the table. "nvi-check" refers to the "run NVI until convergence" method, i.e. the second number in the NVI column. We stress that due to ODV being based on stochastic methods, the number of explored states and thus execution time might vary significantly between executions. Further, we fixed a small bug in the implementation of ODV which improves its performance on most models. We will update the corresponding values in the tables of the final version. Please note that the perfomance of MultiGain may be slightly lower (roughly 20%) as in the artifact it uses the default lpSolve instead of gurobi. Gurobi cannot be included in the artifact due to licencing reasons. For more information how to install gurobi, see below. Furthermore, mec-lp unfortuantely crashes for the "cs_nfail" model due to an error in the JNI calls to glpk. We suspect that this is caused by an implementation error of the PRISM code responsible for constructing the LP. Lastly, we want to mention that our experiments were carried out on comparatively old hardware and operating system. On current state-of-the-art hardware, the execution times usually are faster by a factor of 2 to 3. = Image = The image was prepared on VirtualBox version 5.0.36-dfsg-0ubuntu1.16.04.2 The used operating system is the current stable Debian 8.7.1 x64. We tested the machine on multiple personal computers, including one with Intel(R) Core(TM) i7-4700MQ CPU @ 2.40GHz, 8 GB RAM. Note that the VM is quite restricted, only requiring 1 Core and 2 GB of memory in the initial configuration. == FURTHER DETAILS == = run.sh = The "eval.sh" script actually only delegates to the "run.sh" script found in the home directory. It is intended for in-depth evaluation and used as follows. ./run.sh ? where - is one of - mg: MultiGain - mg-gur: MultiGain with Gurobi (note that gurobi needs to be installed for this, see below) - nvi: Naive value iteration - nvi-check: Naive value iteration which runs until actual convergence - mec-vi: Value iteration together with MEC decomposition and the default reachability solver of PRISM - mec-lp: ... with LP reachability - mec-brtdp: ... with BRTDP reachability, "MD" heuristic - mec-brtdp-rr: ... with BRTDP reachability, "RR" heuristic - mec-brtdp-pr: ... with BRTDP reachability, "PR" heuristic - odv: The on-the-fly value iteration method with "MD" heuristic - odv-rr: with "RR" heuristic - odv-pr: with "PR" heuristic - is the path to the model - the path to the properties file. Note that since MultiGain uses a different syntax for their objectives, we included both ".mg.props" for MultiGain and ".props" for our methods. - specifies an upper bound on the maximal reward in the model. This is only needed for the ODV-variants and can be omitted otherwise. To obtain the total execution time, instead run /usr/bin/time -v ./run.sh In order to further experiment with the methods and parameters, feel free to inspect and modify the run.sh script. = Files = All relevant files are found in the home directory of the cav user. They are structured as follows. - prism-cav/ Contains our code and compiled binaries. If you want to modify the code you need to install several dependencies [1]. We excluded them to reduce size of the image. The relevant parts of the source code can be found in prism/src/heuristics/search/MpRtdpUnbounded.java and prism/src/explicit/MDPMeanPayoffModelChecker.java together with related classes. - multigain/ Contains the binary distribution of MultiGain which we used in our experiments - models/ Contains the used benchmarks and some more models for experimenting = Installing Gurobi = Due to licencing restrictions, we cannot provide a version of Gurobi with the artifact. In order to obtain an academic version for free, follow the instructions provided at [2]. After installation, please set the GUROBI_HOME in run.sh to the appropriate folder. Furthermore, to use it in the eval script, one has to replace occurences of "mg" by "mg-gur". = Links = [1] apt install build-essentials automake libtool-bin maven swig [2] http://www.gurobi.com/academia/for-universities