From 04fac60cfcfa1486240efb6a360c5a1c7adc8300 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Tue, 31 Jan 2023 12:53:17 +0100
Subject: [PATCH] [aimos] Add test case.
---
tests/aimos.t | 25 +++++++++++++++++++++++++
tests/autodetect.t | 12 +++++++++---
tests/bin/aimos | 12 ++++++++++++
tests/dune | 1 +
4 files changed, 47 insertions(+), 3 deletions(-)
create mode 100644 tests/aimos.t
create mode 100644 tests/bin/aimos
diff --git a/tests/aimos.t b/tests/aimos.t
new file mode 100644
index 0000000..db58028
--- /dev/null
+++ b/tests/aimos.t
@@ -0,0 +1,25 @@
+Test verify
+ $ cat - > test_data.csv << EOF
+ > 4.000000000000000000e+02,4.000000000000000222e-01,-3.139370431367570990e+00,2.333333333333333428e+02,0.000000000000000000e+00
+ > 2.500000000000000000e+02,2.000000000000000111e-01,-3.138814875812015348e+00,2.333333333333333428e+02,0.000000000000000000e+00
+ > 2.500000000000000000e+02,2.222222222222222376e-01,-3.138814875812015348e+00,2.333333333333333428e+02,0.000000000000000000e+00
+ > EOF
+
+ $ chmod u+x bin/aimos
+
+ $ bin/aimos --version
+ AIMOS 1.0
+
+ $ PATH=$(pwd)/bin:$PATH
+
+ $ caisar verify -L . --format whyml --prover=AIMOS --dataset=test_data.csv - 2>&1 <<EOF
+ > theory ACASXU_P5
+ > use TestNetwork.AsArray
+ > use ieee_float.Float64
+ > use caisar.DatasetClassification
+ > use caisar.DatasetClassificationProps
+ >
+ > goal G: meta_robust model dataset (1.0:t)
+ > end
+ > EOF
+ [caisar] Goal G: Valid
diff --git a/tests/autodetect.t b/tests/autodetect.t
index 36d66f1..702408e 100644
--- a/tests/autodetect.t
+++ b/tests/autodetect.t
@@ -4,7 +4,7 @@ Test autodetect
> echo "2.4.0"
> EOF
- $ chmod u+x bin/alt-ergo bin/pyrat.py bin/Marabou bin/saver bin/cvc5 bin/nnenum.sh
+ $ chmod u+x bin/alt-ergo bin/pyrat.py bin/Marabou bin/saver bin/aimos bin/cvc5 bin/nnenum.sh
$ bin/alt-ergo
2.4.0
@@ -18,6 +18,9 @@ Test autodetect
$ bin/saver --version
v1.0
+ $ bin/aimos --version
+ AIMOS 1.0
+
$ bin/cvc5 --version
This is cvc5 version 1.0.2 [git tag 1.0.2 branch HEAD]
@@ -31,6 +34,7 @@ Test autodetect
[caisar][DEBUG] Automatic detection
<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/alt-ergo --version) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/Marabou --version) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/nnenum.sh --version) > $TMPFILE 2>&1
@@ -45,8 +49,10 @@ Test autodetect
<autodetect>Found prover PyRAT version 1.1 (alternative: ACAS)
<autodetect>Found prover nnenum version dummy, OK.
<autodetect>Found prover SAVer version v1.0, OK.
- <autodetect>8 prover(s) added
- [caisar] Alt-Ergo 2.4.0
+ <autodetect>Found prover AIMOS version 1.0, OK.
+ <autodetect>9 prover(s) added
+ [caisar] AIMOS 1.0
+ Alt-Ergo 2.4.0
CVC5 1.0.2
Marabou 1.0.+
PyRAT 1.1
diff --git a/tests/bin/aimos b/tests/bin/aimos
new file mode 100644
index 0000000..a2ef03a
--- /dev/null
+++ b/tests/bin/aimos
@@ -0,0 +1,12 @@
+#!/bin/sh
+
+
+case $1 in
+ --version)
+ echo "AIMOS 1.0"
+ ;;
+ *)
+ echo "Goal:"
+ cat $2
+ echo "ACASXU_1_1.nnet, reluplex_rotation, 1.0"
+esac
diff --git a/tests/dune b/tests/dune
index d9400d2..26d2955 100644
--- a/tests/dune
+++ b/tests/dune
@@ -7,6 +7,7 @@
bin/pyrat.py
bin/Marabou
bin/saver
+ bin/aimos
bin/cvc5
bin/nnenum.sh
filter_tmpdir.sh)
--
GitLab