Skip to content
Snippets Groups Projects
Commit cc4df3cc authored by Michele Alberti's avatar Michele Alberti
Browse files

[tests] Use /\ instead of -> the most in ACAS-Xu.

parent 27a8f47e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
tests/interpretation_acasxu.t
+ 83
− 86
View file @ cc4df3cc
......@@ -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)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment