Commit dba4992a authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.34 Tue, 19 Feb 2002 10:40:58 +0100 by jahier

Parent-Version:      0.33
Version-Log:

Fix a bug when computing the power of two.

Project-Description: Lurette
parent ee4eb63d
......@@ -5,11 +5,11 @@
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 2296 1014051154 51_env_state. 1.9)
(source/graph.ml 2476 1012914629 14_graph.ml 1.3)
(source/util.ml 9037 1014051154 35_util.ml 1.9)
(source/util.ml 9166 1014111658 35_util.ml 1.10)
(source/wtree.ml 9644 1014051154 b/1_wtree.ml 1.8)
(source/solver.ml 12350 1014051154 39_solver.ml 1.9)
(source/solver.ml 12281 1014111658 39_solver.ml 1.10)
(source/command_line.ml 3971 1014048376 b/20_command_li 1.3)
(source/lurette.ml 11178 1014051154 12_lurette.ml 1.20)
(source/lurette.ml 11196 1014111658 12_lurette.ml 1.21)
(source/solver.mli 969 1014048376 38_solver.mli 1.7)
(source/env.mli 2506 1013445149 15_env.mli 1.8)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
......@@ -23,10 +23,10 @@
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(source/sim2chro.mli 1421 1014051154 b/23_sim2chro.m 1.2)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/eval.ml 7903 1013445149 49_eval.ml 1.4)
(source/eval.ml 7930 1014111658 49_eval.ml 1.5)
(source/gen_stubs.ml 32194 1013519411 24_generate_l 1.16)
(source/parse_env.ml 9215 1012914629 41_parse_env. 1.4)
(test/lurette.rif.exp 4746 1014048376 b/22_lurette.ri 1.3)
(test/lurette.rif.exp 4746 1014111658 b/22_lurette.ri 1.4)
(interface/TAGS 1956 1007380262 26_TAGS 1.3)
(source/sim2chro.ml 2668 1014051154 b/24_sim2chro.m 1.2)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
......@@ -40,7 +40,7 @@
(source/eval.mli 1668 1013445149 48_eval.mli 1.4)
(README 74 1011881677 10_README 1.2)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(OcamlMakefile 18458 1014048376 17_OcamlMakef 1.15)
(OcamlMakefile 18631 1014111658 17_OcamlMakef 1.16)
(source/show_env.ml 2961 1014048376 43_show_env.m 1.3)
(test/tram.env 806 1012914629 b/15_tram.env 1.1)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
......@@ -48,11 +48,11 @@
(interface/Makefile 197 1008255910 25_Makefile 1.6)
(source/show_env.mli 826 1014048376 42_show_env.m 1.4)
(test/tram_simple.h 1746 1013519411 b/25_tram_simpl 1.1)
(Makefile 1641 1014051154 18_Makefile 1.19)
(Makefile 1645 1014111658 18_Makefile 1.20)
(test/vrai_tram.c 3060 1012914629 b/8_vrai_tram. 1.2)
(source/print.mli 597 1014048376 46_print.mli 1.5)
(source/graph.mli 1499 1014048376 13_graph.mli 1.5)
(source/formula.ml 3689 1013445149 45_formula.ml 1.5)
(source/lurette.mli 396 1012914629 11_lurette.ml 1.10)
(source/print.ml 5316 1014048376 47_print.ml 1.6)
(source/print.ml 5340 1014111658 47_print.ml 1.7)
(test/vrai_tram.h 2468 1012914629 b/7_vrai_tram. 1.2)
......@@ -2,8 +2,8 @@ LURETTE_DIR = ..
OCAMLMAKEFILE = $(LURETTE_DIR)/OcamlMakefile
OCAMLFLAGS = -noassert -unsafe
OCAMLNCFLAGS = -inline 10
# OCAMLFLAGS = -noassert -unsafe
# OCAMLNCFLAGS = -inline 10
-include ./lurette.in
......
......@@ -5,7 +5,7 @@
# For updates see:
# http://miss.wu-wien.ac.at/~mottl/ocaml_sources
#
# $Id: OcamlMakefile 1.15 Mon, 18 Feb 2002 17:06:16 +0100 jahier $
# $Id: OcamlMakefile 1.16 Tue, 19 Feb 2002 10:40:58 +0100 jahier $
#
###########################################################################
......@@ -502,6 +502,10 @@ try:
# ./lurette 10 2 2 tram.env usager.env porte.env passerelle.env | sim2chro -ecran
./lurette 10 2 2 tram.env usager.env porte.env passerelle.env
vroum:
$(LURETTE_DIR)/make_lurette ControleurPorte vrai_tram nc; \
times ./lurette 4500 1 1 tram.env usager.env porte.env passerelle.env -seed 1014422484 -ns2c --no-oracle
# Non regression test
test:
$(LURETTE_DIR)/make_lurette ControleurPorte vrai_tram; \
......@@ -511,14 +515,14 @@ test:
# In order to time profile lurette
gprof:
$(LURETTE_DIR)/make_lurette ControleurPorte vrai_tram pnc; \
./lurette 100 10 10 tram.env x usager.env x porte.env x passerelle.env -seed 1013219512 -ns2c ;\
./lurette 4500 1 1 tram.env usager.env porte.env passerelle.env -seed 1014422484 -ns2c ;\
gprof ./lurette > lurette.gprof ; \
echo " ---> The result of the profiling is in the lurette.gprof file"
# In order to time profile lurette
ocamlprof:
$(LURETTE_DIR)/make_lurette ControleurPorte vrai_tram pbc; \
./lurette 100 10 10 tram.env usager.env porte.env passerelle.env -seed 1013219512 -ns2c ;\
./lurette 4500 1 1 tram.env usager.env porte.env passerelle.env -seed 1014422484 -ns2c ;\
ocamlprof ../source/solver.ml > prof/solver.count.ml ; \
ocamlprof ../source/wtree.ml > prof/wtree.count.ml ; \
ocamlprof ../source/env.ml > prof/env.count.ml ; \
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 33)
(Parent-Version lurette 0 32)
(Project-Version lurette 0 34)
(Parent-Version lurette 0 33)
(Version-Log "
Avoid recomputing everytime the list of output vars by storing it
in an env_state field.
Fix a bug when computing the power of two.
")
(New-Version-Log "")
(Checkin-Time "Mon, 18 Feb 2002 17:52:34 +0100")
(Checkin-Time "Tue, 19 Feb 2002 10:40:58 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -20,7 +19,7 @@ in an env_state field.
;; Sources files
(source/lurette.mli (lurette/11_lurette.ml 1.10 644))
(source/lurette.ml (lurette/12_lurette.ml 1.20 644))
(source/lurette.ml (lurette/12_lurette.ml 1.21 644))
(source/graph.mli (lurette/13_graph.mli 1.5 644))
(source/graph.ml (lurette/14_graph.ml 1.3 644))
......@@ -28,10 +27,10 @@ in an env_state field.
(source/env.mli (lurette/15_env.mli 1.8 644))
(source/env.ml (lurette/16_env.ml 1.14 644))
(source/util.ml (lurette/35_util.ml 1.9 644))
(source/util.ml (lurette/35_util.ml 1.10 644))
(source/solver.mli (lurette/38_solver.mli 1.7 644))
(source/solver.ml (lurette/39_solver.ml 1.9 644))
(source/solver.ml (lurette/39_solver.ml 1.10 644))
(source/parse_env.mli (lurette/40_parse_env. 1.3 644))
(source/parse_env.ml (lurette/41_parse_env. 1.4 644))
......@@ -43,10 +42,10 @@ in an env_state field.
(source/formula.ml (lurette/45_formula.ml 1.5 644))
(source/print.mli (lurette/46_print.mli 1.5 644))
(source/print.ml (lurette/47_print.ml 1.6 644))
(source/print.ml (lurette/47_print.ml 1.7 644))
(source/eval.mli (lurette/48_eval.mli 1.4 644))
(source/eval.ml (lurette/49_eval.ml 1.4 644))
(source/eval.ml (lurette/49_eval.ml 1.5 644))
(source/env_state.mli (lurette/50_env_state. 1.8 644))
(source/env_state.ml (lurette/51_env_state. 1.9 644))
......@@ -63,8 +62,8 @@ in an env_state field.
(source/gen_stubs.ml (lurette/24_generate_l 1.16 644))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.15 644))
(Makefile (lurette/18_Makefile 1.19 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.16 644))
(Makefile (lurette/18_Makefile 1.20 644))
(test/Makefile (../Makefile) :symlink)
(interface/Makefile (lurette/25_Makefile 1.6 644))
(make_lurette (lurette/27_make_luret 1.7 744))
......@@ -101,7 +100,7 @@ in an env_state field.
(test/vrai_tram.c (lurette/b/8_vrai_tram. 1.2 644))
(test/tram_simple.h (lurette/b/25_tram_simpl 1.1 644))
(test/lurette.rif.exp (lurette/b/22_lurette.ri 1.3 644))
(test/lurette.rif.exp (lurette/b/22_lurette.ri 1.4 644))
)
......
......@@ -34,85 +34,86 @@ let rec (eval : formula -> env_in -> formula) =
** (in the environment memory) are replaced by their values. Then,
** the formula is simplified; e.g., `true and f' is simplified into `f'.
*)
fun f input -> match f with
And(f1, f2) ->
let ef1 = (eval f1 input) in
if (ef1 = False) then False
else
let ef2 = (eval f2 input) in
if ef1 = True then ef2
else if ef2 = False then False
else if ef2 = True then ef1
else And(ef1, ef2)
fun f input ->
match f with
And(f1, f2) ->
let ef1 = (eval f1 input) in
if (ef1 = False) then False
else
let ef2 = (eval f2 input) in
if ef1 = True then ef2
else if ef2 = False then False
else if ef2 = True then ef1
else And(ef1, ef2)
| Or(f1, f2) ->
let ef1 = (eval f1 input) in
if ef1 = True then True
else
let ef2 = (eval f2 input) in
if ef1 = False then ef2
else if ef2 = True then True
else if ef2 = False then ef1
else Or(ef1, ef2)
| Or(f1, f2) ->
let ef1 = (eval f1 input) in
if ef1 = True then True
else
let ef2 = (eval f2 input) in
if ef1 = False then ef2
else if ef2 = True then True
else if ef2 = False then ef1
else Or(ef1, ef2)
| Not(f1) ->
let ef1 = (eval f1 input) in
if ef1 = True then False
else if ef1 = False then True
else Not(ef1)
| Not(f1) ->
let ef1 = (eval f1 input) in
if ef1 = True then False
else if ef1 = False then True
else Not(ef1)
| True -> True
| False -> False
| True -> True
| False -> False
| Bvar(str) ->
( match (lookup input str) with
Some(Bool(bool)) ->
if bool then True else False
| Some(_) ->
print_string (str ^ " is not a boolean!\n");
assert false
| None ->
(match (lookup env_state.local str) with
Some(Bool(bool)) ->
if bool then True else False
| Some(_) ->
print_string (str ^ " is not a boolean!\n");
assert false
| None -> Bvar(str)
)
)
| Eq(e1, e2) ->
(
let ee1 = eval_expr e1 input in
let ee2 = eval_expr e2 input in
match (ee1, ee2) with
| Bvar(str) ->
( match (lookup input str) with
Some(Bool(bool)) ->
if bool then True else False
| Some(_) ->
print_string (str ^ " is not a boolean!\n");
assert false
| None ->
(match (lookup env_state.local str) with
Some(Bool(bool)) ->
if bool then True else False
| Some(_) ->
print_string (str ^ " is not a boolean!\n");
assert false
| None -> Bvar(str)
)
)
| Eq(e1, e2) ->
(
let ee1 = eval_expr e1 input in
let ee2 = eval_expr e2 input in
match (ee1, ee2) with
(Ival(i1), Ival(i2)) -> if (i1 = i2) then True else False
| (Fval(f1), Fval(f2)) ->
if (f1 = f2) then True else False
(* XXX Meaningless with floats ??? *)
| _ -> Eq(ee1, ee2)
)
| Ge(e1, e2) ->
(
let ee1 = eval_expr e1 input in
let ee2 = eval_expr e2 input in
match (ee1, ee2) with
)
| Ge(e1, e2) ->
(
let ee1 = eval_expr e1 input in
let ee2 = eval_expr e2 input in
match (ee1, ee2) with
(Ival(i1), Ival(i2)) -> if (i1 >= i2) then True else False
| (Fval(f1), Fval(f2)) ->
if (f1 >= f2) then True else False
(* XXX Meaningless with floats ??? *)
| _ -> Ge(ee1, ee2)
)
| G(e1, e2) ->
(
let ee1 = eval_expr e1 input in
let ee2 = eval_expr e2 input in
match (ee1, ee2) with
)
| G(e1, e2) ->
(
let ee1 = eval_expr e1 input in
let ee2 = eval_expr e2 input in
match (ee1, ee2) with
(Ival(i1), Ival(i2)) -> if (i1 > i2) then True else False
| (Fval(f1), Fval(f2)) ->
if (f1 > f2) then True else False
| _ -> Ge(ee1, ee2)
)
)
and
(eval_expr : expr -> env_in -> expr) =
fun e input ->
......
......@@ -351,21 +351,21 @@ and
Env.env_step nll input loc ;
let str =
if (options.step_by_step) then (
Show_env.generate_env_graph previous_nodes "environment" ;
Sim2chro.put_current_step_values
stdout t input output env_state.local options.display_local_var;
output_string stderr
"\nOne more loop ? [type any char to stop, `CR' to continue]\n";
flush stderr;
flush stdout;
read_line ()
)
else (
Sim2chro.put_current_step_values
rif t input output env_state.local options.display_local_var;
if (options.step_by_step) then (
Show_env.generate_env_graph previous_nodes "environment" ;
Sim2chro.put_current_step_values
stdout t input output env_state.local options.display_local_var;
output_string stderr
"\nOne more loop ? [type any char to stop, `CR' to continue]\n";
flush stderr;
flush stdout;
read_line ()
)
else (
Sim2chro.put_current_step_values
rif t input output env_state.local options.display_local_var;
""
)
)
in
(* Decides whether to loop once more *)
......
......@@ -176,7 +176,7 @@ let (bdd_with_dot: Bdd.t -> (int -> string) -> string -> unit) =
fun bdd index_to_vn label ->
let arcs = bdd_to_graph bdd (index_to_vn) in
let dot_file = label ^ ".dot" in
let _ = Sys.command ("rm " ^ dot_file) in
let _ = Sys.command ("touch " ^ dot_file ^ "; rm " ^ dot_file) in
let ps_file = label ^ ".ps" in
let dot_oc = open_out dot_file in
let put = output_string dot_oc in
......
......@@ -125,7 +125,7 @@ let rec (build_sol_nb_table: Bdd.t -> Bdd.t -> sol_nb * sol_nb) =
print_string " = "; print_float card_sol_t;
print_string " + "; print_float card_sol_e ;
print_string "\n\n"; flush stdout ;
Print.bdd_with_dot bdd (Env_state.index_to_vn) ("bbd" ^ (string_of_int (Hashtbl.hash bdd))) ;
Print.bdd_with_dot bdd (Env_state.index_to_vn) "bdd" ;
print_string "(Not) Lurette computes: "; print_string (string_of_sol_nb (add_sol_nb not_nt not_ne));
print_string " = ";print_string (string_of_sol_nb not_nt);
......@@ -135,7 +135,7 @@ let rec (build_sol_nb_table: Bdd.t -> Bdd.t -> sol_nb * sol_nb) =
print_string " = "; print_float card_sol_t_not;
print_string " + "; print_float card_sol_e_not ;
print_string "\n\n"; flush stdout ;
Print.bdd_with_dot bdd (Env_state.index_to_vn) ("bbd_not" ^ (string_of_int (Hashtbl.hash bdd_not))) ;
Print.bdd_with_dot bdd_not (Env_state.index_to_vn) "bdd_not" ;
Util.gv "bdd.ps";
Util.gv "bdd_not.ps";
......@@ -318,15 +318,15 @@ let (solve_formula: int -> formula list -> var_name list -> (subst list * subst
(* XXX Recompute the solution number everytime as long as the bdds interface sucks *)
let _ =
begin
Hashtbl.clear env_state.snt ;
Hashtbl.add env_state.snt
(Bdd.dtrue ()) (one_sol, zero_sol);
Hashtbl.add env_state.snt
(Bdd.dfalse ()) (zero_sol, one_sol)
end
in
let _ =
begin
Hashtbl.clear env_state.snt ;
Hashtbl.add env_state.snt
(Bdd.dtrue ()) (one_sol, zero_sol);
Hashtbl.add env_state.snt
(Bdd.dfalse ()) (zero_sol, one_sol)
end
in
let _ =
if not (Hashtbl.mem env_state.snt bdd)
then
......
......@@ -59,18 +59,20 @@ let sorted list =
(**
[power a b] returns a to the power of b
*)
let (power: int -> int -> int) =
fun a n ->
let _ = 0 >= n in
if
n < Nativeint.size
then
2 lsl n
else
failwith ("*** Too many solutions. " ^
"try to use --use-big-int or --use-float option instead.\n")
let power_2 = power 2
let (power_2: int -> int) =
fun n ->
let _ = assert (0 <= n) in
if n = 0 then 1 else
if (n < (Nativeint.size - 2)) then 2 lsl (n-1)
else
failwith ("*** Too many solutions. " ^
"try to use --use-big-int or --use-float option instead.\n")
let _ = assert (power_2 0 = 1)
let _ = assert (power_2 1 = 2)
let _ = assert (power_2 29 = int_of_float (2. ** 29.))
(**
[readfile file] outputs the whole contents of [file] in a string.
......
......@@ -18,202 +18,202 @@ porte_et_pass_ok:bool
rentrer_pass:bool
@#
#step 1
t f f t t f f f t #outs
f f f f f t f t t #outs
#step 2
t t f f f f t f f #outs t f f f f
f f t f f f t t f #outs t f f f f
#step 3
f f f f t f t t t #outs t f f f f
t f f t f f t f f #outs t f f f f
#step 4
t t f t f f f t t #outs t f f f f
t t f t f t f f t #outs t f f f f
#step 5
t f f f f t t t f #outs t f f f t
t f f t t f t f f #outs f t f t f
#step 6
t f f f f f t t f #outs f t f t t
t f f t f f t t t #outs f f f f f
#step 7
f f t f t f t t f #outs t f f f t
t t f t f f t t f #outs t f f f t
#step 8
f f f t f t t f f #outs t f f f t
t f t t f f t t f #outs t f f f t
#step 9
f t f t f f f t t #outs t f f f f
t f f t f f t t f #outs t f f f t
#step 10
t f f f f t t t t #outs t f f f t
t t f f f t t t f #outs t f f f t
#step 11
f f t t f f f t f #outs f t f t t
t t f f t f f t f #outs f t f f t
#step 12
f t f f f f t t t #outs t f f f f
f f t t t t f t t #outs f f f f t
#step 13
f f t t f f f t t #outs t f f f f
t f f t f f t t f #outs f f f f f
#step 14
f f f f t f f f f #outs t f f f f
f t f f f f f f f #outs t t f f f
#step 15
t t f f f f f t f #outs t f t f f
t t f t t f t t f #outs t f f f f
#step 16
t t f t f f t t f #outs f t f f f
t f t t f f t t f #outs t f f f t
#step 17
f t f t f f t t f #outs t f f f t
f f f f f f t f f #outs f f f t t
#step 18
f f f t f t t t f #outs t f f f t
f t f t t f t t f #outs t f f f f
#step 19
t f t f t f t f t #outs f t f f t
f f t t f f t t f #outs t f f f f
#step 20
t f t f t f t f f #outs f f t t f
f f t t f f t t f #outs t f f f f
#step 21
f t f f f f t t f #outs f f t f f
t t f t t f t t f #outs t f f f f
#step 22
t f t t f f t t f #outs t f f f t
f f f t t f t f t #outs f t f f f
#step 23
f f f f f f t t t #outs t f f f f
f t f t t f f t f #outs f f t f f
#step 24
f t f t t f t t f #outs t f f f f
f t f t t f t t f #outs t f t f f
#step 25
f t f t f f t t f #outs t f f f f
f f t t t f t f f #outs t f t f f
#step 26
t f f t t f t t f #outs t f f f f
t f t t f t f f f #outs t f t f f
#step 27
t f t f f f f t f #outs t f f f f
f t f f f f f f t #outs t f f f f
#step 28
f t f t t t f t f #outs t f f f f
f f t t t f f f f #outs t f f f f
#step 29
f f t t f f t f f #outs f t f f t
f t f f f f f t f #outs t f f f f
#step 30
f f f t f f t f f #outs t f f f f
t t f f t f f t f #outs t f f f t
#step 31
t t f t f f t f f #outs t f f f f
f f t f t f f t f #outs f f t t t
#step 32
f t f f f t t f f #outs f f f t f
f f f t f f f f f #outs f f t f t
#step 33
t f t t t t t f t #outs f t f f f
f f f f f f t f f #outs f f f f f
#step 34
f t f t f f f t f #outs f f t f f
t f f f f f t f f #outs t f f f f
#step 35
f f t t f t t f f #outs t f f f t
f f f t f t f f t #outs t f f f f
#step 36
f f t t f f f t t #outs f t f f f
t f t t f f f t f #outs t f f f f
#step 37
t t f t f f f t f #outs f f f f t
t t f t t f t t f #outs f t f f f
#step 38
t t f t t t t t f #outs f f f t t
f f f t t f t f f #outs t f f f f
#step 39
f t f t f f t t t #outs t t f f t
f f f f f f f f t #outs t f f f f
#step 40
f f t t f f t t f #outs t f f f t
t f f f f f t f f #outs t f f f f
#step 41
t f f t t f t t t #outs t f f f t
t f t t t f t f f #outs t f f f f
#step 42
f t f t t t t t f #outs t f t f t
f f f t f f t f f #outs t f f f f
#step 43
f f f t t f f t f #outs f t f f t
t f f t f f t f f #outs t f f f f
#step 44
t t f f f f f f f #outs f f f f t
f f f f f f t f f #outs t f f f f
#step 45
f f t t f f f t f #outs f f f f f
f t f f t f t t f #outs t f f f f
#step 46
t t f t f f f t t #outs f f f f f
f t f f f f f t f #outs t f f f f
#step 47
t f t t f f f f f #outs f f f t t
t f t t f f t t f #outs t f f f f
#step 48
f t f f t f t t t #outs f f f f f
f f f f f f t t f #outs t f f f f
#step 49
t t f t f f t t f #outs t f t f t
f f f f f f t t f #outs t f f f f
#step 50
t f f f f f t t f #outs t f f f f
f f t t f f f t f #outs t f f f f
#step 51
t t f f f f f t f #outs t f f f f
f f t t f t t f f #outs t f f f f
#step 52
f f f f t f t f f #outs f f f t t
f f f t f f t f f #outs t f f f f
#step 53
f t f f f t t t t #outs t f t f f
f f f t t f t f f #outs t f f f f
#step 54
f f t f f t f t t #outs f t t f t
t t f f f f f f t #outs t f t f f
#step 55
f f t t f t t t f #outs f f f f t
f t f t t f f t f #outs f t t f f
#step 56
t t f t t f t f f #outs t f f f f
t t f f f f t t f #outs t f f f t
#step 57
f f f f f f f t f #outs f t f f f
t t f f f f f t f #outs f f f t t
#step 58
f f t t f f f t f #outs t f f f f
f f f t f f t f f #outs t f f f t
#step 59
t f f t t f t t f #outs t f f f f
t f t t t f t f f #outs t f f f f
#step 60
t t f t t f f t f #outs t f f f f
t f f f t f f t f #outs t f f f f
#step 61
f t f t t f f t t #outs t f f f f
t f f f f f t f f #outs t f f f f