MRMC-users

mrmc-users@lists.rwth-aachen.de

36 Diskussionen

von Hubert Garavel

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

10 Jahre, 5 Monate

CTMC transient analysis

von Osank Jain

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

10 Jahre, 11 Monate

MRMC feature request

von David N. Jansen

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.

11 Jahre, 1 Monat

Show steady-state probabilities

von Daniel Schemala

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

12 Jahre, 1 Monat

[patch] Bug in timings on x86

von Bram Geron

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

12 Jahre, 6 Monate

Bugs in Methods for Reward-Bounded Until

von Ernst Moritz Hahn

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

13 Jahre, 1 Monat

help with model checking CTMDP

von Ana Medina Ayala

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

13 Jahre, 1 Monat

***** VIRUS REMOVED / ENTFERNT *****Undelivered Mail Returned to Sender

von Mail Delivery System

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"

13 Jahre, 7 Monate

*****SPAM***** mrmc-users@lists.rwth-aachen.de Rolex For You -73%

von Rolex.com

13 Jahre, 8 Monate

***** VIRUS REMOVED / ENTFERNT *****Delivery Status Notification

von Mail Delivery Service

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

13 Jahre, 8 Monate

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

MRMC-users