Dear Daniel,

Op 9 mei 2012, om 10:31 heeft Daniel Schemala het volgende geschreven:

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?

There is no command-line or interactive feature to get these probabilities, because MRMC only calculates them in part. I looked into the source code of src/modelchecking/steady.c again and found that MRMC calculates two things:

1. For each BSCC and each state of this BSCC, the probability to be in the state under the condition that the system is in the BSCC. This calculation happens in function solveBSCCs().

2. For a given set of states, the probability to be in this set on the long run. This is calculated in function getS_F_Solution(), which calls getReachProbability() to calculate for each relevant BSCC and each state, the probability to reach the BSCC from the state. This auxiliary calculation is done in function getReachProbability().

Because the second step is only done for the *relevant* BSCCs (i.e. the BSCCs that contain at least one desired state), we cannot get exactly what you are asking for. If you want, you can uncomment a few lines in the source code to print the partial results: lines 337-338 and 400-402 in src/modelchecking/steady.c.

Kind regards, David N. Jansen.