Hi Moritz, Next time I'll consult you first :) Viet Y.en On Apr 20, 2010, at 6:11 , Ernst Moritz Hahn wrote:

Hello,

you can the the minimum probabilities by changing

P{<=0.9}[tt U[0,5] label]

to

P{>=0.9}[tt U[0,5] label]

Regards, Moritz

Am Montag, den 19.04.2010, 08:41 -0400 schrieb Viet Yen Nguyen:

...

Hi Amir,

The minimum probabilities are not built-in, but you can modify the source code to achieve that.

Good luck,

Viet Yen

On Apr 18, 2010, at 10:09 , Amir Molzam Sharifloo wrote:

...

Hello,

I'm using MRMC to do model checking of CTMDP. when I check a property like

P{<=0.9}[tt U[0,5] label]

it gives me back the maximum probability, but I need the minimum probability. How can I get it? Thanks in advance.

Amir _______________________________________________ MRMC-users mailing list MRMC-users@lists.rwth-aachen.de https://mailman.rwth-aachen.de/mailman/listinfo/mrmc-users

Viet Yen -- http://moves.rwth-aachen.de/~nguyen

_______________________________________________ MRMC-users mailing list MRMC-users@lists.rwth-aachen.de https://mailman.rwth-aachen.de/mailman/listinfo/mrmc-users

_______________________________________________ MRMC-users mailing list MRMC-users@lists.rwth-aachen.de https://mailman.rwth-aachen.de/mailman/listinfo/mrmc-users

Viet Yen -- http://moves.rwth-aachen.de/~nguyen