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/%7Enguyen
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/%7Enguyen
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/%7Enguyen
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/%7Enguyen
mrmc-users@lists.rwth-aachen.de
-
Amir Molzam Sharifloo -
Ernst Moritz Hahn -
Viet Yen Nguyen