diff --git a/src/lv6MainArgs.ml b/src/lv6MainArgs.ml index 49007e343034a00ab3d48fb0ad1b6631adc54e15..508f2f0ae863dc2846a21d9aa7e602198ba8c087 100644 --- a/src/lv6MainArgs.ml +++ b/src/lv6MainArgs.ml @@ -30,6 +30,7 @@ type t = { mutable oc : Pervasives.out_channel; mutable tlex : bool; mutable exec : bool; + mutable precision : int option; } (* Those are really too boring to be functionnal (used in all over the places) *) @@ -77,6 +78,7 @@ let (make_opt : unit -> t) = oc = Pervasives.stdout; tlex = false; exec = false; + precision = None; } @@ -303,6 +305,11 @@ let mkoptab (opt:t) : unit = ( (Arg.Unit (fun () -> opt.run_unit_test<-true)) ["Run embedded unit tests"] ; + mkopt opt ~hide:true + ["--precision"] + (Arg.Int (fun i -> opt.precision <- Some i)) + ["Number of digits after ther dot used to print floats"] + ; mkopt opt ~hide:true ["--nonreg-test"] (Arg.Unit (fun () -> global_opt.nonreg_test <- true)) diff --git a/src/lv6MainArgs.mli b/src/lv6MainArgs.mli index 269207d6373049444b84ddfcc275a92c5ad8ab97..c230dfcf78bac44a6992e198381d42ecbcf06111 100644 --- a/src/lv6MainArgs.mli +++ b/src/lv6MainArgs.mli @@ -22,6 +22,7 @@ type t = { mutable oc : Pervasives.out_channel; mutable tlex : bool; mutable exec : bool; + mutable precision : int option; } (* Those are really too boring to be functionnal (used in all over the places) *) diff --git a/src/main.ml b/src/main.ml index 30c3e79540b336a423ba89a9a2205e4f670d3feb..8c4335f4dd2a3a51ea1c40dcc7c1fad6ac613143 100644 --- a/src/main.ml +++ b/src/main.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 25/04/2013 (at 17:09) by Erwan Jahier> *) +(* Time-stamp: <modified the 26/04/2013 (at 10:51) by Erwan Jahier> *) open Verbose open AstV6 @@ -55,18 +55,23 @@ let (gen_autotest_files : LicPrg.t -> Ident.idref option -> Lv6MainArgs.t -> uni let msk, zesoc = Lic2soc.f lic_prg (Lic.node_key_of_idref main_node) in msk, zesoc, main_node in - let my_type_to_string t = + let my_type_to_string range_flag t = (* Remove the module name to have correct Lutin and lv4 type decl *) let str = Data.type_to_string t in let idref = Ident.idref_of_string str in - idref.Ident.id_id + idref.Ident.id_id ^ (if range_flag then ( + match t with + | Data.Real -> " [-10000.0;10000.0]" + | Data.Int -> " [-10000;10000]" + | _ -> "" + ) else "") in let soc = try Soc.SocMap.find msk zesoc with Not_found -> assert false in let invars,outvars=soc.Soc.profile in let invars = SocExec.expand_profile invars in let outvars = SocExec.expand_profile outvars in - let invars_str = List.map (fun (n,t) -> n^":"^(my_type_to_string t)) invars in - let outvars_str = List.map (fun (n,t) -> n^":"^(my_type_to_string t)) outvars in + let invars_str = List.map (fun (n,t) -> n^":"^(my_type_to_string true t)) invars in + let outvars_str = List.map (fun (n,t) -> n^":"^(my_type_to_string false t)) outvars in let name = main_node.Ident.id_id in let lutin_file_name = ("_"^name^"_env.lut") in let oc = open_out lutin_file_name in @@ -78,12 +83,12 @@ let (gen_autotest_files : LicPrg.t -> Ident.idref option -> Lv6MainArgs.t -> uni output_string stdout (lutin_file_name ^" generated.\n"); let oracle_file_name = ("_"^name^"_oracle.lus") in let oc = open_out oracle_file_name in -(* let invars,outvars=soc.Soc.profile in *) + (* let invars,outvars=soc.Soc.profile in *) let locals = List.map (fun (n,t) -> n^"_bis",t) outvars in - let invars_str = List.map (fun (n,t) -> n^":"^(my_type_to_string t)) invars in - let outvars_str = List.map (fun (n,t) -> n^":"^(my_type_to_string t)) outvars in + let invars_str = List.map (fun (n,t) -> n^":"^(my_type_to_string false t)) invars in + let outvars_str = List.map (fun (n,t) -> n^":"^(my_type_to_string false t)) outvars in let prg = "node "^name^"_oracle("^(String.concat ";" (invars_str@outvars_str)) in - let locals_str = List.map (fun (n,t) -> n^":"^(my_type_to_string t)) locals in + let locals_str = List.map (fun (n,t) -> n^":"^(my_type_to_string false t)) locals in let ok = (* avoid name clash*) let all_vars = List.map fst (List.rev_append (List.rev_append locals invars) outvars) in let rec gen_ok str = if List.mem str all_vars then gen_ok ("_"^str) else str in @@ -92,11 +97,15 @@ let (gen_autotest_files : LicPrg.t -> Ident.idref option -> Lv6MainArgs.t -> uni let prg = prg ^") returns("^ok^":bool;"^(String.concat ";" locals_str)^");\nlet\n" in let locals_name = List.map fst locals in let invars_name = List.map fst invars in - let outvars_name = List.map fst outvars in let prg = prg^" ("^(String.concat "," locals_name)^") = "^name in let prg = prg^"("^(String.concat "," invars_name)^");\n "^ok^" = (" in - let prg = try prg^(String.concat " and\n \t\t " (List.map2 (fun x y -> x^"="^y) - outvars_name locals_name)) ^ ");\ntel;\n" + let var_to_equals (x,t) (y,_) = + match t with + | Data.Real -> x^"-"^y^" < 0.1 and "^ y^"-"^x^" < 0.1 " + | _ -> x^"="^y + in + let prg = try prg^(String.concat " and\n \t\t " + (List.map2 var_to_equals locals outvars)) ^ ");\ntel;\n" with _ -> assert false in Lv6util.dump_entete oc; diff --git a/src/socExec.ml b/src/socExec.ml index f57b3d70e7d5943b592fbdf5aa3b53966ba6cc90..ee9b64695d73695725133ad61917418aab4da04c 100644 --- a/src/socExec.ml +++ b/src/socExec.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 24/04/2013 (at 11:31) by Erwan Jahier> *) +(* Time-stamp: <modified the 26/04/2013 (at 09:42) by Erwan Jahier> *) open Soc open Data @@ -288,9 +288,9 @@ let (read_soc_input : var list -> Data.vntl -> out_channel -> substs -> substs) let s:Data.subst list = Rif_base.read stdin (Some oc) exp_vntl_i_str in add_data_subst vntl_i s ctx_s -let rec (loop_step : Soc.tbl -> Soc.var list -> Data.vntl -> Data.vntl +let rec (loop_step : Lv6MainArgs.t -> Soc.tbl -> Soc.var list -> Data.vntl -> Data.vntl -> Soc.t -> SocExecValue.ctx -> int -> out_channel -> unit) = - fun soc_tbl vntl_i exp_vntl_i_str exp_vntl_o_str soc ctx step_nb oc -> + fun opt soc_tbl vntl_i exp_vntl_i_str exp_vntl_o_str soc ctx step_nb oc -> Rif_base.write oc ("\n#step " ^ (string_of_int step_nb)^"\n"); let ctx = { ctx with s = read_soc_input vntl_i exp_vntl_i_str oc ctx.s } in let step = match soc.step with [step] -> step | _ -> assert false in @@ -299,11 +299,12 @@ let rec (loop_step : Soc.tbl -> Soc.var list -> Data.vntl -> Data.vntl (* dump_substs ctx.s; *) let s = SocExecValue.filter_top_subst ctx.s in let s = List.flatten(List.map expand_subst s) in + let f2s = SocUtils.my_string_of_float_precision opt.Lv6MainArgs.precision in Rif_base.write oc " #outs "; - Rif_base.write_outputs oc (SocUtils.my_string_of_float_precision 6) exp_vntl_o_str s; + Rif_base.write_outputs oc f2s exp_vntl_o_str s; Rif_base.flush oc; Verbose.exe ~flag:dbg (fun () -> dump_substs ctx.s; flush stdout); - loop_step soc_tbl vntl_i exp_vntl_i_str exp_vntl_o_str soc ctx (step_nb+1) oc + loop_step opt soc_tbl vntl_i exp_vntl_i_str exp_vntl_o_str soc ctx (step_nb+1) oc let (f : Lv6MainArgs.t -> Soc.tbl -> Soc.key -> unit) = fun opt soc_tbl sk -> @@ -325,7 +326,7 @@ let (f : Lv6MainArgs.t -> Soc.tbl -> Soc.key -> unit) = Lv6util.dump_entete oc; Rif_base.write_interface oc exp_vntl_i_str exp_vntl_o_str None None; Rif_base.flush oc; - try loop_step soc_tbl (fst soc.profile) exp_vntl_i_str exp_vntl_o_str soc ctx 1 oc + try loop_step opt soc_tbl (fst soc.profile) exp_vntl_i_str exp_vntl_o_str soc ctx 1 oc with Rif_base.Bye -> close_out oc diff --git a/src/socUtils.ml b/src/socUtils.ml index 0d5f6a9e3473bdd475b6d3ac24517fa26d391273..c49f0a90cf986c337e0beb02a0196d22a700de71 100644 --- a/src/socUtils.ml +++ b/src/socUtils.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 12/04/2013 (at 16:06) by Erwan Jahier> *) +(** Time-stamp: <modified the 26/04/2013 (at 09:42) by Erwan Jahier> *) open Soc @@ -334,7 +334,10 @@ let _ = assert (gen_index_list 5 = [0;1;2;3;4]) external format_float: string -> float -> string = "caml_format_float" (* external format_float: string -> float -> string = "format_float" *) -let (my_string_of_float_precision : int -> float -> string) = - fun p f -> - let precision_str = string_of_int p in - format_float ("%." ^ precision_str ^ "f") f +let (my_string_of_float_precision : int option -> float -> string) = + fun p_opt f -> + match p_opt with + | None -> string_of_float f + | Some p -> + let precision_str = string_of_int p in + format_float ("%." ^ precision_str ^ "f") f diff --git a/src/socUtils.mli b/src/socUtils.mli index 96602d5a2f069b4cf93cbd1310ae1a6501e293c0..7b81391c564773df3817a1210dbcb89431a07f59 100644 --- a/src/socUtils.mli +++ b/src/socUtils.mli @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 12/04/2013 (at 16:06) by Erwan Jahier> *) +(** Time-stamp: <modified the 26/04/2013 (at 09:43) by Erwan Jahier> *) (** Donne toute les méthodes d'un composant. *) @@ -47,4 +47,4 @@ val find_no_exc : Soc.key -> Soc.tbl -> Soc.t (* gen_index_list 5 = [0;1;2;3;4] *) val gen_index_list : int -> int list -val my_string_of_float_precision : int -> float -> string +val my_string_of_float_precision : int option -> float -> string diff --git a/test/lus2lic.sum b/test/lus2lic.sum index 12758ffad1426a6f468c976655a199767170666a..4f29fb2c5eab0f41d4cd06dd0048ce5f9a45a602 100644 --- a/test/lus2lic.sum +++ b/test/lus2lic.sum @@ -1,4 +1,4 @@ -Test Run By jahier on Thu Apr 25 17:19:15 2013 +Test Run By jahier on Fri Apr 26 10:51:37 2013 Native configuration is i686-pc-linux-gnu === lus2lic tests === @@ -20,7 +20,7 @@ PASS: ../utils/test_lus2lic_no_node should_work/argos.lus PASS: ./lus2lic {-o /tmp/ck5.lic should_work/ck5.lus} PASS: ./lus2lic {-ec -o /tmp/ck5.ec should_work/ck5.lus} PASS: ./ec2c {-o /tmp/ck5.c /tmp/ck5.ec} -FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/ck5.lus +UNRESOLVED: Time out: ../utils/test_lus2lic_no_node should_work/ck5.lus PASS: ./lus2lic {-o /tmp/assertion.lic should_work/assertion.lus} PASS: ./lus2lic {-ec -o /tmp/assertion.ec should_work/assertion.lus} PASS: ./ec2c {-o /tmp/assertion.c /tmp/assertion.ec} @@ -116,7 +116,7 @@ FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node shou PASS: ./lus2lic {-o /tmp/deSimone.lic should_work/deSimone.lus} PASS: ./lus2lic {-ec -o /tmp/deSimone.ec should_work/deSimone.lus} PASS: ./ec2c {-o /tmp/deSimone.c /tmp/deSimone.ec} -PASS: ../utils/test_lus2lic_no_node should_work/deSimone.lus +FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/deSimone.lus PASS: ./lus2lic {-o /tmp/bug2.lic should_work/bug2.lus} PASS: ./lus2lic {-ec -o /tmp/bug2.ec should_work/bug2.lus} PASS: ./ec2c {-o /tmp/bug2.c /tmp/bug2.ec} @@ -180,7 +180,7 @@ FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node shou PASS: ./lus2lic {-o /tmp/iter.lic should_work/iter.lus} PASS: ./lus2lic {-ec -o /tmp/iter.ec should_work/iter.lus} PASS: ./ec2c {-o /tmp/iter.c /tmp/iter.ec} -FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/iter.lus +PASS: ../utils/test_lus2lic_no_node should_work/iter.lus PASS: ./lus2lic {-o /tmp/call05.lic should_work/call05.lus} PASS: ./lus2lic {-ec -o /tmp/call05.ec should_work/call05.lus} PASS: ./ec2c {-o /tmp/call05.c /tmp/call05.ec} @@ -413,7 +413,7 @@ FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node shou PASS: ./lus2lic {-o /tmp/bad_call03.lic should_work/bad_call03.lus} PASS: ./lus2lic {-ec -o /tmp/bad_call03.ec should_work/bad_call03.lus} PASS: ./ec2c {-o /tmp/bad_call03.c /tmp/bad_call03.ec} -FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/bad_call03.lus +PASS: ../utils/test_lus2lic_no_node should_work/bad_call03.lus PASS: ./lus2lic {-o /tmp/onlyroll.lic should_work/onlyroll.lus} PASS: ./lus2lic {-ec -o /tmp/onlyroll.ec should_work/onlyroll.lus} PASS: ./ec2c {-o /tmp/onlyroll.c /tmp/onlyroll.ec} @@ -469,7 +469,7 @@ FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node shou PASS: ./lus2lic {-o /tmp/initial.lic should_work/initial.lus} PASS: ./lus2lic {-ec -o /tmp/initial.ec should_work/initial.lus} PASS: ./ec2c {-o /tmp/initial.c /tmp/initial.ec} -FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/initial.lus +PASS: ../utils/test_lus2lic_no_node should_work/initial.lus PASS: ./lus2lic {-o /tmp/declaration.lic should_work/declaration.lus} PASS: ./lus2lic {-ec -o /tmp/declaration.ec should_work/declaration.lus} PASS: ./ec2c {-o /tmp/declaration.c /tmp/declaration.ec} @@ -652,7 +652,7 @@ FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node shou PASS: ./lus2lic {-o /tmp/iterFibo.lic should_work/iterFibo.lus} PASS: ./lus2lic {-ec -o /tmp/iterFibo.ec should_work/iterFibo.lus} PASS: ./ec2c {-o /tmp/iterFibo.c /tmp/iterFibo.ec} -FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/iterFibo.lus +PASS: ../utils/test_lus2lic_no_node should_work/iterFibo.lus PASS: ./lus2lic {-o /tmp/morel2.lic should_work/morel2.lus} PASS: ./lus2lic {-ec -o /tmp/morel2.ec should_work/morel2.lus} PASS: ./ec2c {-o /tmp/morel2.c /tmp/morel2.ec} @@ -792,7 +792,7 @@ PASS: ../utils/test_lus2lic_no_node should_work/_N_uu.lus PASS: ./lus2lic {-o /tmp/X2.lic should_work/X2.lus} PASS: ./lus2lic {-ec -o /tmp/X2.ec should_work/X2.lus} PASS: ./ec2c {-o /tmp/X2.c /tmp/X2.ec} -UNRESOLVED: Time out: ../utils/test_lus2lic_no_node should_work/X2.lus +FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/X2.lus PASS: ./lus2lic {-o /tmp/alias.lic should_work/alias.lus} PASS: ./lus2lic {-ec -o /tmp/alias.ec should_work/alias.lus} PASS: ./ec2c {-o /tmp/alias.c /tmp/alias.ec} @@ -904,7 +904,7 @@ FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node shou PASS: ./lus2lic {-o /tmp/iterate.lic should_work/iterate.lus} PASS: ./lus2lic {-ec -o /tmp/iterate.ec should_work/iterate.lus} PASS: ./ec2c {-o /tmp/iterate.c /tmp/iterate.ec} -FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/iterate.lus +PASS: ../utils/test_lus2lic_no_node should_work/iterate.lus PASS: ./lus2lic {-o /tmp/overload.lic should_work/overload.lus} PASS: ./lus2lic {-ec -o /tmp/overload.ec should_work/overload.lus} PASS: ./ec2c {-o /tmp/overload.c /tmp/overload.ec} @@ -1045,8 +1045,8 @@ XPASS: Test bad programs (semantics): lus2lic {-o /tmp/bug.lic should_fail/seman === lus2lic Summary === -# of expected passes 823 -# of unexpected failures 144 +# of expected passes 827 +# of unexpected failures 140 # of unexpected successes 11 # of expected failures 37 # of unresolved testcases 18 diff --git a/utils/test_lus2lic_no_node b/utils/test_lus2lic_no_node index 107672c4a0eada7e307f15a6db19d7efa4490d75..4eb44ca2515de5a5aef2a1ce1fb9261bf852040a 100755 --- a/utils/test_lus2lic_no_node +++ b/utils/test_lus2lic_no_node @@ -40,7 +40,7 @@ else exit 2 fi if -./lurettetop -rp "sut:v6:$lustre_file:$node" -rp "env:lutin:$env" -rp "oracle:ec:$oracle.ec:$oracle" -go -l 10 -ns2c --stop-on-oracle-error; +./lurettetop -p 6 -seed 42 -rp "sut:v6:$lustre_file:$node" -rp "env:lutin:$env" -rp "oracle:ec:$oracle.ec:$oracle" -go -l 10 -ns2c --stop-on-oracle-error; then echo "lurettetop ok" else