[examples] Use program syntax in ACAS Xu example specification.

examples/acasxu/acasxu.why

@@ -19,42 +19,44 @@ theory ACASXU
 
   type input = vector t
 
-  constant distance_to_intruder: int = 0
-  constant angle_to_intruder: int = 1
-  constant intruder_heading: int = 2
-  constant speed: int = 3
-  constant intruder_speed: int = 4
+  let constant distance_to_intruder: int = 0
+  let constant angle_to_intruder: int = 1
+  let constant intruder_heading: int = 2
+  let constant speed: int = 3
+  let constant intruder_speed: int = 4
 
   (****************************************************************************)
   (* Meaningful names for actions acting as indices of output vectors. *)
 
   type action = int
 
-  constant clear_of_conflict: action = 0
-  constant weak_left: action = 1
-  constant weak_right: action = 2
-  constant strong_left: action = 3
-  constant strong_right: action = 4
+  let constant clear_of_conflict: action = 0
+  let constant weak_left: action = 1
+  let constant weak_right: action = 2
+  let constant strong_left: action = 3
+  let constant strong_right: action = 4
 
   (****************************************************************************)
   (* Model filename and format.
   
-     The [model_filename] and [is_onnx] constants are meant to be defined from
+     The [model_filename] and [is_onnx] let constants are meant to be defined from
      the command-line.
   *)
 
-  constant model_filename: string
-  constant nn: model nn = read_model model_filename
+  val constant model_filename: string
+  let constant nn: model nn = read_model model_filename
 
   (****************************************************************************)
   (* Utilities. *)
 
-  constant pi: t = 3.141592653589793115997963468544185161590576171875000
+  type output = vector t
 
-  function denormalize_t (i: t) (mean: t) (range: t) : t =
+  let constant pi: t = 3.141592653589793115997963468544185161590576171875000
+
+  let function denormalize_t (i: t) (mean: t) (range: t) : t =
     (i .* range) .+ mean
 
-  function denormalize_by_index (idx: int) (t: t) : t =
+  let function denormalize_by_index (idx: int) (t: t) : t =
     if idx = distance_to_intruder then denormalize_t t (19791.0:t) (60261.0:t)
     else if idx = angle_to_intruder then denormalize_t t (0.0:t) (6.2831853071800001231395071954466402530670166015625:t)
     else if idx = intruder_heading then denormalize_t t (0.0:t) (6.2831853071800001231395071954466402530670166015625:t)
@@ -62,12 +64,29 @@ theory ACASXU
     else if idx = intruder_speed then denormalize_t t (600.0:t) (1200.0:t)
     else t
 
-  function denormalize_input (i:input) : input =
+  let function denormalize_input (i: input) : input =
     Vector.mapi i denormalize_by_index
 
-  function denormalize_output (o: t) : t =
+  let function denormalize_output_t (o: t) : t =
     denormalize_t o (7.51888402010059753166615337249822914600372314453125:t) (373.9499200000000200816430151462554931640625:t)
 
+  let function normalize_t (i: t) (mean: t) (range: t) : t =
+    (i .- mean) ./ range
+
+  let function normalize_by_index (idx: int) (t: t) : t =
+    if idx = distance_to_intruder then normalize_t t (19791.0:t) (60261.0:t)
+    else if idx = angle_to_intruder then normalize_t t (0.0:t) (6.2831853071800001231395071954466402530670166015625:t)
+    else if idx = intruder_heading then normalize_t t (0.0:t) (6.2831853071800001231395071954466402530670166015625:t)
+    else if idx = speed then normalize_t t (650.0:t) (1100.0:t)
+    else if idx = intruder_speed then normalize_t t (600.0:t) (1200.0:t)
+    else t
+
+  let function normalize_input (i: input) : input =
+    Vector.mapi i normalize_by_index
+
+  let function normalize_output_t (o: t) : t =
+    normalize_t o (7.51888402010059753166615337249822914600372314453125:t) (373.9499200000000200816430151462554931640625:t)
+
   (****************************************************************************)
   (* Common predicates. *)  
 
@@ -81,15 +100,13 @@ theory ACASXU
   predicate valid_action (a: action) =
     clear_of_conflict <= a <= strong_right
 
-  predicate advises_min_score (nn: model nn) (i: input) (a: action) =
+  predicate advises_min_score (o: output) (a: action) =
     valid_action a ->
-    forall b: action.
-      valid_action b ->  a <> b -> (nn @@ i)[a] .<= (nn @@ i)[b]
+    forall b: action. valid_action b ->  a <> b -> o[a] .<= o[b]
 
-  predicate advises_max_score (nn: model nn) (i: input) (a: action) =
+  predicate advises_max_score (o: output) (a: action) =
     valid_action a ->
-    forall b: action.
-      valid_action b ->  a <> b -> (nn @@ i)[a] .>= (nn @@ i)[b]
+    forall b: action. valid_action b ->  a <> b -> o[a] .>= o[b]
 
   (****************************************************************************)
   (* Property 1.
@@ -109,7 +126,16 @@ theory ACASXU
       let j = denormalize_input i in
       valid_input j /\ intruder_distant_and_slow j ->
       let o = (nn @@ i)[clear_of_conflict] in
-      (denormalize_output o) .<= (1500.0:t)
+      (denormalize_output_t o) .<= (1500.0:t)
+
+  let runP1 (i: input) : t
+    requires { has_length i 5 }
+    requires { valid_input i }
+    requires { intruder_distant_and_slow i }
+    ensures { result .<= (1500.0:t) }  =
+      let j = normalize_input i in
+      let o = (nn @@ j)[clear_of_conflict] in
+      (denormalize_output_t o)
 
   (****************************************************************************)
   (* Property 2.
@@ -123,7 +149,14 @@ theory ACASXU
       has_length i 5 ->
       let j = denormalize_input i in
       valid_input j /\ intruder_distant_and_slow j ->
-      not (advises_max_score nn i clear_of_conflict)
+      not (advises_max_score (nn @@ i) clear_of_conflict)
+
+  let runP2 (i: input) : output
+    requires { has_length i 5 }
+    requires { valid_input i /\ intruder_distant_and_slow i }
+    ensures { not (advises_max_score result clear_of_conflict) } =
+      let j = normalize_input i in
+      nn @@ j
 
   (****************************************************************************)
   (* Property 3.
@@ -146,7 +179,14 @@ theory ACASXU
       has_length i 5 ->
       let j = denormalize_input i in
       valid_input j /\ directly_ahead j /\ moving_towards j ->
-      not (advises_min_score nn i clear_of_conflict)
+      not (advises_min_score (nn @@ i) clear_of_conflict)
+
+  let runP3 (i: input) : output
+    requires { has_length i 5 }
+    requires { valid_input i /\ directly_ahead i /\ moving_towards i }
+    ensures { not (advises_min_score result clear_of_conflict) } =
+      let j = normalize_input i in
+      nn @@ j
 
   (****************************************************************************)
   (* Property 4.
@@ -157,7 +197,7 @@ theory ACASXU
   *)
 
   predicate moving_away (i: input) =
-    i[intruder_heading] .= (0.0:t)
+    i[intruder_heading] .>= (0.0:t) /\ i[intruder_heading] .<= (0.0:t)
     /\ i[speed] .>= (1000.0:t)
     /\ (700.0:t) .<= i[intruder_speed] .<= (800.0:t)
 
@@ -166,7 +206,14 @@ theory ACASXU
       has_length i 5 ->
       let j = denormalize_input i in
       valid_input j /\ directly_ahead j /\ moving_away j ->
-      not (advises_min_score nn i clear_of_conflict)
+      not (advises_min_score (nn @@ i) clear_of_conflict)
+
+  let runP4 (i: input) : output
+    requires { has_length i 5 }
+    requires { valid_input i /\ directly_ahead i /\ moving_away i }
+    ensures { not (advises_min_score result clear_of_conflict) } =
+      let j = normalize_input i in
+      nn @@ j
 
   (****************************************************************************)
   (* Property 5.
@@ -187,7 +234,14 @@ theory ACASXU
       has_length i 5 ->
       let j = denormalize_input i in
       valid_input j /\ near_and_approaching_from_left j ->
-      advises_min_score nn i strong_right
+      advises_min_score (nn @@ i) strong_right
+
+  let runP5 (i: input) : output
+    requires { has_length i 5 }
+    requires { valid_input i /\ near_and_approaching_from_left i }
+    ensures { advises_min_score result strong_right } =
+      let j = normalize_input i in
+      nn @@ j
 
   (****************************************************************************)
   (* Property 6.
@@ -209,7 +263,14 @@ theory ACASXU
       has_length i 5 ->
       let j = denormalize_input i in
       valid_input j /\ intruder_far_away j ->
-      advises_min_score nn i clear_of_conflict
+      advises_min_score (nn @@ i) clear_of_conflict
+
+  let runP6 (i: input) : output
+    requires { has_length i 5 }
+    requires { valid_input i /\ intruder_far_away i }
+    ensures { advises_min_score result clear_of_conflict } =
+      let j = normalize_input i in
+      nn @@ j
 
   (****************************************************************************)
   (* Property 7.
@@ -230,8 +291,15 @@ theory ACASXU
       has_length i 5 ->
       let j = denormalize_input i in
       valid_input j /\ large_vertical_separation j ->
-      not (advises_min_score nn i strong_left)
-      /\ not (advises_min_score nn i strong_right)
+      not (advises_min_score (nn @@ i) strong_left)
+      /\ not (advises_min_score (nn @@ i) strong_right)
+
+  let runP7 (i: input) : output
+    requires { has_length i 5 }
+    requires { valid_input i /\ large_vertical_separation i }
+    ensures { not (advises_min_score result strong_left) /\ not (advises_min_score result strong_right) } =
+      let j = normalize_input i in
+      nn @@ j
 
   (****************************************************************************)
   (* Property 8.
@@ -253,8 +321,15 @@ theory ACASXU
       has_length i 5 ->
       let j = denormalize_input i in
       valid_input j /\ large_vertical_separation_and_previous_weak_left j ->
-      (advises_min_score nn i weak_left)
-      \/ (advises_min_score nn i clear_of_conflict)
+      (advises_min_score (nn @@ i) weak_left)
+      \/ (advises_min_score (nn @@ i) clear_of_conflict)
+
+  let runP8 (i: input) : output
+    requires { has_length i 5 }
+    requires { valid_input i /\ large_vertical_separation_and_previous_weak_left i }
+    ensures { (advises_min_score result weak_left) \/ (advises_min_score result clear_of_conflict) } =
+      let j = normalize_input i in
+      nn @@ j
 
   (****************************************************************************)
   (* Property 9.
@@ -276,7 +351,14 @@ theory ACASXU
       has_length i 5 ->
       let j = denormalize_input i in
       valid_input j /\ previous_weak_right_and_nearby_intruder j ->
-      advises_min_score nn i strong_left
+      advises_min_score (nn @@ i) strong_left
+
+  let runP9 (i: input) : output
+    requires { has_length i 5 }
+    requires { valid_input i /\ previous_weak_right_and_nearby_intruder i }
+    ensures { (advises_min_score result strong_left) } =
+      let j = normalize_input i in
+      nn @@ j
 
   (****************************************************************************)
   (* Property 10.
@@ -296,6 +378,13 @@ theory ACASXU
       has_length i 5 ->
       let j = denormalize_input i in
       valid_input j /\ intruder_far_away_2 j ->
-      advises_min_score nn i clear_of_conflict
+      advises_min_score (nn @@ i) clear_of_conflict
+
+  let runP10 (i: input) : output
+    requires { has_length i 5 }
+    requires { valid_input i /\ intruder_far_away_2 i }
+    ensures { (advises_min_score result clear_of_conflict) } =
+      let j = normalize_input i in
+      nn @@ j
 
 end