From 777738d64d18e733e77119b615f166414196bb1c Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 11 Apr 2024 15:42:14 +0200
Subject: [PATCH] [examples] Use program syntax in ACAS Xu example
specification.
---
examples/acasxu/acasxu.why | 163 ++++++++++++++++++++++++++++---------
1 file changed, 126 insertions(+), 37 deletions(-)
diff --git a/examples/acasxu/acasxu.why b/examples/acasxu/acasxu.why
index d1e34e0..07fe0a7 100644
--- a/examples/acasxu/acasxu.why
+++ b/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
--
GitLab