- MRMC-users - lists.rwth-aachen.de

***** VIRUS REMOVED / ENTFERNT *****Delivery Status Notification
by Mail Delivery Service 31 Oct '10

31 Oct '10

- These recipients of your message have been processed by the mail server: abc(a)vnn.vn; Failed; 5.2.1 (mailbox disabled, not accepting messages)

1 0

Segmentation fault running MRMC
by Esteban Pavese 14 Jun '10

14 Jun '10

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?

3 2

urgent, Memory limitation in MRMC?
by Diana El Rabih 17 May '10

17 May '10

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

2 1

minimum probability
by Amir Molzam Sharifloo 20 Apr '10

20 Apr '10

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

3 3

mrmc 1.4.1 segfault on Linux amd64
by Matthias Guedemann 23 Mar '10

23 Mar '10

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 \____/ \__/\__/ __________________________________________________________

2 1

The statistics gathering script
by Ivan Zapreev 27 Jan '10

27 Jan '10

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.

1 0

Problems with download
by Stefano Schivo 21 Jan '10

21 Jan '10

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

2 1

MRMC an Mac OsX Snow Leopard
by Florian Leitner-Fischer 17 Dec '09

17 Dec '09

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

2 1

Other serious problem in the Fox Glynn implementation
by Elvio Amparore 15 Dec '09

15 Dec '09

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.

1 1

Bug in Fox-Glynn algorithm implementation
by Elvio Amparore 15 Dec '09

15 Dec '09

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

2 1