Hi,
I was just getting into mmrc.I want to know how the transient analysis of
CTMC is done by uniformization or diiferential equations
I'd be great if someone give some details and point me towards it's code in
the package as I not getting it.
Thanks in advance
Osank jain
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.
Hello,
we are using MRMC for DMRMs. Currently, it is possible to compute the
states where the long-run probabilities hold a given property.
Is there also a possibility to show the steady-state (or long-run)
probability for each state, as in PRISM?
Greetings,
Daniel
Hi,
On my 32-bit machine MRMC gives incorrect timings. This is due to the
fact that the clock type is converted to an unsigned long, which is
32-bit on 32-bit systems. A patch follows, which also fixes a typo.
By the way, the /new ticket/ link at mrmc-tool.org/trac/wiki/Contact
<http://www.mrmc-tool.org/trac/wiki/Contact> doesn't work, because it
wants me to log in and I can't seem to make an account.
Cheers,
Bram Geron
CS student at Eindhoven University of Technology
--- a/src/io/parser/parser_to_core.c Mon Dec 19 17:13:47 2011 +0100
+++ b/src/io/parser/parser_to_core.c Mon Dec 19 17:28:30 2011 +0100
@@ -103,7 +103,7 @@
}
timer_started = FALSE;
- return ((unsigned long) (stop_time - start_time) * 1000
+ return ((clock_t) (stop_time - start_time) * 1000
+ CLOCKS_PER_SEC / 2) / CLOCKS_PER_SEC;
}
@@ -567,7 +567,7 @@
/* Clean the old results */
clearOldModelCheckingResults();
- /* Star the timer */
+ /* Start the timer */
startTimer();
/* In case of simulation engine on we have to traverse the tree */
Hello all,
I think there are bugs in the methods to handle the reward-bounded until
in the MRMC. The problem occurs with the latest version 1.5 as well as
the version in the repository. As already pointed out by David Jansen in
a comment in transient_ctmrm.c at lines 644 and 645, I think the
rounding should be different. When changing these lines it seems to
work. The problem also occurs in practise, for instance the results for
time bounds 0.99 and 1.0 are completely different. The discretisation
factor needs to be quite small to be accepted by MRMC, such that the
model checking process takes a lot of time, but I think this is not a bug.
For the uniformisation method, I get completely useless results,
although I set the parameter "w" to a rather small value.
The attachment contains the archive bugreport.zip to demonstrate this
phenomenon. The model files are google_mrmc.tra, google_mrmc.lab,
google_mrmc.rew and google_mrmc.lab. The file input_dis.inp demonstrates
that the discretisation method is seemingly broken and input_uni.inp is
for the uniformisation method.
I'm not sure who is currently responsible for this part of the MRMC. It
would be nice if the problem could be handled in time. We are currently
preparing a paper for MSCS and want to add some experimental results
involving the reward-bounded until for a model similar to the one in the
attachment.
Best regards,
Moritz
Hi,
I am getting familiar with the MRMC tool and I would appreciate if somebody
can provide a simple example on how to use the tool to get an optimal
policy for a CTMDP given a specification in CSL.
Any help will be very appreciated.
Thanks a lot,
Ana
This is the mail system at host mx1.tailieu.vn.
I'm sorry to have to inform you that your message could not
be delivered to one or more recipients. It's attached below.
For further assistance, please send mail to <postmaster>
If you do so, please include this problem report. You can
delete your own text from the attached returned message.
The mail system
<upro_no-reply(a)tailieu.vn>: unknown user: "upro_no-reply"