Skip to content

GitLab

L
lutin
Commit 7c4feb61 authored by Erwan Jahier's avatar Erwan Jahier
Browse files
Options

lurette 0.115 Thu, 07 Nov 2002 14:19:37 +0100 by jahier 

Parent-Version:      0.114
Version-Log:

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.

Project-Description: Lurette
parent f55cbb26
Hide whitespace changes
Inline Side-by-side
Showing with 231 additions and 178 deletions
.lurette.prcs_aux
View file @ 7c4feb61
;; 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)
......
ihm/xlurette/xlurette_glade_main.ml
View file @ 7c4feb61
......@@ -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 _ ->
......
lurette.prj
View file @ 7c4feb61
;; -*- 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))
......
source/automata.ml
View file @ 7c4feb61
......@@ -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
......
source/command_line_luc_exe.ml
View file @ 7c4feb61
......@@ -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 =
......
source/command_line_luc_exe.mli
View file @ 7c4feb61
......@@ -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
......
source/control.ml
View file @ 7c4feb61
......@@ -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 ->
......
source/control.mli
View file @ 7c4feb61
......@@ -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.
......
source/env_state.ml
View file @ 7c4feb61
......@@ -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) =
......
source/env_state.mli
View file @ 7c4feb61
......@@ -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
source/luc_exe.ml
View file @ 7c4feb61
......@@ -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
......
source/lurette.ml
View file @ 7c4feb61
......@@ -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 "))
......
source/show_env.ml
View file @ 7c4feb61
......@@ -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
......
source/solver.ml
View file @ 7c4feb61
......@@ -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) *)
......
source/util.ml
View file @ 7c4feb61
......@@ -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)
(****************************************************************************)
......
test/time.exp
View file @ 7c4feb61
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