[doc] Integrate changes to acas-xu and mnist.

doc/acas_xu.rst

@@ -18,7 +18,8 @@ The system considers a 2D plane with two entities: the monitored airplane (the
 "ownship") and an incoming airplane (the "intruder").
 
 .. image:: _static/media/acas_xu.png
-  :alt: A picture with two aircrafts seen from above
+  :alt: A schematic with two aircrafts, seen from above, displaying the relative
+   angles of their trajectories
 
 In the original implementation, the system state has seven inputs:
 
@@ -39,10 +40,10 @@ system can give:
 * :math:`WR`: Weak Right
 * :math:`SR`: Strong Right
 
-In the paper, the authors consider :math:`45` neural networks, for several
-values of :math:`\tau` and :math:`a_{prev}`, that operate on five inputs only
-while maintaining the same number of outputs. We will consider five-inputs
-networks in the future.
+In the original paper, the authors consider :math:`45` neural networks, for
+several values of :math:`\tau` and :math:`a_{prev}`, that operate on five inputs
+only while maintaining the same number of outputs. We will consider five-inputs
+networks in the remaining of this example.
 
 Properties
 ----------
@@ -112,16 +113,11 @@ basic programming data structures (arrays, queues, hash tables, *etc.*).
 Let us try to model the property :math:`\phi_1` defined earlier. We will call
 our theory ``ACASXU_P1``.
 
-.. code-block:: whyml
-
-   theory ACASXU_P1
-   end
-
 We will need to write down some numerical values. As of now, CAISAR allows
 writing values using floating-point arithmetic only. 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
+import the ``Float64`` sub-theory, that defines everything we need for 64-bit
 precision floating-point numbers. We thus import it in our theory using the
 ``use`` keyword.
 
@@ -136,10 +132,10 @@ Our file looks like this so far:
 We would like to verify our propety given a certain neural network. To do this,
 CAISAR extends the Why3 standard library for recognizing neural networks in ONNX
 and NNet formats. Given a file of such formats, CAISAR internally builds a
-theory named as the original neural network file, that contains the subtheories
+theory named as the original neural network file, that contains the sub-theories
 ``AsTuple`` and ``AsArray`` that provide logical symbols for describing the
 input-output interface of a neural network as tuples and array, respectively. We
-will only consider the ``AsTuple`` subtheory for this tutorial.
+will only consider the ``AsTuple`` sub-theory for this tutorial.
 
 In particular, the theory built by CAISAR is equivalent to the following WhyML
 file:
@@ -166,7 +162,7 @@ network.
 
 As our neural network takes five inputs and provides five outputs, adding ``use
 filename.AsTuple`` to our theory will provide a ``nn_apply`` function symbol
-that takes a 5-elements tuple as input, and provides a 5-elements tuple as
+that takes a five-elements tuple as input, and provides a five-elements tuple as
 output. Assuming we have a neural network named ``ACASXU_1_1.onnx``, the WhyML
 file looks like this:
 
@@ -248,6 +244,11 @@ Note that the previous commands set the verification time limit to 10 minutes
 file ``ACASXU_1_1.onnx`` that is used by the ``ACASXU_P1`` theory in
 ``property_1.why``.
 
+Under the hood, CAISAR first translates each goal into a compatible form for the
+targeted provers, then calls the provers on them, and finally interprets and
+post-processes the prover results for displaying them in a coherent form to the
+user.
+
 Marabou is not able to prove the property valid in the specified time limit,
 while nnenum does. In general, the result of a CAISAR verification is typically
 either ``Valid``, ``Invalid``, ``Unknown`` or ``Timeout``. CAISAR may output
@@ -278,7 +279,7 @@ However, these two solutions are not advisable in terms of clarity and
 maintainability.
 
 Reassuringly enough, WhyML provides all necessary features to come up with a
-better solution. First, WhyML allows for naming used (sub)theories in order to
+better solution. First, WhyML allows for naming used (sub-)theories in order to
 distinguish identical logic symbols coming from different theories. This is
 critical for identifying the correct ``nn_apply`` symbols in the two
 verification goals we will define. Second, WhyML allows for the hypotheses on
@@ -342,6 +343,12 @@ We can then verify the resulting verification problem as before:
     [caisar] Goal P3_1_1: Valid
     [caisar] Goal P3_2_7: Valid
 
+It is interesting to remark that, since Marabou does not support disjunctive
+formulas, CAISAR first splits a disjunctive goal formula into conjunctive
+sub-goals, then calls Marabou on each sub-goals, and finally post-processes the
+sub-results to provide the final result corresponding to the original goal
+formula.
+
 
 .. [Manfredi2016] G. Manfredi and Y. Jestin, *An introduction to ACAS Xu and the
    challenges ahead*, 2016 IEEE/AIAA 35th Digital Avionics Systems Conference

doc/mnist.rst

@@ -101,7 +101,7 @@ corresponding classification label.
 
 In order to use the ``robust`` predicate in our WhyML specification, we need
 values of types ``model`` and ``dataset``. For the former, CAISAR makes
-available the constant ``model`` upon interpreting the ``AsArray`` subtheory
+available the constant ``model`` upon interpreting the ``AsArray`` sub-theory
 that is built by the extension of the Why3 standard library for recognizing
 neural network ONNX and NNet formats. For the latter, the CAISAR standard
 library provides the constant ``dataset`` in ``DataSetClassification`` that will