prob assertion P_deadlock_free:
!E [Finally "deadlock"]
const xx: core::int
// probability of outcome is 1
prob assertion P_out_1:
Prob=? [Finally DieM::CTRL::stm_ref0 is in DieM::CTRL::stm_ref0::Out
& DieM::CTRL::stm_ref0::d = 1
]
// probability of outcome is xx when xx ranges from 1 to 6
prob assertion P_out_x:
Prob=? [Finally DieM::CTRL::stm_ref0 is in DieM::CTRL::stm_ref0::Out
& DieM::CTRL::stm_ref0::d = xx
]
with constant xx from set {1,2,3,4,5,6}
// probability of outcome is xx when xx ranges from 1 to 6 if we run statistic
// model checking instead of exact model checking above
prob assertion P_out_x_sim:
Prob=? [Finally<=1000 DieM::CTRL::stm_ref0 is in DieM::CTRL::stm_ref0::Out
& DieM::CTRL::stm_ref0::d = xx
]
using sim with CI at alpha=0.01, n=2000, and pathlen=1000
with constant xx from set 1:6:1
// for each flip, give one reward
rewards num_of_flips =
[DieM::CTRL::stm_ref0::flip] true:1;
endrewards
// average number of flips before an outcome is produced
prob assertion R_out:
Reward=? [Reachable DieM::CTRL::stm_ref0 is in DieM::CTRL::stm_ref0::Out]