*******************************************************************************
          README: Interactive Markov Chain Analyzer 1.6 beta (IMCA)
*******************************************************************************

IMCA 1.6 beta is a command-line tool for analyzing unbounded reachability 
probabilities, expected-time, and long-run averages. We support analyzing of 
Interactive Markov Chains and Markov Automata. This version do not provide all 
functionalities from prior Versions including a GUI, as well as a Scheduler 
synthesis.

In this document you will find general information about the IMCA
distribution.

NOTE: Below we assume that IMCA is the folder you obtained after
unpacking the IMCA-distribution archive.

-------------------------------------------------------------------------------
                             Contents
-------------------------------------------------------------------------------
 1. General information
 2. Distribution structure
 3. Makefile information
 4. bcg2imca information
 5. Miscellaneous
 
-------------------------------------------------------------------------------
                      1. General information
-------------------------------------------------------------------------------

The tool is distributed under the GNU General Public License (GPL):

	IMCA/LICENSE
	
	
For the use of bcg2imca you need to acquire a CADP Licence 
(free for academical usage):

	http://cadp.inria.fr/registration/
	
Note, that the .imc input format have only legacy support, which 
can lead to problems. If it is possible, use the .ma input format.


IMCA can be compiled with 2 different linear programming solvers!

The default solver is "SoPlex" which licence can be found here:

http://soplex.zib.de/licence.shtml

Note: Soplex is free for academic use. How to compile with SoPlex is described
in Section 3.

The second solver is "LP_SOLVE" which is distributwet under LGPL:

http://lpsolve.sourceforge.net/5.5/LGPL.htm

Note: lpsolve is currently not integrated!


    
-------------------------------------------------------------------------------
                    2. Distribution structure
-------------------------------------------------------------------------------

FILE STRUCTURE:
    -IMCA/bin/imca               -- the IMCA binary
                                    (might not be present before compilation)
    -IMCA/lib/imca.a             -- the static library containing the IMCA core
                                    (might not be present before compilation)
    -IMCA/obj                    -- the object-file directory
    -IMCA/include                -- the header files
    -IMCA/src                    -- the source code
    -IMCA/tmp                    -- directory for temporary files
                                    (might not be present before compilation)
     
    -IMCA/examples               -- some example files
    -IMCA/examples/PollingSystem -- the Polling System with and without 
	                                confluence reduction
    -IMCA/examples/ProcessorGrid -- a processor grid example with and without 
	                                confluence reduction
                               
    -IMCA/LICENSE                -- the licensing information
    -IMCA/README                 -- the file you are reading now
    -IMCA/makefile               -- the main makefile
    -IMCA/compile.sh             -- the bcg2imca compile script
                                    (environment variable $CADP has to be set)
    
-------------------------------------------------------------------------------
                    3. Makefile information
-------------------------------------------------------------------------------

If you want to use Soplex you have to follow those two steps:

1. adjust the path location for the Soplex library.

   Line 57: SOPLEXSRC = your_path_to_the_soplex_library
   
2. compile IMCA as follows:

   make
   
3. if you don't have Soplex use
	
   make SOPLEX=false
   
   NOTE: not functional at the moment without Soplex!

-------------------------------------------------------------------------------
                    4. bcg2imca information
-------------------------------------------------------------------------------

To compile bcg2imca you can just run the compile script.
The program is elementary and will give no proper error messages!

The usage of the program is as follows:
    bcg2imca <input> <output> <goal action>
        <input>         - inputFile.bcg (have to exist)
        <output>        - outputFile.ma (will be created if not present)
        <goal action>   - transition leading to success
		
Note, that the condition for extracting goal states currently only support the 
identification over one action. Further, selfloops are ignored in the 
translation!

-------------------------------------------------------------------------------
                    5. Miscellaneous information
-------------------------------------------------------------------------------

If you run into a segmentation fault for computing the long-run average, your 
available stack memory is to small. In Unix systems you can set the stack 
memory as follows:

ulimit -s <kb>

where <kb> should be substituted with the new memory size in kb. By omitting
<kb>, the command will print the current stack size in kb.

If you have trouble with compiling Soplex, try to add the following to the 
Makefile:

USRCXXFLAGS = -arch x86_64 -arch i386

It can be possible that you have to add execution rights to the compile.sh by

chmod +x compile.sh

*******************************************************************************