diff --git a/.lurette.prcs_aux b/.lurette.prcs_aux index 7e59073aba74097a1d8dbee551375bb036fcddec..04cda1c5420830c1a53aec3ab9b43b55546322df 100644 --- a/.lurette.prcs_aux +++ b/.lurette.prcs_aux @@ -1,7 +1,7 @@ ;; This file is automatically generated, editing may cause PRCS to do ;; REALLY bad things. (Created-By-Prcs-Version 1 3 3) -(source/automata.ml 15777 1033723811 b/47_automata.m 1.5) +(source/automata.ml 15954 1036675177 b/47_automata.m 1.6) (source/formula.mli 2805 1033397911 44_formula.ml 1.18) (test/heater_float.lus 177 1034351455 b/44_heater_flo 1.2) (test/passerelle.luc 984 1032789516 b/17_passerelle 1.8) @@ -24,7 +24,7 @@ (user-rules.skel 973 1034006019 c/25_user-rules 1.1) (source/Makefile.gen_stubs 212 1036048863 b/42_Makefile.g 1.5) (test/temp_int.luc 685 1033723811 b/50_temp_int.e 1.3) -(source/luc_exe.ml 12191 1034351455 b/32_ima_exe.ml 1.21) +(source/luc_exe.ml 12191 1036675177 b/32_ima_exe.ml 1.22) (test/heater_float.rif.exp 1485 1034951022 b/30_heater_flo 1.11) (source/graph.ml 2563 1027066799 14_graph.ml 1.7) (ihm/xlurette/makefile 1583 1036048863 c/16_makefile 1.6) @@ -36,25 +36,25 @@ (source/env.ml 8013 1027349504 16_env.ml 1.29) (demo/chaudiere/buggy_chaudiere_ctrl.lus 219 1031732392 c/10_buggy_chau 1.1) (source/Makefile.show_luc 937 1034351455 b/40_Makefile.s 1.7) -(source/env_state.mli 6734 1033125605 50_env_state. 1.24) +(source/env_state.mli 6791 1036675177 50_env_state. 1.25) (mlcuddidl/idd.ml 7061 1034006019 d/0_idd.ml 1.1) (source/print.mli 1145 1033397911 46_print.mli 1.12) (mlcuddidl/rdd.mli 7174 1034006019 c/40_rdd.mli 1.1) (test/Makefile 32 1035531408 c/0_Makefile 1.8) (source/parse_env.ml 31317 1036585364 41_parse_env. 1.31) -(ihm/xlurette/xlurette_glade_main.ml 23753 1036048863 c/12_xlurette_g 1.14) +(ihm/xlurette/xlurette_glade_main.ml 23620 1036675177 c/12_xlurette_g 1.15) (demo/chaudiere/chaudiere_oracle.lus 107 1031732392 c/8_chaudiere_ 1.1) -(source/solver.ml 31941 1036048863 39_solver.ml 1.33) +(source/solver.ml 32174 1036675177 39_solver.ml 1.34) (test/ControleurPorte.lus 3219 1032940601 c/17_Controleur 1.1) (source/gen_fake_lutin.ml 3449 1036048863 d/16_gen_fake_l 1.1) -(source/lurette.ml 14202 1035898240 12_lurette.ml 1.59) +(source/lurette.ml 14219 1036675177 12_lurette.ml 1.60) (source/Makefile 1377 1036585364 c/20_Makefile 1.9) -(source/util.ml 20341 1036048863 35_util.ml 1.34) +(source/util.ml 20779 1036675177 35_util.ml 1.35) (mlcuddidl/manager.mli 7912 1034006019 c/46_manager.ml 1.1) -(test/time.res 6325 1036585364 b/49_time.res 1.22) +(test/time.res 6326 1036675177 b/49_time.res 1.23) (doc/Interface_draft 5232 1003928781 19_Interface_ 1.1) (source/sim2chro.mli 1455 1027943375 b/23_sim2chro.m 1.5) -(source/command_line_luc_exe.mli 1082 1034006019 b/34_command_li 1.5) +(source/command_line_luc_exe.mli 1055 1036675177 b/34_command_li 1.6) (test/giro/onlyroll.lus 18298 1031732392 c/7_onlyroll.l 1.1) (source/Makefile.lucky 2003 1035531408 b/41_Makefile.i 1.8) (TAGS 9825 1007379917 21_TAGS 1.6) @@ -69,7 +69,7 @@ (cuddaux/cuddauxCompose.c 13638 1034006019 c/30_cuddauxCom 1.1) (test/porte.luc 1050 1032789516 b/16_porte.env 1.8) (make_lurette 1306 1034006019 27_make_luret 1.17) -(source/control.ml 4416 1030975996 c/4_control.ml 1.3) +(source/control.ml 4445 1036675177 c/4_control.ml 1.4) (ihm/xlurette/xlurette_glade_interface.ml 32774 1035885606 c/15_xlurette_g 1.8) (source/lurettetop.ml 30402 1036048863 c/1_lurettetop 1.22) (mlcuddidl/README 1574 1034006019 d/8_README 1.1) @@ -78,13 +78,13 @@ (source/ne.mli 2376 1033723811 c/22_ne.mli 1.1) (README 2264 1034951022 10_README 1.4) (test/vrai_tram.lus 564 1027066799 b/6_vrai_tram. 1.2) -(source/env_state.ml 20782 1036511217 51_env_state. 1.31) +(source/env_state.ml 21094 1036675177 51_env_state. 1.32) (mlcuddidl/manager_caml.c 39233 1034006019 c/45_manager_ca 1.1) (mlcuddidl/mtbdd.mli 4395 1034006019 c/43_mtbdd.mli 1.1) (source/env.mli 2027 1033738731 15_env.mli 1.16) (mlcuddidl/rdd_caml.c 41613 1034006019 c/39_rdd_caml.c 1.1) (Makefile.common.in 528 1034951022 d/12_Makefile.c 1.2) -(user-rules 14209 1036048863 c/14_myrules 1.17) +(user-rules 14217 1036675177 c/14_myrules 1.18) (doc/archi.fig 3693 1003928781 20_archi.fig 1.1) (source/lurette.mli 448 1016027474 11_lurette.ml 1.12) (source/gne.mli 1552 1033397911 b/36_gne.mli 1.4) @@ -110,7 +110,7 @@ (source/eval.mli 1395 1027066799 48_eval.mli 1.10) (mlcuddidl/mtbdd.ml 10185 1034006019 c/44_mtbdd.ml 1.1) (demo/chaudiere/chaudiere_ctrl.lus 177 1031732392 c/9_chaudiere_ 1.1) -(source/control.mli 3202 1030975671 c/3_control.ml 1.2) +(source/control.mli 3208 1036675177 c/3_control.ml 1.3) (source/formula.ml 5759 1035898240 45_formula.ml 1.22) (cuddaux/Makefile 3091 1034006019 c/35_Makefile 1.1) (doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1) @@ -130,16 +130,16 @@ (test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1) (configure.in 5208 1034351455 d/11_configure. 1.1) (cuddaux/cuddauxBridge.c 6099 1034006019 c/31_cuddauxBri 1.1) -(source/show_env.ml 3436 1034351455 43_show_env.m 1.14) +(source/show_env.ml 3594 1036675177 43_show_env.m 1.15) (mlcuddidl/Changes 64 1034006019 d/10_Changes 1.1) (source/parse_poc.ml 7093 1036048863 d/15_parse_poc. 1.1) (cuddaux/cuddauxAddIte.c 12812 1034006019 c/32_cuddauxAdd 1.1) (source/rnumsolver.mli 2198 1033732198 b/26_rnumsolver 1.9) (source/sim2chro.ml 2721 1033397911 b/24_sim2chro.m 1.14) -(source/command_line_luc_exe.ml 2786 1034006019 b/33_command_li 1.7) +(source/command_line_luc_exe.ml 2759 1036675177 b/33_command_li 1.8) (mlcuddidl/cudd_caml.h 1210 1034006019 d/2_cudd_caml. 1.1) (source/value.ml 2355 1033723811 c/23_value.ml 1.1) -(test/time.exp 6325 1036585364 b/48_time.exp 1.19) +(test/time.exp 6326 1036675177 b/48_time.exp 1.20) (test/giro/allocator.lus 1087 1031732392 c/5_allocator. 1.1) (lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2) (mlcuddidl/idd.mli 5470 1034006019 c/51_idd.mli 1.1) diff --git a/ihm/xlurette/xlurette_glade_main.ml b/ihm/xlurette/xlurette_glade_main.ml index 319499520fb54e0f08b6949ab15f0c8e3aef48ef..b1144ac501880aaed8521e1420bce94291c5d88e 100644 --- a/ihm/xlurette/xlurette_glade_main.ml +++ b/ihm/xlurette/xlurette_glade_main.ml @@ -182,7 +182,12 @@ class customized_callbacks = object(self) method show_env_button_clicked () = - let env = self#top_xlurette#env_name#text in + let env0 = self#top_xlurette#env_name#text in + let env = + if Util.get_extension env0 = ".lut" + then ((Util.remove_extension env0) ^ ".luc") + else env0 + in let cmd_show = ("set_env \"" ^ env ^ "\"\n show \n") in output_string oc cmd_show ; @@ -465,20 +470,14 @@ class customized_callbacks = object(self) method read_commands line = let lexer = Genlex.make_lexer [] in - let (remove_extension : string -> string) = - fun str -> - let file_ext = Filename.basename str - and dir = Filename.dirname str in - let file = try Filename.chop_extension file_ext with _ -> file_ext in - if dir = "." then file else (Filename.concat dir file) - in + let (parse_file_name : tok -> string) = fun tok -> try match tok with parser | [< 'Genlex.String str >] -> - if str = "" then "" else remove_extension str + if str = "" then "" else Util.remove_extension str | [< 'Genlex.Ident id >] -> id | [< >] -> "" with _ -> diff --git a/lurette.prj b/lurette.prj index 39d95105c504d276e0719f321e342c5434a5425e..652888a7d02cf4a9a76a3322109870edccf39863 100644 --- a/lurette.prj +++ b/lurette.prj @@ -1,19 +1,23 @@ ;; -*- Prcs -*- (Created-By-Prcs-Version 1 3 3) (Project-Description "Lurette") -(Project-Version lurette 0 114) -(Parent-Version lurette 0 113) +(Project-Version lurette 0 115) +(Parent-Version lurette 0 114) (Version-Log " -source/parse_env.ml: - When floats output vars are not constraint, use [-10^11, 10^11] - as default domain. The rational for this change is that sim2chro - does not seem to be able to print bigger floats (probably because - it does not understand the 123e+234 notation. +source/automata.ml: + Fix a bug where esp loops were not always cutted properly in some cases. + +source/show_env.ml: + Truncate too long for in the dot output (which bugs dot or gv). + +ihm/xlurette/xlurette_glade_main.ml: + Accept both .lut or .lut files as anv files, and make the show buttons + behave properly in both cases. ") (New-Version-Log "" ) -(Checkin-Time "Wed, 06 Nov 2002 13:22:44 +0100") +(Checkin-Time "Thu, 07 Nov 2002 14:19:37 +0100") (Checkin-Login jahier) (Populate-Ignore ()) (Project-Keywords) @@ -25,14 +29,14 @@ source/parse_env.ml: ;; Sources files for luc_exe (source/luc_exe.mli (lurette/b/31_ima_exe.ml 1.2 644)) - (source/luc_exe.ml (lurette/b/32_ima_exe.ml 1.21 644)) + (source/luc_exe.ml (lurette/b/32_ima_exe.ml 1.22 644)) - (source/command_line_luc_exe.ml (lurette/b/33_command_li 1.7 644)) - (source/command_line_luc_exe.mli (lurette/b/34_command_li 1.5 644)) + (source/command_line_luc_exe.ml (lurette/b/33_command_li 1.8 644)) + (source/command_line_luc_exe.mli (lurette/b/34_command_li 1.6 644)) ;; Sources files for lurette only (source/lurette.mli (lurette/11_lurette.ml 1.12 644)) - (source/lurette.ml (lurette/12_lurette.ml 1.59 644)) + (source/lurette.ml (lurette/12_lurette.ml 1.60 644)) (source/command_line.ml (lurette/b/20_command_li 1.10 644)) (source/command_line.mli (lurette/b/21_command_li 1.9 644)) @@ -44,10 +48,10 @@ source/parse_env.ml: (source/env.mli (lurette/15_env.mli 1.16 644)) (source/env.ml (lurette/16_env.ml 1.29 644)) - (source/util.ml (lurette/35_util.ml 1.34 444)) + (source/util.ml (lurette/35_util.ml 1.35 444)) (source/solver.mli (lurette/38_solver.mli 1.13 644)) - (source/solver.ml (lurette/39_solver.ml 1.33 644)) + (source/solver.ml (lurette/39_solver.ml 1.34 644)) (source/rnumsolver.mli (lurette/b/26_rnumsolver 1.9 644)) (source/rnumsolver.ml (lurette/b/27_rnumsolver 1.14 644)) @@ -56,7 +60,7 @@ source/parse_env.ml: (source/parse_env.ml (lurette/41_parse_env. 1.31 644)) (source/show_env.mli (lurette/42_show_env.m 1.8 644)) - (source/show_env.ml (lurette/43_show_env.m 1.14 644)) + (source/show_env.ml (lurette/43_show_env.m 1.15 644)) (source/formula.mli (lurette/44_formula.ml 1.18 644)) (source/formula.ml (lurette/45_formula.ml 1.22 644)) @@ -67,11 +71,11 @@ source/parse_env.ml: (source/eval.mli (lurette/48_eval.mli 1.10 644)) (source/eval.ml (lurette/49_eval.ml 1.13 644)) - (source/env_state.mli (lurette/50_env_state. 1.24 644)) - (source/env_state.ml (lurette/51_env_state. 1.31 644)) + (source/env_state.mli (lurette/50_env_state. 1.25 644)) + (source/env_state.ml (lurette/51_env_state. 1.32 644)) (source/automata.mli (lurette/b/46_automata.m 1.3 644)) - (source/automata.ml (lurette/b/47_automata.m 1.5 644)) + (source/automata.ml (lurette/b/47_automata.m 1.6 644)) (source/sim2chro.mli (lurette/b/23_sim2chro.m 1.5 644)) (source/sim2chro.ml (lurette/b/24_sim2chro.m 1.14 644)) @@ -82,8 +86,8 @@ source/parse_env.ml: (source/lurettetop.ml (lurette/c/1_lurettetop 1.22 644)) (source/gen_stubs.ml (lurette/24_generate_l 1.41 644)) - (source/control.mli (lurette/c/3_control.ml 1.2 644)) - (source/control.ml (lurette/c/4_control.ml 1.3 644)) + (source/control.mli (lurette/c/3_control.ml 1.3 644)) + (source/control.ml (lurette/c/4_control.ml 1.4 644)) (source/constraint.mli (lurette/c/18_constraint 1.4 644)) (source/constraint.ml (lurette/c/19_constraint 1.4 644)) @@ -106,7 +110,7 @@ source/parse_env.ml: (Makefile.common.in (lurette/d/12_Makefile.c 1.2 644)) (OcamlMakefile (lurette/17_OcamlMakef 1.45 644)) (Makefile.lurette (lurette/b/38_Makefile.l 1.15 644)) - (user-rules (lurette/c/14_myrules 1.17 644)) + (user-rules (lurette/c/14_myrules 1.18 644)) (user-rules.skel (lurette/c/25_user-rules 1.1 644)) (Makefile (lurette/d/13_Makefile 1.1 644)) @@ -133,8 +137,8 @@ source/parse_env.ml: (lurette.depfull.dot (lurette/b/5_lurette.de 1.2 644)) (TAGS (lurette/21_TAGS 1.6 644)) - (test/time.exp (lurette/b/48_time.exp 1.19 644)) - (test/time.res (lurette/b/49_time.res 1.22 644)) + (test/time.exp (lurette/b/48_time.exp 1.20 644)) + (test/time.res (lurette/b/49_time.res 1.23 644)) ;; Various files used for testing purposes (test/usager.luc (lurette/b/14_usager.env 1.9 644)) @@ -172,7 +176,7 @@ source/parse_env.ml: (test/Makefile (lurette/c/0_Makefile 1.8 644)) ;; xlurette - (ihm/xlurette/xlurette_glade_main.ml (lurette/c/12_xlurette_g 1.14 644)) + (ihm/xlurette/xlurette_glade_main.ml (lurette/c/12_xlurette_g 1.15 644)) (ihm/xlurette/xlurette.glade (lurette/c/13_xlurette.g 1.9 644)) (ihm/xlurette/xlurette_glade_interface.ml (lurette/c/15_xlurette_g 1.8 644)) (ihm/xlurette/makefile (lurette/c/16_makefile 1.6 644)) diff --git a/source/automata.ml b/source/automata.ml index 1774d4c7cb4c83e95ae9a492e9d23d0b996228b7..c993ecae89a7586ad161e228f4d682fc6400053a 100644 --- a/source/automata.ml +++ b/source/automata.ml @@ -119,15 +119,20 @@ let rec (get_automaton: node -> t) = and st = Env_state.ctrl_state () and t = Graph.create () in - get_automaton_acc g n n t st; + get_automaton_acc g (IntSet.singleton n) n t st; (* Show_env.graph_to_dot [] [] "toto" (intset_to_string) *) (* (arc_info_static_to_string) t; *) (IntSet.singleton n, t) and - (get_automaton_acc: dyn_trans_list -> node -> node -> stat_trans_list + (get_automaton_acc: dyn_trans_list -> IntSet.t -> node -> stat_trans_list -> Control.state -> unit) = - fun g n0 n t st0 -> - (** n0 is the node get_automaton was initially called from. *) + fun g handled_nodes n t st0 -> + + (* + handled_nodes is the set of nodes get_automaton was called with. This + set is used to detect loop of eps transitions. + + *) let tnl = Graph.get_list_of_target_nodes g n in (* Add the current transitions and draw weights *) List.iter @@ -141,7 +146,7 @@ and ( match f with Eps -> - if nt <> n0 then + if not (IntSet.mem nt handled_nodes) then (* In order to cut epsilon loops *) ( Graph.add_trans @@ -149,7 +154,7 @@ and (IntSet.singleton n) (get_weight w st1, f, None) (IntSet.singleton nt) ; - get_automaton_acc g n0 nt t st1 + get_automaton_acc g (IntSet.add nt handled_nodes) nt t st1 ) | Form(f2) -> if diff --git a/source/command_line_luc_exe.ml b/source/command_line_luc_exe.ml index 1c990145946b84a74329e832bc5a18fdaa03f9ea..b4f5b9bc56bc9e5e63f09a0deb413d4b22f6f763 100644 --- a/source/command_line_luc_exe.ml +++ b/source/command_line_luc_exe.ml @@ -12,8 +12,7 @@ type optionsT = { mutable show_automata : bool ; mutable boot : bool ; - mutable user_seed : int ; - mutable verbose : bool + mutable user_seed : int } type cmd_line_optionT = diff --git a/source/command_line_luc_exe.mli b/source/command_line_luc_exe.mli index 3177e5bac2598c2d6eaea888292feb7a83846c0e..a56faf838fc406fd17feb9887e57abc92ebb0ac0 100644 --- a/source/command_line_luc_exe.mli +++ b/source/command_line_luc_exe.mli @@ -15,8 +15,7 @@ type optionsT = { mutable show_automata : bool ; mutable boot : bool ; - mutable user_seed : int ; - mutable verbose : bool + mutable user_seed : int } val usage : string diff --git a/source/control.ml b/source/control.ml index ef0056f415438107bcfcaf3a4367d0feda6ffe08..274b61a815ca3661102296b7267af66509907438 100644 --- a/source/control.ml +++ b/source/control.ml @@ -60,7 +60,7 @@ let (print_state : state -> unit) = fun id (i, recov) -> output_string stderr ("\t" ^ id ^ " = "); output_string stderr (string_of_int i); - output_string stderr (" (" ^ (string_of_recov recov) ^ ")\n"); + output_string stderr (" (" ^ (string_of_recov recov) ^ ")\n") in output_string stderr ("Control state: \n"); StringMap.iter pp st; @@ -79,7 +79,7 @@ let (set : string -> int -> state -> state) = (* exported *) let (set_between : string -> int -> int -> int -> state -> state) = fun id i min max st -> - StringMap.add id (i, Some(min, max)) st + StringMap.add id (i, Some(min, max)) st (* exported *) @@ -111,7 +111,9 @@ let (dec : string -> state -> state) = let (return : string -> state -> int) = fun id st -> try fst (StringMap.find id st) - with _ -> failwith ("*** " ^ id ^ " is an undefined control expression.\n") + with _ -> + print_state st; + failwith ("*** " ^ id ^ " is an undefined control expression.\n") (* exported *) let (return_comp : string -> state -> int) = fun id st -> diff --git a/source/control.mli b/source/control.mli index e9d01b795531c5a9e3aaacc662bfd4bf3b7ca6c5..f84157c1ecd4f91233abd389c27b923d9ba2393c 100644 --- a/source/control.mli +++ b/source/control.mli @@ -57,7 +57,7 @@ val is_recoverable : string -> state -> bool too. Therefore, if: - a loop is garded by the value of v, - [v] is bound to 0 at the current step, - - no satisfiable formula can drawn in the end branch of the + - no satisfiable formula can be drawn in the end branch of the loop, then, since [v] could have been drawn to a bigger value (7, 8, or 9), @@ -66,7 +66,7 @@ val is_recoverable : string -> state -> bool Similarly, if: - [v] is not bound to 0 at the current step, but at least 2 steps have performed - - the formula in the body of the loop not satisfiable + - the formula in the body of the loop is not satisfiable then it means that the end branch can be tried. diff --git a/source/env_state.ml b/source/env_state.ml index 9852c744c7a5515e945a7384a3f5cff374cc219d..05379125fede6d4bf31a49e316f89814aa674c07 100644 --- a/source/env_state.ml +++ b/source/env_state.ml @@ -101,6 +101,8 @@ type env_stateT = { mutable draw_mode : draw_mode; (** Whether we draw on verteces, edges, or inside the convex hull of solution *) + mutable verbose : bool; + mutable pre: subst list; (** Stores the values of pre variables. *) mutable input : env_in ; @@ -127,9 +129,10 @@ let (env_state:env_stateT) = { local = []; current_nodes = []; snt = Hashtbl.create 3; - ce_label = Hashtbl.create 0 ; + ce_label = Hashtbl.create 0 ; ctrl_state = Control.new_state (); draw_mode = Inside; + verbose = false; bdd_tbl = Hashtbl.create 0; bdd_tbl_global = Hashtbl.create 0; linear_constraint_to_index = Hashtbl.create 0; @@ -247,6 +250,18 @@ let (set_draw_mode: draw_mode -> unit) = env_state.draw_mode <- dm +(****************************************************************************) +(* Exported *) +let (verbose: unit -> bool) = + fun _ -> + env_state.verbose + +(* Exported *) +let (set_verbose: bool -> unit) = + fun b -> + env_state.verbose <- b + + (****************************************************************************) let (pre: unit -> subst list) = diff --git a/source/env_state.mli b/source/env_state.mli index e3c22e1487485281ef8ce61828ed869c2c4d53a2..43995421cfb53948ac3c3b29c35a38e0f98175c6 100644 --- a/source/env_state.mli +++ b/source/env_state.mli @@ -196,3 +196,6 @@ val set_draw_mode: draw_mode -> unit (** outputs various statistic about the size of env_state tables *) val dump_env_state_stat : out_channel -> unit + +val set_verbose: bool -> unit +val verbose: unit -> bool diff --git a/source/luc_exe.ml b/source/luc_exe.ml index fb487e6357446b3a0fca9a365a20b2c1c4d97e47..2c2d8a0bb13a55d0aa6a83e913f41387070fd433 100644 --- a/source/luc_exe.ml +++ b/source/luc_exe.ml @@ -23,8 +23,7 @@ open Command_line_luc_exe let (options:Command_line_luc_exe.optionsT) = { show_automata = false ; user_seed = 0 ; - boot = false ; - verbose = false + boot = false } (*------------------------------------------------------------------------*) @@ -242,7 +241,7 @@ let rec (main : unit -> 'a) = Failure(errmsg) -> output_string stderr errmsg | e -> (* Env_state.dump_env_state_stat (); *) - print_string Command_line_luc_exe.usage ; +(* print_string Command_line_luc_exe.usage ; *) raise e and @@ -255,7 +254,7 @@ and ShowAut -> options.show_automata <- true ; (n+1) | NoShowAut -> options.show_automata <- false ; (n+1) | Boot -> options.boot <- true ; (n+1) - | Verbose -> options.verbose <- true ; (n+1) + | Verbose -> Env_state.set_verbose true ; (n+1) | Seed -> let str = (Sys.argv.(n+1)) in options.user_seed <- cmd_line_string_to_int str @@ -369,7 +368,7 @@ and let nl = List.flatten previous_nodes in let _ = - if options.verbose then + if Env_state.verbose () then ( List.iter (fun n -> @@ -380,7 +379,7 @@ and ) ; print_string ("\n# step " ^ (string_of_int t)) ; - if options.verbose then + if Env_state.verbose () then ( print_string "("; if (List.length nl) > 1 diff --git a/source/lurette.ml b/source/lurette.ml index 5305c804f909ba29c284a9b8311b04cec391fc74..b6ab27b80690d5e33d16c4823c2f0ede4832ff5d 100644 --- a/source/lurette.ml +++ b/source/lurette.ml @@ -137,12 +137,12 @@ let rec (main : unit -> 'a) = res with Failure(errmsg) -> - if options.verbose then Env_state.dump_env_state_stat stdout; + if Env_state.verbose () then Env_state.dump_env_state_stat stdout; print_string errmsg; flush stdout; exit 2 | e -> - if options.verbose then Env_state.dump_env_state_stat stdout; + if Env_state.verbose () then Env_state.dump_env_state_stat stdout; print_string (Printexc.to_string e); flush stdout; exit 2 @@ -164,7 +164,7 @@ and | NoSim2chro -> options.display_sim2chro <- false ; (n+1) | NoOracle -> options.oracle <- false ; (n+1) - | Verbose -> options.verbose <- true ; (n+1) + | Verbose -> Env_state.set_verbose true; (n+1) | ShowStep -> options.show_step <- true ; (n+1) | Inside -> Env_state.set_draw_mode Env_state.Inside ; (n+1) | Edges -> Env_state.set_draw_mode Env_state.Edges ; (n+1) @@ -310,7 +310,7 @@ and let _ = if options.show_step then output_string stdout ("\n--- step " ^ (string_of_int t) ^ ":\n"); - if options.verbose then + if Env_state.verbose () then List.iter (fun n -> output_string stdout ("current nodes:" ^ (string_of_int n) ^ "\n ")) diff --git a/source/show_env.ml b/source/show_env.ml index 6c2e752f5c8e01bbb390421000185f2061c29d41..acc8394f8fcfe4bd2ac303ba82e9f7f74b342c90 100644 --- a/source/show_env.ml +++ b/source/show_env.ml @@ -112,10 +112,17 @@ let (graph_to_dot: 'node list -> 'node list -> string -> (* Exported *) + +let arc_to_string_trunc arc = + let str = Formula.arc_info_to_string arc in + if String.length str <= 40 + then str + else ((String.sub str 0 40) ^ " ...") + let (luc_to_dot: Formula.node list -> Formula.node list -> string -> (Formula.node, Formula.arc_info) Graph.t -> unit) = fun pnodes cnodes str graph -> - graph_to_dot pnodes cnodes str string_of_int Formula.arc_info_to_string graph + graph_to_dot pnodes cnodes str string_of_int arc_to_string_trunc graph diff --git a/source/solver.ml b/source/solver.ml index 2df86e7c18bec7f11b5aa06a69ad0787a60c7a9a..7601b305529d64570f21123d01253aa0616c2604 100644 --- a/source/solver.ml +++ b/source/solver.ml @@ -507,6 +507,14 @@ and (* Exported *) let rec (is_satisfiable: env_in -> formula -> bool) = fun input f -> + +(* let _ = if Env_state.verbose () then *) +(* ( *) +(* print_string (formula_to_string f); *) +(* print_string " ...test whether this formula is satisfiable...\n"; *) +(* flush stdout *) +(* ) *) +(* in *) let (bdd, _) = formula_to_bdd input f in not (Bdd.is_false bdd) && ( @@ -973,13 +981,15 @@ let (draw : vn list -> vnt list -> Bdd.t -> Bdd.t -> subst list * subst list) = (* Exported *) let (solve_formula: env_in -> int -> formula -> formula -> vnt list -> (subst list * subst list) list option) = - fun input p f bool_vars_to_gen_f num_vars_to_gen -> - -(* let _ = *) -(* print_string (formula_to_string f); *) -(* print_string "\n"; *) -(* flush stdout *) -(* in *) + fun input p f bool_vars_to_gen_f num_vars_to_gen -> + + let _ = if Env_state.verbose () then + ( + print_string (formula_to_string f); + print_string "\n"; + flush stdout + ) + in let bdd = (* The bdd of f has necessarily been computed (by is_satisfiable) *) diff --git a/source/util.ml b/source/util.ml index fcf7f482a50856b1a90bac2d74498b927ccc6483..1078be295a0d1853e06c91ef7a353ea35637ac75 100644 --- a/source/util.ml +++ b/source/util.ml @@ -15,7 +15,9 @@ let lurette_path = Sys.getenv "LURETTE_PATH" with _ -> print_string "Environment var LURETTE_PATH is unset.\n"; - exit 2 + print_string "You can either quit (ctrl-c), set it, and restart or type it here now.\nLURETTE_PATH=" ; + let path = read_line ()in + if path = "" then exit 2 else path (** [rm x l] returns [l] without [x]. @@ -33,7 +35,7 @@ let (string_to_string_list : string -> string list) = fun str -> Str.split (Str.regexp " ") str -let _ = assert ((string_to_string_list "a aa aaa aa") = ["a";"aa";"aaa";"aa"]) +let _ = assert ((string_to_string_list "a aa aaa aa") = ["a";"aa";"aaa";"aa"]) (** [rm_first x l] returns [l] without the left-most occurence of [x]. @@ -589,6 +591,15 @@ let (get_extension : string -> string) = let _ = assert ((get_extension "/home/jahier/toto.ml") = ".ml") + +let (remove_extension : string -> string) = + fun str -> + let file_ext = Filename.basename str + and dir = Filename.dirname str in + let file = try Filename.chop_extension file_ext with _ -> file_ext in + if dir = "." then file else (Filename.concat dir file) + + (****************************************************************************) diff --git a/test/time.exp b/test/time.exp index ed2f9456c34e33150ef546fd119aaead6ed43f75..ecf39247b4db4f32ae20be0d8447efd38330b8a0 100644 --- a/test/time.exp +++ b/test/time.exp @@ -1,15 +1,15 @@ - Command being timed: "/tmp/lurette53/lurette 10000 1 1 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/tram.luc /home/jahier/lurette/test/usager.luc /home/jahier/lurette/test/porte.luc /home/jahier/lurette/test/passerelle.luc" - User time (seconds): 10.62 - System time (seconds): 0.07 - Percent of CPU this job got: 85% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:12.52 + Command being timed: "/tmp/lurette56/lurette 10000 1 1 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/tram.luc /home/jahier/lurette/test/usager.luc /home/jahier/lurette/test/porte.luc /home/jahier/lurette/test/passerelle.luc" + User time (seconds): 11.03 + System time (seconds): 0.09 + Percent of CPU this job got: 86% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:12.90 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 260 + Major (requiring I/O) page faults: 258 Minor (reclaiming a frame) page faults: 2457 Voluntary context switches: 0 Involuntary context switches: 0 @@ -22,19 +22,19 @@ Page size (bytes): 4096 Exit status: 0 - Command being timed: "/tmp/lurette53/lurette 10 100 100 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/tram.luc /home/jahier/lurette/test/usager.luc /home/jahier/lurette/test/porte.luc /home/jahier/lurette/test/passerelle.luc" - User time (seconds): 23.30 - System time (seconds): 0.45 - Percent of CPU this job got: 93% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:25.50 + Command being timed: "/tmp/lurette56/lurette 10 100 100 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/tram.luc /home/jahier/lurette/test/usager.luc /home/jahier/lurette/test/porte.luc /home/jahier/lurette/test/passerelle.luc" + User time (seconds): 23.43 + System time (seconds): 0.40 + Percent of CPU this job got: 88% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:26.91 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 260 - Minor (reclaiming a frame) page faults: 17783 + Major (requiring I/O) page faults: 258 + Minor (reclaiming a frame) page faults: 17650 Voluntary context switches: 0 Involuntary context switches: 0 Swaps: 0 @@ -46,19 +46,19 @@ Page size (bytes): 4096 Exit status: 0 - Command being timed: "/tmp/lurette53/lurette 100 50 50 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/tram.luc /home/jahier/lurette/test/usager.luc /home/jahier/lurette/test/porte.luc /home/jahier/lurette/test/passerelle.luc" - User time (seconds): 51.92 - System time (seconds): 0.81 + Command being timed: "/tmp/lurette56/lurette 100 50 50 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/tram.luc /home/jahier/lurette/test/usager.luc /home/jahier/lurette/test/porte.luc /home/jahier/lurette/test/passerelle.luc" + User time (seconds): 51.85 + System time (seconds): 0.88 Percent of CPU this job got: 92% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:56.77 + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:56.79 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 260 - Minor (reclaiming a frame) page faults: 37361 + Major (requiring I/O) page faults: 258 + Minor (reclaiming a frame) page faults: 37909 Voluntary context switches: 0 Involuntary context switches: 0 Swaps: 0 @@ -70,19 +70,19 @@ Page size (bytes): 4096 Exit status: 0 - Command being timed: "/tmp/lurette53/lurette 10000 1 1 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_float.luc" - User time (seconds): 3.59 - System time (seconds): 0.11 - Percent of CPU this job got: 90% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:04.10 + Command being timed: "/tmp/lurette56/lurette 10000 1 1 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_float.luc" + User time (seconds): 3.58 + System time (seconds): 0.10 + Percent of CPU this job got: 82% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:04.48 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 279 - Minor (reclaiming a frame) page faults: 2451 + Major (requiring I/O) page faults: 278 + Minor (reclaiming a frame) page faults: 2452 Voluntary context switches: 0 Involuntary context switches: 0 Swaps: 0 @@ -94,19 +94,19 @@ Page size (bytes): 4096 Exit status: 0 - Command being timed: "/tmp/lurette53/lurette 10 100 100 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_float.luc" - User time (seconds): 8.42 - System time (seconds): 0.22 + Command being timed: "/tmp/lurette56/lurette 10 100 100 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_float.luc" + User time (seconds): 8.57 + System time (seconds): 0.18 Percent of CPU this job got: 92% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:09.38 + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:09.45 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 279 - Minor (reclaiming a frame) page faults: 7476 + Major (requiring I/O) page faults: 278 + Minor (reclaiming a frame) page faults: 7281 Voluntary context switches: 0 Involuntary context switches: 0 Swaps: 0 @@ -118,19 +118,19 @@ Page size (bytes): 4096 Exit status: 0 - Command being timed: "/tmp/lurette53/lurette 10000 1 1 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_int.luc" - User time (seconds): 3.02 - System time (seconds): 0.08 - Percent of CPU this job got: 89% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:03.44 + Command being timed: "/tmp/lurette56/lurette 10000 1 1 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_int.luc" + User time (seconds): 3.05 + System time (seconds): 0.09 + Percent of CPU this job got: 81% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:03.84 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 274 - Minor (reclaiming a frame) page faults: 2450 + Major (requiring I/O) page faults: 272 + Minor (reclaiming a frame) page faults: 2452 Voluntary context switches: 0 Involuntary context switches: 0 Swaps: 0 @@ -142,19 +142,19 @@ Page size (bytes): 4096 Exit status: 0 - Command being timed: "/tmp/lurette53/lurette 10 100 100 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_int.luc" - User time (seconds): 9.79 - System time (seconds): 0.22 - Percent of CPU this job got: 85% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:11.66 + Command being timed: "/tmp/lurette56/lurette 10 100 100 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_int.luc" + User time (seconds): 10.21 + System time (seconds): 0.12 + Percent of CPU this job got: 81% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:12.66 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 274 - Minor (reclaiming a frame) page faults: 7807 + Major (requiring I/O) page faults: 272 + Minor (reclaiming a frame) page faults: 7678 Voluntary context switches: 0 Involuntary context switches: 0 Swaps: 0 diff --git a/test/time.res b/test/time.res index ed2f9456c34e33150ef546fd119aaead6ed43f75..ecf39247b4db4f32ae20be0d8447efd38330b8a0 100644 --- a/test/time.res +++ b/test/time.res @@ -1,15 +1,15 @@ - Command being timed: "/tmp/lurette53/lurette 10000 1 1 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/tram.luc /home/jahier/lurette/test/usager.luc /home/jahier/lurette/test/porte.luc /home/jahier/lurette/test/passerelle.luc" - User time (seconds): 10.62 - System time (seconds): 0.07 - Percent of CPU this job got: 85% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:12.52 + Command being timed: "/tmp/lurette56/lurette 10000 1 1 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/tram.luc /home/jahier/lurette/test/usager.luc /home/jahier/lurette/test/porte.luc /home/jahier/lurette/test/passerelle.luc" + User time (seconds): 11.03 + System time (seconds): 0.09 + Percent of CPU this job got: 86% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:12.90 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 260 + Major (requiring I/O) page faults: 258 Minor (reclaiming a frame) page faults: 2457 Voluntary context switches: 0 Involuntary context switches: 0 @@ -22,19 +22,19 @@ Page size (bytes): 4096 Exit status: 0 - Command being timed: "/tmp/lurette53/lurette 10 100 100 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/tram.luc /home/jahier/lurette/test/usager.luc /home/jahier/lurette/test/porte.luc /home/jahier/lurette/test/passerelle.luc" - User time (seconds): 23.30 - System time (seconds): 0.45 - Percent of CPU this job got: 93% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:25.50 + Command being timed: "/tmp/lurette56/lurette 10 100 100 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/tram.luc /home/jahier/lurette/test/usager.luc /home/jahier/lurette/test/porte.luc /home/jahier/lurette/test/passerelle.luc" + User time (seconds): 23.43 + System time (seconds): 0.40 + Percent of CPU this job got: 88% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:26.91 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 260 - Minor (reclaiming a frame) page faults: 17783 + Major (requiring I/O) page faults: 258 + Minor (reclaiming a frame) page faults: 17650 Voluntary context switches: 0 Involuntary context switches: 0 Swaps: 0 @@ -46,19 +46,19 @@ Page size (bytes): 4096 Exit status: 0 - Command being timed: "/tmp/lurette53/lurette 100 50 50 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/tram.luc /home/jahier/lurette/test/usager.luc /home/jahier/lurette/test/porte.luc /home/jahier/lurette/test/passerelle.luc" - User time (seconds): 51.92 - System time (seconds): 0.81 + Command being timed: "/tmp/lurette56/lurette 100 50 50 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/tram.luc /home/jahier/lurette/test/usager.luc /home/jahier/lurette/test/porte.luc /home/jahier/lurette/test/passerelle.luc" + User time (seconds): 51.85 + System time (seconds): 0.88 Percent of CPU this job got: 92% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:56.77 + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:56.79 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 260 - Minor (reclaiming a frame) page faults: 37361 + Major (requiring I/O) page faults: 258 + Minor (reclaiming a frame) page faults: 37909 Voluntary context switches: 0 Involuntary context switches: 0 Swaps: 0 @@ -70,19 +70,19 @@ Page size (bytes): 4096 Exit status: 0 - Command being timed: "/tmp/lurette53/lurette 10000 1 1 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_float.luc" - User time (seconds): 3.59 - System time (seconds): 0.11 - Percent of CPU this job got: 90% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:04.10 + Command being timed: "/tmp/lurette56/lurette 10000 1 1 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_float.luc" + User time (seconds): 3.58 + System time (seconds): 0.10 + Percent of CPU this job got: 82% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:04.48 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 279 - Minor (reclaiming a frame) page faults: 2451 + Major (requiring I/O) page faults: 278 + Minor (reclaiming a frame) page faults: 2452 Voluntary context switches: 0 Involuntary context switches: 0 Swaps: 0 @@ -94,19 +94,19 @@ Page size (bytes): 4096 Exit status: 0 - Command being timed: "/tmp/lurette53/lurette 10 100 100 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_float.luc" - User time (seconds): 8.42 - System time (seconds): 0.22 + Command being timed: "/tmp/lurette56/lurette 10 100 100 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_float.luc" + User time (seconds): 8.57 + System time (seconds): 0.18 Percent of CPU this job got: 92% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:09.38 + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:09.45 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 279 - Minor (reclaiming a frame) page faults: 7476 + Major (requiring I/O) page faults: 278 + Minor (reclaiming a frame) page faults: 7281 Voluntary context switches: 0 Involuntary context switches: 0 Swaps: 0 @@ -118,19 +118,19 @@ Page size (bytes): 4096 Exit status: 0 - Command being timed: "/tmp/lurette53/lurette 10000 1 1 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_int.luc" - User time (seconds): 3.02 - System time (seconds): 0.08 - Percent of CPU this job got: 89% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:03.44 + Command being timed: "/tmp/lurette56/lurette 10000 1 1 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_int.luc" + User time (seconds): 3.05 + System time (seconds): 0.09 + Percent of CPU this job got: 81% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:03.84 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 274 - Minor (reclaiming a frame) page faults: 2450 + Major (requiring I/O) page faults: 272 + Minor (reclaiming a frame) page faults: 2452 Voluntary context switches: 0 Involuntary context switches: 0 Swaps: 0 @@ -142,19 +142,19 @@ Page size (bytes): 4096 Exit status: 0 - Command being timed: "/tmp/lurette53/lurette 10 100 100 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_int.luc" - User time (seconds): 9.79 - System time (seconds): 0.22 - Percent of CPU this job got: 85% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:11.66 + Command being timed: "/tmp/lurette56/lurette 10 100 100 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_int.luc" + User time (seconds): 10.21 + System time (seconds): 0.12 + Percent of CPU this job got: 81% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:12.66 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 274 - Minor (reclaiming a frame) page faults: 7807 + Major (requiring I/O) page faults: 272 + Minor (reclaiming a frame) page faults: 7678 Voluntary context switches: 0 Involuntary context switches: 0 Swaps: 0 diff --git a/user-rules b/user-rules index 7b9e2e5d6d66e866523378cdaedcc425702846d1..06d95d7aef72b1efb6ff4989103e8dfa467505b0 100644 --- a/user-rules +++ b/user-rules @@ -16,7 +16,7 @@ export OCAMLDOT # Generates emacs tags tags: - $(OTAGS) -v $(ALL_SOURCES) ; cp TAGS ../source + $(OTAGS) -v $(SOURCES_LURETTE_LIB) ; cp TAGS ../source # Generates the modules dependency graph using ocamldot # (results in lurette.dep.ps and lurette.depfull.ps).