*******************
**** SMC / MDP ****
*******************

This text file contains instructions on how to build and run the Statistical Model Checking for Markov Decisions Processes software.

You may build with Eclipse or without Eclipse.

In the following, we will refer to / as the base directory into which the GitHub repository was downloaded. There should be a Makefile, an IMPORT file, an smc.sh file and the src directory.

********************
**** REQUISITES ****
********************

1) PRISM, version 4.0.2 was used (http:https://www.prismmodelchecker.org/)
2) Scala, version 2.9.1 was used (http:https://www.scala-lang.org/)
3) SSJ, version 2.4 was used (http:https://www.iro.umontreal.ca/~simardr/ssj/indexe.html)


*********************
**** PREPARATION ****
*********************

STEP 1:

First, you will need to modify two PRISM source code files. Navigate to the PRISM directory, denoted PRISM_PATH, and make the following modifications:

1) In PRISM_PATH/src/parser/State.java, change the code inside the "public int hashCode()" method to:
     return varValues.length > 0 ? Arrays.deepHashCode(varValues) : 0;

  This allows states to be efficiently stored and accessed within a hash table, which is of paramount importance.

2) In PRISM_PATH/src/simulator/SimulatorEngine.java, find "private RandomNumberGenerator rng;" and make it protected or public, e.g. "protected RandomNumberGenerator rng;"

  This makes it so that we can run modifications of the SimulatorEngine with the same RNG.


STEP 2:

You should modify the IMPORT file to indicate where all the dependencies are located. Do not use any variables such as $HOME - use only plain relative or absolute paths.


****************************
**** BUILD WITH ECLIPSE ****
****************************

This guide will focus on getting the software running within an Eclipse project for ease of modification. It can be easier to use the Makefile, but it will then be harder to modify the code.

The main folder / should serve as the base directory for the project, with /src/ being the source folder and /bin/ being the binary folder.


(1) Compile PRISM

  Please follow PRISM's instructions for compiling it for your machine. The result will be the PRISM native library. We will also need to perform some minimal changes to PRISM's source Java code which are crucial for efficiency. PRISM's location is irrelevant.

To include the PRISM Java sources inside the Eclipse project:
 - Go to the project's properties
 - Click on Java Build Path
 - Click on Add Folder
 - Find and select PRISM's Java source folder (typically PRISM_PATH/src/)

  You will then need to add PRISM's dependencies to the project, which can be found inside the PRISM_PATH  /lib/ folder (namely colt.jar, epsgraphics.jar, jcommon.jar, jfreechart.jar and pepa.jar to remove all compile errors). To do this click on "Add External JARs…" in the Java Build Path panel.

(2) Compile Scala formula parser

Please add the Scala libraries to your Eclipse project (i.e. SCALA_PATH/lib/scala-library.jar). Alternatively, install Scala for Eclipse and use the "Add Library" button in the Java Build Path panel.

  The compilation of the Scala formula parser is not automated through Eclipse. To compile it simply type "make parser" in /. This should compile only the scala component of SMC/MDP, and create /bin/ and /bin/smcmdp, populated with .class files. Eclipse should detect these files automatically and recognise them.

(3) Compile SMC/MDP

  At this point, PRISM should be successfully compiled within the /bin/ folder and the Scala parser should be within /bin/smcmdp/. The SMC/MDP code should still have a few errors. Please add the SSJ and dependencies to the project (ssj.jar, optimization.jar).

  If Eclipse still identifies errors, they are likely due to the visibility of some of PRISM's methods. Find their location and change them to public.

  Eclipse should now successfully compile the PRISM modified source code and SMC/MDP code! It is ready to use! :)

  To clean SMC/MDP binaries, simply run "make clean" from /. Don't forget you can also use the makefile to compile automatically.


*******************************
**** BUILD WITHOUT ECLIPSE ****
*******************************

This method is suggested if you are more comfortable with the command line, or if you have to get SMC/MDP working on a remote server.

The main folder / should serve as the base directory, with /src/ containing SMC/MDP sources.


(1) Compile PRISM

  Please follow PRISM's instructions for compiling it for your machine. This will typically involve going to PRISM_PATH and running "make". This should populate the PRISM_PATH/lib/ directory with compiled libraries and the PRISM_PATH/classes/ folder with compiled java class files.

To compile, simply go to / and run "make".


*******************
**** PROBLEMS? ****
*******************

Sometimes, the Scala compiler will not recognise a change of directory in the shell, and will thus complain that a certain file cannot be found. If this happens to you, simple run "ps -A" and find the java processes associated with the Scala compiler, then kill it off, e.g. "kill -9 <process number>".

After this process has been terminated, running "make" or "make parser" again from / should work.


*************
**** RUN ****
*************

  To run, simply make smc.sh executable and then use "./smc.sh" or use "sh smc.sh" directly.  If you run it without any parameters, some help text should appear... have fun tweaking the millions of options! :)

  
*** WARNING ***
 The default options are aimed at very high-end systems, so 10gb are initially allocated to Java, and some non-standard garbage collection algorithms are used. These can be easily set by modifying the JFLAGS variable in "smc.sh".