# ---
# jupyter:
#   jupytext:
#     text_representation:
#       extension: .jl
#       format_name: light
#       format_version: '1.5'
#       jupytext_version: 1.14.4
#   kernelspec:
#     display_name: Julia 1.0.2
#     language: julia
#     name: julia-1.0
# ---

# # ACAS Xu Network Verification

# A lot of effort has been put into using DNNs as controllers for safety-critical systems such as autonomous vehicles. In this notebook we will use NeuralVerification.jl to verify one of the properties of the ACAS Xu networks ["Deep neural network compression for aircraft collision avoidance systems," <NAME>, <NAME> (Joournal of Guidane, Control and Dynamics, 2019](https://arc.aiaa.org/doi/10.2514/1.G003724). This network was trained to approximate the tabular representation of the ACAS Xu controller aiming to improve storage effiency.

#  However, it is widely known that networks can have significantly different outputs for small perturbations in their inputs. This unexpected behavior of DNNs is likely to result in unsafe systems.

# <img src="img/verification_fig.png" alt="Drawing" style="width: 60%;"/>

# In ["Reluplex: An Efficient SMT Solver for Verifying Deep Neural Network" <NAME>, <NAME>, <NAME>, <NAME>, and <NAME> (International Conference on Computer Aided Verification, 2017](https://arxiv.org/abs/1903.06758) multiple properties were introduced and have since been used as a benchmark for other algorithms implemented in NeuralVerification.jl. In this notebook we will verify Property 10 (or a subset of it for time's sake)

# ## ACAS Xu Network

# The ACAS Xu network works as a value function in the context of Markov Decision Processes. It maps input variables, corresponding to the state of the system, to action advisories by assigning a score to each of the possible actions. The action corresponding to the lowest score is the best action to take. The input is composed of seven dimensions, 5 of which are described in the image below.

# <img src="img/acas_geometry.png" alt="Drawing" style="width: 30%;"/>

# 1. $\rho$ - Distance from ownship ti intruder
# 2. $\theta$ - Angle to intruder relative to ownship heading direction
# 3. $\psi$ - Heading angle of intruder relative to ownship heading direction
# 4. $v_{own}$ - Speed of ownship
# 5. $v_{int}$ - Speed of intruder
# 6. $\tau$ - Time until loss of vertical separation
# 7. $a_{prev}$ - Previous advisory

# There are five outputs which represent the different advisories that can be produced by the ACAS Xu system:
#
# 1. Clear-of-Conflict
# 2. weak right
# 3. strong right
# 4. weak left
# 5. strong left
#
# To facilitate the training of the networks an array of 45 DNNs was produced by discretizing $\tau$ and $a_{prev}$ and generating one network for each discretized combination. Each of thse networks has 5 inputs and 5 outputs. The DNNs are fully connected, use ReLU activation functions and have 6 hidden layers with a total of 300 ReLU nodes.

# ## Property 10

# This property encodes that for a far away introduer the network should advise Clear-of-Conflict. The input set corresponds to:
#
# $36000 \leq \rho \leq 60760$
#
# $.7 \leq \theta \leq 3.141592$
#
# $-3.141592 \leq \psi \leq -3.141592 + 0.01$
#
# $900 \leq v_{own} \leq 1200$
#
# $600 \leq v_{int} \leq 1200$
#
# And the output set encodes that $y_1 \leq y_i \forall i \in \{2,3,4,5\}$ because we cannot encode conjunction as a set of linear constraints this property is broken than into 4 subproperties corresponding to comparing $y_1$ to each of the other different output scores.
#
# Property 10 can be visualized in the plot below, where $\psi, v_{own}$ and $v_{int}$ have been fixed and the policy has been evaluated in the networks that corresponds to $\tau = 4$ and $a_{prev} = 5$.

# <img src="img/property10.png" alt="Drawing" style="width: 80%;"/>

# In this plot the ownship is in the center heading to the right and each point in the plot corresponds to different locations of the intruder. The heading of the intruder is fixed. The light green color corresponds to Clear-of-Conflict and the dark green to another advisory. The region with the red border corresponds to the positions of the ownship in this slice of Property 10 for which the advisory should output Clear-of-Conflict. The sample based approach used to generate the plot shows that the Property apparently holds but we will now formally verify it using NeuralVerification.jl

# ## Verification using NeuralVerification.jl

using NeuralVerification, LazySets, Test, LinearAlgebra, GLPKMathProgInterface
import NeuralVerification: ReLU, Id

# ### load the network from an .nnet file

acas_file = "$(@__DIR__)/models/ACASXU_run2a_4_5_batch_2000.nnet"
acas_nnet = read_nnet(acas_file, last_layer_activation = Id());

# ### encode property 10

# Verifying the full property for this networks takes close to one hour so for the purposes of this tutorial we will inspect a subset of the input region. The original upper and lower bounds are provided in the commented lines below. Notice that the networks was trained using normalized inputs which explains why the input ranges do not map directly to those previously described for each dimension. For the technical details refer to [1](https://arc.aiaa.org/doi/10.2514/1.G003724).

# As mentioned earlier, this property is broken down into 4 subproperties that correspond to comparing the score of Clear-of-Conflict $y_1$ with each of the other scores $y_i$. In this example we only verify that $y_1 \leq y_5$.

# Feel free to play around with different upper and lower bounds within the original bounds to inspect different regions of the input space. Note that the runtime for the verification algorithm can vary significantly.

# +
# ACAS PROPERTY 10 - modified
# Original input range: 
# LOWER BOUND: array([[ 0.21466922,  0.11140846, -0.4999999 ,  0.3920202 ,  0.15      ]])
# UPPER BOUND: array([[ 0.58819589,  0.4999999 , -0.49840835,  0.66474747,  0.65      ]])

b_lower = [ 0.21466922,  0.11140846, -0.4999999 ,  0.3920202 ,  0.4      ]
#b_upper = [ 0.58819589,  0.4999999 , -0.49840835,  0.66474747,  0.4      ]
b_upper = [ 0.3,  0.2 , -0.49840835,  0.3920202,  0.4      ]

in_hyper  = Hyperrectangle(low = b_lower, high = b_upper)
inputSet = convert(HPolytope, in_hyper)

# output1 <= output 5
outputSet = HPolytope([HalfSpace([1.0, 0.0, 0.0, 0.0, -1.0], 0.0)])

problem_polytope_polytope_acas = Problem(acas_nnet, in_hyper, outputSet);
# -

# ### Finally, we pick Reluplex as the solver and time and verify the property.

solver=Reluplex()
println("$(typeof(solver)) - acas")
timed_result =@timed solve(solver, problem_polytope_polytope_acas)
println(" - Time: " * string(timed_result[2]) * " s")
println(" - Output: ")
println(timed_result[1])
println("")

# As expected, the property was shown to hold.

# # References 
# [1] ["Deep neural network compression for aircraft collision avoidance systems," <NAME>, <NAME> (Joournal of Guidane, Control and Dynamics, 2019](https://arc.aiaa.org/doi/10.2514/1.G003724)
#
# [2] ["Reluplex: An Efficient SMT Solver for Verifying Deep Neural Network" <NAME>, <NAME>, <NAME>, <NAME>, and <NAME> (International Conference on Computer Aided Verification, 2017](https://arxiv.org/abs/1903.06758)
#
# [3]

StarcoderdataJupyterScriptsDedupFiltered