minimum probability
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
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
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
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
participants (3)
-
Amir Molzam Sharifloo -
Ernst Moritz Hahn -
Viet Yen Nguyen