IMCA is a command-line tool for analysing Markov automata
C++ C Makefile
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
examples
include
src
LICENSE
Makefile
README
compile.sh

README

*******************************************************************************
          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. IMCA currently requieres Soplex version <= 1.7.2

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

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