Commit 3a6425a6 authored by Erwan Jahier's avatar Erwan Jahier

lurette 1.39 Tue, 14 Dec 2004 11:29:46 +0100 by jahier

Parent-Version:      1.38
Version-Log:

source/run_aut.mli
source/run_aut.ml:
  Fix a bug when drawing transitions in the automata that made the distribution
  wrong wrt weights (oups)...

source/lucky.ml
source/run_aut.mli
run_aut.ml:
  Fix a bug where the repartition wrt the automata transitions was wrong in
  case of backtracking.

source/lurette.ml
  Fix a bug related to the thickness (when only all the vertices where
required).

demo-xlurette/fault-tolerant-heater/heater_control_env.luc
share/show_luc.sh
share/show_luc.bat

source/gen_fake_lucky.ml
source/lurettetop.ml
source/util.ml
ihm/xlurette/xlurette_glade_main.ml
ihm/xlurette/xlurette.glade
   Add a button in xlurette that generates default environments.
   Add a buildenv command for lurettetop to do it.

Project-Description: Lurette
parent 1d4d5e4c
This diff is collapsed.
V1.39
* Fix a bug where the probability of a translation was sligthly wrong
in some circumstances (namely, when a formula happens to be false
because of the numeric part; in such a case, the draw was done again
from the current node instead of doing it from the last choice point).
* Add a button in xlurette that generates default environments for the
current SUT.
V1.38
......
......@@ -2,22 +2,9 @@
*********** BUGS
* pourquoi, pour l'exemple de MM, ca se met a ramer quand j'en tire 10
à l'interieur (DNI) ??
* pourquoi, tjrs pour cet ex, quand je met DNB à 100, l'épaisseur calcul
* quand une formule s'avere fausse du point de vue des variables
numeriques, il ne faut pas repartir du haut du graphe, mais backtraker
depuis la branche qui s'avere fausse. Sinon, les probabilités induites
par les poids sont un peu contre-intuitives.
En plus, en backtraquant ainsi, je n'ai plus de problemes de dag2three !
et je ne suis plus obligé de ...
* Le remplacement dynamique de .luc est tres surement cassé (les current_nodes
ne sont pas mis a jour) -> le retester
(nb : cette feature n'est pas documenté de toutes facons)
* time lucky -l 100 six_lines.luc
......@@ -28,10 +15,7 @@ time lucky -l 10 six_lines.luc
prend 170 secondes pour n=10000
!!!
* NF : Je viens d'avoir une erreur en utilisant un dosier dont le nom
* NF : Je viens d'avoir une erreur en utilisant un dossier dont le nom
contient un espace (erreur de gen_stubs). Ceci doit pouvoir être
éviter en mettant entre guillemets chaques arguments. Ca ne vaut
peut être pas le coup de corriger cela (modification du script
......@@ -41,11 +25,11 @@ prend 170 secondes pour n=10000
*********** A faire
* gen_stubs devrait etre une API, pas un script
* quand on quitte lurette, on perd les .o et les executables, ce qui
est dommage quand les .c générés sont énormes !!!
* parametrer le node_env.luc de la meme maniere que le node_env_UD.luc
* il me faudrait un bouton "gen fake env" qui fasse l'appel idoine explicitement
plutot que d'avoir a le faire en donnant un environement vide.
......@@ -53,7 +37,8 @@ plutot que d'avoir a le faire en donnant un environement vide.
est un peu penible, parce que le plus pratique devient alors de
changer de repertoire en allant dans celui-ci, puis de relancer lurette ...
* XXX attention a l'affichade du .rif quabd lus est syntaxiquement faux
* XXX attention a l'affichage du .rif quand lus est syntaxiquement faux dans
l'onglet "diagram manager" d'xlurette.
* Au sujet des l'heuristique nbac -> lucky, il faudrait peut-etre verifier
que tous les points sont ergodiques (recurrents).
......
-- Automatically generated from /tmp/lurette2/heater_control_env.h by gen_fake_lucky.
-- Automatically generated from /tmp/lurette2/heater_control.h by gen_fake_lucky.
inputs {
Heat_on : bool}
......@@ -7,13 +7,20 @@ outputs {
T1 : real;
T2 : real;
T3 : real}
locals {
downR : real ~alias -100.0;
upR : real ~alias 100.0;
downI : int ~alias -100;
upI : int ~alias 100;
}
states { 0 : stable }
start_state { 0 }
transitions {
0 -> 0 ~cond (0.0 < T) and (T < 1.0)
and (0.0 < T1) and (T1 < 1.0)
and (0.0 < T2) and (T2 < 1.0)
and (0.0 < T3) and (T3 < 1.0)
0 -> 0 ~cond (downR < T) and (T < upR)
and (downR < T1) and (T1 < upR)
and (downR < T2) and (T2 < upR)
and (downR < T3) and (T3 < upR)
;
}
......@@ -235,47 +235,6 @@
</widget>
</widget>
<widget>
<class>GtkToolbar</class>
<name>toolbar26</name>
<orientation>GTK_ORIENTATION_HORIZONTAL</orientation>
<type>GTK_TOOLBAR_ICONS</type>
<space_size>5</space_size>
<space_style>GTK_TOOLBAR_SPACE_EMPTY</space_style>
<relief>GTK_RELIEF_NORMAL</relief>
<tooltips>True</tooltips>
<child>
<left_attach>2</left_attach>
<right_attach>3</right_attach>
<top_attach>0</top_attach>
<bottom_attach>1</bottom_attach>
<xpad>0</xpad>
<ypad>0</ypad>
<xexpand>False</xexpand>
<yexpand>False</yexpand>
<xshrink>False</xshrink>
<yshrink>False</yshrink>
<xfill>True</xfill>
<yfill>False</yfill>
</child>
<widget>
<class>GtkButton</class>
<child_name>Toolbar:button</child_name>
<name>button92</name>
<width>30</width>
<height>30</height>
<tooltip>Browse for a reactive program file to test (.saofdm, .lus or .c) that is not in the current directory. Note that the current directory of Lurette will become the one of the sut if it changes.</tooltip>
<signal>
<name>clicked</name>
<handler>browse_sut_clicked</handler>
<last_modification_time>Fri, 18 Oct 2002 12:08:35 GMT</last_modification_time>
</signal>
<label></label>
<icon>open.xpm</icon>
</widget>
</widget>
<widget>
<class>GtkToolbar</class>
<name>toolbar27</name>
......@@ -760,6 +719,68 @@ sildex
</child>
</widget>
</widget>
<widget>
<class>GtkEventBox</class>
<name>eventbox4</name>
<child>
<left_attach>2</left_attach>
<right_attach>3</right_attach>
<top_attach>0</top_attach>
<bottom_attach>1</bottom_attach>
<xpad>0</xpad>
<ypad>0</ypad>
<xexpand>False</xexpand>
<yexpand>False</yexpand>
<xshrink>False</xshrink>
<yshrink>False</yshrink>
<xfill>True</xfill>
<yfill>False</yfill>
</child>
<widget>
<class>GtkToolbar</class>
<name>toolbar26</name>
<orientation>GTK_ORIENTATION_HORIZONTAL</orientation>
<type>GTK_TOOLBAR_ICONS</type>
<space_size>5</space_size>
<space_style>GTK_TOOLBAR_SPACE_EMPTY</space_style>
<relief>GTK_RELIEF_NORMAL</relief>
<tooltips>True</tooltips>
<widget>
<class>GtkButton</class>
<child_name>Toolbar:button</child_name>
<name>button92</name>
<width>30</width>
<height>30</height>
<tooltip>Browse for a reactive program file to test (.saofdm, .lus or .c) that is not in the current directory. Note that the current directory of Lurette will become the one of the sut if it changes.</tooltip>
<signal>
<name>clicked</name>
<handler>browse_sut_clicked</handler>
<last_modification_time>Fri, 18 Oct 2002 12:08:35 GMT</last_modification_time>
</signal>
<label></label>
<icon>open.xpm</icon>
</widget>
<widget>
<class>GtkButton</class>
<child_name>Toolbar:button</child_name>
<name>build_env_button</name>
<width>30</width>
<height>30</height>
<tooltip>Generates default environments for this SUT</tooltip>
<signal>
<name>clicked</name>
<handler>build_env_clicked</handler>
<last_modification_time>Fri, 10 Dec 2004 09:42:20 GMT</last_modification_time>
</signal>
<label></label>
<icon>linegraph.xpm</icon>
</widget>
</widget>
</widget>
</widget>
<widget>
......
......@@ -162,29 +162,6 @@ let button91 = toolbar25#insert_button
()
in
let _ = tooltips#set_tip ~text:"Browse to add an environment to the curent one(s) (.lut or .luc) that is not in the current direstory." button91#coerce in
let toolbar26 = GButton.toolbar
~packing:(table8#attach ~left:2
~top:0
~right:3
~bottom:1
~xpadding:0
~ypadding:0
~expand:`NONE
~shrink:`NONE
~fill:`X
)
~orientation:`HORIZONTAL
~button_relief:`NORMAL
~tooltips:true
~space_size:5
~space_style:`EMPTY
()
in
let button92 = toolbar26#insert_button
~icon:(GMisc.pixmap (GDraw.pixmap_from_xpm ~file:((Unix.getenv "PIXMAP_DIR") ^ "open.xpm") ()) ())#coerce
()
in
let _ = tooltips#set_tip ~text:"Browse for a reactive program file to test (.saofdm, .lus or .c) that is not in the current directory. Note that the current directory of Lurette will become the one of the sut if it changes." button92#coerce in
let toolbar27 = GButton.toolbar
~packing:(table8#attach ~left:2
~top:2
......@@ -484,6 +461,38 @@ let _ = button98#misc#add_accelerator
GtkSignal.classe = `base }
~modi:[]
in
let eventbox4 = GBin.event_box
~packing:(table8#attach ~left:2
~top:0
~right:3
~bottom:1
~xpadding:0
~ypadding:0
~expand:`NONE
~shrink:`NONE
~fill:`X
)
()
in
let toolbar26 = GButton.toolbar
~packing:eventbox4#add
~orientation:`HORIZONTAL
~button_relief:`NORMAL
~tooltips:true
~space_size:5
~space_style:`EMPTY
()
in
let button92 = toolbar26#insert_button
~icon:(GMisc.pixmap (GDraw.pixmap_from_xpm ~file:((Unix.getenv "PIXMAP_DIR") ^ "open.xpm") ()) ())#coerce
()
in
let _ = tooltips#set_tip ~text:"Browse for a reactive program file to test (.saofdm, .lus or .c) that is not in the current directory. Note that the current directory of Lurette will become the one of the sut if it changes." button92#coerce in
let build_env_button = toolbar26#insert_button
~icon:(GMisc.pixmap (GDraw.pixmap_from_xpm ~file:((Unix.getenv "PIXMAP_DIR") ^ "linegraph.xpm") ()) ())#coerce
()
in
let _ = tooltips#set_tip ~text:"Generates default environments for this SUT" build_env_button#coerce in
let vpaned2 = GPack.paned
`VERTICAL~handle_size:10
~packing:(vbox26#pack ~padding:2
......@@ -858,6 +867,10 @@ let _ = button99#connect#clicked
~callback:callbacks#run_lurette in
let _ = set_parameters#connect#clicked
~callback:callbacks#on_set_parameters_clicked in
let _ = build_env_button#connect#clicked
~callback:callbacks#build_env_clicked in
let _ = button92#connect#clicked
~callback:callbacks#browse_sut_clicked in
let _ = button98#connect#clicked
~callback:callbacks#show_env_button_clicked in
let _ = sut_compiler_entry#connect#changed
......@@ -878,8 +891,6 @@ let _ = oracle_name_entry#connect#changed
~callback:callbacks#on_oracle_name_changed in
let _ = button93#connect#clicked
~callback:callbacks#browse_oracle_clicked in
let _ = button92#connect#clicked
~callback:callbacks#browse_sut_clicked in
let _ = button91#connect#clicked
~callback:callbacks#add_env_clicked in
let _ = button90#connect#clicked
......@@ -899,8 +910,6 @@ method hbox39 = hbox39
method toolbar25 = toolbar25
method button90 = button90
method button91 = button91
method toolbar26 = toolbar26
method button92 = button92
method toolbar27 = toolbar27
method button93 = button93
method oracle_hbox = oracle_hbox
......@@ -927,6 +936,10 @@ method hbox42 = hbox42
method env_name = env_name
method env_name_entry = env_name
method button98 = button98
method eventbox4 = eventbox4
method toolbar26 = toolbar26
method button92 = button92
method build_env_button = build_env_button
method vpaned2 = vpaned2
method scrolledwindow8 = scrolledwindow8
method output_window = output_window
......
......@@ -731,6 +731,8 @@ class customized_callbacks = object(self)
self#update_lucky_files_combo ()
method ok_sut_clicked () =
let sut_file = cygpath_w2u self#top_fileselection_sut#fileselection_sut#get_filename in
let dir = Filename.dirname sut_file
......@@ -1040,6 +1042,16 @@ class customized_callbacks = object(self)
flush oc
method build_env_clicked () =
let sut = String.escaped self#top_xlurette#sut_name#entry#text
and sut_node = self#get_sut_node ()
and all_cmds = (self#get_all_cmds ())
in
output_string oc all_cmds ;
output_string oc ("build_env\n" );
flush oc;
self#update_lucky_files_combo ()
method call_sim2chro_clicked () =
let cmd_display =
if (get_rif_file ()) = "" then "" else
......@@ -1360,7 +1372,6 @@ class customized_callbacks = object(self)
self#top_xlurette#env_name#entry#set_text env
)
method run_lurette () =
......
This diff is collapsed.
......@@ -5,24 +5,24 @@ set LURETTE_PATH=/home/jahier/lurette
set PIXMAP_DIR=/home/jahier/lurette/share/pixmaps/
set path=/home/jahier/lurette/sparc-sun/bin:$path
set PATH=/home/jahier/lurette/sparc-sun/bin:$PATH
set path=/home/jahier/lurette/i386-linux/bin:$path
set PATH=/home/jahier/lurette/i386-linux/bin:$PATH
set PS_VIEWER=gv
set DOT=dot
set LUS2EC=lus2ec
set EC2C=ec2c
set SIM2CHRO=/home/jahier/lurette/sparc-sun/bin/sim2chrogtk
set HOST_TYPE=sparc-sun
set SIM2CHRO=/home/jahier/lurette/i386-linux/bin/sim2chrogtk
set HOST_TYPE=i386-linux
set GNUPLOTRIF=/home/jahier/lurette/share/gnuplot-rif
set PLOT=/home/jahier/lurette/share/plot
# scade
set SCADE2LUSTRE=scade2lustre
set SCADE_CG=scade_cg
set LUSTRE2C=lustre2C
set SCADE_INSTALL_DIR=/usr/local/tools/SCADE/SCADE-4.1.4/
set SCADE2LUSTRE=no
set SCADE_CG=no
set LUSTRE2C=no
set SCADE_INSTALL_DIR=
set SCADE_COMPIL_OPTION=" -noexp @ALL@ "
# Other options migth also work.
......
......@@ -5,6 +5,6 @@ arg=$@
# to put rif file in
[ -d Data ] || mkdir Data
. /home/jahier/lurette/sparc-sun/set_env_var
. /home/jahier/lurette/i386-linux/set_env_var
exec /home/jahier/lurette/sparc-sun/bin/show_luc_exe $arg
exec /home/jahier/lurette/i386-linux/bin/show_luc_exe $arg
......@@ -28,6 +28,20 @@ open Type
open Gen_stubs_common
let rec (no_numeric : typedef list -> Gen_stubs_common.vn_ct list -> bool) =
fun tdl vl ->
(* returns true iff [vl] contains no numeric variables *)
match vl with
| [] -> true
| (_,ct)::tail ->
(match (c_type_to_lucky_type tdl ct) with
| BoolT -> true
| UT(EnumT el) -> true
| _ -> false
)
&& (no_numeric tdl tail)
let (generate_lucky: string -> string -> typedef list ->
Gen_stubs_common.vn_ct list -> Gen_stubs_common.vn_ct list -> string ->
unit) =
......@@ -36,8 +50,7 @@ let (generate_lucky: string -> string -> typedef list ->
let file = (Filename.concat dir ((Filename.basename mod_name) ^ ".luc")) in
if Sys.file_exists file then
(
print_string ("\n*** " ^ file ^ " already exists in the " ^
"current directory: therefore i do nothing.\n") ;
output_string stdout ("\n\n\t " ^ file ^ " already exists.\n") ;
flush stdout
)
else
......@@ -104,8 +117,10 @@ let (generate_lucky: string -> string -> typedef list ->
put ";\n";
put " }\n";
close_out oc
close_out oc;
print_string ("\n\t -> " ^ file ^ " has been created;\n");
flush stdout
......@@ -117,8 +132,7 @@ let (generate_lucky2: string -> string -> typedef list ->
let file = (Filename.concat dir ((Filename.basename mod_name) ^ ".luc")) in
if Sys.file_exists file then
(
print_string ("\n*** " ^ file ^ " already exists in the " ^
"current directory: therefore i do nothing.\n") ;
output_string stdout ("\n\n\t " ^ file ^ " already exists.\n") ;
flush stdout
)
else
......@@ -206,7 +220,12 @@ let (generate_lucky2: string -> string -> typedef list ->
put " deltaI : int ~alias 5;\n";
put "\n";
put " init_cstr : bool ~alias \n";
List.iter (put_init_constraints) vo ;
if
no_numeric tdl vo
then
put "\t true"
else
List.iter (put_init_constraints) vo ;
put ";";
put "\n}\n";
......@@ -220,15 +239,24 @@ let (generate_lucky2: string -> string -> typedef list ->
put " -- we need two initialisation steps because the up_and_down \n";
put " -- macro refers to `pre pre var'\n";
put "\n";
put " loop -> loop ~cond \n";
List.iter (put_up_and_down_constraints) vo ;
put " loop -> loop ";
if
not (no_numeric tdl vo)
then
(
put " ~cond \n";
List.iter (put_up_and_down_constraints) vo
);
put ";\n";
put " }\n";
close_out oc
close_out oc;
print_string ("\n\t -> " ^ file ^ " has been created.\n");
flush stdout
let generate_up_and_down_macro _ =
let oc = open_out "up_and_down_macro" in
let generate_up_and_down_macro dir =
let file = (Filename.concat dir "up_and_down_macro") in
let oc = open_out file in
output_string oc "// % -*- mode: C; c-mode -*-
// use cpp to make Var goes up and down (and so on) between Min and Max,
......@@ -308,7 +336,7 @@ let rec (main : unit -> unit) =
in
generate_lucky compiler (mod_name) tdl vo vi dir;
generate_lucky2 compiler (mod_name) tdl vo vi dir;
generate_up_and_down_macro ()
generate_up_and_down_macro dir
;;
......
......@@ -33,8 +33,8 @@ type acc_solve_formula = (Run_aut.path list * sl * sl) list * Run_aut.t list
let (solve_formula: Var.env_in -> Env_state.t -> int -> Thickness.numeric ->
acc_solve_formula -> Run_aut.path -> formula -> Run_aut.t ->
var list -> var list -> acc_solve_formula) =
fun input state p num_thickness (acc, al_acc) path f a bool_vars_to_gen
num_vnt_to_gen ->
fun input state p num_thickness (acc, al_acc) path f a
bool_vars_to_gen num_vnt_to_gen ->
(**
Returns [p] solutions for the formula [f]; a solution is a
triple containing
......@@ -53,8 +53,8 @@ let (solve_formula: Var.env_in -> Env_state.t -> int -> Thickness.numeric ->
let (sl_sl_l, new_a) =
match
Solver.solve_formula input state p num_thickness f bool_vars_to_gen_f
num_vnt_to_gen
Solver.solve_formula input state p num_thickness f
bool_vars_to_gen_f num_vnt_to_gen
with
None ->
let new_a = Run_aut.remove_formula a path state.d.verbose in
......@@ -94,7 +94,9 @@ let (solve_formula: Var.env_in -> Env_state.t -> int -> Thickness.numeric ->
open Env_state
let (solve_formula_list: Var.env_in -> Env_state.t -> int -> Thickness.numeric
(* nb : the each formula of the list is independant (i.e., concerns
different output variables *)
let (solve_formula_indep_list: Var.env_in -> Env_state.t -> int -> Thickness.numeric
-> (pathl * sl * sl) list list * Run_aut.t list
-> pathl * formula list
-> (pathl * sl * sl) list list * Run_aut.t list) =
......@@ -139,11 +141,10 @@ let (cartesian_product_list: ('p * 'f) list list -> ('p list * 'f list) list) =
)
let rec (draw_values : Var.env_in -> Env_state.t -> bool -> int ->
Thickness.numeric -> Run_aut.t list ->
Thickness.numeric -> Run_aut.t list -> Run_aut.path option list ->
Run_aut.t list * (Run_aut.path list * sl * sl) list) =
fun input state draw_all_formula p num_thickness al ->
fun input state draw_all_formula p num_thickness al path_option_list ->
if al = [] then raise Not_found else
let pathl_fl_l =
(* Draw one formula, or get them all *)
......@@ -154,7 +155,9 @@ let rec (draw_values : Var.env_in -> Env_state.t -> bool -> int ->
assert (for_all (fun l -> l <> []) path_f_ll) ;
cartesian_product_list path_f_ll
else
let path_f_l = rev_map (Run_aut.choose_one_formula input state) al in
let path_f_l =
rev_map2 (Run_aut.choose_one_formula input state) path_option_list al
in
let pathl_fl =
List.fold_left
(fun acc path_f ->
......@@ -170,13 +173,14 @@ let rec (draw_values : Var.env_in -> Env_state.t -> bool -> int ->
(*
Draw [p] solutions for each of the [n] formula. Whenever a formula
is unsatisfiable for numerical reasons, the automata [a] is
updated by [solve_formula_list] and returned in [new_a].
updated by [solve_formula_indep_list] and returned in [new_a].
*)
let (pathl_sl_sl_ll, new_al) =
List.fold_left (solve_formula_list input state p num_thickness)
List.fold_left
(solve_formula_indep_list input state p num_thickness)
([], al) pathl_fl_l
in
let pathl_sl_sl_l = List.flatten pathl_sl_sl_ll in
let pathl_sl_sl_l = List.flatten pathl_sl_sl_ll in
if
pathl_sl_sl_l <> []
then
......@@ -187,10 +191,15 @@ let rec (draw_values : Var.env_in -> Env_state.t -> bool -> int ->
constraints. We redraw. Note that whenever no formula
can be drawn anymore, the [Not_found] exception is raised
*)
(
assert (al <> new_al);
(draw_values input state draw_all_formula p num_thickness new_al)
)
let pathl = fst (hd pathl_fl_l) in
(
assert (al <> new_al);
assert (not draw_all_formula);
(draw_values
input state draw_all_formula p num_thickness new_al
(List.map (fun x -> Some x) pathl)
)
)
(****************************************************************************)
......@@ -256,7 +265,6 @@ type solution = Var.env_out * Var.env_loc
(* to avoid to call Run_aut.get in step *)
let some_al = ref None
(* Exported *)
let (env_try_do : Thickness.t -> env_in -> Env_state.t ->
(pathl * env_out * env_loc) list) =
fun ((draw_all_f, p), num_thickness) input state ->
......@@ -265,10 +273,14 @@ let (env_try_do : Thickness.t -> env_in -> Env_state.t ->
None -> Run_aut.get input state state.d.current_nodes
| Some al -> al
in
let (new_al, sol) = draw_values input state draw_all_f p num_thickness al in
let (new_al, sol) =
draw_values input state draw_all_f p num_thickness
al (map (fun _ -> None) al)
in
some_al := Some new_al;
sol
(* Exported *)
let (env_try : Thickness.t -> env_in -> Env_state.t -> (env_out * env_loc) list) =
fun t input state ->
let sol = env_try_do t input state in
......
......@@ -576,7 +576,7 @@ and
main_loop t s p k1 k2 k3 rif input state =
let _ =
if (k1 = 0 && k2 = 0 && k3 = 0) then () else
if (k1 = 0 && k2 = 0 && k3 = 0 && not(options.draw_all_vertices)) then () else
(
let num_thickness =
(k1, k2,
......
......@@ -638,7 +638,7 @@ let clean _ =
)
in
let _ = try Sys.command rm_cmd with _ -> 0 in
print_string (rm_cmd ^ "\n")
output_string stderr (rm_cmd ^ "\n")