From 1f2c4fc1d780e2a4a068986f452351096843e5e0 Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Mon, 25 Mar 2024 19:09:46 +0100
Subject: [PATCH] Added constant instancitation in command line inside MNIST
example documentation
---
doc/mnist.rst | 10 ++++++++++
1 file changed, 10 insertions(+)
diff --git a/doc/mnist.rst b/doc/mnist.rst
index 1e7fd36..0b9b0b0 100644
--- a/doc/mnist.rst
+++ b/doc/mnist.rst
@@ -165,6 +165,16 @@ for which nnenum is sure that the model ``MNIST_256_2.onnx`` is not robust with
respect to :math:`1 \%` perturbation. At the moment, CAISAR is not able to tell
which are the images in the dataset that cause such result.
+For more flexibility, it is possible to define the concrete values from the
+command line. See the ``--define`` option. For instane, to verify the aforementioned `mnist.why
+<https://git.frama-c.com/pub/caisar/-/blob/master/examples/mnist/mnist.why>`_
+file, the command line is the following:
+
+.. code-block:: console
+
+ $ caisar verify -p nnenum --define model_filename:nets/MNIST_256_2.onnx --define dataset_filename:csv/mnist_test.csv examples/mnist/mnist.why
+ [caisar] Goal robustness: Invalid
+
.. [LiDeng2012] Li Deng, *The MNIST Database of Handwritten Digit Images for
Machine Learning Research*, IEEE Signal Process. Mag., 2012, pp.
--
GitLab