verify ( (strategy) => Real.({
valid_strategy(strategy) ==>
( expected_reward (
make_scenario_pmf(pDoorsBiased,strategy)
) <= 2000000.0 / 3.0 )
}))
module CX : sig val strategy : door -> choice -> Q.t end
Counterexample (after 0 steps, 0.012s):
let strategy x_0 x_1 =
match (x_0, x_1) with
| (DoorA, Stay) -> (Real.mk_of_string "399997/600000")
| (DoorC, Swap) -> (Real.mk_of_string "200003/600000")
| _ -> 0.
Refuted.