MRMC-users Mai 2013

mrmc-users@lists.rwth-aachen.de

3 Teilnehmer
2 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, 2 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.

10 Jahre, 11 Monate

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

MRMC-users Mai 2013