From 018f47795dbefa2ac262297879bbb324194273f7 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 22 Sep 2023 10:02:50 +0200
Subject: [PATCH] [tests] Rename script to setup the testing env.
---
tests/aimos.t | 4 +---
tests/autodetect.t | 26 ++++++++++++++++++++++++--
tests/cvc5.t | 4 +---
tests/dataset.t | 4 +---
tests/define.t | 5 +----
tests/dune | 2 +-
tests/interpretation_acasxu.t | 5 +----
tests/interpretation_dataset.t | 4 +---
tests/marabou.t | 4 +---
tests/pyrat.t | 4 +---
tests/pyrat_onnx.t | 4 +---
tests/saver.t | 4 +---
tests/{master.sh => setup_env.sh} | 0
tests/verify_json.t | 4 +---
tests/xgboost.t | 2 +-
15 files changed, 37 insertions(+), 39 deletions(-)
rename tests/{master.sh => setup_env.sh} (100%)
diff --git a/tests/aimos.t b/tests/aimos.t
index 245ba43..0e37f12 100644
--- a/tests/aimos.t
+++ b/tests/aimos.t
@@ -5,13 +5,11 @@ Test verify
> 2.500000000000000000e+02,2.222222222222222376e-01,-3.138814875812015348e+00,2.333333333333333428e+02,0.000000000000000000e+00
> EOF
- $ chmod u+x bin/aimos
+ $ . ./setup_env.sh
$ bin/aimos --version
AIMOS 1.0
- $ . ./master.sh
-
$ caisar verify -L . --format whyml --prover=AIMOS --dataset=test_data.csv - 2>&1 <<EOF
> theory ACASXU_P5
> use TestNetwork.AsArray
diff --git a/tests/autodetect.t b/tests/autodetect.t
index f666828..ef82fd1 100644
--- a/tests/autodetect.t
+++ b/tests/autodetect.t
@@ -4,7 +4,7 @@ Test autodetect
> echo "2.4.0"
> EOF
- $ . ./master.sh
+ $ . ./setup_env.sh
$ bin/alt-ergo
2.4.0
@@ -30,7 +30,29 @@ Test autodetect
$ bin/abcrown.sh --version
dummy-version
- $ caisar config -d -v 2>&1 | ./filter_tmpdir.sh
+ $ caisar config -d --ltag=Autodetect -v 2>&1 | ./filter_tmpdir.sh
+ <autodetect>Run: ($TESTCASE_ROOT/bin/nnenum.sh --version) > $TMPFILE 2>&1
+ <autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1
+ <autodetect>Run: ($TESTCASE_ROOT/bin/saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
+ <autodetect>Run: ($TESTCASE_ROOT/bin/aimos --version) > $TMPFILE 2>&1
+ <autodetect>Run: ($TESTCASE_ROOT/bin/abcrown.sh --version) > $TMPFILE 2>&1
+ <autodetect>Run: ($TESTCASE_ROOT/bin/alt-ergo --version) > $TMPFILE 2>&1
+ <autodetect>Run: ($TESTCASE_ROOT/bin/Marabou --version) > $TMPFILE 2>&1
+ <autodetect>Run: ($TESTCASE_ROOT/bin/cvc5 --version) > $TMPFILE 2>&1
+ <autodetect>0 prover(s) added
+ <autodetect>Generating strategies:
+ <autodetect>Found prover Alt-Ergo version 2.4.0, OK.
+ <autodetect>Found prover CVC5 version 1.0.2, OK.
+ <autodetect>Found prover Marabou version 1.0.+, OK.
+ <autodetect>Found prover PyRAT version 1.1, OK.
+ <autodetect>Found prover PyRAT version 1.1 (alternative: VNNLIB)
+ <autodetect>Found prover PyRAT version 1.1 (alternative: ACAS)
+ <autodetect>Found prover nnenum version dummy-version, OK.
+ <autodetect>Found prover alpha-beta-CROWN version dummy-version, OK.
+ <autodetect>Found prover alpha-beta-CROWN version dummy-version (alternative: ACAS)
+ <autodetect>Found prover SAVer version v1.0, OK.
+ <autodetect>Found prover AIMOS version 1.0, OK.
+ <autodetect>11 prover(s) added
AIMOS 1.0
Alt-Ergo 2.4.0
CVC5 1.0.2
diff --git a/tests/cvc5.t b/tests/cvc5.t
index 22ecd80..cc1a1cd 100644
--- a/tests/cvc5.t
+++ b/tests/cvc5.t
@@ -1,11 +1,9 @@
Test verify
- $ chmod u+x bin/cvc5
+ $ . ./setup_env.sh
$ bin/cvc5 --version
This is cvc5 version 1.0.2 [git tag 1.0.2 branch HEAD]
- $ . ./master.sh
-
$ caisar verify -L . --format whyml --prover=CVC5 --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory CVC5
> use TestNetworkONNX.AsTuple as TN
diff --git a/tests/dataset.t b/tests/dataset.t
index 69b782a..3476ac3 100644
--- a/tests/dataset.t
+++ b/tests/dataset.t
@@ -4,7 +4,7 @@ Test verify on dataset
> 0,0.941176471,0,0,0.011764706,0.039215686
> EOF
- $ chmod u+x bin/pyrat.py bin/Marabou
+ $ . ./setup_env.sh
$ bin/pyrat.py --version
PyRAT 1.1
@@ -12,8 +12,6 @@ Test verify on dataset
$ bin/Marabou --version
1.0.+
- $ . ./master.sh
-
$ caisar verify -L . --format whyml --ltag=ProverSpec --prover=PyRAT --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
> use TestNetwork.AsArray as TN
diff --git a/tests/define.t b/tests/define.t
index 25fcf7f..058ca5b 100644
--- a/tests/define.t
+++ b/tests/define.t
@@ -1,12 +1,9 @@
Test interpretation of on-the-fly definition of toplevel constants
-
- $ chmod u+x bin/pyrat.py
+ $ . ./setup_env.sh
$ bin/pyrat.py --version
PyRAT 1.1
- $ . ./master.sh
-
$ cat > file.mlw <<EOF
> theory T
> use int.Int
diff --git a/tests/dune b/tests/dune
index 25a3d7d..e2e8736 100644
--- a/tests/dune
+++ b/tests/dune
@@ -1,7 +1,7 @@
(cram
(deps
(package caisar)
- master.sh
+ setup_env.sh
TestNetwork.nnet
TestNetworkONNX.onnx
TestSVM.ovo
diff --git a/tests/interpretation_acasxu.t b/tests/interpretation_acasxu.t
index 7520af9..2e04d6c 100644
--- a/tests/interpretation_acasxu.t
+++ b/tests/interpretation_acasxu.t
@@ -1,12 +1,9 @@
Test interpret on acasxu
-
- $ chmod u+x bin/pyrat.py
+ $ . ./setup_env.sh
$ bin/pyrat.py --version
PyRAT 1.1
- $ . ./master.sh
-
$ caisar verify --format whyml --prover PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
> use ieee_float.Float64
diff --git a/tests/interpretation_dataset.t b/tests/interpretation_dataset.t
index 42bf51e..2c140ad 100644
--- a/tests/interpretation_dataset.t
+++ b/tests/interpretation_dataset.t
@@ -4,13 +4,11 @@ Test interpret on dataset
> 0,1.0,0.0,0.019607843,0.776470588,0.784313725
> EOF
- $ chmod u+x bin/Marabou
+ $ . ./setup_env.sh
$ bin/Marabou --version
1.0.+
- $ . ./master.sh
-
$ caisar verify --format whyml --prover Marabou --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
> use ieee_float.Float64
diff --git a/tests/marabou.t b/tests/marabou.t
index 122a56d..e79433a 100644
--- a/tests/marabou.t
+++ b/tests/marabou.t
@@ -1,11 +1,9 @@
Test verify
- $ chmod u+x bin/Marabou
+ $ . ./setup_env.sh
$ bin/Marabou --version
1.0.+
- $ . ./master.sh
-
$ caisar verify --format whyml --prover=Marabou --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
> use ieee_float.Float64
diff --git a/tests/pyrat.t b/tests/pyrat.t
index b70860c..85acd38 100644
--- a/tests/pyrat.t
+++ b/tests/pyrat.t
@@ -1,11 +1,9 @@
Test verify
- $ chmod u+x bin/pyrat.py
+ $ . ./setup_env.sh
$ bin/pyrat.py --version
PyRAT 1.1
- $ . ./master.sh
-
$ caisar verify --format whyml --prover=PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory PyRAT
> use TestNetwork.AsTuple
diff --git a/tests/pyrat_onnx.t b/tests/pyrat_onnx.t
index 465ba63..5d2be1d 100644
--- a/tests/pyrat_onnx.t
+++ b/tests/pyrat_onnx.t
@@ -1,11 +1,9 @@
Test verify
- $ chmod u+x bin/pyrat.py
+ $ . ./setup_env.sh
$ bin/pyrat.py --version
PyRAT 1.1
- $ . ./master.sh
-
$ caisar verify --format whyml --prover=PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory PyRAT_ONNX
> use ieee_float.Float64
diff --git a/tests/saver.t b/tests/saver.t
index 5b21fb0..4fccd53 100644
--- a/tests/saver.t
+++ b/tests/saver.t
@@ -4,13 +4,11 @@ Test verify
> 1,0.5,0.5,0.0,
> EOF
- $ chmod u+x bin/saver
+ $ . ./setup_env.sh
$ bin/saver --version
v1.0
- $ . ./master.sh
-
$ caisar verify -L . --format whyml --prover=SAVer --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
> use TestSVM.AsArray
diff --git a/tests/master.sh b/tests/setup_env.sh
similarity index 100%
rename from tests/master.sh
rename to tests/setup_env.sh
diff --git a/tests/verify_json.t b/tests/verify_json.t
index ccad950..c3990cf 100644
--- a/tests/verify_json.t
+++ b/tests/verify_json.t
@@ -7,13 +7,11 @@ Test verify-json
> {"id":"foo","prover":["PyRAT"],"model":"TestNetwork.nnet","property":{"dataset":"test_data.csv","kind":["Robust",0.3]},"time_limit":null,"memory_limit":null,"output_file":null}
> EOF
- $ chmod u+x bin/pyrat.py
+ $ . ./setup_env.sh
$ bin/pyrat.py --version
PyRAT 1.1
- $ . ./master.sh
-
$ caisar verify-json --ltag=ProverSpec config.json 2>&1 | ./filter_tmpdir.sh
[DEBUG]{ProverSpec} Prover-tailored specification:
;;; produced by PyRAT/VNN-LIB driver
diff --git a/tests/xgboost.t b/tests/xgboost.t
index c0366e0..4c73ef7 100644
--- a/tests/xgboost.t
+++ b/tests/xgboost.t
@@ -1,5 +1,5 @@
Test verify
- $ . ./master.sh
+ $ . ./setup_env.sh
$ caisar verify-xgboost ../lib/xgboost/example/california.json ../lib/xgboost/example/california.csv --prover CVC5 2>&1 | ./filter_tmpdir.sh
result: Unknown
--
GitLab