From cc4df3ccd75f1102d58110e123fac0d10b0542b2 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 12 Apr 2023 14:16:21 +0200
Subject: [PATCH] [tests] Use /\ instead of -> the most in ACAS-Xu.
---
tests/interpretation_acasxu.t | 169 +++++++++++++++++-----------------
1 file changed, 83 insertions(+), 86 deletions(-)
diff --git a/tests/interpretation_acasxu.t b/tests/interpretation_acasxu.t
index 93fae2a..4d0b064 100644
--- a/tests/interpretation_acasxu.t
+++ b/tests/interpretation_acasxu.t
@@ -28,11 +28,11 @@ Test interpret on acasxu
> constant pi: t = 3.141592999999999857863031138549558818340301513671875
>
> predicate valid_input (i: input) =
- > (0.0:t) .<= i[distance_to_intruder] .<= (60760.0:t) ->
- > .- pi .<= i[angle_to_intruder] .<= pi ->
- > .- pi .<= i[intruder_heading] .<= pi ->
- > (100.0:t) .<= i[speed] .<= (1200.0:t) ->
- > (0.0:t) .<= i[intruder_speed] .<= (1200.0:t)
+ > (0.0:t) .<= i[distance_to_intruder] .<= (60760.0:t)
+ > /\ .- pi .<= i[angle_to_intruder] .<= pi
+ > /\ .- pi .<= i[intruder_heading] .<= pi
+ > /\ (100.0:t) .<= i[speed] .<= (1200.0:t)
+ > /\ (0.0:t) .<= i[intruder_speed] .<= (1200.0:t)
>
> predicate valid_action (a: action) = 0 <= a <= 4
>
@@ -42,9 +42,9 @@ Test interpret on acasxu
> valid_action b -> a <> b -> (c%%i)[a] .< (c%%i)[b]
>
> predicate intruder_distant_and_slow (i: input) =
- > i[distance_to_intruder] .>= (55947.6909999999988940544426441192626953125:t) ->
- > i[speed] .>= (1145.0:t) ->
- > i[intruder_speed] .<= (60.0:t)
+ > i[distance_to_intruder] .>= (55947.6909999999988940544426441192626953125:t)
+ > /\ i[speed] .>= (1145.0:t)
+ > /\ i[intruder_speed] .<= (60.0:t)
>
> function denormalize_t (i: t) (mean: t) (range: t) : t = (i .* range) .+ mean
>
@@ -66,63 +66,60 @@ Test interpret on acasxu
> forall i: input.
> has_length i 5 ->
> let j = denormalize_input i in
- > valid_input j ->
- > intruder_distant_and_slow j ->
+ > valid_input j /\ intruder_distant_and_slow j ->
> let o = (classifier%%i)[clear_of_conflict] in
> (denormalize_output o) .<= (1500.0:t)
>
> predicate directly_ahead (i: input) =
- > (1500.0:t) .<= i[distance_to_intruder] .<= (1800.0:t) ->
- > .- (0.059999999999999997779553950749686919152736663818359375:t) .<= i[angle_to_intruder] .<= (0.059999999999999997779553950749686919152736663818359375:t)
+ > (1500.0:t) .<= i[distance_to_intruder] .<= (1800.0:t)
+ > /\ .- (0.059999999999999997779553950749686919152736663818359375:t) .<= i[angle_to_intruder] .<= (0.059999999999999997779553950749686919152736663818359375:t)
>
> predicate moving_towards (i: input) =
- > i[intruder_heading] .>= (3.100000000000000088817841970012523233890533447265625:t) ->
- > i[speed] .>= (900.0:t) ->
- > i[intruder_speed] .>= (960.0:t)
+ > i[intruder_heading] .>= (3.100000000000000088817841970012523233890533447265625:t)
+ > /\ i[speed] .>= (900.0:t)
+ > /\ i[intruder_speed] .>= (960.0:t)
>
> goal P2:
> forall i: input.
> has_length i 5 ->
> let j = denormalize_input i in
- > valid_input j ->
- > directly_ahead j ->
- > moving_towards j ->
+ > valid_input j /\ directly_ahead j /\ moving_towards j ->
> not (advises classifier i clear_of_conflict)
> end
> EOF
P1 : forall caisar_v:t, caisar_v1:t, caisar_v2:t, caisar_v3:t, caisar_v4:t.
- (le (0.0:t) (add RNE (mul RNE caisar_v (60261.0:t)) (19791.0:t)) /\
- le (add RNE (mul RNE caisar_v (60261.0:t)) (19791.0:t)) (60760.0:t) ->
- le (neg (3.141592999999999857863031138549558818340301513671875:t))
- (add RNE
- (mul RNE caisar_v1
- (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t)) /\
- le
- (add RNE
- (mul RNE caisar_v1
- (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t))
- (3.141592999999999857863031138549558818340301513671875:t) ->
- le (neg (3.141592999999999857863031138549558818340301513671875:t))
- (add RNE
- (mul RNE caisar_v2
- (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t)) /\
- le
- (add RNE
- (mul RNE caisar_v2
- (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t))
- (3.141592999999999857863031138549558818340301513671875:t) ->
- le (100.0:t) (add RNE (mul RNE caisar_v3 (1100.0:t)) (650.0:t)) /\
- le (add RNE (mul RNE caisar_v3 (1100.0:t)) (650.0:t)) (1200.0:t) ->
+ ((le (0.0:t) (add RNE (mul RNE caisar_v (60261.0:t)) (19791.0:t)) /\
+ le (add RNE (mul RNE caisar_v (60261.0:t)) (19791.0:t)) (60760.0:t)) /\
+ (le (neg (3.141592999999999857863031138549558818340301513671875:t))
+ (add RNE
+ (mul RNE caisar_v1
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (0.0:t)) /\
+ le
+ (add RNE
+ (mul RNE caisar_v1
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (0.0:t))
+ (3.141592999999999857863031138549558818340301513671875:t)) /\
+ (le (neg (3.141592999999999857863031138549558818340301513671875:t))
+ (add RNE
+ (mul RNE caisar_v2
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (0.0:t)) /\
+ le
+ (add RNE
+ (mul RNE caisar_v2
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (0.0:t))
+ (3.141592999999999857863031138549558818340301513671875:t)) /\
+ (le (100.0:t) (add RNE (mul RNE caisar_v3 (1100.0:t)) (650.0:t)) /\
+ le (add RNE (mul RNE caisar_v3 (1100.0:t)) (650.0:t)) (1200.0:t)) /\
le (0.0:t) (add RNE (mul RNE caisar_v4 (1200.0:t)) (600.0:t)) /\
- le (add RNE (mul RNE caisar_v4 (1200.0:t)) (600.0:t)) (1200.0:t)) ->
- (le (55947.6909999999988940544426441192626953125:t)
- (add RNE (mul RNE caisar_v (60261.0:t)) (19791.0:t)) ->
- le (1145.0:t) (add RNE (mul RNE caisar_v3 (1100.0:t)) (650.0:t)) ->
- le (add RNE (mul RNE caisar_v4 (1200.0:t)) (600.0:t)) (60.0:t)) ->
+ le (add RNE (mul RNE caisar_v4 (1200.0:t)) (600.0:t)) (1200.0:t)) /\
+ le (55947.6909999999988940544426441192626953125:t)
+ (add RNE (mul RNE caisar_v (60261.0:t)) (19791.0:t)) /\
+ le (1145.0:t) (add RNE (mul RNE caisar_v3 (1100.0:t)) (650.0:t)) /\
+ le (add RNE (mul RNE caisar_v4 (1200.0:t)) (600.0:t)) (60.0:t) ->
le
(add RNE
(mul RNE
@@ -140,36 +137,36 @@ Test interpret on acasxu
vector,
(Interpretation.Vector 5)
P2 : forall caisar_v:t, caisar_v1:t, caisar_v2:t, caisar_v3:t, caisar_v4:t.
- (le (0.0:t) (add RNE (mul RNE caisar_v (60261.0:t)) (19791.0:t)) /\
- le (add RNE (mul RNE caisar_v (60261.0:t)) (19791.0:t)) (60760.0:t) ->
- le (neg (3.141592999999999857863031138549558818340301513671875:t))
- (add RNE
- (mul RNE caisar_v1
- (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t)) /\
- le
- (add RNE
- (mul RNE caisar_v1
- (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t))
- (3.141592999999999857863031138549558818340301513671875:t) ->
- le (neg (3.141592999999999857863031138549558818340301513671875:t))
- (add RNE
- (mul RNE caisar_v2
- (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t)) /\
- le
- (add RNE
- (mul RNE caisar_v2
- (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t))
- (3.141592999999999857863031138549558818340301513671875:t) ->
- le (100.0:t) (add RNE (mul RNE caisar_v3 (1100.0:t)) (650.0:t)) /\
- le (add RNE (mul RNE caisar_v3 (1100.0:t)) (650.0:t)) (1200.0:t) ->
+ ((le (0.0:t) (add RNE (mul RNE caisar_v (60261.0:t)) (19791.0:t)) /\
+ le (add RNE (mul RNE caisar_v (60261.0:t)) (19791.0:t)) (60760.0:t)) /\
+ (le (neg (3.141592999999999857863031138549558818340301513671875:t))
+ (add RNE
+ (mul RNE caisar_v1
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (0.0:t)) /\
+ le
+ (add RNE
+ (mul RNE caisar_v1
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (0.0:t))
+ (3.141592999999999857863031138549558818340301513671875:t)) /\
+ (le (neg (3.141592999999999857863031138549558818340301513671875:t))
+ (add RNE
+ (mul RNE caisar_v2
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (0.0:t)) /\
+ le
+ (add RNE
+ (mul RNE caisar_v2
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (0.0:t))
+ (3.141592999999999857863031138549558818340301513671875:t)) /\
+ (le (100.0:t) (add RNE (mul RNE caisar_v3 (1100.0:t)) (650.0:t)) /\
+ le (add RNE (mul RNE caisar_v3 (1100.0:t)) (650.0:t)) (1200.0:t)) /\
le (0.0:t) (add RNE (mul RNE caisar_v4 (1200.0:t)) (600.0:t)) /\
- le (add RNE (mul RNE caisar_v4 (1200.0:t)) (600.0:t)) (1200.0:t)) ->
- (le (1500.0:t) (add RNE (mul RNE caisar_v (60261.0:t)) (19791.0:t)) /\
- le (add RNE (mul RNE caisar_v (60261.0:t)) (19791.0:t)) (1800.0:t) ->
+ le (add RNE (mul RNE caisar_v4 (1200.0:t)) (600.0:t)) (1200.0:t)) /\
+ ((le (1500.0:t) (add RNE (mul RNE caisar_v (60261.0:t)) (19791.0:t)) /\
+ le (add RNE (mul RNE caisar_v (60261.0:t)) (19791.0:t)) (1800.0:t)) /\
le (neg (0.059999999999999997779553950749686919152736663818359375:t))
(add RNE
(mul RNE caisar_v1
@@ -180,14 +177,14 @@ Test interpret on acasxu
(mul RNE caisar_v1
(6.2831853071800001231395071954466402530670166015625:t))
(0.0:t))
- (0.059999999999999997779553950749686919152736663818359375:t)) ->
- (le (3.100000000000000088817841970012523233890533447265625:t)
- (add RNE
- (mul RNE caisar_v2
- (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t)) ->
- le (900.0:t) (add RNE (mul RNE caisar_v3 (1100.0:t)) (650.0:t)) ->
- le (960.0:t) (add RNE (mul RNE caisar_v4 (1200.0:t)) (600.0:t))) ->
+ (0.059999999999999997779553950749686919152736663818359375:t)) /\
+ le (3.100000000000000088817841970012523233890533447265625:t)
+ (add RNE
+ (mul RNE caisar_v2
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (0.0:t)) /\
+ le (900.0:t) (add RNE (mul RNE caisar_v3 (1100.0:t)) (650.0:t)) /\
+ le (960.0:t) (add RNE (mul RNE caisar_v4 (1200.0:t)) (600.0:t)) ->
not (((lt
(nnet_classifier
%% vector caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
--
GitLab