-
Aymeric Varasse authoredAymeric Varasse authored
aimos.t 933 B
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) ("reluplex_rotation":string) (0:int) (0:int) (0:int)
> end
> EOF
[caisar] Goal G: Valid