Commit af07708a authored by Erwan Jahier's avatar Erwan Jahier

lurette 0.32 Mon, 18 Feb 2002 17:06:16 +0100 by jahier

Parent-Version:      0.31
Version-Log:

Add an option --no-oracle to prevent that lurette calls the oracle.

The solution number counting function was wrong.

Also, make it easy to switch to float, or to big_int, to store
the number of solution numbers.

Project-Description: Lurette
parent e682b1ff
LURETTE_DIR = ..
OCAMLMAKEFILE = $(LURETTE_DIR)/OcamlMakefile
# It seems that there is no speed up with those options... Give it another try.
# OCAMLFLAGS = -noassert -unsafe # -inline 10
# OCAMLFLAGS = -noassert -unsafe
# OCAMLNCFLAGS = -inline 10
-include ./lurette.in
INCDIRS = /home/jahier/include
LIBDIRS = /home/jahier/lib /home/jahier/lib/ocaml
LIBDIRS = /home/jahier/lib /home/jahier/lib/ocaml
# Requires cudd and mldd to be installed!
LIBS = dd
LIBS = dd nums
CLIBS = dd_caml cudd mtr st epd util
......@@ -23,9 +23,9 @@ SOURCES_OCAML = \
$(LURETTE_DIR)/source/graph.mli $(LURETTE_DIR)/source/graph.ml \
$(LURETTE_DIR)/source/command_line.mli $(LURETTE_DIR)/source/command_line.ml \
$(LURETTE_DIR)/source/formula.mli $(LURETTE_DIR)/source/formula.ml \
$(LURETTE_DIR)/source/print.mli $(LURETTE_DIR)/source/print.ml \
$(LURETTE_DIR)/source/parse_env.mli $(LURETTE_DIR)/source/parse_env.ml \
$(LURETTE_DIR)/source/env_state.mli $(LURETTE_DIR)/source/env_state.ml \
$(LURETTE_DIR)/source/print.mli $(LURETTE_DIR)/source/print.ml \
$(LURETTE_DIR)/source/solver.mli $(LURETTE_DIR)/source/solver.ml \
$(LURETTE_DIR)/source/wtree.mli $(LURETTE_DIR)/source/wtree.ml \
$(LURETTE_DIR)/source/show_env.mli $(LURETTE_DIR)/source/show_env.ml \
......
......@@ -5,7 +5,7 @@
# For updates see:
# http://miss.wu-wien.ac.at/~mottl/ocaml_sources
#
# $Id: OcamlMakefile 1.14 Tue, 12 Feb 2002 13:42:18 +0100 jahier $
# $Id: OcamlMakefile 1.15 Mon, 18 Feb 2002 17:06:16 +0100 jahier $
#
###########################################################################
......@@ -492,16 +492,46 @@ dot:
dot -Tps $(RESULT).dep.dot > $(RESULT).dep.ps ; \
cp $(RESULT).dep.ps ../doc ; cp $(RESULT).depfull.ps ../doc ; popd
install:
pushd ../interface ; make; popd ; $(LURETTE_DIR)/make_lurette ControleurPorte vrai_tram dc
runbug:
./lurette 10 1 1 tram.env usager.env porte.env passerelle.env -ns2c -seed 1013388978
try:
$(LURETTE_DIR)/make_lurette ControleurPorte vrai_tram; \
# ./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
# Non regression test
test:
$(LURETTE_DIR)/make_lurette ControleurPorte vrai_tram; \
./lurette 100 10 10 tram.env usager.env porte.env passerelle.env -seed 1013219512 -ns2c ;\
diff -u lurette.rif.exp lurette.rif > test.res ; cat test.res
# 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 ;\
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 ;\
ocamlprof ../source/solver.ml > prof/solver.count.ml ; \
ocamlprof ../source/wtree.ml > prof/wtree.count.ml ; \
ocamlprof ../source/env.ml > prof/env.count.ml ; \
ocamlprof ../source/eval.ml > prof/eval.count.ml ; \
ocamlprof ../source/util.ml > prof/util.count.ml ; \
ocamlprof ../source/lurette_stub.ml > prof/lurette_stub.count.ml ; \
ocamlprof ../source/sim2chro.ml > prof/sim2chro.count.ml ; \
ocamlprof ../source/env_state.ml > prof/env_state.count.ml ; \
ocamlprof ../source/lurette.ml > prof/lurette.count.ml ; \
ocamlprof ../source/graph.ml > prof/graph.count.ml ; \
echo " ---> The results of the profiling are in the prof/*.count.ml files"
# Produces an html version of the lurette documentation
dochtml:
ocamldoc -t "Lurette implementation description" -html -d ../doc/html -stars \
-keep-code -colorize-code -I ../source/ $(SOURCES_OCAML) \
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 31)
(Parent-Version lurette 0 30)
(Project-Version lurette 0 32)
(Parent-Version lurette 0 31)
(Version-Log "
Various fixes so that lurette can be build from scratch.
Add an option --no-oracle to prevent that lurette calls the oracle.
The solution number counting function was wrong.
Also, make it easy to switch to float, or to big_int, to store
the number of solution numbers.
")
(New-Version-Log "")
(Checkin-Time "Tue, 12 Feb 2002 14:10:11 +0100")
(Checkin-Time "Mon, 18 Feb 2002 17:06:16 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -19,36 +26,36 @@ Various fixes so that lurette can be build from scratch.
;; Sources files
(source/lurette.mli (lurette/11_lurette.ml 1.10 644))
(source/lurette.ml (lurette/12_lurette.ml 1.18 644))
(source/lurette.ml (lurette/12_lurette.ml 1.19 644))
(source/graph.mli (lurette/13_graph.mli 1.4 644))
(source/graph.mli (lurette/13_graph.mli 1.5 644))
(source/graph.ml (lurette/14_graph.ml 1.3 644))
(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.7 644))
(source/util.ml (lurette/35_util.ml 1.8 644))
(source/solver.mli (lurette/38_solver.mli 1.6 644))
(source/solver.ml (lurette/39_solver.ml 1.7 644))
(source/solver.mli (lurette/38_solver.mli 1.7 644))
(source/solver.ml (lurette/39_solver.ml 1.8 644))
(source/parse_env.mli (lurette/40_parse_env. 1.3 644))
(source/parse_env.ml (lurette/41_parse_env. 1.4 644))
(source/show_env.mli (lurette/42_show_env.m 1.3 644))
(source/show_env.ml (lurette/43_show_env.m 1.2 644))
(source/show_env.mli (lurette/42_show_env.m 1.4 644))
(source/show_env.ml (lurette/43_show_env.m 1.3 644))
(source/formula.mli (lurette/44_formula.ml 1.4 644))
(source/formula.ml (lurette/45_formula.ml 1.5 644))
(source/print.mli (lurette/46_print.mli 1.4 644))
(source/print.ml (lurette/47_print.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/eval.mli (lurette/48_eval.mli 1.4 644))
(source/eval.ml (lurette/49_eval.ml 1.4 644))
(source/env_state.mli (lurette/50_env_state. 1.6 644))
(source/env_state.ml (lurette/51_env_state. 1.7 644))
(source/env_state.mli (lurette/50_env_state. 1.7 644))
(source/env_state.ml (lurette/51_env_state. 1.8 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.5 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.7 644))
......@@ -56,14 +63,14 @@ Various fixes so that lurette can be build from scratch.
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.1 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.1 644))
(source/command_line.ml (lurette/b/20_command_li 1.2 644))
(source/command_line.mli (lurette/b/21_command_li 1.2 644))
(source/command_line.ml (lurette/b/20_command_li 1.3 644))
(source/command_line.mli (lurette/b/21_command_li 1.3 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.16 644))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.14 644))
(Makefile (lurette/18_Makefile 1.17 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.15 644))
(Makefile (lurette/18_Makefile 1.18 644))
(test/Makefile (../Makefile) :symlink)
(interface/Makefile (lurette/25_Makefile 1.6 644))
(make_lurette (lurette/27_make_luret 1.7 744))
......@@ -100,7 +107,7 @@ Various fixes so that lurette can be build from scratch.
(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.2 644))
(test/lurette.rif.exp (lurette/b/22_lurette.ri 1.3 644))
)
......
......@@ -14,14 +14,15 @@ type optionsT = {
mutable display_local_var : bool ;
mutable display_sim2chro : bool ;
mutable cudd_heap_init : int ;
mutable user_seed : int
mutable user_seed : int ;
mutable oracle : bool
}
type cmd_line_optionT =
Step | NoStep
| DisplayLocalVar | NoDisplayLocalVar
| Sim2chro | NoSim2chro
| CuddHeapInit | Seed
| CuddHeapInit | Seed | NoOracle
(* Names of the command line options to override the defaults. *)
let (string_to_option: (string * cmd_line_optionT) list) = [
......@@ -32,6 +33,8 @@ let (string_to_option: (string * cmd_line_optionT) list) = [
("--with-seed", Seed);
("-seed", Seed);
("--no-oracle", NoOracle);
("--display-local-var", DisplayLocalVar);
("--do-not-display-local-var", NoDisplayLocalVar);
("-nlv", NoDisplayLocalVar);
......@@ -54,6 +57,7 @@ let (option_to_usage: cmd_line_optionT -> string) =
| NoSim2chro -> "Do not call sim2chro when lurette resumes.\n"
| CuddHeapInit -> "Set a magic number (related to the gc) that is used by mldd \n\t\t\tfor initializing Dd (Default is 20).\n"
| Seed -> "Set the value of the seed the random engine is initialized with (0 lets the system draw a seed).\n"
| NoOracle -> "Do not need to specify an oracle.\n "
let (group_common_options: (string * cmd_line_optionT) list ->
(string * cmd_line_optionT) list) =
......
......@@ -18,7 +18,8 @@ type optionsT = {
mutable display_local_var : bool ;
mutable display_sim2chro : bool ;
mutable cudd_heap_init : int ;
mutable user_seed : int
mutable user_seed : int ;
mutable oracle : bool
}
val usage : string
......@@ -34,7 +35,7 @@ type cmd_line_optionT =
Step | NoStep
| DisplayLocalVar | NoDisplayLocalVar
| Sim2chro | NoSim2chro
| CuddHeapInit | Seed
| CuddHeapInit | Seed | NoOracle
val string_to_option: (string * cmd_line_optionT) list
......
......@@ -27,6 +27,7 @@ type env_stateT = {
mutable var_name_to_index: ((string, int) Hashtbl.t);
mutable index_to_var_name: ((int, string) Hashtbl.t);
mutable bdd_tbl: (formula, Bdd.t) Hashtbl.t;
mutable snt: (Bdd.t, Util.sol_nb * Util.sol_nb) Hashtbl.t;
mutable pre_expr: vne list;
mutable pre_form: vnf list;
mutable current_nodes: node list list;
......@@ -46,6 +47,7 @@ let (env_state:env_stateT) = {
var_name_to_index = Hashtbl.create 0 ;
index_to_var_name = Hashtbl.create 0 ;
bdd_tbl = Hashtbl.create 0;
snt = Hashtbl.create 3;
pre_expr = [] ;
pre_form = [] ;
current_nodes = [];
......
......@@ -43,6 +43,12 @@ type env_stateT = {
(** Transforming a formula into a bdd is expensive, therefore
we store the result of this transformation in a table. *)
mutable snt: (Bdd.t, Util.sol_nb * Util.sol_nb) Hashtbl.t;
(** Associates to a bdd the (absolute) number of solutions
contained in its lhs (then) and rhs (else) branches. Note that
adding those two numbers only give a number of solution that is
relative to which bdd points to it. *)
mutable pre_expr: vne list;
(** In the [.aut] format, expressions under a pre are represented
by a variable name. The correspondance between those variable
......
(*-----------------------------------------------------------------------
** Copyright (C) 2001 - Verimag.
** Copyright (C) 2001, 2002 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
......@@ -15,7 +15,8 @@
type ('a, 'b) t
(** Graph type, where 'a is the type of nodes, and 'b the type of
arcs. *)
val create: unit -> ('a, 'b) t
(**
......
......@@ -22,8 +22,9 @@ let (options:Command_line.optionsT) = {
step_by_step = false ;
display_local_var = true ;
display_sim2chro = true ;
cudd_heap_init = 20 ;
user_seed = 0
cudd_heap_init = 21 ;
user_seed = 0 ;
oracle = true
}
......@@ -133,6 +134,8 @@ and
| Sim2chro -> options.display_sim2chro <- true ; (n+1)
| NoSim2chro -> options.display_sim2chro <- false ; (n+1)
| NoOracle -> options.oracle <- false ; (n+1)
| CuddHeapInit ->
let str = (Sys.argv.(n+1)) in
......@@ -214,6 +217,7 @@ and
print_string "The random engine was initialized with the seed ";
print_int seed;
print_string "\n ";
flush stdout ;
env_state.local <- local1 ;
......@@ -224,9 +228,10 @@ and
var_decl_are_inconsistent Lurette_stub.sut_input_var_name_and_type_list
Lurette_stub.sut_output_var_name_and_type_list;
(* Sim2chro *)
if options.step_by_step then (
Show_env.generate_env_graph [[]] "environment" ;
Show_env.gv ("environment.ps");
Util.gv ("environment.ps");
Sim2chro.put_var_decl
("lurette chronogram (" ^
(fold_left (fun acc str -> (acc ^ " " ^ str)) "" (flatten env_llist)) ^ ")")
......@@ -242,9 +247,16 @@ and
Lurette_stub.sut_output_var_name_and_type_list
rif options.display_local_var;
(* Initializing Dd (bdd's) libs. *)
(* Initializing Dd's libs. *)
Dd.initialize 0 options.cudd_heap_init ;
Dd.disable_autoreorder ();
(* Initializing the solution number table *)
Hashtbl.add env_state.snt
(Bdd.dtrue ()) (Util.one_sol, Util.zero_sol);
Hashtbl.add env_state.snt
(Bdd.dfalse ()) (Util.zero_sol, Util.one_sol);
main_loop 1 s n p rif [] ;
flush stdout;
......@@ -267,53 +279,56 @@ and
(* Tries the sut `n*p'^nth times *)
let (outputs: env_in list) = List.map Lurette_stub.sut_try inputs in
(* Tries the oracle `n*p'^nth times *)
let (results: bool list) =
List.map2 (fun x y -> Lurette_stub.oracle_try x y) inputs outputs
in
(* Aborts if at least one of the pairs (input, output) breaks the oracle *)
let _ =
if (List.mem false results)
then (
let print_vntl =
(fun (vn,vt) ->
print_string "\n*** ";
print_string vn;
print_string ":";
print_string vt
)
let _ =
if options.oracle
then
(* Tries the oracle `n*p'^nth times *)
let (results: bool list) =
List.map2 (fun x y -> Lurette_stub.oracle_try x y) inputs outputs
in
print_string ("*** An assertion of the oracle has been violated" ^
" at time " ^ (string_of_int t) ^
" with the following values:\n ");
print_string "\n*** sut inputs names and types:" ;
List.iter (print_vntl) Lurette_stub.sut_input_var_name_and_type_list;
print_string "\n*** sut outputs names and types: " ;
List.iter (print_vntl) Lurette_stub.sut_output_var_name_and_type_list;
print_string "\n***" ;
Util.list_iter3
(fun i o r ->
if (not r) then
(
print_string "\n*** sut inputs:" ;
print_subst_list i stdout;
print_string " sut outputs: " ;
print_subst_list o stdout
)
else
()
)
inputs
outputs
results ;
flush stdout;
flush rif;
Sim2chro.call_sim2chro ();
assert false
)
else ()
(* Aborts if at least one of the pairs (input, output) breaks the oracle *)
if (List.mem false results)
then (
let print_vntl =
(fun (vn,vt) ->
print_string "\n*** ";
print_string vn;
print_string ":";
print_string vt
)
in
print_string ("*** An assertion of the oracle has been violated" ^
" at time " ^ (string_of_int t) ^
" with the following values:\n ");
print_string "\n*** sut inputs names and types:" ;
List.iter (print_vntl) Lurette_stub.sut_input_var_name_and_type_list;
print_string "\n*** sut outputs names and types: " ;
List.iter (print_vntl) Lurette_stub.sut_output_var_name_and_type_list;
print_string "\n***" ;
Util.list_iter3
(fun i o r ->
if (not r) then
(
print_string "\n*** sut inputs:" ;
print_subst_list i stdout;
print_string " sut outputs: " ;
print_subst_list o stdout
)
else
()
)
inputs
outputs
results ;
flush stdout;
flush rif;
Sim2chro.call_sim2chro ();
assert false
)
else ()
in
let previous_nodes = env_state.current_nodes in
......@@ -324,8 +339,8 @@ and
let (nll, input, loc) = List.nth nll_inputs_loc ran in
(* Performs the steps *)
let _ = Lurette_stub.sut_step input
and _ = Lurette_stub.oracle_step input output in
let _ = Lurette_stub.sut_step input in
let _ = if (options.oracle) then Lurette_stub.oracle_step input output else true in
Env.env_step nll input loc ;
let str =
......
......@@ -44,25 +44,7 @@ let (arc_info : Formula.arc_info -> unit) =
print_string (" " ^ str ^ "\n");
end
(*
let rec (print_bdd : Bdd.t -> unit) =
fun bdd ->
Bdd._print bdd
let (snt: (Bdd.t, (float*int)*(float*int)) Hashtbl.t -> unit) =
fun t ->
Hashtbl.iter
(fun bdd ((a,n),(b,m)) ->
print_bdd bdd;
print_string (" -> ") ;
print_float a ; print_string ("*2^") ; print_int n ;
print_string (" | ") ;
print_float b ; print_string ("*2^") ; print_int m ;
print_string (" \n \n") ;
flush stdout
)
t
*)
......@@ -121,4 +103,107 @@ let (pwtt: Wtree.wtree_table -> unit) =
) wtt ;
flush stdout
let (comb2: Bdd.t -> unit) =
fun supp ->
List.iter
(fun var -> print_string (var ^ " "))
(List.map (Env_state.index_to_vn) (Bdd.int_of_support supp));
print_string "\n" ;
flush stdout
let rec (comb : Bdd.t -> unit) =
fun supp ->
if Bdd.is_cst supp then print_string "\n"
else
begin
print_string ( (Env_state.index_to_vn (Bdd.topvar supp)) ^ " ");
comb (Bdd.dthen supp);
flush stdout
end
(* let _ = *)
(* List.iter *)
(* (fun x -> print_int (Dd.level_of_var (Env_state.vn_to_index x)) ; print_string " ") *)
(* vars_to_gen; *)
(* print_string "\n"; *)
(* flush stdout *)
(* in *)
let rec (print_bdd : Bdd.t -> unit) =
fun bdd ->
Bdd._print bdd
(****************************************************************************)
(* printing bbd's with dot *)
let (bdd_to_graph: Bdd.t -> (int -> string) -> (string * string * string) list) =
fun bdd index_to_string ->
let get_label bdd =
if Bdd.is_true bdd then "True"
else if Bdd.is_false bdd then "False"
else index_to_string (Bdd.topvar bdd)
in
let rec (bdd_to_graph_acc: (string * string * string) list -> Bdd.t -> (string * string * string) list) =
fun acc0 bdd ->
if Bdd.is_cst bdd then acc0
else
let bddt = Bdd.dthen bdd in
let bdde = Bdd.delse bdd in
let label = get_label bdd in
let labelt = get_label bddt in
let labele = get_label bdde in
let acc1 =
if List.mem (label, "t", labelt) acc0
then acc0
else ((label,"t", labelt)::acc0)
in
let acc2 =
if List.mem (label, "f", labele) acc1
then acc1
else ((label, "f", labele)::acc1)
in
let acc3 = bdd_to_graph_acc acc2 bddt in
bdd_to_graph_acc acc3 bdde
in
bdd_to_graph_acc [] bdd
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 ps_file = label ^ ".ps" in
let dot_oc = open_out dot_file in
let put = output_string dot_oc in
let _ =
put "digraph G {\n\n ordering=out;\n\n";
put " ratio = compress;\n\n";
List.iter (fun (n, _, _) -> put ("\t" ^ n ^ "\t ; \n")) arcs ;
List.iter (fun (f, l, t) -> put ("\t" ^ f ^ " -> " ^ t ^ "\t [label = " ^ l ^ " ] ; \n")) arcs ;
put "} \n";
flush dot_oc ;
close_out dot_oc
in
(* Calling dot to create the postscript file *)
let exit_code_dot = Sys.command ("dot -Tps " ^ dot_file ^ " -o " ^ ps_file)
in if (exit_code_dot <> 0)
then print_string " Can't call dot; is dot in your path?\n\n"
else ()
open Util
let (snt: (Bdd.t, (Util.sol_nb * Util.sol_nb)) Hashtbl.t -> unit) =
fun t ->
Hashtbl.iter
(fun bdd (n,m) ->
let n_str = string_of_sol_nb n
and m_str = string_of_sol_nb m in
bdd_with_dot bdd (Env_state.index_to_vn)
("bdd__" ^ n_str ^ "__" ^ m_str ^ "_" ^ (string_of_int (Hashtbl.hash bdd)));
)
t
......@@ -6,8 +6,6 @@
val print_int_string_hashtbl : (int, string) Hashtbl.t -> unit
val print_string_int_hashtbl : (string, int) Hashtbl.t -> unit
(* val print_bdd : Bdd.t -> unit *)
(* val snt: (Bdd.t, (float*int)*(float*int)) Hashtbl.t -> unit *)
val arc_info : Formula.arc_info -> unit
......@@ -17,3 +15,15 @@ open Wtree
val pft: Wtree.formula_table -> unit
val pwt: int -> Wtree.wtree -> unit
val pwtt: Wtree.wtree_table -> unit
val comb: Bdd.t -> unit
val print_bdd : Bdd.t -> unit
(* open Big_int *)
(* val snt: (Bdd.t, (big_int * big_int)) Hashtbl.t -> unit *)
val bdd_to_graph: Bdd.t -> (int -> string) -> (string * string * string) list
val bdd_with_dot: Bdd.t -> (int -> string) -> string -> unit
......@@ -14,12 +14,6 @@
open Formula
open Env_state
let (gv: string -> unit) =
fun ps_file ->
let exit_code = (Sys.command ("gv " ^ ps_file ^ " &")) in
if (exit_code <> 0)
then print_string " Can't call gv; is gv in your path?\n\n"
else ();;