long-run average in Prism-games

瀏覽次數：14 次

跳到第一則未讀訊息

Shibashis

未讀,

2018年3月13日下午2:27:282018/3/13

收件者：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

回覆所有人

回覆作者

轉寄

0 則新訊息