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

Bug report for MRMC 1.5
by Hubert Garavel 29 Jan '14

29 Jan '14

Dear MRMC developers, I started experimenting MRMC 1.5 and found a bug. I tried to report it using the bug tracker at http://www.mrmc-tool.org/trac/newticket but the system asks me to log in, and provides no means for registering as a new user. So, this is the bug (produced on a Debian Linux Squeeze running in a VirtualBox): launching the command mrmc dtmc x.tra x.lab produces the following error > ------------------------------------------------------------------- > | Markov Reward Model Checker | > | MRMC Version 1.5 | > | Copyright (C) RWTH Aachen, 2006-2011. | > | Copyright (C) The University of Twente, 2004-2008. | > | Authors: | > | Ivan S. Zapreev (2004-2011), David N. Jansen (since 2007), | > | E. Moritz Hahn (2007-2010), Falko Dulat (2009-2010), | > | Christina Jansen (2007-2008), Sven Johr (2006-2007), | > | Tim Kemna (2005-2006), Maneesh Khattri (2004-2005) | > | MRMC is distributed under the GPL conditions | > | (GPL stands for GNU General Public License) | > | The product comes with ABSOLUTELY NO WARRANTY. | > | This is a free software, and you are welcome to redistribute it. | > ------------------------------------------------------------------- > Logic = PCTL > Loading the 'x.tra' file, please wait. > *** glibc detected *** mrmc: double free or corruption (!prev): 0x09e3b008 *** > ======= Backtrace: ========= > /lib/i686/cmov/libc.so.6(+0x6af71)[0xb7437f71] > /lib/i686/cmov/libc.so.6(+0x6c7c8)[0xb74397c8] > /lib/i686/cmov/libc.so.6(cfree+0x6d)[0xb743c8ad] > /lib/i686/cmov/libc.so.6(fclose+0x14a)[0xb742841a] > mrmc[0x804b70a] > mrmc[0x8049e67] > mrmc[0x804a27a] > /lib/i686/cmov/libc.so.6(__libc_start_main+0xe6)[0xb73e3ca6] > mrmc[0x8049261] > ======= Memory map: ======== > 08048000-08087000 r-xp 00000000 08:01 410935 /home/moi/Desktop/mrmc_src_v1.5/bin/mrmc > 08087000-08088000 rw-p 0003e000 08:01 410935 /home/moi/Desktop/mrmc_src_v1.5/bin/mrmc > 09e3b000-09e5c000 rw-p 00000000 00:00 0 [heap] > b7200000-b7221000 rw-p 00000000 00:00 0 > b7221000-b7300000 ---p 00000000 00:00 0 > b739d000-b73ba000 r-xp 00000000 08:01 16387 /lib/libgcc_s.so.1 > b73ba000-b73bb000 rw-p 0001c000 08:01 16387 /lib/libgcc_s.so.1 > b73cc000-b73cd000 rw-p 00000000 00:00 0 > b73cd000-b750d000 r-xp 00000000 08:01 33220 /lib/i686/cmov/libc-2.11.3.so > b750d000-b750e000 ---p 00140000 08:01 33220 /lib/i686/cmov/libc-2.11.3.so > b750e000-b7510000 r--p 00140000 08:01 33220 /lib/i686/cmov/libc-2.11.3.so > b7510000-b7511000 rw-p 00142000 08:01 33220 /lib/i686/cmov/libc-2.11.3.so > b7511000-b7514000 rw-p 00000000 00:00 0 > b7514000-b7538000 r-xp 00000000 08:01 32919 /lib/i686/cmov/libm-2.11.3.so > b7538000-b7539000 r--p 00023000 08:01 32919 /lib/i686/cmov/libm-2.11.3.so > b7539000-b753a000 rw-p 00024000 08:01 32919 /lib/i686/cmov/libm-2.11.3.so > b753a000-b753b000 rw-p 00000000 00:00 0 > b753b000-b756c000 r-xp 00000000 08:01 165735 /usr/lib/libgslcblas.so.0.0.0 > b756c000-b756d000 rw-p 00030000 08:01 165735 /usr/lib/libgslcblas.so.0.0.0 > b756d000-b7751000 r-xp 00000000 08:01 165734 /usr/lib/libgsl.so.0.15.0 > b7751000-b7760000 rw-p 001e3000 08:01 165734 /usr/lib/libgsl.so.0.15.0 > b7770000-b7773000 rw-p 00000000 00:00 0 > b7773000-b7774000 r-xp 00000000 00:00 0 [vdso] > b7774000-b778f000 r-xp 00000000 08:01 18385 /lib/ld-2.11.3.so > b778f000-b7790000 r--p 0001b000 08:01 18385 /lib/ld-2.11.3.so > b7790000-b7791000 rw-p 0001c000 08:01 18385 /lib/ld-2.11.3.so > bfd7d000-bfd92000 rw-p 00000000 00:00 0 [stack] > Aborted with file x.tra containing : << 11 55 0 0 0.2 0 5 0.2 0 4 0.2 0 0 0.2 0 10 0.2 1 1 0.2 1 6 0.2 1 4 0.2 1 3 0.2 1 9 0.2 2 2 0.2 2 7 0.2 2 4 0.2 2 6 0.2 2 8 0.2 3 3 0.2 3 8 0.2 3 4 0.2 3 9 0.2 3 7 0.2 4 4 0.2 4 9 0.2 4 4 0.2 4 1 0.2 4 6 0.2 5 5 0.2 5 10 0.2 5 4 0.2 5 4 0.2 5 5 0.2 6 6 0.2 6 0 0.2 6 4 0.2 6 7 0.2 6 4 0.2 7 7 0.2 7 1 0.2 7 4 0.2 7 10 0.2 7 3 0.2 8 8 0.2 8 2 0.2 8 4 0.2 8 2 0.2 8 2 0.2 9 9 0.2 9 3 0.2 9 4 0.2 9 5 0.2 9 1 0.2 10 10 0.2 10 4 0.2 10 4 0.2 10 8 0.2 10 0 0.2 >> and file x.lab containing << #DECLARATION initial #END 0 initial >> I am aware that the .tra file is a PRISM one, not an MRMC one. I am also unsure about the x.lab one. Yet, this should not cause a crash. Best regards Hubert (in Saarbrücken) -- ',',',',',',',',',',' Hubert GARAVEL | Inria - LIG / CONVECS ',',',',',',',',',',' hubert.garavel(a)inria.fr | 655, avenue de l'Europe ',',',',',',',',',',' tel: +(33) 4 76 61 52 24 | 38330 Montbonnot St Martin ',',',',',',',',',',' fax: +(33) 4 76 61 52 52 | France ',',',',',',',',',',' http://convecs.inria.fr/people/Hubert.Garavel

2 3

CTMC transient analysis
by Osank Jain 09 Jul '13

09 Jul '13

Hi, I was just getting into mmrc.I want to know how the transient analysis of CTMC is done by uniformization or diiferential equations I'd be great if someone give some details and point me towards it's code in the package as I not getting it. Thanks in advance Osank jain

3 5

MRMC feature request
by David N. Jansen 21 May '13

21 May '13

Dear all, It is possible, in MRMC, to verify several until properties of CTMCs. The general syntax is “phi U[low, high] psi”, where “low” and “high” may be real numbers. However, it should also be allowed that high = infinity. If low = 0, then one can write “phi U psi”, but what if low > 0? I propose that it becomes allowed to write “inf” or “infinity” in the position of high, similar to what is printed by printf("%g", HUGE_VAL);. Example formula: P{<=0.1} [ tt U[10,infinity] crash ] “The probability to crash no earlier than after 10 time units is at most 10%.” Kind regards, David N. Jansen.

2 1

Show steady-state probabilities
by Daniel Schemala 09 May '12

09 May '12

Hello, we are using MRMC for DMRMs. Currently, it is possible to compute the states where the long-run probabilities hold a given property. Is there also a possibility to show the steady-state (or long-run) probability for each state, as in PRISM? Greetings, Daniel

2 1

[patch] Bug in timings on x86
by Bram Geron 04 Jan '12

04 Jan '12

Hi, On my 32-bit machine MRMC gives incorrect timings. This is due to the fact that the clock type is converted to an unsigned long, which is 32-bit on 32-bit systems. A patch follows, which also fixes a typo. By the way, the /new ticket/ link at mrmc-tool.org/trac/wiki/Contact <http://www.mrmc-tool.org/trac/wiki/Contact> doesn't work, because it wants me to log in and I can't seem to make an account. Cheers, Bram Geron CS student at Eindhoven University of Technology --- a/src/io/parser/parser_to_core.c Mon Dec 19 17:13:47 2011 +0100 +++ b/src/io/parser/parser_to_core.c Mon Dec 19 17:28:30 2011 +0100 @@ -103,7 +103,7 @@ } timer_started = FALSE; - return ((unsigned long) (stop_time - start_time) * 1000 + return ((clock_t) (stop_time - start_time) * 1000 + CLOCKS_PER_SEC / 2) / CLOCKS_PER_SEC; } @@ -567,7 +567,7 @@ /* Clean the old results */ clearOldModelCheckingResults(); - /* Star the timer */ + /* Start the timer */ startTimer(); /* In case of simulation engine on we have to traverse the tree */

3 3

Bugs in Methods for Reward-Bounded Until
by Ernst Moritz Hahn 23 May '11

23 May '11

Hello all, I think there are bugs in the methods to handle the reward-bounded until in the MRMC. The problem occurs with the latest version 1.5 as well as the version in the repository. As already pointed out by David Jansen in a comment in transient_ctmrm.c at lines 644 and 645, I think the rounding should be different. When changing these lines it seems to work. The problem also occurs in practise, for instance the results for time bounds 0.99 and 1.0 are completely different. The discretisation factor needs to be quite small to be accepted by MRMC, such that the model checking process takes a lot of time, but I think this is not a bug. For the uniformisation method, I get completely useless results, although I set the parameter "w" to a rather small value. The attachment contains the archive bugreport.zip to demonstrate this phenomenon. The model files are google_mrmc.tra, google_mrmc.lab, google_mrmc.rew and google_mrmc.lab. The file input_dis.inp demonstrates that the discretisation method is seemingly broken and input_uni.inp is for the uniformisation method. I'm not sure who is currently responsible for this part of the MRMC. It would be nice if the problem could be handled in time. We are currently preparing a paper for MSCS and want to add some experimental results involving the reward-bounded until for a model similar to the one in the attachment. Best regards, Moritz

2 2

help with model checking CTMDP
by Ana Medina Ayala 21 May '11

21 May '11

Hi, I am getting familiar with the MRMC tool and I would appreciate if somebody can provide a simple example on how to use the tool to get an optimal policy for a CTMDP given a specification in CSL. Any help will be very appreciated. Thanks a lot, Ana

2 1

***** VIRUS REMOVED / ENTFERNT *****Undelivered Mail Returned to Sender
by Mail Delivery System 15 Nov '10

15 Nov '10

This is the mail system at host mx1.tailieu.vn. I'm sorry to have to inform you that your message could not be delivered to one or more recipients. It's attached below. For further assistance, please send mail to <postmaster> If you do so, please include this problem report. You can delete your own text from the attached returned message. The mail system <upro_no-reply(a)tailieu.vn>: unknown user: "upro_no-reply"

1 0

*****SPAM***** mrmc-users@lists.rwth-aachen.de Rolex For You -73%
by Rolex.com 02 Nov '10

02 Nov '10

1 0

***** 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