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 2df025660ab2b6ba2895d75c8ad515d145bd2ae5..8253dc6a32e228f035ebaea00fde0a0bd593fdd1 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 ()