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.