From 8d2fb49e0141846339f863d5763163dad0857a1f Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 15 Mar 2023 11:39:47 +0100
Subject: [PATCH] [tests] Add test case for interpretion on dataset.

---
 tests/interpretation_dataset.t | 49 ++++++++++++++++++++++++++++++++++
 1 file changed, 49 insertions(+)
 create mode 100644 tests/interpretation_dataset.t

diff --git a/tests/interpretation_dataset.t b/tests/interpretation_dataset.t
new file mode 100644
index 0000000..12ab389
--- /dev/null
+++ b/tests/interpretation_dataset.t
@@ -0,0 +1,49 @@
+Test interpret on mnist
+  $ cat - > dataset.csv << EOF
+  > 1,0.0,1.0,0.784313725,0.019607843,0.776470588
+  > 0,1.0,0.0,0.019607843,0.776470588,0.784313725
+  > EOF
+
+  $ caisar interpret -L . --format whyml - 2>&1 <<EOF | ./filter_tmpdir.sh
+  > theory T
+  >   use ieee_float.Float64
+  >   use bool.Bool
+  >   use int.Int
+  >   use Vector
+  >   use Tensor
+  >   use Classifier
+  >   use Dataset
+  >
+  >   type image = tensor t
+  >   type label_ = int
+  >
+  >   predicate valid_image (i: image) =
+  >     forall v: index. valid_index i v -> (0.0: t) .<= i#v .<= (1.0: t)
+  >
+  >   predicate valid_label (l: label_) = 0 <= l <= 1
+  >
+  >   predicate advises (c: classifier) (i: image) (l: label_) =
+  >     valid_label l ->
+  >     forall j: int. valid_label j /\  j <> l -> (c@@i)[l] .> (c@@i)[j]
+  >
+  >   predicate bounded_by_epsilon (i: image) (eps: t) =
+  >     forall v: index. valid_index i v -> .- eps .<= i#v .<= eps
+  >
+  >   predicate robust_around (c: classifier) (eps: t) (i: image) (l: label_) =
+  >     forall perturbed_image: image.
+  >       valid_image perturbed_image ->
+  >       equal_shape i perturbed_image ->
+  >       let p = perturbed_image - i in
+  >       bounded_by_epsilon p eps ->
+  >       advises c perturbed_image l
+  >
+  >   predicate robust (c: classifier) (d: dataset image label_) (eps: t) =
+  >     Dataset.L.forall_ d (robust_around c eps)
+  >
+  >   goal G:
+  >     let classifier = read_classifier "TestNetwork.nnet" NNet in
+  >     let dataset = read_dataset "dataset.csv" CSV in
+  >     let eps = (0.375:t) in
+  >     robust classifier dataset eps
+  > end
+  > EOF
-- 
GitLab