Hi all,
I'm trying out MRMC and encountered a segfault on one of my first tries. I'm
attaching the model so you can take a look. It is a smallish (~600 states)
model, so I thought I would have no problems. By the way, what is the max
state count MRMC can handle?
Some considerations
I generated the model automatically, so I cannot give you many insights on
what it does.
It has CTMDPI format, but it really is not, as it has rate 1 on every
transition (or else, it is a quite simple CTMDPI). The model loads with no
problems
One of the states (which is reachable via many other ones) is labeled
"goal", when trying to verify the CSL formula
P{<1}[tt U[0,10] goal]
it segfaults
in fact, the upper time bound is inconsequential, I've tried setting to
other values to no avail.
I tried it first on an Ubuntu 9.04 64-bit machine with 2GB RAM. I thought it
may have been a 64-bit issue, so I tried it too on a FreeBSD 6.4 32-bit 2GB
machine but it failed too. Will try on a Mac later. I've compiled from
source on both tries.
Am I doing something wrong here?
Thanks
Esteban
PS on an unrelated note, what I really want to do is to do verification for
MDPs. I saw MRMC does not provide MDP verification, and I thought it had
steady-state CTMDPI verification, but it didn't. Can I get away with
approximating via big timebounds on CTMDPIs or something like that?
Hi,
I have use MRMC statistical version and I have obtained a memory problem for some state spaces.
Then I have questions please:
As I understood from your new paper about MRMC in Qest 2009, there is a memory limitation
in numerical MRMC and you say that statistical MRMC is not based on the fly simulation.
1) What do you mean by on the fly simulation?
2) There is a memory limitation (out of memory message) when using statistical version of MRMC?
Thanks.
Diana
Hello,
I'm using MRMC to do model checking of CTMDP. when I check a property like
P{<=0.9}[tt U[0,5] label]
it gives me back the maximum probability, but I need the minimum
probability. How can I get it? Thanks in advance.
Amir
Hello,
I used MRMC on a DTMC model to check a bounded until formula. Depending on the
chosen time bounds and error_bound setting, it segfaulted on several occasions.
MRMC Version 1.4.1 built from source
OS: Debian/testing on amd64
GCC: gcc version 4.4.3 20100108 (prerelease) (Debian 4.4.2-9)
Nevertheless it works well on 32 Bit OpenBSD -current with gcc 3.3.5
Is this behavior to be expected on 64 bit systems? Or is it maybe a gcc issue?
Sorry if I missed something, but I did not find information about this on the
webpage.
best regards
Matthias
--
__________________________________________________________
___ __ __
Dipl. Inf. Matthias Guedemann / __\/ _\ /__\
Computer Systems in Engineering / / \ \ /_\
Otto-von-Guericke Universitaet Magdeburg / /___ _\ \//__
Tel.: 0391 / 67-19359 \____/ \__/\__/
__________________________________________________________
Dear Moritz,
Here is the updated version of the on-wait statistics gathering script, the
previous one was buggy. It seems to me that I did not send you this update
yet.
The script I sent you last Friday was not quite correct. This one seems to
work.
Best regards,
Ivan.
Sorry to bother you, but it seems to me that the download link is not being
sent when requested. Some days ago I tried to get a download link for the
source code of MRMC, but no link was sent. Today I tried again, this time
accepting to subscribe also to the mailing list. The mailing list
subscription was confirmed and done, but I have not received any download
link for the tool yet. If you have problems sending the source code, I will
be happy to use a compiled version for Ubuntu 9.10 32bit.
If it would be possible to send the link as soon as possible, I would be
very grateful, as I need the tool for a project whose deadline is
approaching very fast.
Thank you
--
Stefano Schivo
Dear all,
I have downloaded the Mac OsX Version of mrmc and tried to run bin/mrmc, I get the following message:
dyld: Library not loaded: /opt/local/lib/libgsl.0.dylib
Referenced from: /Users/leitnerf/Documents/Uni/Research/Tools/mrmc_mac_v1.4.1/bin/mrmc
Reason: image not found
Trace/BPT trap
If I try to do "make all" I get the following error:
Best regards,
Florian
--
Florian Leitner-Fischer
Chair for Software Engineering
Department of Computer and Information Science
University of Konstanz, Box 67
D-78457 Konstanz, Germany
Office: Building E, Room 223
Phone: +49 (0)7531 88 4762
Fax: +49 (0)7531 88 3577
WWW: http://www.inf.uni-konstanz.de/soft
Dear MRMC developers,
I think I have found another (more severe) problem in the MRMC
FoxGlynn implementation.
The algorithm generates wrong Left Poisson tail values for lambdas in
interval [25; 40].
I send you a table of the expected values (L', R'), and the values
generated by MRMC (L, R) with epsilon = 1.0e-7.
L' R' L R
1 0 173 0 173
2 0 174 0 174
3 0 175 0 175
4 0 176 0 176
5 0 177 0 177
6 0 178 0 178
7 0 179 0 179
8 0 180 0 180
9 0 181 0 181
10 0 182 0 182
11 0 183 0 183
12 0 184 0 184
13 0 185 0 185
14 0 186 0 186
15 0 187 0 187
16 0 188 0 188
17 0 189 0 189
18 0 190 0 190
19 0 191 0 191
20 0 192 0 192
21 0 193 0 193
22 0 194 0 194
23 0 195 0 195
24 0 196 0 196
25 0 197 23 197
26 0 198 24 198
27 0 199 25 199
28 0 200 26 200
29 0 201 27 201
30 0 202 28 202
31 0 203 29 203
32 0 204 30 204
33 0 205 31 205
34 0 206 32 206
35 0 207 33 207
36 0 208 34 208
37 0 209 35 209
38 0 210 36 210
39 0 211 37 211
40 0 212 38 212
41 0 213 0 213
42 0 214 0 214
43 1 215 1 215
44 1 216 1 216
45 2 217 2 217
46 3 218 3 218
47 3 219 3 219
48 4 220 4 220
49 4 221 4 221
50 5 222 5 222
I send you also a PDF with an Excel plot of these values. As you can
see, the left tail is computed wrongly with lambda=[25 to 40].
I suspect that the problem lies in the following lines (132-157 of foxglynn.c):
if( lambda >= lambda_25 )
{
/*The starting point for looking for the left truncation point*/
const double start_k = 1.0 / ( sqrt( 2.0 * lambda ) );
/*Here we choose the max possible value of k such that
(m - k * sqrt_lambda - 3/2) >= 0*/
const double stop_k = ( m - 3.0/2.0 ) / sqrt_lambda;
/*Start looking for the left truncation point*/
double k, k_ltp = 0;
/*For lambda >= 25 we can use the upper bound for b_lambda,
here lambda is always at least 400:
b_lambda_sup = 1.05;
b_lambda = ( 1.0 + 1.0 / lambda ) * exp( 1.0 / ( 8.0*lambda ) ) <=
a_lambda_sup*/
const double b_lambda_sup = 1.05;
double k_prime, c_m_inf, result;
for( k = start_k; k <= stop_k; k = k + 1 )
if( b_lambda_sup * exp(- 1.0 / 2.0 * k*k) / ( k * sqrt_2_pi ) <
epsilon / 2.0 )
{
k_ltp = k;
break;
}
/*Finally the left truncation point is found*/
pFG->left = (int) floor( m - k_ltp * sqrt_lambda - 3.0 / 2.0 );
I dont know why stop_k is defined as:
const double stop_k = ( m - 3.0/2.0 ) / sqrt_lambda;
because I couldn't find it in the paper, however I believe that this
upper limit estimate is too small. Maybe a value of lambda would be
more appropriate, but I'm not sure. I think that this code should be
modified in this way:
if( lambda >= lambda_25 )
{
/*The starting point for looking for the left truncation point*/
const double start_k = 1.0 / ( sqrt( 2.0 * lambda ) );
/*Here we choose the max possible value of k such that
(m - k * sqrt_lambda - 3/2) >= 0*/
const double stop_k = lambda; //( m - 3.0/2.0 ) / sqrt_lambda;
<<<<<<<<<<<MODIFIED
/*Start looking for the left truncation point*/
double k, k_ltp = 0;
/*For lambda >= 25 we can use the upper bound for b_lambda,
here lambda is always at least 400:
b_lambda_sup = 1.05;
b_lambda = ( 1.0 + 1.0 / lambda ) * exp( 1.0 / ( 8.0*lambda ) ) <=
a_lambda_sup*/
const double b_lambda_sup = 1.05;
double k_prime, c_m_inf, result;
for( k = start_k; k <= stop_k; k = k + 1 )
if( b_lambda_sup * exp(- 1.0 / 2.0 * k*k) / ( k * sqrt_2_pi ) <
epsilon / 2.0 )
{
k_ltp = k;
break;
}
/*Finally the left truncation point is found*/
pFG->left = (int) floor( m - k_ltp * sqrt_lambda - 3.0 / 2.0 );
pFG->left = max(0, pFG->left); <<<<<<<<<<MODIFIED
With these changes the code seems to behave correctly, but I'm not
completely sure of the upper limit stop_k. Note also the last line,
that checks that pFG->left is never < 0.
P.S.: I don't know how to reply in the mailing list, so send me
e-mails to my email address elvio.amparore AT gmail.com if you have
any questions.
Dear MRMC developers,
I believe I've found a bug in mrmc. When using transient analysis, MRMC
outputs:
>>>>ERROR: Fox-Glynn: lambda >= 25, underflow. The results are
UNRELIABLE.
which, I think, is the result of a wrong formula in foxglynn.c, line 199:
k_prime = k_rtp * sqrt_2 + 3.0 / 2.0 * sqrt_lambda;
This line should be:
k_prime = k_rtp * sqrt_2 + 3.0 / (2.0 * sqrt_lambda);
as written in Corollary 3 of the "Computing Poisson Probabilities" paper.
Without this line, mrmc always thinks that the right Poisson tail will
underflow, writing the warning message.
Amparore Elvio
----- Message transféré ----
De : Diana El Rabih <dianarabih(a)yahoo.fr>
À : mrmc-users(a)lists.rwth-aachen.de
Envoyé le : Mar 10 Novembre 2009, 9 h 53 min 46 s
Objet : user of mrmc, having runing problem
Hi,
I had installed mrmc by doing unzip of mrmc_lin_v1.3.zip and by doing make all in the directory mrmc_lin_v1.3.zip
when doing make all I had obtained this message when making:
mrmc_tokenizer.c:1: warning: ISO C forbids an empty source file
make[1]: Leaving directory `/root/Desktop/mrmc_lin_v1.3/obj'
make: *** [lib] Error 2
and then going to bash command line and running ./bin/mrmc I obtain this meaasge:
bash cannot execute mrmc binary file
I don't know where is the problem, can you help me plz?
Thanks.
Diana
