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)
Dear Hubert,
Op 2 mei 2013, om 15:18 heeft Hubert Garavel het volgende geschreven:
I started experimenting MRMC 1.5 and found a bug.
The point is that the file x.tra does not follow the file format in the documentation http://www.mrmc-tool.org/downloads/MRMC/Specs/MRMC_Manual_1.5.pdf, page 13, section 4.1. First, the number of states and transitions have to be given on separate lines (as below). Second, state indices start with 1 and transitions must be given in ascending order of first row and then column index. I think the smallest change is to renumber your state 0 to state 11 and then sort the transitions. And finally, if you repeat a transition, the new probability will replace the old one; they will not be added (perhaps this is different from PRISM’s behaviour and could be considered a bug).
Then the file x.tra becomes:
STATES 11 TRANSITIONS 55 1 1 0.2 1 3 0.2 1 4 0.2 1 6 0.2 1 9 0.2 2 2 0.2 2 4 0.2 2 6 0.2 2 7 0.2 2 8 0.2 3 3 0.2 3 4 0.2 3 7 0.2 3 8 0.2 3 9 0.2 4 1 0.2 4 4 0.4 4 6 0.2 4 9 0.2 5 4 0.4 5 5 0.4 5 10 0.2 6 4 0.4 6 6 0.2 6 7 0.2 6 11 0.2 7 1 0.2 7 3 0.2 7 4 0.2 7 7 0.2 7 10 0.2 8 2 0.6 8 4 0.2 8 8 0.2 9 1 0.2 9 3 0.2 9 4 0.2 9 5 0.2 9 9 0.2 10 4 0.4 10 8 0.2 10 10 0.2 10 11 0.2 11 4 0.2 11 5 0.2 11 10 0.2 11 11 0.4
and x.lab is:
#DECLARATION initial #END 11 initial
Kind regards, David N. Jansen.
Dear David N. Jansen,
Thanks for your answer dated May 2, 2013. I apologize for the delay in responding but after submitting the bug, I did not receive any answer in my mailbox. I now understand that the answer was posted to the MRMC mailing list, to which I did not register, so I only saw your anwser today by chance browsing the mailing-list.
Indeed, I agree that the .tra file was not a correct input file for MRMC, because it was in PRISM format, which is similar yet slightly different.
The point of my bug report was different: given a wrong input file, MRMC should emit an error message, instead of crashing with a memory problem *** mrmc: double free or corruption (!prev): 0x09e3b008 ***
This was really the essence of my bug report.
All the best Hubert
Dear Hubert,
Op 28 jan. 2014, om 09:38 heeft Hubert Garavel hubert.garavel@inria.fr het volgende geschreven:
Thanks for your answer dated May 2, 2013. I apologize for the delay in responding but after submitting the bug, I did not receive any answer in my mailbox. I now understand that the answer was posted to the MRMC mailing list, to which I did not register, so I only saw your anwser today by chance browsing the mailing-list.
Indeed, I agree that the .tra file was not a correct input file for MRMC, because it was in PRISM format, which is similar yet slightly different.
The point of my bug report was different: given a wrong input file, MRMC should emit an error message, instead of crashing with a memory problem *** mrmc: double free or corruption (!prev): 0x09e3b008 ***
This was really the essence of my bug report.
You are right. I sent another mail to Joost-Pieter with a proposed fix of the bug. It basically is:
In the branch https://svn-i2.informatik.rwth-aachen.de/repos/mrmc/branches/nijmegen-small-..., I added more strict tests of the file contents that produce an error message whenever a line does not follow the format exactly. This branch also includes a number of other improvements to the MRMC code, e.g. stricter type checking, a corrected Fox-Glynn algorithm (see my report https://pms.cs.ru.nl/iris-diglib/src/getContent.php?id=2011-Jansen-Understan...), and more efficient solving of linear equation systems.
It also includes my implementation of sparse matrices (see Appendix D of the MRMC user manual, also available as a patch from http://www.mrmc-tool.org/downloads.php), which we did not insert in the trunk because simulation became inefficient. Shortly after releasing MRMC 1.5, I found the error and corrected that inefficiency.
Sorry for the delay... I had thought that this fix would be quickly included into the trunk of the svn repository by someone in Joost-Pieters group. (If the person responsible for the repository desires, I can merge the mentioned branch into the trunk. The branch passes all tests. However, I will not produce a full new release.)
Kind regards, David.
mrmc-users@lists.rwth-aachen.de
-
David N. Jansen -
Hubert Garavel