Skip to content

GitLab

Commit 1d806ea1 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Add command to launch pdf doc fron the lurettetop prompt

parent a072aedb
Hide whitespace changes
Inline Side-by-side
source/Lurettetop/cmd.ml
View file @ 1d806ea1
......@@ -37,7 +37,8 @@ Equivalently, you can directly set values at the command line:
... [... testing ...]
You migth also want to try the info command (i for short) to get the values
of the test parameters.
of the test parameters, and the h (help) command to obtain the list of
possible commands.
"
......@@ -66,8 +67,8 @@ let (info : unit -> unit) =
test length: " ^ (string_of_int args.step_nb) ^ "
precision: " ^ (string_of_int args.precision) ^ "
seed: " ^ (match args.seed with
None -> "chosen randomly"
| Some i -> (string_of_int i)) ^ "
None -> "chosen randomly"
| Some i -> (string_of_int i)) ^ "
verbosity level: " ^ (string_of_int (args.verbose)) ^ "
rif file name: " ^ args.output ^ "
overwrite rif file? "
......@@ -75,21 +76,21 @@ let (info : unit -> unit) =
coverage file name: " ^ args.cov_file ^ "
do we stop when an oracle returns false? "
^ (if args.stop_on_oracle_error then "yes" else "no") ^
(match args.extra_cfiles with
(match args.extra_cfiles with
None -> ""
| Some str -> ("
extra_source_files: " ^ str)) ^
(match args.extra_libs with
None -> ""
| Some str -> ("
(match args.extra_libs with
None -> ""
| Some str -> ("
extra_libs: " ^ str)) ^
(match args.extra_libdirs with
None -> ""
| Some str -> ("
(match args.extra_libdirs with
None -> ""
| Some str -> ("
extra_libdirs: " ^ str)) ^
(match args.extra_includedirs with
None -> ""
| Some str -> ("
(match args.extra_includedirs with
None -> ""
| Some str -> ("
extra_includedirs: " ^ str)) ^ "
display local var? " ^ (if (args.display_local_var) then "yes" else "no") ^ "
......@@ -116,7 +117,12 @@ info, i
Display a sum-up of the test parameters
man
display a small user manual
Display a small user manual
man_lurette
man_lutin
tuto_lutin
Launch pdf documentation
add_rp "^rp_help^"
The current value of the rp fields are
......@@ -141,47 +147,47 @@ stl <integer>, set_test_length <integer>
(string_of_int args.step_nb) ^ "\"
set_precision <int>
to set te number of digit after the dot used for real computation.
Set the number of digit after the dot used for real computation.
current precision is " ^ (string_of_int args.precision) ^ "
set_seed <integer>
to set the seed the random engine is initialised with.
Set the seed the random engine is initialised with.
Its current value is " ^ (match args.seed with
None -> "chose randomly"
| Some i -> ("\"" ^ (string_of_int i) ^ "\"")) ^ "
set_seed_randomly
to let the system set a seed randomly.
Let the system set a seed randomly.
set_verbose (0,1,2)
to set on and off a verbose mode. Its current value is "
Set on and off a verbose mode. Its current value is "
^ (string_of_int (args.verbose)) ^ "
set_rif <string>, set_output <string>
to set the name of the file the (rif) output of the test is
Set the name of the file the (rif) output of the test is
put into. Its current value is \"" ^ args.output ^ "\"
set_overwrite_output <bool>
to set the overwrite_output mode
Set the overwrite_output mode
sim2chro, s
call sim2chro to visualize (rif) data
Call sim2chro to visualize (rif) data
gnuplot, g
call gnuplot (> 3.7) to visualize (rif) data.
Call gnuplot (> 3.7) to visualize (rif) data.
set_cov_file <string>
set the coverage file name. Its current value is \"" ^ args.cov_file ^ "\"
Set the coverage file name. Its current value is \"" ^ args.cov_file ^ "\"
reset_cov_file <bool>
reset the coverage info in the coverage file before the next run.
Reset the coverage info in the coverage file before the next run.
Its current value is \"" ^ (if args.reset_cov_file then "true" else "false") ^ "\"
stop_on_oracle_error <bool>
set a boolean flag stating what to do when an oracle returns false
Set a boolean flag stating what to do when an oracle returns false
Its current value is \"" ^ (if args.stop_on_oracle_error then "true" else "false") ^ "\"
more
Display advanded commands.
Display more commands.
"
in
......@@ -193,13 +199,13 @@ let (display2 : unit -> unit) =
let msg = "The advanced commands are:
set_draw_nb <integer>
to set the number of draw to be done in each formula at each step
Set the number of draw to be done in each formula at each step
Its current value is \"" ^ (string_of_int args.draw_nb) ^ "\"
set_draw_inside <integer>
set_draw_edges <integer>
set_draw_vertices <integer>
to set the number of draw to be made:
Set the number of draw to be made:
- inside: i.e., draw inside the convex hull of solutions.
- edges : i.e., draw on the edges of the convex hull of solutions.
- vertices : i.e., draw among the vertices of the convex hull of solutions.
......@@ -210,10 +216,10 @@ set_draw_vertices <integer>
vertices: \"" ^ (string_of_int args.draw_vertices ) ^ "\"
set_step_mode {inside|edges|vertices}
set the mode used to perform the step
Set the mode used to perform the step
set_draw_all_formula <Boolean>
to a set Boolean that indicates whether lurette should tries
Set a Boolean that indicates whether lurette should tries
one or all the formula reachable from the current step.
Its current value is "
^ (if (args.all_formula)
......@@ -221,7 +227,7 @@ set_draw_all_formula <Boolean>
else "\"false\"") ^ "
set_draw_all_vertices <Boolean>
to set a Boolean that indicates whether lurette should tries
Set a Boolean that indicates whether lurette should tries
all polyhedra vertices.
Its current value is "
^ (if (args.all_vertices)
......@@ -229,7 +235,7 @@ set_draw_all_vertices <Boolean>
else "\"false\"") ^ "
set_compute_volume <Boolean>
to set a Boolean that indicates whether lurette should compute
Set a Boolean that indicates whether lurette should compute
polyhedra volumes (achieve fairness, but more expensive).
Its current value is "
^ (if (args.compute_volume)
......@@ -237,48 +243,48 @@ set_compute_volume <Boolean>
else "\"false\"") ^ "
set_extra_source_files <string>
to set the EXTRA_SOURCE_FILES environment variable.
Set the EXTRA_SOURCE_FILES environment variable.
Its current value is " ^
(match args.extra_cfiles with
None -> "unset"
| Some str -> ("\"" ^ str ^ "\"")) ^ "
set_extra_libs <string>
to set the EXTRA_LIBS environment variable.
Set the EXTRA_LIBS environment variable.
Its current value is " ^
(match args.extra_libs with
None -> "unset"
| Some str -> ("\"" ^ str ^ "\"")) ^ "
set_extra_libdirs <string>
to set the EXTRA_LIBDIRS environment variable.
Set the EXTRA_LIBDIRS environment variable.
Its current value is " ^
(match args.extra_libdirs with
None -> "unset"
| Some str -> ("\"" ^ str ^ "\"")) ^ "
set_extra_includedirs <string>
to set the EXTRA_INCLUDEDIRS environment variable.
Set the EXTRA_INCLUDEDIRS environment variable.
Its current value is " ^
(match args.extra_includedirs with
None -> "unset"
| Some str -> ("\"" ^ str ^ "\"")) ^ "
set_display_local_var <boolean>
to set a flag saying whether or not the local var be displayed in
Set a flag saying whether or not the local var be displayed in
sim2chro. Its current value is " ^ (if (args.display_local_var)
then "\"true\""
else "\"false\"") ^ "
set_prefix <string>
to set the string that is appended before the call to lurette.
Set the string that is appended before the call to lurette.
This useful, e.g., for timings.
Its current value is \"" ^ args.prefix ^ "\"
set_step_by_step <int>
to set the step_by_step mode on.
Set the step_by_step mode on.
set_step_by_step_off
to set the step_by_step mode off.
Set the step_by_step mode off.
change_dir <string>
Change the current directory.
......@@ -339,6 +345,9 @@ type t =
| Help
| HelpMore
| Man
| LurettePdfMan
| LutinPdfMan
| LutinPdfTuto
| Prompt of string
| Prefix of string
| Pack of string
......@@ -385,15 +394,15 @@ let rec (parse_tok : tok -> t) =
| [< 'Genlex.Ident(_, "set_draw_vertices") ; 'Genlex.Int(_, i) >] -> DrawVertices(i)
| [< 'Genlex.Ident(_, "set_draw_all_formula"); str = parse_ident_or_string
>] ->
if List.mem str ["t";"true"]
then AllFormula(true)
else AllFormula(false)
>] ->
if List.mem str ["t";"true"]
then AllFormula(true)
else AllFormula(false)
| [< 'Genlex.Ident(_, "set_draw_all_vertices"); str = parse_ident_or_string
>] ->
if List.mem str ["t";"true"]
then AllVertices(true)
else AllVertices(false)
>] ->
if List.mem str ["t";"true"]
then AllVertices(true)
else AllVertices(false)
| [< 'Genlex.Ident(_, "set_direct_mode") >] -> args.direct_mode <- true; Nop
| [< 'Genlex.Ident(_, "set_old_mode") >] -> args.direct_mode <- false; Nop
......@@ -405,7 +414,7 @@ let rec (parse_tok : tok -> t) =
| [< 'Genlex.Ident(_, "set_env") ; str = parse_ident_or_string >] -> Env(str)
| [< 'Genlex.Ident(_, "set_dbg_on") >] -> args.debug_ltop <- true; Nop
| [< 'Genlex.Ident(_, "set_dbg_off") >] -> args.debug_ltop <- false; Nop
(* | [< 'Genlex.Ident(_, "set_env") ; str = parse_env >] -> Env(str) *)
(* | [< 'Genlex.Ident(_, "set_env") ; str = parse_env >] -> Env(str) *)
| [< 'Genlex.Ident(_, "add_rp") ; 'Genlex.String(_, str) >] ->
......@@ -417,13 +426,13 @@ let rec (parse_tok : tok -> t) =
| [< 'Genlex.Ident(_, "set_root_node") ; node = parse_node >] -> RootNode(node)
| [< 'Genlex.Ident(_, "set_sut") ; str = parse_file_name ; node = parse_node >] -> Sut(str, node)
| [< 'Genlex.Ident(_, "set_sut_cmd") ;
str = parse_ident_or_string
>] -> SutCmd(str)
str = parse_ident_or_string
>] -> SutCmd(str)
| [< 'Genlex.Ident(_, "set_oracle_cmd") ;
str = parse_ident_or_string >]
-> OracleCmd(str)
str = parse_ident_or_string >]
-> OracleCmd(str)
| [< 'Genlex.Ident(_, "set_oracle") ; str = parse_file_name ; node = parse_node>] -> Oracle(str, node)
(* | [< 'Genlex.Ident(_, "set_make_opt") ; str = parse_ident_or_string >] -> MakeOpt(str) *)
(* | [< 'Genlex.Ident(_, "set_make_opt") ; str = parse_ident_or_string >] -> MakeOpt(str) *)
| [< 'Genlex.Ident(_, "stl") ; 'Genlex.Int(_, i) >] -> StepNb(i)
| [< 'Genlex.Ident(_, "set_test_length") ; 'Genlex.Int(_, i) >] -> StepNb(i)
| [< 'Genlex.Ident(_, "set_draw_nb") ; 'Genlex.Int(_, i) >] -> DrawNb(i)
......@@ -434,91 +443,91 @@ let rec (parse_tok : tok -> t) =
| [< 'Genlex.Ident(_, "set_preprocessor"); pp = parse_ident_or_string>] -> PP(Some pp)
| [< 'Genlex.Ident(_, "set_sut_compiler"); s = parse_ident_or_string >] ->
( match (string_to_compiler s) with
Some comp -> SetSutCompiler(comp)
| None -> Error ("'" ^ s ^ "' is not a supported compiler.\n")
)
( match (string_to_compiler s) with
Some comp -> SetSutCompiler(comp)
| None -> Error ("'" ^ s ^ "' is not a supported compiler.\n")
)
| [< 'Genlex.Ident(_, "set_oracle_compiler"); s = parse_ident_or_string >] ->
( match (string_to_compiler s) with
Some comp -> SetOracleCompiler(comp)
| None -> Error ("'" ^ s ^ "' is not a supported compiler.\n")
)
( match (string_to_compiler s) with
Some comp -> SetOracleCompiler(comp)
| None -> Error ("'" ^ s ^ "' is not a supported compiler.\n")
)
| [< 'Genlex.Ident(_, "set_extra_cfiles") ; 'Genlex.String(_, str) >] ->
ExtraCFiles(str)
ExtraCFiles(str)
| [< 'Genlex.Ident(_, "set_extra_source_files") ; 'Genlex.String(_, str) >] ->
ExtraCFiles(str)
ExtraCFiles(str)
| [< 'Genlex.Ident(_, "set_extra_libs") ; 'Genlex.String(_, str) >] ->
ExtraLibs(str)
ExtraLibs(str)
| [< 'Genlex.Ident(_, "set_extra_libdirs") ; 'Genlex.String(_, str) >] ->
ExtraLibDirs(str)
ExtraLibDirs(str)
| [< 'Genlex.Ident(_, "set_extra_includedirs") ; 'Genlex.String(_, str) >] ->
ExtraIncludeDirs(str)
ExtraIncludeDirs(str)
| [< 'Genlex.Ident(_, "set_stdin_mode") ; str = parse_ident_or_string >] ->
if List.mem str ["t";"true"]
then StdinMode(true)
else StdinMode(false)
if List.mem str ["t";"true"]
then StdinMode(true)
else StdinMode(false)
| [< 'Genlex.Ident(_, "set_step_by_step") ; 'Genlex.Int(_, i) >] ->
StepByStep(Some i)
StepByStep(Some i)
| [< 'Genlex.Ident(_, "set_step_by_step_off") >] ->
StepByStep(None)
StepByStep(None)
| [< 'Genlex.Ident(_, "set_display_sim2chro") ;
str = parse_ident_or_string
>] ->
if List.mem str ["t";"true"]
then DisplaySim2chro(true)
else DisplaySim2chro(false)
str = parse_ident_or_string
>] ->
if List.mem str ["t";"true"]
then DisplaySim2chro(true)
else DisplaySim2chro(false)
| [< 'Genlex.Ident(_, "reset_cov_file") ;
str = parse_ident_or_string
>] ->
if List.mem str ["t";"true"]
then ResetCovFile(true)
else ResetCovFile(false)
str = parse_ident_or_string
>] ->
if List.mem str ["t";"true"]
then ResetCovFile(true)
else ResetCovFile(false)
| [< 'Genlex.Ident(_, "set_cov_file") ;'Genlex.String(_, str) >] ->
CovFile(str)
CovFile(str)
| [< 'Genlex.Ident(_, "stop_on_oracle_error") ;
str = parse_ident_or_string
>] ->
if List.mem str ["t";"true"]
then StopOnOracleError(true)
else StopOnOracleError(false)
str = parse_ident_or_string
>] ->
if List.mem str ["t";"true"]
then StopOnOracleError(true)
else StopOnOracleError(false)
| [< 'Genlex.Ident(_, "set_display_local_var") ;
str = parse_ident_or_string >] ->
if List.mem str ["t";"true"]
then DisplayLocalVar(true)
else DisplayLocalVar(false)
str = parse_ident_or_string >] ->
if List.mem str ["t";"true"]
then DisplayLocalVar(true)
else DisplayLocalVar(false)
| [< 'Genlex.Ident(_, "set_compute_volume") ;
str = parse_ident_or_string >] ->
if List.mem str ["t";"true"]
then ComputeVolume(true)
else ComputeVolume(false)
str = parse_ident_or_string >] ->
if List.mem str ["t";"true"]
then ComputeVolume(true)
else ComputeVolume(false)
| [< 'Genlex.Ident(_, "set_verbose") ; 'Genlex.Int(_, i) >] ->
Verbose(i)
Verbose(i)
| [< 'Genlex.Ident(_, "set_reactive") ; str = parse_ident_or_string >] ->
if List.mem str ["t";"true"]
then Reactive(true)
else Reactive(false)
if List.mem str ["t";"true"]
then Reactive(true)
else Reactive(false)
| [< 'Genlex.Ident(_, "set_show_step") ; str = parse_ident_or_string >] ->
if List.mem str ["t";"true"]
then ShowStep(true)
else ShowStep(false)
if List.mem str ["t";"true"]
then ShowStep(true)
else ShowStep(false)
| [< 'Genlex.Ident(_, "set_rif") ; str = parse_file_name>] -> Output(str)
| [< 'Genlex.Ident(_, "set_output") ; str = parse_file_name>] -> Output(str)
......@@ -543,10 +552,15 @@ let rec (parse_tok : tok -> t) =
| [< 'Genlex.Ident(_, "m") >] -> Man
| [< 'Genlex.Ident(_, "man") >] -> Man
| [< 'Genlex.Ident(_, "man_lurette") >] -> LurettePdfMan
| [< 'Genlex.Ident(_, "man_lutin") >] -> LutinPdfMan
| [< 'Genlex.Ident(_, "tuto") >] -> LutinPdfTuto
| [< 'Genlex.Ident(_, "tuto_lutin") >] -> LutinPdfTuto
| [< 'Genlex.Ident(_, "pack") ; file = parse_ident_or_string >] -> Pack(file)
| [< 'Genlex.Ident(_, "set_c_generator_flag");
file = parse_ident_or_string >] -> CGeneratorFlag(file)
file = parse_ident_or_string >] -> CGeneratorFlag(file)
| [< 'Genlex.Ident(_, "more") >] -> HelpMore
| [< 'Genlex.Ident(_, "help") >] -> Help
......@@ -557,59 +571,59 @@ let rec (parse_tok : tok -> t) =
and
(parse_ident_or_string : tok -> string) =
(parse_ident_or_string : tok -> string) =
fun tok ->
try
match tok with parser
| [< 'Genlex.Ident(_, id ) >] -> id
| [< 'Genlex.String(_, id )>] -> id
| [< >] -> ""
with _ ->
output_string args.ocr
"*** parse error.\n";
flush args.ocr;
""
| [< 'Genlex.Ident(_, id ) >] -> id
| [< 'Genlex.String(_, id )>] -> id
| [< >] -> ""
with _ ->
output_string args.ocr
"*** parse error.\n";
flush args.ocr;
""
and
(parse_node : tok -> string) =
(parse_node : tok -> string) =
fun tok ->
try
match tok with parser
| [< 'Genlex.Ident(_, id ) >] -> id
| [< 'Genlex.String(_, id )>] -> id
| [< >] -> ""
with _ ->
output_string args.ocr
"*** parse error: cannot parse that node name.\n";
flush args.ocr;
""
| [< 'Genlex.Ident(_, id ) >] -> id
| [< 'Genlex.String(_, id )>] -> id
| [< >] -> ""
with _ ->
output_string args.ocr
"*** parse error: cannot parse that node name.\n";
flush args.ocr;
""
and
(parse_file_name : tok -> string) =
(parse_file_name : tok -> string) =
fun tok ->
try
match tok with parser
| [< 'Genlex.String(_, str )>] -> str
| [< 'Genlex.Ident(_, id ) >] -> id
| [< >] -> ""
with _ ->
output_string args.ocr
"*** parse error: cannot parse that file name.\n";
flush args.ocr;
""
| [< 'Genlex.String(_, str )>] -> str
| [< 'Genlex.Ident(_, id ) >] -> id
| [< >] -> ""
with _ ->
output_string args.ocr
"*** parse error: cannot parse that file name.\n";
flush args.ocr;
""
and
(parse_env : tok -> string) =
(parse_env : tok -> string) =
fun tok ->
try
(
match tok with parser
(* | [< 'Genlex.Ident(_, "x") ; tail = parse_env >] -> (" x " ^ tail) *)
| [< 'Genlex.String(_, str ); tail = parse_env >] -> (str ^ " " ^tail)
(* | [< 'Genlex.Ident(_, id ) ; tail = parse_env >] -> (id ^ ".luc " ^ tail) *)
| [< _ >] -> ""
match tok with parser
(* | [< 'Genlex.Ident(_, "x") ; tail = parse_env >] -> (" x " ^ tail) *)
| [< 'Genlex.String(_, str ); tail = parse_env >] -> (str ^ " " ^tail)
(* | [< 'Genlex.Ident(_, id ) ; tail = parse_env >] -> (id ^ ".luc " ^ tail) *)
| [< _ >] -> ""
)
with e ->
output_string args.ocr (Printexc.to_string e);
output_string args.ocr
"*** Error when parsing the environment field.\n";
"*** Error when parsing the environment field.\n";
flush args.ocr;
""
......@@ -920,6 +934,9 @@ let (read : (unit -> string) -> bool) =
| HelpMore -> display2 (); true
| Man -> output_string args.ocr man ; flush args.ocr; true
| LurettePdfMan -> Util2.lurette_man (); true
| LutinPdfMan -> Util2.lutin_man (); true
| LutinPdfTuto -> Util2.lutin_tuto (); true
| CGeneratorFlag(str) ->
args.c_generator <- str; true
......
source/Lurettetop/ltopArg.ml
View file @ 1d806ea1
......@@ -28,7 +28,7 @@ let rp_help ="
If your caml program depends on library, or on other files, please generate
the f.cmxs file by yourself (cf the ocaml documentation).
[ex_exe] In the 'ec_exe' mode, lurette suppose that 'file.ec' has been compiled
[ec_exe] In the 'ec_exe' mode, lurette suppose that 'file.ec' has been compiled
into an executable that is named 'file' (for instance, via ec2c -loop).
That executable must read/write its I/O using the RIF convention.
The rationale for that mode is to be able to deal with Lustre programs that
......@@ -467,49 +467,49 @@ let rec speclist =
"--sut", Arg.String
(fun file -> args.sut <- file),
"<string>\tFile name of the system under test.";
"<string>\tFile name of the system under test [works with --old-mode only!].";
"-sut", Arg.String
(fun file -> args.sut <- file),
" <string>\n" ;
"--sut-cmd", Arg.String
(fun cmd -> args.sut_cmd <- cmd),
"<string>\tCommand that launches the system under test.";
"<string>\tCommand that launches the system under test [works with --old-mode only!].";
"-sut-cmd", Arg.String
(fun cmd -> args.sut_cmd <- cmd),
" <string>\n" ;
"--oracle-cmd", Arg.String
(fun cmd -> args.oracle_cmd <- cmd),
"<string>\tCommand that launches the oracle.";
"<string>\tCommand that launches the oracle [works with --old-mode only!].";
"-oracle-cmd", Arg.String
(fun cmd -> args.oracle_cmd <- cmd),
" <string>\n" ;
"--main-sut-node", Arg.String
(fun s -> args.sut_node <- s),
"<string>\tMain node name of the system under test.";
"<string>\tMain node name of the system under test [works with --old-mode only!].";
"-msn", Arg.String
(fun s -> args.sut_node <- s),
" <string>\n" ;
"--main-env-node", Arg.String
(fun s -> args.env_node <- s),
"<string>\tMain node name of the environment (meaningful for lutin only).";
"<string>\tMain node name of the environment (meaningful for lutin only) [works with --old-mode only!].";
"-men", Arg.String
(fun s -> args.env_node <- s),
" <string>\n" ;
"--oracle", Arg.String (fun file -> args.oracle <-
Some (file)),
"<string>\tFile name of the oracle.";
"<string>\tFile name of the oracle [works with --old-mode only!].";
"-oracle", Arg.String (fun file -> args.oracle <-
Some (file)),
" <string>\n";