-
Notifications
You must be signed in to change notification settings - Fork 5
/
README
147 lines (100 loc) · 5.6 KB
/
README
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
*******************************************************************************
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
*******************************************************************************