long-run average in Prism-games

14 views

Skip to first unread message

Shibashis

unread,

Mar 13, 2018, 2:27:28 PM3/13/18

to PRISM model checker

Hello,

Is it possible to specify in Prism-games a property to compute the minimum expected long-run average (mean payoff) value that can be guaranteed by player 1?

I tend to use the following

<<1>> Rmin=? [ S ]

which gives an 

Error: Can't convert class java.lang.Boolean to type double. 

Regards
- Shibashis

Reply all

Reply to author

Forward

0 new messages