KKostya
10/21/2018 - 5:33 PM

monty_hall_verify_no_larger_third.re

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.