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)