From 108933bc5afe243a1ed0799ac53d09fd0f418fd4 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Tue, 20 Jun 2023 12:19:23 +0200
Subject: [PATCH] [doc] Remove unnecessary command-line options in example
commands.
---
doc/acas_xu.rst | 13 +++++--------
1 file changed, 5 insertions(+), 8 deletions(-)
diff --git a/doc/acas_xu.rst b/doc/acas_xu.rst
index 469ad4d..2e4a586 100644
--- a/doc/acas_xu.rst
+++ b/doc/acas_xu.rst
@@ -247,19 +247,16 @@ verifying the ACAS-Xu property :math:`\phi_1`:
.. code-block:: console
- $ caisar verify --prover Marabou -L examples/acasxu/nets/onnx --format whyml examples/acasxu/property_1.why -t 10m
+ $ caisar verify --prover Marabou examples/acasxu/property_1.why -t 10m
[caisar] Goal P1_1_1: Timeout
.. code-block:: console
- $ caisar verify --prover nnenum -L examples/acasxu/nets/onnx --format whyml examples/acasxu/property_1.why -t 10m
+ $ caisar verify --prover nnenum examples/acasxu/property_1.why -t 10m
[caisar] Goal P1_1_1: Valid
Note that the previous commands set the verification time limit to 10 minutes
-(*cf.* ``-t`` option), and the additional location ``examples/acasxu/nets/onnx``
-(*cf.* ``-L`` option) for letting CAISAR correctly locate the neural network
-file ``ACASXU_1_1.onnx`` that is used by the ``ACASXU_P1`` theory in
-``property_1.why``.
+(*cf.* ``-t`` option).
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
@@ -340,13 +337,13 @@ We can then verify the resulting verification problem as before:
.. code-block:: console
- $ caisar verify --prover Marabou -L examples/acasxu/nets/onnx --format whyml examples/acasxu/property_3.why -t 10m
+ $ caisar verify --prover Marabou examples/acasxu/property_3.why -t 10m
[caisar] Goal P3_1_1: Timeout
[caisar] Goal P3_2_7: Valid
.. code-block:: console
- $ caisar verify --prover nnenum -L examples/acasxu/nets/onnx --format whyml examples/acasxu/property_3.why -t 10m
+ $ caisar verify --prover nnenum examples/acasxu/property_3.why -t 10m
[caisar] Goal P3_1_1: Valid
[caisar] Goal P3_2_7: Valid
--
GitLab