verify_biased_reward_2_3rds.re

verify ( (strategy) => Real.({
  valid_strategy(strategy) ==>
  ( expected_reward (
      make_scenario_pmf(pDoorsBiased,strategy)
  ) <= 2000000.0 / 3.0 ) 
}))

~output

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.