From 2e3169a260b25912040d4cf4228a75f3d060cd48 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 12 Jun 2023 14:36:21 +0200
Subject: [PATCH] [log] Rework logging API and tag names. Also update the doc.
---
doc/usage.rst | 5 ++--
src/logging.ml | 10 ++++++--
src/logging.mli | 17 +++++++------
src/main.ml | 2 +-
src/verification.ml | 5 ++--
tests/cvc5.t | 4 ++--
tests/dataset.t | 44 +++++++++++++++++-----------------
tests/interpretation_acasxu.t | 6 ++---
tests/interpretation_dataset.t | 10 ++++----
tests/marabou.t | 18 +++++++-------
tests/pyrat.t | 18 +++++++-------
tests/pyrat_onnx.t | 6 ++---
tests/verify_json.t | 4 ++--
13 files changed, 79 insertions(+), 70 deletions(-)
diff --git a/doc/usage.rst b/doc/usage.rst
index 2386eb5..9e00ec4 100644
--- a/doc/usage.rst
+++ b/doc/usage.rst
@@ -63,8 +63,9 @@ verbosity level allows logging with all tags enabled. To enable a particular
tag, use the option ``--ltag=TAG``, with ``TAG`` one of the following:
* ``Autodetect``: display the output of the autodetect routine of CAISAR described in :ref:`prover-registration`
-* ``Specification``: display the actual specification provided to the prover
-* ``CallProver``: display the actual command used to call the prover
+* ``ProverSpec``: display the actual specification provided to the prover
+* ``ProverCall``: display the actual command used to call the prover
+* ``StackTrace``: display the stack trace upon a CAISAR error
Built-in properties
-------------------
diff --git a/src/logging.ml b/src/logging.ml
index 2a2e468..559260d 100644
--- a/src/logging.ml
+++ b/src/logging.ml
@@ -21,10 +21,16 @@
(**************************************************************************)
let src_autodetect = Logs.Src.create "Autodetect" ~doc:"Prover autodetection"
-let src_spec = Logs.Src.create "Spec" ~doc:"Prover-tailored specification"
-let src_call = Logs.Src.create "Call" ~doc:"Call prover"
+
+let src_prover_spec =
+ Logs.Src.create "ProverSpec" ~doc:"Prover-tailored specification"
+
+let src_prover_call = Logs.Src.create "ProverCall" ~doc:"Prover call"
let src_stack_trace = Logs.Src.create "StackTrace" ~doc:"Print stack trace"
+let all_srcs () =
+ [ src_autodetect; src_prover_spec; src_prover_call; src_stack_trace ]
+
let is_debug_level src =
match Logs.Src.level src with Some Debug -> true | _ -> false
diff --git a/src/logging.mli b/src/logging.mli
index b957d9b..48e43c3 100644
--- a/src/logging.mli
+++ b/src/logging.mli
@@ -20,16 +20,19 @@
(* *)
(**************************************************************************)
-(** {2 Debug Tags} *)
-val src_autodetect : Logs.src
-
-val src_spec : Logs.src
-
-val src_call : Logs.src
+(** {2 Sources} *)
+val src_autodetect : Logs.src
+val src_prover_spec : Logs.src
+val src_prover_call : Logs.src
val src_stack_trace : Logs.src
+val all_srcs : unit -> Logs.src list
+(** @return all available sources. *)
+
(** {2 Logs} *)
val is_debug_level : Logs.src -> bool
-val setup : Fmt.style_renderer option -> Logs.level option -> Logs.src list -> unit
+
+val setup :
+ Fmt.style_renderer option -> Logs.level option -> Logs.src list -> unit
diff --git a/src/main.ml b/src/main.ml
index 83d8014..ea8183c 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -37,7 +37,7 @@ let () =
(* -- Logs *)
let log_tags =
- let all_tags = Logs.Src.list () in
+ let all_tags = Logging.all_srcs () in
let doc =
Fmt.str "Logging tags. Available $(docv)s: %s."
(Arg.doc_alts
diff --git a/src/verification.ml b/src/verification.ml
index 2a2953b..3aa186a 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -22,7 +22,6 @@
open Why3
open Base
-module Filename = Caml.Filename
module File = struct
type t =
@@ -164,7 +163,7 @@ let build_command config_prover ~nn_filename =
let log_prover_task driver task =
let print fmt task = ignore (Driver.print_task_prepared driver fmt task) in
- Logs.debug ~src:Logging.src_spec (fun m ->
+ Logs.debug ~src:Logging.src_prover_spec (fun m ->
m "@[Prover-tailored specification:@.%a@]" print task)
let call_prover_on_task limit config command driver task =
@@ -302,7 +301,7 @@ let open_file ?format env file =
let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern
file =
- let debug = Logging.(is_debug_level src_call) in
+ let debug = Logging.(is_debug_level src_prover_call) in
(if debug then Debug.(set_flag (lookup_flag "call_prover")));
let env, config = create_env loadpath in
let main = Whyconf.get_main config in
diff --git a/tests/cvc5.t b/tests/cvc5.t
index 7565e7c..e55696f 100644
--- a/tests/cvc5.t
+++ b/tests/cvc5.t
@@ -6,7 +6,7 @@ Test verify
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify -L . --format whyml --prover=CVC5 --ltag=Spec - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify -L . --format whyml --prover=CVC5 --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory CVC5
> use TestNetworkONNX.AsTuple as TN
> use ieee_float.Float64
@@ -17,7 +17,7 @@ Test verify
> (0.0:t) .< y1 .< (0.5:t) /\ (0.0:t) .< y2 .< (1.0:t)
> end
> EOF
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
;; produced by cvc5.drv ;;
(set-logic ALL)
(set-info :smt-lib-version 2.6)
diff --git a/tests/dataset.t b/tests/dataset.t
index 4b2abb4..0e96584 100644
--- a/tests/dataset.t
+++ b/tests/dataset.t
@@ -14,7 +14,7 @@ Test verify on dataset
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify -L . --format whyml --ltag=Spec --prover=PyRAT --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.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
> use ieee_float.Float64
@@ -27,7 +27,7 @@ Test verify on dataset
> robust TN.model dataset (0.0100000000000000002081668171172168513294309377670288085937500000:t)
> end
> EOF
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
;;; produced by PyRAT/VNN-LIB driver
;;; produced by VNN-LIB driver
;; X_0
@@ -99,7 +99,7 @@ Test verify on dataset
(and (>= Y_4 Y_1))
))
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
;;; produced by PyRAT/VNN-LIB driver
;;; produced by VNN-LIB driver
;; X_0
@@ -171,7 +171,7 @@ Test verify on dataset
(and (>= Y_4 Y_0))
))
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
;;; produced by PyRAT/VNN-LIB driver
;;; produced by VNN-LIB driver
;; X_0
@@ -243,7 +243,7 @@ Test verify on dataset
(and (>= Y_4 Y_1))
))
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
;;; produced by PyRAT/VNN-LIB driver
;;; produced by VNN-LIB driver
;; X_0
@@ -318,7 +318,7 @@ Test verify on dataset
Goal G: Unknown ()
Goal H: Unknown ()
- $ caisar verify -L . --format whyml --ltag=Spec --prover=Marabou --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify -L . --format whyml --ltag=ProverSpec --prover=Marabou --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
> use TestNetwork.AsArray as TN
> use ieee_float.Float64
@@ -331,7 +331,7 @@ Test verify on dataset
> robust TN.model dataset (0.0100000000000000002081668171172168513294309377670288085937500000:t)
> end
> EOF
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.0
x1 >= 1.0
@@ -344,7 +344,7 @@ Test verify on dataset
x4 <= 0.776470588000000017103729987866245210170745849609375
+y0 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.0
x1 >= 1.0
@@ -357,7 +357,7 @@ Test verify on dataset
x4 <= 0.776470588000000017103729987866245210170745849609375
+y2 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.0
x1 >= 1.0
@@ -370,7 +370,7 @@ Test verify on dataset
x4 <= 0.776470588000000017103729987866245210170745849609375
+y3 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.0
x1 >= 1.0
@@ -383,7 +383,7 @@ Test verify on dataset
x4 <= 0.776470588000000017103729987866245210170745849609375
+y4 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.94117647100000001447739350624033249914646148681640625
x0 <= 0.94117647100000001447739350624033249914646148681640625
x1 >= 0.0
@@ -396,7 +396,7 @@ Test verify on dataset
x4 <= 0.0392156859999999996002628677160828374326229095458984375
+y1 -y0 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.94117647100000001447739350624033249914646148681640625
x0 <= 0.94117647100000001447739350624033249914646148681640625
x1 >= 0.0
@@ -409,7 +409,7 @@ Test verify on dataset
x4 <= 0.0392156859999999996002628677160828374326229095458984375
+y2 -y0 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.94117647100000001447739350624033249914646148681640625
x0 <= 0.94117647100000001447739350624033249914646148681640625
x1 >= 0.0
@@ -422,7 +422,7 @@ Test verify on dataset
x4 <= 0.0392156859999999996002628677160828374326229095458984375
+y3 -y0 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.94117647100000001447739350624033249914646148681640625
x0 <= 0.94117647100000001447739350624033249914646148681640625
x1 >= 0.0
@@ -435,7 +435,7 @@ Test verify on dataset
x4 <= 0.0392156859999999996002628677160828374326229095458984375
+y4 -y0 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.01000000000000000020816681711721685132943093776702880859375
x1 >= 0.9899999999999999911182158029987476766109466552734375
@@ -448,7 +448,7 @@ Test verify on dataset
x4 <= 0.7864705880000000259855141848674975335597991943359375
+y0 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.01000000000000000020816681711721685132943093776702880859375
x1 >= 0.9899999999999999911182158029987476766109466552734375
@@ -461,7 +461,7 @@ Test verify on dataset
x4 <= 0.7864705880000000259855141848674975335597991943359375
+y2 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.01000000000000000020816681711721685132943093776702880859375
x1 >= 0.9899999999999999911182158029987476766109466552734375
@@ -474,7 +474,7 @@ Test verify on dataset
x4 <= 0.7864705880000000259855141848674975335597991943359375
+y3 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.01000000000000000020816681711721685132943093776702880859375
x1 >= 0.9899999999999999911182158029987476766109466552734375
@@ -487,7 +487,7 @@ Test verify on dataset
x4 <= 0.7864705880000000259855141848674975335597991943359375
+y4 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.93117647100000000559560930923908017575740814208984375
x0 <= 0.95117647100000002335917770324158482253551483154296875
x1 >= 0.0
@@ -500,7 +500,7 @@ Test verify on dataset
x4 <= 0.049215686000000001543153160810106783173978328704833984375
+y1 -y0 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.93117647100000000559560930923908017575740814208984375
x0 <= 0.95117647100000002335917770324158482253551483154296875
x1 >= 0.0
@@ -513,7 +513,7 @@ Test verify on dataset
x4 <= 0.049215686000000001543153160810106783173978328704833984375
+y2 -y0 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.93117647100000000559560930923908017575740814208984375
x0 <= 0.95117647100000002335917770324158482253551483154296875
x1 >= 0.0
@@ -526,7 +526,7 @@ Test verify on dataset
x4 <= 0.049215686000000001543153160810106783173978328704833984375
+y3 -y0 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.93117647100000000559560930923908017575740814208984375
x0 <= 0.95117647100000002335917770324158482253551483154296875
x1 >= 0.0
diff --git a/tests/interpretation_acasxu.t b/tests/interpretation_acasxu.t
index af2dd1e..28695a7 100644
--- a/tests/interpretation_acasxu.t
+++ b/tests/interpretation_acasxu.t
@@ -7,7 +7,7 @@ Test interpret on acasxu
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify --format whyml --prover PyRAT --ltag=Spec - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify --format whyml --prover PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
> use ieee_float.Float64
> use bool.Bool
@@ -95,7 +95,7 @@ Test interpret on acasxu
> not (advises nn i clear_of_conflict)
> end
> EOF
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
-0.328421367053318091766556108268559910356998443603515625 <= x0
x0 <= 0.67985927880386987087746319957659579813480377197265625
-0.499999999999967081887319864108576439321041107177734375 <= x1
@@ -111,7 +111,7 @@ Test interpret on acasxu
x4 <= -0.450000000000000011102230246251565404236316680908203125
y0 <= 3.991125645861615112153231166303157806396484375
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
-0.328421367053318091766556108268559910356998443603515625 <= x0
x0 <= 0.67985927880386987087746319957659579813480377197265625
-0.499999999999967081887319864108576439321041107177734375 <= x1
diff --git a/tests/interpretation_dataset.t b/tests/interpretation_dataset.t
index 2f0c09f..eb6ef3e 100644
--- a/tests/interpretation_dataset.t
+++ b/tests/interpretation_dataset.t
@@ -11,7 +11,7 @@ Test interpret on dataset
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify --format whyml --prover Marabou --ltag=Spec - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify --format whyml --prover Marabou --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
> use ieee_float.Float64
> use bool.Bool
@@ -53,7 +53,7 @@ Test interpret on dataset
> robust nn dataset eps
> end
> EOF
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 1.0
x1 >= 0.0
@@ -76,7 +76,7 @@ Test interpret on dataset
x4 <= 1.151470588000000017103729987866245210170745849609375
+y0 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 1.0
x1 >= 0.0
@@ -99,7 +99,7 @@ Test interpret on dataset
x4 <= 1.151470588000000017103729987866245210170745849609375
+y2 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 1.0
x1 >= 0.0
@@ -122,7 +122,7 @@ Test interpret on dataset
x4 <= 1.159313725000000072640204962226562201976776123046875
+y1 -y0 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 1.0
x1 >= 0.0
diff --git a/tests/marabou.t b/tests/marabou.t
index f424b8e..8ded847 100644
--- a/tests/marabou.t
+++ b/tests/marabou.t
@@ -6,7 +6,7 @@ Test verify
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify --format whyml --prover=Marabou --ltag=Spec - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify --format whyml --prover=Marabou --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
> use ieee_float.Float64
> use bool.Bool
@@ -41,17 +41,17 @@ Test verify
> (nn@@i)[1] .< (nn@@i)[0] \/ (nn@@i)[0] .< (nn@@i)[1]
> end
> EOF
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.5
y0 <= 0.0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.5
y0 >= 0.5
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.5
x1 >= 0.5
@@ -59,21 +59,21 @@ Test verify
y0 <= 0.0
y0 <= 0.5
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.5
x1 >= 0.5
x1 <= 1.0
y1 <= 0.0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.5
x1 >= 0.5
x1 <= 1.0
y1 >= 0.5
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.5
x1 >= 0.5
@@ -81,7 +81,7 @@ Test verify
+y1 -y0 >= 0
+y0 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.5
x1 >= 0.5
@@ -89,7 +89,7 @@ Test verify
+y1 -y0 >= 0
+y0 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.75
x0 <= 1.0
x1 >= 0.5
diff --git a/tests/pyrat.t b/tests/pyrat.t
index 20802e8..f34d87e 100644
--- a/tests/pyrat.t
+++ b/tests/pyrat.t
@@ -6,7 +6,7 @@ Test verify
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify --format whyml --prover=PyRAT --ltag=Spec - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify --format whyml --prover=PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory PyRAT
> use TestNetwork.AsTuple
> use ieee_float.Float64
@@ -30,52 +30,52 @@ Test verify
> ((0.0:t) .< (nn@@i)[0] \/ (0.5:t) .< (nn@@i)[0]) /\ (0.0:t) .< (nn@@i)[1] .< (0.5:t)
> end
> EOF
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
0.0 < y0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
y0 < 0.5
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
0.5 <= x1
x1 <= 1.0
(0.0 < y0 or 0.5 < y0)
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
0.5 <= x1
x1 <= 1.0
0.0 < y1
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
0.5 <= x1
x1 <= 1.0
y1 < 0.5
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
0.375 <= x0
x0 <= 0.75
0.5 <= x1
x1 <= 1.0
(0.0 < y0 or 0.5 < y0)
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
0.375 <= x0
x0 <= 0.75
0.5 <= x1
x1 <= 1.0
0.0 < y1
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
0.375 <= x0
x0 <= 0.75
0.5 <= x1
diff --git a/tests/pyrat_onnx.t b/tests/pyrat_onnx.t
index c0a18ae..2c983e6 100644
--- a/tests/pyrat_onnx.t
+++ b/tests/pyrat_onnx.t
@@ -6,7 +6,7 @@ Test verify
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify --format whyml --prover=PyRAT --ltag=Spec - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify --format whyml --prover=PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory PyRAT_ONNX
> use ieee_float.Float64
> use bool.Bool
@@ -23,12 +23,12 @@ Test verify
> (0.0:t) .< (nn@@i)[0] .< (0.5:t)
> end
> EOF
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
0.0 < y0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
y0 < 0.5
diff --git a/tests/verify_json.t b/tests/verify_json.t
index a087029..d34b2e3 100644
--- a/tests/verify_json.t
+++ b/tests/verify_json.t
@@ -14,8 +14,8 @@ Test verify-json
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify-json --ltag=Spec config.json 2>&1 <<EOF | ./filter_tmpdir.sh
- [DEBUG]{Spec} Prover-tailored specification:
+ $ caisar verify-json --ltag=ProverSpec config.json 2>&1 <<EOF | ./filter_tmpdir.sh
+ [DEBUG]{ProverSpec} Prover-tailored specification:
;;; produced by PyRAT/VNN-LIB driver
;;; produced by VNN-LIB driver
;; X_0
--
GitLab