This file describes how to use the prism_dectree.jar executable used to produce results presented in 
Counterexample Explanation by Learning Small Strategies in Markov Decision Processes

Please note that the computation of the decision trees is probabilistic in many steps.
Therefore, every run of the program returns different results.
Furthermore, the best parameters for decision tree learning can not be known beforehand.
The scripts performs a limited binary search from a best guess M parameter, 
that might not be accurate for the current run.

Reproducing the results of the paper:
	To reproduce the results presented in Table 1/2
	1) cd scripts
	2) ./table1.sh or ./table2.sh
	3) Read off tree size, value of the strategy, reference value from PRISM or BRTDP and 
	error from output of the script.
	4) View the decision tree, timing logs and PRISM output in output/txt
	5) View detailed statistics in output/csv

The computation of one number usually takes several minutes.
Note that the firewire model is rather big, 
so the calculations of table1 to be slow on this example and 
bdd construction might run out of memory.
The expected running time of the scripts are
	1 hour for table1.sh before firewire_prism numbers 
	2 hours for table2.sh
To obtain more precise results, increase the verify=x parameters in the scripts.
For example verify=10000 should produce good accurate evaluations and 
well steered binary searches for all examples.
To perform a full binary search, change search=number to search only.

More parameters to fine-tune the calculations can be found in parameters.txt
Note that LD_LIBRARY_PATH needs to point to this the lib directory (see first line in the scripts).

Name encoding
	I ... importance measure is taken into account when learning
	O ... importance measure is neglected
	
	R ... only successful simulations are learned
	A ... all simulations are learned
	
	E ... the importance measure is calculated w.r.t. the expected value of reaching the target
	P ... the importance measure is calculated w.r.t. the empiric probability of reaching the target

The artifact is organized as follows:

prism_dectree.jar 
	the jar executable of PRISM including the code for decision tree construction & evaluation.

lib/ 
	contains libraries that are required for execution.
	Libraries for Linux and Windows are included.

scripts/
	contains predefined use cases of the executable that are the experiments performed 
	to obtain the data presented in the paper.
	The scripts produce csv files containing measurements of the experiment.
	The output of prism, including the decision tree itself is stored in a text file.

output/ 
	contains the data produced by the scripts.
	
prism-examples/
	contains the examples from the PRISM benchmark library presented in the paper.
	Two additional examples (brp, dining_crypt) are included that show quantitative performance of our implementation.
	
src/
	contains the source code of prism including our implementation.
	Most of the contributions for this paper can be found in the heuristics.decisiontree package
	The other heuristics.* packages were created both for this paper and [1].
	prism.Prism.java and prism.PrismCL were altered to include our code into 
	the work flow of PRISM and implement parameters.
	Minor changes were done to other files.
	
CAV_2015_submission_111.pdf
	The version of the paper that was submitted to CAV 2015.

parameters.txt
	Describes the most important parameters for conducting various experiments with our implementation. 

README.txt
	This file

[1] Brzdil, Tom, et al. "Verification of Markov decision processes using learning algorithms." 
Automated Technology for Verification and Analysis. Springer International Publishing, 2014. 98-114.