KKostya

let reward = (scenario) =>
  if( scenario.prize == scenario.first_guess ) { 
      if(scenario.choice == Stay) prize else 0.0;
  } else { 
      if(scenario.choice == Swap) prize else 0.0;
  }

KKostya

let valid_door_pmf : (door => real) => bool =  
  (pmf) => Real.(
    (pmf(DoorA) + pmf(DoorB) + pmf(DoorC) == 1.0) &&
    (pmf(DoorA) >= 0.0) &&
    (pmf(DoorB) >= 0.0) &&
    (pmf(DoorC) >= 0.0)  
  );

valid_door_pmf(pDoorsEqual)

KKostya

type t = A | B | C
let sum = (f) => f(A) + f(B) + f(C)
instance( (f) => f(A) > 0 && f(B) > 0 && sum(f) == 42 )

KKostya

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

KKostya

theorem stopping_if_for_all state =
  let open Sensor_msgs in
  match state.incoming with None | Some (Clock _ ) -> true 
  | Some ( Sensor data ) ->
  (  data.laserScan_ranges <> []
  && List.for_all (fun x -> x < 20000) data.laserScan_ranges    
  ) ==> (one_step state).mode = Turning

KKostya

- : state =
{mode = Turning; min_range = Some 7719; direction = None;
 incoming =
  Some
   (Sensor
     { Sensor_msgs.laserScan_range_min = 3
     ; laserScan_range_max = 25001
     ; laserScan_ranges = []
     });
 outgoing = None}

KKostya

verify ( fun state ->
  let open Sensor_msgs in
  match state.incoming with None | Some (Clock _ ) -> true 
  | Some ( Sensor data ) ->
  (  List.for_all (fun x -> x < 20000) data.laserScan_ranges    
  ) ==> (one_step state).mode = Turning
)

KKostya

theorem never_goes_back state = 
  state.incoming <> None
  ==>
  no_moving_back (one_step state).outgoing

KKostya

- : state =
 { mode = Turning; min_range = Some 2282
 ; direction = None; incoming = None
 ; outgoing = Some (Twist
   { twist_linear  = {vector3_x = -1; vector3_y = 9; vector3_z = 10}
   ; twist_angular = {vector3_x = 11; vector3_y = 1; vector3_z = 13}
 })}

KKostya

let no_moving_back msg = 
    let open Geometry_msgs in
    match msg with None -> true 
    | Some (Twist data) -> data.twist_linear.vector3_x >= 0
  
verify ( fun state -> no_moving_back (one_step state).outgoing  )