From 8a00455ed695a3b4c8f3a81ecefd5004d680f0de Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 12 Jun 2023 13:54:27 +0200
Subject: [PATCH] [log] Use Logs.Src instead of Logs.Tag when logging.
---
src/autodetect.ml | 2 +-
src/logging.ml | 123 ++++++---------------------------
src/logging.mli | 17 ++---
src/main.ml | 15 ++--
src/verification.ml | 8 +--
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, 95 insertions(+), 180 deletions(-)
diff --git a/src/autodetect.ml b/src/autodetect.ml
index 3dfec3c..3bc6996 100644
--- a/src/autodetect.ml
+++ b/src/autodetect.ml
@@ -31,7 +31,7 @@ let rec lookup_file dirs filename =
if Caml.Sys.file_exists file then file else lookup_file dirs filename
let autodetection () =
- let debug = Logging.(is_debug_level () || is_tag_enabled Autodetect) in
+ let debug = Logging.(is_debug_level src_autodetect) in
if debug then Debug.set_flag Autodetection.debug;
let caisar_conf =
lookup_file Dirs.Sites.config "caisar-detection-data.conf"
diff --git a/src/logging.ml b/src/logging.ml
index 2d93d00..2a2e468 100644
--- a/src/logging.ml
+++ b/src/logging.ml
@@ -20,117 +20,34 @@
(* *)
(**************************************************************************)
-type tag =
- | Autodetect
- | Specification
- | CallProver
-[@@deriving show { with_path = false }]
+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_stack_trace = Logs.Src.create "StackTrace" ~doc:"Print stack trace"
-let tags_available () = [ Autodetect; Specification; CallProver ]
-let tag_defs_enabled = ref []
+let is_debug_level src =
+ match Logs.Src.level src with Some Debug -> true | _ -> false
-let tag_def_auto =
- Logs.Tag.def "autodetect" ~doc:"Prover autodetection" Fmt.string
-
-let tag_def_spec =
- Logs.Tag.def "spec" ~doc:"Prover-tailored specification" Fmt.string
-
-let tag_def_call = Logs.Tag.def "call_prover" ~doc:"Call prover" Fmt.string
-
-let tag_def_of_tag = function
- | Autodetect -> tag_def_auto
- | Specification -> tag_def_spec
- | CallProver -> tag_def_call
-
-let tag_auto = Logs.Tag.add tag_def_auto "AUTO"
-let tag_spec = Logs.Tag.add tag_def_spec "SPEC"
-let tag_call = Logs.Tag.add tag_def_call "CALL_PROVER"
-
-let add_tag = function
- | Autodetect -> tag_auto
- | Specification -> tag_spec
- | CallProver -> tag_call
-
-let tag dt = add_tag dt Logs.Tag.empty
-
-let is_tag_enabled tag =
- let tag_def = tag_def_of_tag tag in
- List.memq tag_def !tag_defs_enabled
-
-let is_debug_level () =
- match Logs.level () with Some Debug -> true | _ -> false
-
-let style_of_level = function
- | Logs.App -> Logs_fmt.app_style
- | Logs.Error -> Logs_fmt.err_style
- | Logs.Warning -> Logs_fmt.warn_style
- | Logs.Info -> Logs_fmt.info_style
- | Logs.Debug -> Logs_fmt.debug_style
-
-let pp_header ~pp_h ppf (l, h) =
- let style = style_of_level l in
- match l with
- | Logs.App -> ( match h with None -> () | Some h -> pp_h ppf style h)
- | Logs.Error ->
- pp_h ppf style Fmt.(str "ERROR%a" (option (any ":" ++ string)) h)
- | Logs.Warning ->
- pp_h ppf style Fmt.(str "WARNING%a" (option (any ":" ++ string)) h)
- | Logs.Info ->
- pp_h ppf style Fmt.(str "INFO%a" (option (any ":" ++ string)) h)
- | Logs.Debug ->
- pp_h ppf style Fmt.(str "DEBUG%a" (option (any ":" ++ string)) h)
-
-let pp_header ~space =
- let pp_h ppf style h =
- Fmt.pf ppf "[%a]%s" Fmt.(styled style string) h (if space then " " else "")
- in
- pp_header ~pp_h
-
-let pp_header_tag ppf (l, t) =
- let style = style_of_level l in
- Fmt.pf ppf "{%a}" Fmt.(styled style string) t
-
-let tag_defs_available = List.map tag_def_of_tag (tags_available ())
-
-let reporter ppf =
- let report _src level ~over k msgf =
+let reporter =
+ let report src level ~over k msgf =
let k _ =
over ();
k ()
in
- let with_tags ~header ~tags k ppf fmt =
- let tag =
- Base.List.filter_map tag_defs_available ~f:(fun td ->
- Logs.Tag.find td tags)
- |> List.hd
- in
- Fmt.kpf k ppf
- ("%a%a @[" ^^ fmt ^^ "@]@.")
- (pp_header ~space:false) (level, header) pp_header_tag (level, tag)
+ msgf @@ fun ?header ?tags:_ fmt ->
+ let ppf = if level = Logs.App then Fmt.stdout else Fmt.stderr in
+ let print_src fmt src =
+ if not (Logs.Src.equal Logs.default src)
+ then Fmt.pf fmt "@[{%s}@] " (Logs.Src.name src)
in
-
- msgf @@ fun ?header ?tags fmt ->
- match tags with
- | None ->
- Fmt.kpf k ppf
- ("%a@[" ^^ fmt ^^ "@]@.")
- (pp_header ~space:true) (level, header)
- | Some tags ->
- let tag_is_enabled =
- not
- Base.(
- List.filter_map !tag_defs_enabled ~f:(fun td ->
- Logs.Tag.find td tags)
- |> List.is_empty)
- in
- if is_debug_level () || tag_is_enabled
- then with_tags ~header ~tags k ppf fmt
- else Fmt.kpf k Format.str_formatter fmt
+ Format.kfprintf k ppf
+ ("%a%a@[" ^^ fmt ^^ "@]@.")
+ Logs.pp_header (level, header) print_src src
in
{ Logs.report }
-let setup style_renderer level tags =
- tag_defs_enabled := List.map tag_def_of_tag tags;
+let setup style_renderer level srcs =
+ Logs.set_level ~all:true level;
+ List.iter (fun src -> Logs.Src.set_level src (Some Debug)) srcs;
Fmt_tty.setup_std_outputs ?style_renderer ();
- Logs.set_level level;
- Logs.set_reporter (reporter Fmt.stdout)
+ Logs.set_reporter reporter
diff --git a/src/logging.mli b/src/logging.mli
index e406e0d..b957d9b 100644
--- a/src/logging.mli
+++ b/src/logging.mli
@@ -21,18 +21,15 @@
(**************************************************************************)
(** {2 Debug Tags} *)
+val src_autodetect : Logs.src
-type tag =
- | Autodetect
- | Specification
- | CallProver
-[@@deriving show { with_path = false }]
+val src_spec : Logs.src
-val tags_available : unit -> tag list
-val tag : tag -> Logs.Tag.set
-val is_tag_enabled : tag -> bool
+val src_call : Logs.src
+
+val src_stack_trace : Logs.src
(** {2 Logs} *)
-val is_debug_level : unit -> bool
-val setup : Fmt.style_renderer option -> Logs.level option -> tag list -> unit
+val is_debug_level : Logs.src -> bool
+val setup : Fmt.style_renderer option -> Logs.level option -> Logs.src list -> unit
diff --git a/src/main.ml b/src/main.ml
index 66ddbbb..83d8014 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -37,14 +37,17 @@ let () =
(* -- Logs *)
let log_tags =
- let all_tags = Logging.tags_available () in
+ let all_tags = Logs.Src.list () in
let doc =
- Fmt.str "Logging tags. Available $(docv)s: %a."
- (Fmt.list ~sep:Fmt.comma Logging.pp_tag)
- all_tags
+ Fmt.str "Logging tags. Available $(docv)s: %s."
+ (Arg.doc_alts
+ (List.map
+ ~f:(fun src ->
+ Fmt.str "%s (%s)" (Logs.Src.name src) (Logs.Src.doc src))
+ all_tags))
in
let enum_log_tags =
- Arg.enum (List.map ~f:(fun c -> (Logging.show_tag c, c)) all_tags)
+ Arg.enum (List.map ~f:(fun c -> (Logs.Src.name c, c)) all_tags)
in
Arg.(
value & opt_all enum_log_tags []
@@ -422,5 +425,5 @@ let () =
Cmd.group ~default:default_cmd default_info
[ config_cmd; verify_cmd; verify_json_cmd; verify_xgboost_cmd ]
|> Cmd.eval ~catch:false |> Caml.exit
- with exn when not (Logging.is_debug_level ()) ->
+ with exn when not Logging.(is_debug_level src_stack_trace) ->
Logs.err (fun m -> m "@[%a@]" Why3.Exn_printer.exn_printer exn)
diff --git a/src/verification.ml b/src/verification.ml
index 1361fdd..2a2953b 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -164,10 +164,8 @@ 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.app (fun m ->
- m
- ~tags:Logging.(tag Specification)
- "@[Prover-tailored specification:@.%a@]" print task)
+ Logs.debug ~src:Logging.src_spec (fun m ->
+ m "@[Prover-tailored specification:@.%a@]" print task)
let call_prover_on_task limit config command driver task =
log_prover_task driver task;
@@ -304,7 +302,7 @@ let open_file ?format env file =
let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern
file =
- let debug = Logging.(is_debug_level () || is_tag_enabled CallProver) in
+ let debug = Logging.(is_debug_level src_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 02ce615..7565e7c 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=Specification - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify -L . --format whyml --prover=CVC5 --ltag=Spec - 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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 c46da76..4b2abb4 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=Specification --prover=PyRAT --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify -L . --format whyml --ltag=Spec --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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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))
))
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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))
))
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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))
))
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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=Specification --prover=Marabou --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify -L . --format whyml --ltag=Spec --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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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 01769a1..af2dd1e 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=Specification - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify --format whyml --prover PyRAT --ltag=Spec - 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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 4ff8e71..2f0c09f 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=Specification - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify --format whyml --prover Marabou --ltag=Spec - 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} Prover-tailored specification:
x0 >= 0.0
x0 <= 1.0
x1 >= 0.0
diff --git a/tests/marabou.t b/tests/marabou.t
index 291c4ca..f424b8e 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=Specification - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify --format whyml --prover=Marabou --ltag=Spec - 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.5
y0 <= 0.0
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.5
y0 >= 0.5
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.5
x1 >= 0.5
@@ -59,21 +59,21 @@ Test verify
y0 <= 0.0
y0 <= 0.5
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.5
x1 >= 0.5
x1 <= 1.0
y1 <= 0.0
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.5
x1 >= 0.5
x1 <= 1.0
y1 >= 0.5
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.5
x1 >= 0.5
@@ -81,7 +81,7 @@ Test verify
+y1 -y0 >= 0
+y0 -y1 >= 0
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.5
x1 >= 0.5
@@ -89,7 +89,7 @@ Test verify
+y1 -y0 >= 0
+y0 -y1 >= 0
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} Prover-tailored specification:
x0 >= 0.75
x0 <= 1.0
x1 >= 0.5
diff --git a/tests/pyrat.t b/tests/pyrat.t
index 5920ac2..20802e8 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=Specification - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify --format whyml --prover=PyRAT --ltag=Spec - 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
0.0 < y0
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
y0 < 0.5
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
0.5 <= x1
x1 <= 1.0
(0.0 < y0 or 0.5 < y0)
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
0.5 <= x1
x1 <= 1.0
0.0 < y1
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
0.5 <= x1
x1 <= 1.0
y1 < 0.5
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} Prover-tailored specification:
0.375 <= x0
x0 <= 0.75
0.5 <= x1
x1 <= 1.0
(0.0 < y0 or 0.5 < y0)
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} Prover-tailored specification:
0.375 <= x0
x0 <= 0.75
0.5 <= x1
x1 <= 1.0
0.0 < y1
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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 2003a89..c0a18ae 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=Specification - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify --format whyml --prover=PyRAT --ltag=Spec - 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
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
0.0 < y0
- {SPEC} Prover-tailored specification:
+ [DEBUG]{Spec} 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 ac7fddd..a087029 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=Specification config.json 2>&1 <<EOF | ./filter_tmpdir.sh
- {SPEC} Prover-tailored specification:
+ $ caisar verify-json --ltag=Spec config.json 2>&1 <<EOF | ./filter_tmpdir.sh
+ [DEBUG]{Spec} Prover-tailored specification:
;;; produced by PyRAT/VNN-LIB driver
;;; produced by VNN-LIB driver
;; X_0
--
GitLab