[doc] Added example for ACAS-Xu property 1.

doc/acas_xu.rst

+.. _acas_xu:
+
+ACAS-Xu
+*******
+
+ACAS-Xu stands for Aircraft Collision Avoidance System.
+Introduced for instance in [Manfredi2016]_, it is a
+specification of a program which aim to output signals for
+an aircraft in a situation where there is a potential for
+collision.
+In the rest of this tutorial, we will use the flavour
+ACAS-Xu defined in [Katz2017]_, where the authors aim to
+verify a neural network implementing part of the ACAS-Xu
+specification.
+Its low dimensionality and well defined semantics
+make it a *de facto* benchmark for machine learning
+verification.
+
+Use-case presentation
+=====================
+
+The system considers a 2D plane with two entities: the
+monitored plane (the "ownship") and an incoming plane (the "intruder").
+
+.. image:: _static/media/acas_xu.png
+  :alt: A picture with two aircrafts seen from above
+
+In the original implementation, the system state has seven
+inputs:
+
+* :math:`v_{own}`: speed of ownship
+* :math:`v_{int}`: speed of intruder
+* :math:`\rho`: distance from ownship to intruder
+* :math:`\theta`: angle to intruder relative to ownship heading direction
+* :math:`\psi`: heading angle of intruder relative to ownship heading direction
+* :math:`\tau`: time until vertical separation
+* :math:`a_{prev}`: previous advisory
+
+It has five outputs, that correspond to the different
+direction advisories the system can give:
+
+* :math:`COC`: Clear Of Conflict
+* :math:`WL`: Weak Left
+* :math:`SL`: Strong Left
+* :math:`WR`: Weak Right
+* :math:`SR`: Strong Right
+
+In the paper, the authors are producing multiple neural
+network that correspond to several values of :math:`\tau`
+and :math:`a_{prev}`, producing an array of 45 neural
+networks, with only five inputs (and the same number of
+outputs). We will consider five-inputs network in the
+future.
+
+Properties
+----------
+
+There are several functional properties one may want to verify on this system, for instance:
+
+* guarantee that the system will never output COC advisory when the intruder is nearby
+* guarantee that the system will never output an advisory that may result in a collision
+* guarantee that the system will not output a Strong advisory where a Weak variant would be enough
+
+Authors of [Katz2017]_ propose ten properties to verify. We
+will reproduce the first here, and try to check whether a
+given neural network respects it. 
+
+**property** 
+    :math:`\phi_1`
+
+**definition**
+    If the intruder is distant and is significantly slower than the ownship, the score of a COC advisory will always be below a certain fixed threshold.
+
+**input constraints**
+
+   * :math:`\rho` ≥ 55947.691
+   * :math:`v_{own}` ≥ 1145
+   * :math:`v_{int}` ≤ 60
+
+**desired output property**
+
+   * :math:`COC` ≤ 1500
+
+Modelling the problem using WhyML
+---------------------------------
+
+The first step for verifying anything with CAISAR is to
+write a WhyML file that describe the problem to solve.
+Inside this file, we will create a *theory*. A theory can be
+seen as a namespace inside CAISAR, inside which are defined logical terms,
+formulas and verification goals.
+
+Let us try to model the property :math:`\phi_1` defined
+earlier. We will call our theory `ACAS_XU_P1`.
+
+.. code-block:: ocaml
+
+   theory ACAS_XU_P1
+   end
+
+We will need to write down some numerical values. As of now,
+CAISAR support writting values using floating point arithmetic. 
+Why3 defines a float type and the relevant arithmetic
+operations according to the IEEE floating
+point standard in a theory, astutely called ``ieee_float``.
+Specifically, we will import the ``Float64`` subtheory, that
+defines everything we need for 64 bit precision floating
+point numbers.
+We thus import it in our theory using the ``use`` keyword.
+
+Our file looks like this so far:
+
+.. code-block:: ocaml
+
+   theory ACAS_XU_P1
+     use ieee_float.Float64
+   end
+
+We would like to verify our propety given a certain neural network.
+To do this, we can write the filename in our theory.
+Internally, when provided with a neural network file, CAISAR will perform some basic sanity checks (mainly, checks that the network is in a supported format).
+If those checks pass, then CAISAR will internally build a theory, named as the original neural network. This theory will contain two subtheories that provide
+logical symbols we can use in our theory: ``AsTuple`` and ``AsArray``.
+We will only consider the ``AsTuple`` subtheory for this tutorial.
+
+This theory is equivalent to the following WhyML file:
+
+.. code-block:: ocaml
+
+   theory Name_of_neural_network_file
+     theory AsTuple
+       type t
+       (* Tuple with as many elements as there are input *)
+       function nn_apply (t,_,...)
+       (* Tuple with as many elements as there are outputs *)
+         : (t,_,...)
+     end
+     (* Other stuff *)
+   end
+
+CAISAR defines the ``AsTuple`` theory, inside which there is a
+``nn_apply`` function symbol. The input of this function as a tuple with
+as many elements as there are inputs on the original neural network,
+and return a tuple with as many elements as there are outputs
+original neural network.
+
+As our neural network takes five inputs and five outputs, by
+adding ``use filename.AsTuple`` will provide a ``nn_apply``
+function symbol that takes a 5-elements tuple as input, and output
+a 5-element tuple. Supposing we have a neural network named
+*ACAS_XU_P1.nnet*, our file looks like this:
+
+.. code-block:: ocaml
+
+   theory ACAS_XU_P1
+     use ACASXU_1_1.AsTuple
+     use ieee_float.Float64
+   end
+
+Now is the time to define our verification goal ``G``.
+
+We first define constraints on our inputs, as defined in
+property :math:`\phi_1`. We define all floating points inputs
+:math:`x_i` for :math:`i \in (0..4)` that respect the
+properties defined in :math:`\phi_1` (in WhyML, ``->`` stands for
+the logical implication).
+
+.. code-block:: ocaml
+  
+  goal G: forall x0 x1 x2 x3 x4.
+     (0.5999999999999999777955395074968691915273666381835937500000000000:t) .<= x0 .<= (0.6798577687000000313588543576770462095737457275390625000000000000:t) ->
+     (-0.5:t) .<= x1 .<= (0.5:t) ->
+     (-0.5:t) .<= x2 .<= (0.5:t) ->
+     (0.4500000000000000111022302462515654042363166809082031250000000000:t) .<= x3 .<= (0.5:t) ->
+     (-0.5:t) .<= x4 .<= (-0.4500000000000000111022302462515654042363166809082031250000000000:t) ->
+
+Then, whe define the result of the application of ``net_apply`` on the inputs as the following, taking advantage of the pattern-matching of WhyML, and define
+the output constraint we want to enforce.
+
+.. code-block:: ocaml
+
+  let (y0, _, _, _, _) = nn_apply x0 x1 x2 x3 x4 in
+  y0 .< (3.9911256458999999630066213285317644476890563964843750000000000000:t)
+
+The final file looks like this:
+
+.. code-block:: ocaml
+
+  theory ACAS_XU_P1
+    use ACASXU_1_1.AsTuple
+    use ieee_float.Float64
+  
+    goal G: forall x0 x1 x2 x3 x4.
+       (0.5999999999999999777955395074968691915273666381835937500000000000:t) .<= x0 .<= (0.6798577687000000313588543576770462095737457275390625000000000000:t) ->
+       (-0.5:t) .<= x1 .<= (0.5:t) ->
+       (-0.5:t) .<= x2 .<= (0.5:t) ->
+       (0.4500000000000000111022302462515654042363166809082031250000000000:t) .<= x3 .<= (0.5:t) ->
+       (-0.5:t) .<= x4 .<= (-0.4500000000000000111022302462515654042363166809082031250000000000:t) ->
+       let (y0, _, _, _, _) = nn_apply x0 x1 x2 x3 x4 in
+       y0 .< (3.9911256458999999630066213285317644476890563964843750000000000000:t)
+  end
+
+This file is available as is, under the example folder of our repo: `property_1.why <https://git.frama-c.com/pub/caisar/-/blob/master/examples/acasxu/property_1.why>`_.
+A neural network in NNet format that should respect this
+property is available here: `ACASXU_1_1.nnet <https://git.frama-c.com/pub/caisar/-/blob/master/examples/acasxu/nets/https://git.frama-c.com/pub/caisar/-/blob/master/examples/acasxu/nets/ACASXU_1_1.nnet>`_ (from the Marabou repository).
+
+
+Checking the property with CAISAR
+---------------------------------
+
+Assuming the chosen prover is on your path and you are in
+CAISAR's root, you may launch caisar using the following command line:
+
+
+.. code-block:: bash
+
+    caisar verify --prover Marabou -L examples/acasxu/nets/ --format whyml examples/acasxu/property_1.why -vv -t 10m
+
+Take note that this may take some time, depending to your
+machine.
+
+CAISAR will return you either ``Valid``, ``Invalid`` or
+``Timeout``
+
+
+
+References
+----------
+
+
+.. [Manfredi2016] G. Manfredi and Y. Jestin, "An introduction
+   to ACAS Xu and the challenges ahead," 2016 IEEE/AIAA
+   35th Digital Avionics Systems Conference (DASC),
+   2016, pp. 1-9, doi: 10.1109/DASC.2016.7778055.
+
+.. [Katz2017] Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J. (2017). Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In: Majumdar, R., Kunčak, V. (eds) Computer Aided Verification. CAV 2017. Lecture Notes in Computer Science(), vol 10426. Springer, Cham. https://doi.org/10.1007/978-3-319-63387-9_5

doc/conf.py

@@ -49,4 +49,4 @@ html_theme = 'alabaster'
 # Add any paths that contain custom static files (such as style sheets) here,
 # relative to this directory. They are copied after the builtin static files,
 # so a file named "default.css" will overwrite the builtin "default.css".
-html_static_path = ['_static']
\ No newline at end of file
+html_static_path = ['_static']

doc/contents.rst

-Table of content
-================
-
-.. toctree::
-   :maxdepth: 2
-   :caption: Contents:
-
-   installation
-   usage
-   modules

doc/examples.rst

+.. _examples:
+
+Examples
+========
+
+This page regroups some examples use cases for CAISAR. All
+examples will describe the use case, the formalization using
+WhyML, and the CAISAR execution.
+
+.. toctree::
+   :maxdepth: 2
+   :caption: Examples:
+
+   acas_xu

doc/index.rst

@@ -26,6 +26,7 @@ Content
 
    installation
    usage
+   examples
    modules