verify ( (strategy) => Real.({
valid_strategy(strategy) ==>
( expected_reward (
make_scenario_pmf(pDoorsEqual,strategy)
) <= 1000000.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, Swap) -> (Real.mk_of_string "3/1000000")
| (DoorB, Stay) -> (Real.mk_of_string "999997/1000000")
| _ -> 0.
Refuted.