Markov Reward Model Checker: Ticket Query
http://www.mrmc-tool.org/trac/query?group=status&component=Core&milestone=MRMC+future&row=description
en-USMarkov Reward Model Checkerhttp://www.mrmc-tool.org/trac/chrome/../../images/mrmc-logo.png
http://www.mrmc-tool.org/trac/query?group=status&component=Core&milestone=MRMC+future&row=description
Trac 0.11.4rc1
http://www.mrmc-tool.org/trac/ticket/57
http://www.mrmc-tool.org/trac/ticket/57#57: Lumping fails with the new sparse matrix implementatationThu, 11 Feb 2010 12:05:59 GMTivan.zapreev<p>
With the DTMC lumping the wscl performance test was crushing.
</p>
<p>
Here is the reply by David N. Jansen and a fix
</p>
<p>
Dear Ivan,
</p>
<p>
I think the problem is really a bug in bscc.c. visit_non_rec() sometimes adds states to a BSCC twice. That doesn't give large problems, only the size of a BSCC is then registered too large. I added a patch that includes a bugfix and an additional internal test as regression test. I took the .tra file from the CTMC lumping test because that file exposed the bug first, and I also found a very small .tra file that still shows the bug. Basically, visit_non_rec() proceeds as follows:
1. Process state 0:
</p>
<blockquote>
<p>
1.1. Push all successors of 0 onto dfs_stack, i.e. states 1 and 2
</p>
</blockquote>
<p>
2. Process state 2:
</p>
<blockquote>
<p>
2.1. Push all successors of 2 onto dfs_stack, i.e. state 1
</p>
</blockquote>
<p>
-- At this moment, state 1 is on the dfs_stack twice. It may be that the second time, it is no longer necessary to handle it. I found a small bugfix, but perhaps you can find a better one that doesn't handle state 1 twice in this situation.
</p>
<p>
I tried a few functional tests and the wscl performance test, which now works out fine (wscl03 fails, but that is due to the fact that MRMC now correctly sees that the Markov chain is ergodic).
</p>
<p>
Kind regards,
David.
</p>
Resultshttp://www.mrmc-tool.org/trac/ticket/57#changelog
http://www.mrmc-tool.org/trac/ticket/28
http://www.mrmc-tool.org/trac/ticket/28#28: PRCTL, lumping: The E operator problem.Fri, 27 Jun 2008 13:15:10 GMTivan.zapreev<p>
PRCTL, E operator gives different results with and without formula independent lumping, compare tests:
</p>
<pre class="wiki">test/functional_tests/dtmrm/prctl/syntax/prctl_general_input_02
</pre><p>
and
</p>
<pre class="wiki">test/functional_tests/dtmrm/prctl/syntax/prctl_general_input_01
</pre>Resultshttp://www.mrmc-tool.org/trac/ticket/28#changelog
http://www.mrmc-tool.org/trac/ticket/33
http://www.mrmc-tool.org/trac/ticket/33#33: Improve and unify the error/warning/info messages.Fri, 27 Jun 2008 13:41:03 GMTivan.zapreev<p>
Should be done as a part of Architectural change of MRMC.
Make a clear distinctions between [WARNING], [ERROR], [INFO] message logging.
</p>
Resultshttp://www.mrmc-tool.org/trac/ticket/33#changelog
http://www.mrmc-tool.org/trac/ticket/34
http://www.mrmc-tool.org/trac/ticket/34#34: Add a possibility to dump the model-checking resultsFri, 27 Jun 2008 13:41:55 GMTivan.zapreev<p>
Add a possibility to dump the model-checking results into a file from the MRMC command prompt. It should be useful in case we have "set print off" and after of checking results with
</p>
<pre class="wiki">$RESULT[i] and $STATE[i]
</pre><p>
we want to store the rest on the hard drive.
</p>
Resultshttp://www.mrmc-tool.org/trac/ticket/34#changelog
http://www.mrmc-tool.org/trac/ticket/35
http://www.mrmc-tool.org/trac/ticket/35#35: Improving $RESULT and $STATE commandsFri, 27 Jun 2008 13:43:51 GMTivan.zapreev<p>
In the command prompt of MRMC, add a possibility to get not just the $RESULT[i] but $RESULT[i..j, ..., k-p] etc. The same goes for $STATE{}.
</p>
<p>
This way users will be able to get resulting probabilities and etc for some set of states, they have interest in.
</p>
Resultshttp://www.mrmc-tool.org/trac/ticket/35#changelog
http://www.mrmc-tool.org/trac/ticket/40
http://www.mrmc-tool.org/trac/ticket/40#40: Error bounds and the numerical model-checking engineFri, 27 Jun 2008 14:40:47 GMTivan.zapreev<p>
Error bounds are not properly computed and used! For nested formulas it is not even known how to derive error bounds. For plain steady-state operator it is known but is not done:
</p>
<ul><li>Since probabilistic results are computed with a certain error bound for the steady-state (long-run) operators of PRCTL, PCTL, CSL and CSRL, we have to check +- error bound bound. <strong>WARNING</strong>: Here the provided error bound is not quite correct, it is tighter than it should be but at least it is something!
<pre class="wiki"> S{<=>p}[phi], err = get_error_bound()
1. In case of ergodic MC we have to take:
error_bound = err * | phi |
2. In case of Non ergodic MC it should be:
error_bound = \Sum_j (y_j * err +
x_ij * err * | phi_j | + err^2 * | phi_j |)
Where \Sum_j ( (x_ij +- err)*(y_j +- err * | phi_j |) )
is the way the probability is computed for the state i.
x_ij - the probability to reach BSCC_j from state i
y_j - the the total steady state probability of phi
states in BSCC_j
phi_j - the phi states in BSCC_j
</pre></li></ul><ul><li>Imagine nested Until formulas, on every level there are computational errors. Now what if one one level due to such an error we include a wrong state / exclude a needed state, how does this affect the error bound of the formulas on the outer level?!
</li></ul><p>
We should be able to set an error bound once and then to derive sub error bounds for sub formulas in such a way that the overall error remains the one the user wants. Right now the same error bound is just used everywhere.
</p>
Resultshttp://www.mrmc-tool.org/trac/ticket/40#changelog