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

[doc] Remove unnecessary command-line options in example commands.

parent f7cd2f53
No related branches found
No related tags found
No related merge requests found
......@@ -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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment