From 5621ba5ec8df59feb0f3dfe6855af24f206267cd Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 16 Dec 2020 09:58:54 +0100
Subject: [PATCH] Some misc improvements.
---
main.ml | 13 +++++++------
property.ml | 2 +-
property_lexer.mll | 2 +-
solver.ml | 4 ++--
solver.mli | 2 +-
5 files changed, 12 insertions(+), 11 deletions(-)
diff --git a/main.ml b/main.ml
index 9ff0112..3f2da3a 100644
--- a/main.ml
+++ b/main.ml
@@ -52,7 +52,7 @@ let verify cmd model property solver raw_options () =
let open Result in
Model.build ~filename:model >>= fun model ->
Property.build ~filename:property >>= fun property ->
- Solver.exec ?raw_options solver property model
+ Solver.exec ?raw_options solver model property
in
match do_verify () with
| Ok () -> Logs.app (fun m -> m "Done.")
@@ -88,18 +88,18 @@ let verify_cmd =
let docv_model = "MODEL" in
let model =
let doc = "The $(b,filename) of a neural network model." in
- Arg.(required & pos 1 (some file) None & info [] ~docv:docv_model ~doc)
+ Arg.(required & pos 0 (some file) None & info [] ~docv:docv_model ~doc)
in
let docv_property = "PROPERTY" in
let property =
let doc = "The $(b,filename) of a property to verify." in
- Arg.(required & pos 0 (some file) None & info [] ~docv:docv_property ~doc)
+ Arg.(required & pos 1 (some file) None & info [] ~docv:docv_property ~doc)
in
let solver_raw_options =
let doc = "Additional options provided to the solver." in
Arg.(value & opt (some string) None & info ["raw"; "raw-options"] ~doc)
in
- let doc = "property verification of neural networks" in
+ let doc = "Property verification of neural networks." in
let exits = Term.default_exits in
let man = [
`S Manpage.s_description;
@@ -115,11 +115,12 @@ let verify_cmd =
in
Term.(const verify
$ const cmdname
- $ model $ property $ solver $ solver_raw_options $ setup_logs),
+ $ model $ property $ solver
+ $ solver_raw_options $ setup_logs),
Term.info cmdname ~sdocs:Manpage.s_common_options ~envs ~exits ~doc ~man
let default_cmd =
- let doc = "framework for neural networks property verification and more" in
+ let doc = "Framework for neural networks property verification and more." in
let sdocs = Manpage.s_common_options in
let man =
[ `S Manpage.s_common_options;
diff --git a/property.ml b/property.ml
index 560006b..4414673 100644
--- a/property.ml
+++ b/property.ml
@@ -27,7 +27,7 @@ let do_build ~property line =
| Property_parser.Error ->
Error
(Format.sprintf
- "At offset %d: syntax error."
+ "Property syntax error at offset %d."
(Lexing.lexeme_start linebuf))
let build ~filename =
diff --git a/property_lexer.mll b/property_lexer.mll
index e6fe6d7..14bc3f4 100644
--- a/property_lexer.mll
+++ b/property_lexer.mll
@@ -53,4 +53,4 @@ and token = parse
| '\n'
{ EOL }
| _
- { raise (Error (Printf.sprintf "At offset %d: unexpected character.\n" (Lexing.lexeme_start lexbuf))) }
+ { raise (Error (Printf.sprintf "Property lexer at offset %d: unexpected character.\n" (Lexing.lexeme_start lexbuf))) }
diff --git a/solver.ml b/solver.ml
index 3c7029e..85f52fc 100644
--- a/solver.ml
+++ b/solver.ml
@@ -76,7 +76,7 @@ let check_availability solver =
(Format.sprintf
"Command `%s' failed.@ \
Hint: Set either the PATH or \
- use variable `%s' to directly provide the executable."
+ use variable `%s' to directly provide the path to the executable."
cmd (env_var_of_solver solver))
else begin
(try
@@ -145,7 +145,7 @@ let build_command ?raw_options solver property model =
Ok (tmp, cmd)
end
-let exec ?raw_options solver property model =
+let exec ?raw_options solver model property =
let open Result in
(* Check solver availability in PATH. *)
check_availability solver >>= fun () ->
diff --git a/solver.mli b/solver.mli
index c89f7ee..e85cb9c 100644
--- a/solver.mli
+++ b/solver.mli
@@ -13,4 +13,4 @@ val env_vars: string list
[model] with the provided [raw_options], if any. *)
val exec:
?raw_options:string ->
- solver -> Property.t -> Model.t -> (unit, string) Result.t
+ solver -> Model.t -> Property.t -> (unit, string) Result.t
--
GitLab