Commit 819bb7c5 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Look if the current control state is final or not in order to exit

with an error code of 0 or 2.
parent bd9c508e
......@@ -613,6 +613,16 @@ let (is_node_transient : LucParse.node -> t -> bool) =
flush stdout;
assert false
(* exported *)
let (is_node_final : LucParse.node -> t -> bool) =
fun n prog ->
try (Hashtbl.find prog.node n).node_type = Final
with Not_found ->
print_string ("Node " ^ n ^ " not found.\n");
flush stdout;
assert false
(* exported *)
let (get_original_name : LucParse.node -> LucParse.node) =
fun n ->
......
......@@ -33,6 +33,7 @@ type t = {
val make : string option -> string list -> t
val is_node_transient : LucParse.node -> t -> bool
val is_node_final : LucParse.node -> t -> bool
(** exploit the internal naming convention to get the original name (XXX beurk). *)
val get_original_name : LucParse.node -> LucParse.node
......@@ -84,7 +84,7 @@ let rec (main : unit -> 'a) =
raise e
and
(get_luc_exe_options: int -> int) =
(get_luc_exe_options: int -> int) =
fun n ->
try
begin
......@@ -96,9 +96,9 @@ and
| Verbose ->
let str = (Sys.argv.(n+1)) in
options.verb <- (cmd_line_string_to_int str
("*** Error when calling lurette: an " ^
"integer is expected after the " ^
"option --verbose\n")) ;
("*** Error when calling lurette: an " ^
"integer is expected after the " ^
"option --verbose\n")) ;
n+2
| Locals -> options.locals <- true ; (n+1)
| Help -> print_string Command_line_luc_exe.usage; exit 0
......@@ -115,24 +115,24 @@ and
| StepNb ->
let str = (Sys.argv.(n+1)) in
options.max_step_number <- (Some (cmd_line_string_to_int str
("*** Error when calling lurette: an " ^
"integer is expected after the " ^
"option --step-number (or -l)\n")));
("*** Error when calling lurette: an " ^
"integer is expected after the " ^
"option --step-number (or -l)\n")));
n+2
| Precision ->
let str = (Sys.argv.(n+1)) in
Util.precision := (cmd_line_string_to_int str
("*** Error when calling lurette: an " ^
"integer is expected after the " ^
"option --precision\n"));
("*** Error when calling lurette: an " ^
"integer is expected after the " ^
"option --precision\n"));
Util.update_eps ();
n+2
| Seed ->
let str = (Sys.argv.(n+1)) in
options.user_seed <- Some (cmd_line_string_to_int str
("*** Error when calling luc_exe: an " ^
"integer is expected after the " ^
"option --with-seed (or -seed)\n")) ;
("*** Error when calling luc_exe: an " ^
"integer is expected after the " ^
"option --with-seed (or -seed)\n")) ;
n+2
| ComputeVolume ->
options.compute_volume <- true ; (n+1)
......@@ -144,12 +144,12 @@ and
end
with Not_found -> n
and
(** Returns the environment file names given at top-level into a
list of list.
(** Returns the environment file names given at top-level into a
list of list.
Also set the lurette command line options if any.
Also set the lurette command line options if any.
*)
(get_env_from_args: int -> string list -> string list) =
(get_env_from_args: int -> string list -> string list) =
fun n file_l ->
if (n = arg_nb) then file_l
else
......@@ -171,7 +171,7 @@ and
get_env_from_args (n+1) (arg::file_l)
and
(main2 : unit -> 'a) =
(main2 : unit -> 'a) =
fun _ ->
(* Clean up tables as non-reg assert stuff migth have filled them *)
......@@ -201,33 +201,33 @@ and
in
let _ =
pid_oracle :=
if options.oracle = "" then 0 else
let args_str_oracle = options.oracle in
let arg_list_oracle0 = string_to_string_list args_str_oracle in
let arg_list_oracle =
match arg_list_oracle0 with
"ecexe"::tail ->
if
(* force the use of -r with ecexe *)
List.mem "-r" tail
then
arg_list_oracle0
else
"ecexe"::"-r"::tail
| _ -> arg_list_oracle0
in
let prog_oracle = List.hd arg_list_oracle in
let args_oracle = Array.of_list arg_list_oracle in
let pid = Unix.create_process prog_oracle args_oracle
oracle_stdin_in oracle_stdout_out Unix.stderr
in
List.iter (fun x -> output_string stderr (x ^ " ")) arg_list_oracle;
output_string stderr "\n";
output_string stderr (
"\nThe oracle Pid is " ^ (string_of_int pid) ^ "\n");
flush stderr;
pid
if options.oracle = "" then 0 else
let args_str_oracle = options.oracle in
let arg_list_oracle0 = string_to_string_list args_str_oracle in
let arg_list_oracle =
match arg_list_oracle0 with
"ecexe"::tail ->
if
(* force the use of -r with ecexe *)
List.mem "-r" tail
then
arg_list_oracle0
else
"ecexe"::"-r"::tail
| _ -> arg_list_oracle0
in
let prog_oracle = List.hd arg_list_oracle in
let args_oracle = Array.of_list arg_list_oracle in
let pid = Unix.create_process prog_oracle args_oracle
oracle_stdin_in oracle_stdout_out Unix.stderr
in
List.iter (fun x -> output_string stderr (x ^ " ")) arg_list_oracle;
output_string stderr "\n";
output_string stderr (
"\nThe oracle Pid is " ^ (string_of_int pid) ^ "\n");
flush stderr;
pid
in
(* Initialisation of the random engine *)
......@@ -282,7 +282,10 @@ and
"# No transition is labelled by a satisfiable formula.\n" ^
"# The Lucky automata is blocked.\n");
flush stdout;
exit 2
if init_state.s.is_final init_state.d.ctrl_state then
exit 0
else
exit 2
in
print_string ("\n#step 1\n");
print_string "\n#outs ";
......@@ -302,14 +305,14 @@ and
flush stdout
and
main_loop t state =
main_loop t state =
let step_str =
(
("#step " ^ (string_of_int t)) ^
(if state.d.verbose >= 1 then
(" (" ^ (Prog.ctrl_state_to_string_long state.d.ctrl_state) ^ "):")
else "") ^ "\n"
(if state.d.verbose >= 1 then
(" (" ^ (Prog.ctrl_state_to_string_long state.d.ctrl_state) ^ "):")
else "") ^ "\n"
)
in
let _ =
......@@ -331,7 +334,10 @@ and
"# No transition is labelled by a satisfiable formula.\n" ^
"# The Lucky automata is blocked.\n");
flush stdout;
exit 2
if state.s.is_final state.d.ctrl_state then
exit 0
else
exit 2
in
let rec read_oracle _ =
let res = Util.string_to_string_list (input_line oracle_ic) in
......@@ -356,7 +362,7 @@ and
print_string "\n#outs ";
Rif.write stdout next_state.s.Prog.out_vars out ;
if options.locals then (
print_string "\n#locs ";
Rif.write stdout next_state.s.Prog.loc_vars loc
......
......@@ -93,12 +93,9 @@ let (maybe_update_one_pre_var : env_in -> env_out -> env_loc -> subst list ->
(* E.g., at the second step, input vars migth still not
be available if the env starts to generate outputs. *)
(** [update_pre input output local] Updates the values of pre
(** [update_pre input output local] Updates the values of pre
variables (updating [env_state.pre]) with [input], [output], and
[local]. *)
let (update_pre: env_in -> env_out -> env_loc -> Prog.state -> subst list) =
fun input output local state ->
let maybe_pre =
......
......@@ -282,6 +282,7 @@ let (solve : bool_expr -> solutions_set) =
initial_ctrl_state = [];
output_var_names = [List.map Var.name vars] ;
get_wtl = (fun _ _ -> assert false);
is_final = (fun _ -> assert false);
gen_dot = (fun _ _ _ -> assert false);
}
}
......
......@@ -721,7 +721,10 @@ and
| FGen.NoMoreFormula ->
output_string stdout ("# " ^ (Prog.ctrl_state_to_string_long state.d.ctrl_state));
flush stdout;
lurette_exit 2
if state.s.is_final state.d.ctrl_state then
lurette_exit 0
else
lurette_exit 2
in
(* Extracts the outputs and locals from the couple *)
......@@ -750,7 +753,10 @@ and
with FGen.NoMoreFormula ->
output_string stdout ("# : " ^ (Prog.ctrl_state_to_string_long state.d.ctrl_state));
flush stdout;
lurette_exit 2
if state.s.is_final state.d.ctrl_state then
lurette_exit 0
else
lurette_exit 2
in
let output = List.rev_append luciole_outputs output in
let sut_output = Sut.step output in
......
......@@ -14,6 +14,8 @@
type atomic_ctrl_state = LucParse.node
type ctrl_state = atomic_ctrl_state list
(****************************************************************************)
type dyn_weight = V of int | Infin
......@@ -48,6 +50,7 @@ type t = {
reactive : bool ; (* A scorie to remove. At least, it should be a list of bool *)
get_wtl : Var.env_in -> state -> ctrl_state -> wt list;
is_final : ctrl_state list -> bool;
gen_dot : ctrl_state list -> ctrl_state list -> string -> int
}
......@@ -259,6 +262,9 @@ let luc_to_dot graph csl1 csl2 file =
let (make_luc : string option -> string list -> t) =
fun pp_opt files ->
let luc_prog = LucProg.make pp_opt files in
let is_final_atomic n =
LucProg.is_node_final n luc_prog
in
{
reactive = luc_prog.LucProg.reactive ;
bool_vars_to_gen = luc_prog.LucProg.bool_vars_to_gen ;
......@@ -272,11 +278,12 @@ let (make_luc : string option -> string list -> t) =
initial_ctrl_state = luc_prog.LucProg.initial_ctrl_state ;
get_wtl = get_wtl luc_prog;
is_final = List.for_all (List.for_all is_final_atomic);
gen_dot = luc_to_dot luc_prog.LucProg.graph;
}
(****************************************************************************)
(***************************************************************************)
(* exported *)
let rec (make_state : string option -> string list -> state) =
fun pp_opt files ->
......
......@@ -12,6 +12,7 @@
type atomic_ctrl_state
type ctrl_state = atomic_ctrl_state list
(** Weigths, once evaluated (no more memories nor inputs) *)
type dyn_weight = V of int | Infin
......@@ -24,7 +25,7 @@ and children =
(** The Digested Lucky program (form the static part of the state).
Holds a list of independant programs (i.e., they don't share ant I/O).
Holds a list of independant programs (i.e., they don't share any I/O).
*)
type t = {
initial_ctrl_state : ctrl_state list;
......@@ -32,7 +33,7 @@ type t = {
out_vars : Exp.var list;
loc_vars : Exp.var list;
ext_func_tbl : Exp.ext_func_tbl;
memories_names : (string * Exp.var) list ;
memories_names : (string * Exp.var) list ; (* redundant, but useful *)
bool_vars_to_gen : Exp.var list list ;
num_vars_to_gen : Exp.var list list ;
output_var_names : Var.name list list ; (* redundant, but useful *)
......@@ -41,8 +42,9 @@ type t = {
(** Computes the weigthed tree from the static program *)
get_wtl : Var.env_in -> state -> ctrl_state -> wt list;
is_final : ctrl_state list -> bool;
(** to generate a pdf dot file for the source. Return the error code
(** to generate a pdf dot file for the source. Returns the error code
of the system call (dot -Tpdf). *)
gen_dot : ctrl_state list -> ctrl_state list -> string -> int
}
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment