From 9dc59b4ff5bbcb1a4dce5f11342d3cdb1e845092 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 1 Dec 2022 10:14:19 +0100
Subject: [PATCH] [tests] Add test using Marabou on dataset.
---
tests/{pyrat_vnnlib.t => dataset.t} | 22 +++++++++++++++++++++-
1 file changed, 21 insertions(+), 1 deletion(-)
rename tests/{pyrat_vnnlib.t => dataset.t} (53%)
diff --git a/tests/pyrat_vnnlib.t b/tests/dataset.t
similarity index 53%
rename from tests/pyrat_vnnlib.t
rename to tests/dataset.t
index 2df0256..8253dc6 100644
--- a/tests/pyrat_vnnlib.t
+++ b/tests/dataset.t
@@ -4,11 +4,14 @@ Test verify
> 0,240,0,0,3,10
> EOF
- $ chmod u+x bin/pyrat.py
+ $ chmod u+x bin/pyrat.py bin/Marabou
$ bin/pyrat.py --version
PyRAT 1.1
+ $ bin/Marabou --version
+ 1.0.+
+
$ PATH=$(pwd)/bin:$PATH
$ caisar verify -L . --format whyml --prover=PyRAT --dataset-csv=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
@@ -27,3 +30,20 @@ Test verify
> EOF
[caisar] Goal G: Unknown ()
[caisar] Goal H: Unknown ()
+
+ $ caisar verify -L . --format whyml --prover=Marabou --dataset-csv=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
+ > theory T
+ > use TestNetwork.AsArray as TN
+ > use ieee_float.Float64
+ > use caisar.DataSetClassification
+ > use caisar.DataSetProps
+ >
+ > goal G: correct TN.model dataset
+ >
+ > goal H:
+ > let dataset = min_max_scale true (0.0:t) (1.0:t) dataset in
+ > robust TN.model dataset (0.0100000000000000002081668171172168513294309377670288085937500000:t)
+ > end
+ > EOF
+ [caisar] Goal G: Unknown ()
+ [caisar] Goal H: Unknown ()
--
GitLab