Commit 79b18f3b authored by Erwan Jahier's avatar Erwan Jahier

lurette 1.7 Fri, 10 Oct 2003 14:01:43 +0200 by jahier

Parent-Version:      1.6
Version-Log:

source/fair_bddd.ml: [new]
source/fair_bddd.mli: [new]
   The same as bddd, but taking polyhedron volume into account.

source/bddd.ml:
   It is useless to store both bdd and not bdd, because it is just
   so easy to recompute the sol nb of not bdd (by switchinf the
   pair of sol numbers!).

source/lurettetop.ml:
source/lurette.ml:
source/luc_exe.ml:
   add a --compute-poly-volume option that makes lurette use
   fair_bddd instead of bddd.

Project-Description: Lurette
parent 7189e37a
This diff is collapsed.
*********** BUGS
* ZZZ une contrainte du style "0<x<100 and x<>2" va tirer "1" une fois sur 2 !!!
car "x<>2" est traduit en "x<2 or x>2" et le choix sur le or est effectué de
facon équitable ...
En particulier, je ne peux donc pas representer des enum par des entiers...
* Quand je tire une solution dans le gras de l'épaisseur,
il faut que je tienne compte des poids des transitions
avec l'option --draw-all-formula
-> idem au sein du polyedre ; oui mais laquelle prendre ?
inside ? n'importe laquelle ?
-> if suffit de refaire en un env_try false 1 0 0 ....
=> Solution on remonte du bdd le nombre de solutions entieres presentes
a chaque feuille.
pour cela, je dois changer un peu de philosophie (cf solver.ml).
Avant:
1- calcul du nombre de solutions d'un point de vue Booleen
2- tirage dans le bdd tenant compte des poids obtenu en (1)
en verifiant au fur et a mesure les contraintes numeriques
faciles, a savoir celles de dimensions 1
3- une fois aux feuilles, s'il reste des contraintes de dimensions > 1,
faire appel à Polka.
Apres:
1- calcul du nombre de solutions d'un point de vue Booleen ET
des variables numériques de dimension 1.
2- tirage dans le bdd tenant compte des poids obtenu en (1)
3- comme avant
en d'autre termes, je fais la vérif de satisfiabilité des intervalles
lors du calcul du nombre de solutions, et pas lors du tirage dans le bdd.
* compilé en mode "assert", lurette se fait tuer par un signal 11
au bout d'une dizaine de pas...
* en mode fair, certaine requete aboutisse a qque chose de vraiment
pas satisfaisant : pleins de polyhedres intermediaires inutiles
sont calcules, selon l'ordre dans lequel arrivent les contraintes...
****** Documentation
* Rajouter un mode ecexe dans lurette
* documenter les options ~default, ~alias, etc.
* Decrire l'heuristique utilisée pour choisir le vecteur qui va servir
dans la suite de l'execution ().
* Signaler les approximations faites (en dimension > 1)
- volumes des polyhedres pas calculés (=> pb d'equité)
- pour le choix des entiers, on travaille dans les reels,
......@@ -54,10 +46,15 @@
dans ]0;3[ dans le 1er contre 75% dans le 2eme.
* Il faut aussi documenter les probas de f=1.0 vs 0<f<1. Avec un pas de 10,
ca donne 10% vs 90% ... On pourrait donner un pas plus petit, mais ca
desiquilibrerait l'importance des reels par rapport aux entiers et
aux Booleens. Et puis f=1.0 est une valeur particuliere qu'il est légitime
de vouloir tester plus souvent...
ca donne 10% vs 90% en mode <<efficient draw>>
Faire remarquer que dans certain cas, le fair draw peut etre plus rapide ...
mais que dans d'autre, il peut etre trs tres cher !
(2) Faire une doc utilisateur pour lurette (moins urgent depuis qu'il y
a lurettetop et xlurette...)
......@@ -80,6 +77,8 @@
* Faire l'elimination des DAGS, ie,
finir la fonction duplicate_graph_from_node automata.ml
* ZZZ Changer le epsilon en 1/10^p !!!!!
* faire un passage sur map vs rev_map
......
......@@ -28,6 +28,11 @@
<class>GtkNotebook</class>
<name>notebook1</name>
<can_focus>True</can_focus>
<accelerator>
<modifiers>GDK_CONTROL_MASK</modifiers>
<key>GDK_Tab</key>
<signal>switch_page</signal>
</accelerator>
<show_tabs>True</show_tabs>
<show_border>True</show_border>
<tab_pos>GTK_POS_TOP</tab_pos>
......@@ -68,6 +73,7 @@
<widget>
<class>GtkTable</class>
<name>table2</name>
<height>150</height>
<rows>5</rows>
<columns>3</columns>
<homogeneous>False</homogeneous>
......@@ -843,7 +849,7 @@ scade
<class>GtkLabel</class>
<child_name>Notebook:tab</child_name>
<name>stderr_thumbnail</name>
<label>Misc outputs </label>
<label> Misc outputs </label>
<justify>GTK_JUSTIFY_CENTER</justify>
<wrap>False</wrap>
<xalign>0.5</xalign>
......@@ -858,7 +864,6 @@ scade
<class>GtkHBox</class>
<name>hbox1</name>
<border_width>11</border_width>
<height>72</height>
<homogeneous>False</homogeneous>
<spacing>4</spacing>
<child>
......@@ -1235,7 +1240,7 @@ scade
<tooltip>Try one formula</tooltip>
<can_focus>True</can_focus>
<label>One </label>
<active>True</active>
<active>False</active>
<draw_indicator>True</draw_indicator>
<child>
<padding>0</padding>
......@@ -1529,7 +1534,7 @@ scade
<widget>
<class>GtkRadioButton</class>
<name>radiobutton_draw_all</name>
<name>radiobutton_draw_all_vertices</name>
<tooltip>Try all the possible combination of values of vertices</tooltip>
<can_focus>True</can_focus>
<label>All </label>
......@@ -1544,13 +1549,13 @@ scade
<widget>
<class>GtkRadioButton</class>
<name>radiobuttondraw_some</name>
<name>radiobutton_draw_some_vertices</name>
<tooltip>Try some of the polyhedra vertices (cf the lhs spin button)</tooltip>
<can_focus>True</can_focus>
<label>Some</label>
<active>False</active>
<draw_indicator>True</draw_indicator>
<group>radiobutton_draw_all</group>
<group>radiobutton_draw_all_vertices</group>
<child>
<padding>0</padding>
<expand>False</expand>
......@@ -1733,7 +1738,7 @@ scade
<widget>
<class>GtkRadioButton</class>
<name>radiobutton10</name>
<name>radiobutton_efficient_draw</name>
<tooltip>Favour efficiency over fairness. This means that the draw of numric variable will not be really fair (cf lucky reference manual for more explanation).</tooltip>
<can_focus>True</can_focus>
<label>Efficiency</label>
......
......@@ -26,6 +26,14 @@ let notebook1 = GPack.notebook
()
in
let _ = GtkBase.Widget.set_can_focus notebook1#as_widget true in
let _ = notebook1#misc#add_accelerator
~group:accel_group
GdkKeysyms._Tab
~sgn:{ GtkSignal.name = "switch_page";
GtkSignal.marshaller = GtkSignal.marshal_unit ;
GtkSignal.classe = `base }
~modi:[`CONTROL;]
in
let run_panel = GPack.paned
`VERTICAL~handle_size:10
~border_width:3
......@@ -48,6 +56,7 @@ let table2 = GPack.table
~row_spacings:0
~col_spacings:0
~homogeneous:false
~height:150
~packing:frame1#add
()
in
......@@ -541,7 +550,7 @@ let _ = GtkBase.Widget.set_can_focus error_window#as_widget true in
let _ = GtkBase.Widget.set_can_default error_window#as_widget true in
let _ = GtkBase.Widget.grab_default error_window#as_widget in
let stderr_thumbnail = GMisc.label
~text: "Misc outputs "
~text: " Misc outputs "
~xalign:0.5
~yalign:0.5
~xpad:0
......@@ -552,7 +561,6 @@ in
let hbox1 = GPack.hbox
~spacing:4
~homogeneous:false
~height:72
~packing:(run_panel#add )
()
in
......@@ -816,7 +824,7 @@ let radiobutton_draw_one_formula = GButton.radio_button
)
~label: "One "
~draw_indicator:true
~active:true
~active:false
()
in
let _ = GtkBase.Widget.set_can_focus radiobutton_draw_one_formula#as_widget true in
......@@ -1047,7 +1055,7 @@ let label38 = GMisc.label
~width:210
()
in
let radiobutton_draw_all = GButton.radio_button
let radiobutton_draw_all_vertices = GButton.radio_button
~packing:(hbox22#pack ~padding:0
~fill:false
~expand:false
......@@ -1057,10 +1065,10 @@ let radiobutton_draw_all = GButton.radio_button
~active:true
()
in
let _ = GtkBase.Widget.set_can_focus radiobutton_draw_all#as_widget true in
let _ = tooltips#set_tip ~text:"Try all the possible combination of values of vertices" radiobutton_draw_all#coerce in
let radiobuttondraw_some = GButton.radio_button
~group:radiobutton_draw_all#group
let _ = GtkBase.Widget.set_can_focus radiobutton_draw_all_vertices#as_widget true in
let _ = tooltips#set_tip ~text:"Try all the possible combination of values of vertices" radiobutton_draw_all_vertices#coerce in
let radiobutton_draw_some_vertices = GButton.radio_button
~group:radiobutton_draw_all_vertices#group
~packing:(hbox22#pack ~padding:0
~fill:false
~expand:false
......@@ -1070,8 +1078,8 @@ let radiobuttondraw_some = GButton.radio_button
~active:false
()
in
let _ = GtkBase.Widget.set_can_focus radiobuttondraw_some#as_widget true in
let _ = tooltips#set_tip ~text:"Try some of the polyhedra vertices (cf the lhs spin button)" radiobuttondraw_some#coerce in
let _ = GtkBase.Widget.set_can_focus radiobutton_draw_some_vertices#as_widget true in
let _ = tooltips#set_tip ~text:"Try some of the polyhedra vertices (cf the lhs spin button)" radiobutton_draw_some_vertices#coerce in
let vertices_nb = GEdit.spin_button
~adjustment:(GData.adjustment~value:1.
~lower:0.
......@@ -1178,6 +1186,54 @@ let user_seed = GEdit.spin_button
in
let _ = GtkBase.Widget.set_can_focus user_seed#as_widget true in
let _ = tooltips#set_tip ~text:"The seed used (if the Manual button is selected)" user_seed#coerce in
let hbox33 = GPack.hbox
~spacing:0
~homogeneous:false
~packing:(vbox9#pack ~padding:0
~fill:true
~expand:true
)
()
in
let label60 = GMisc.label
~text: " Draw Fairness versus Efficiency "
~packing:(hbox33#pack ~padding:0
~fill:false
~expand:false
)
~xalign:0.5
~yalign:0.5
~xpad:0
~ypad:0
~line_wrap:true
~width:220
()
in
let radiobutton_fair_draw = GButton.radio_button
~packing:(hbox33#pack ~padding:0
~fill:false
~expand:false
)
~label: "Fairness"
~draw_indicator:true
~active:false
()
in
let _ = GtkBase.Widget.set_can_focus radiobutton_fair_draw#as_widget true in
let _ = tooltips#set_tip ~text:"Favour the draw fairness over efficiency. " radiobutton_fair_draw#coerce in
let radiobutton_efficient_draw = GButton.radio_button
~group:radiobutton_fair_draw#group
~packing:(hbox33#pack ~padding:0
~fill:false
~expand:false
)
~label: "Efficiency"
~draw_indicator:true
~active:true
()
in
let _ = GtkBase.Widget.set_can_focus radiobutton_efficient_draw#as_widget true in
let _ = tooltips#set_tip ~text:"Favour efficiency over fairness. This means that the draw of numric variable will not be really fair (cf lucky reference manual for more explanation)." radiobutton_efficient_draw#coerce in
let hbox2 = GPack.hbox
~spacing:0
~homogeneous:false
......@@ -1325,53 +1381,6 @@ let radiobutton_display_local_no = GButton.radio_button
()
in
let _ = GtkBase.Widget.set_can_focus radiobutton_display_local_no#as_widget true in
let hbox12 = GPack.hbox
~spacing:0
~homogeneous:false
~packing:(vbox9#pack ~padding:0
~fill:false
~expand:false
)
()
in
let label21 = GMisc.label
~text: " Use the progress bar "
~packing:(hbox12#pack ~padding:0
~fill:false
~expand:false
)
~xalign:0.5
~yalign:0.5
~xpad:0
~ypad:0
~line_wrap:true
~width:220
()
in
let radiobutton_show_step_on = GButton.radio_button
~packing:(hbox12#pack ~padding:0
~fill:false
~expand:false
)
~label: "Yes"
~draw_indicator:true
~active:true
()
in
let _ = GtkBase.Widget.set_can_focus radiobutton_show_step_on#as_widget true in
let _ = tooltips#set_tip ~text:"Migth slow down the execution a smidgin" radiobutton_show_step_on#coerce in
let radiobutton_show_step_off = GButton.radio_button
~group:radiobutton_show_step_on#group
~packing:(hbox12#pack ~padding:0
~fill:false
~expand:false
)
~label: "No"
~draw_indicator:true
~active:false
()
in
let _ = GtkBase.Widget.set_can_focus radiobutton_show_step_off#as_widget true in
let hbox6 = GPack.hbox
~spacing:0
~homogeneous:false
......@@ -1464,52 +1473,6 @@ let label56 = GMisc.label
~line_wrap:false
()
in
let hbox30 = GPack.hbox
~spacing:0
~homogeneous:false
~packing:(vbox9#pack ~padding:0
~fill:true
~expand:true
)
()
in
let save_session_label = GMisc.label
~text: " Saved session "
~packing:(hbox30#pack ~padding:0
~fill:false
~expand:false
)
~xalign:0.5
~yalign:0.5
~xpad:0
~ypad:0
~line_wrap:false
()
in
let saved_session_file = GEdit.entry
~packing:(hbox30#pack ~padding:0
~fill:false
~expand:false
)
~text: "lurette.tgz"
~max_length:0
~visibility:true
~editable:true
()
in
let _ = GtkBase.Widget.set_can_focus saved_session_file#as_widget true in
let _ = tooltips#set_tip ~text:"Name of the file the current session is saved under" saved_session_file#coerce in
let button2 = GButton.button
~packing:(hbox30#pack ~padding:0
~fill:false
~expand:false
)
~label: " Save session "
~border_width:4
()
in
let _ = GtkBase.Widget.set_can_focus button2#as_widget true in
let _ = tooltips#set_tip ~text:"Save the current session" button2#coerce in
let label53 = GMisc.label
~packing:(vbox9#pack ~padding:0
~fill:false
......@@ -1674,8 +1637,6 @@ let _ = button15#connect#clicked
~callback:callbacks#save_parameters in
let _ = button14#connect#clicked
~callback:callbacks#call_sim2chro_clicked in
let _ = button2#connect#clicked
~callback:callbacks#save_session in
let _ = test_thickness_button#connect#clicked
~callback:callbacks#on_test_thickness_help_button_clicked in
let _ = quit_button#connect#clicked
......@@ -1805,8 +1766,8 @@ method edges_nb = edges_nb
method hbox22 = hbox22
method label46 = label46
method label38 = label38
method radiobutton_draw_all = radiobutton_draw_all
method radiobuttondraw_some = radiobuttondraw_some
method radiobutton_draw_all_vertices = radiobutton_draw_all_vertices
method radiobutton_draw_some_vertices = radiobutton_draw_some_vertices
method vertices_nb = vertices_nb
method label42 = label42
method hbox9 = hbox9
......@@ -1814,6 +1775,10 @@ method label16 = label16
method radiobutton_random_seed = radiobutton_random_seed
method radiobutton_user_seed = radiobutton_user_seed
method user_seed = user_seed
method hbox33 = hbox33
method label60 = label60
method radiobutton_fair_draw = radiobutton_fair_draw
method radiobutton_efficient_draw = radiobutton_efficient_draw
method hbox2 = hbox2
method label11 = label11
method hbox10 = hbox10
......@@ -1827,10 +1792,6 @@ method hbox5 = hbox5
method display_local_label = display_local_label
method radiobutton_display_local_yes = radiobutton_display_local_yes
method radiobutton_display_local_no = radiobutton_display_local_no
method hbox12 = hbox12
method label21 = label21
method radiobutton_show_step_on = radiobutton_show_step_on
method radiobutton_show_step_off = radiobutton_show_step_off
method hbox6 = hbox6
method label15 = label15
method radiobutton_verbose_on = radiobutton_verbose_on
......@@ -1839,10 +1800,6 @@ method hbox29 = hbox29
method label52 = label52
method rif_file_basename = rif_file_basename
method label56 = label56
method hbox30 = hbox30
method save_session_label = save_session_label
method saved_session_file = saved_session_file
method button2 = button2
method label53 = label53
method toolbar3 = toolbar3
method button14 = button14
......
......@@ -792,6 +792,12 @@ class customized_callbacks = object(self)
else ("set_seed " ^ self#top_xlurette#user_seed#text ^ "\n")
in
let cmd_compute_vol =
if self#top_xlurette#radiobutton_fair_draw#active
then "set_compute_volume true\n"
else "set_compute_volume false\n"
in
let cmd_draw_all_formula =
if self#top_xlurette#radiobutton_draw_all_formula#active
then "set_draw_all_formula true\n"
......@@ -805,7 +811,7 @@ class customized_callbacks = object(self)
in
let cmd_draw_vertices =
if
self#top_xlurette#radiobutton_draw_all#active
self#top_xlurette#radiobutton_draw_all_vertices#active
then
"set_draw_all_vertices true\n"
else
......@@ -832,10 +838,12 @@ class customized_callbacks = object(self)
in
let cmd_show_step =
if (self#top_xlurette#radiobutton_show_step_on#active
|| self#top_xlurette#radiobutton_verbose_on#active )
then "set_show_step true \n"
else "set_show_step false \n"
(* if (self#top_xlurette#radiobutton_show_step_on#active *)
(* || self#top_xlurette#radiobutton_verbose_on#active ) *)
(* then *)
"set_show_step true \n"
(* else *)
(* "set_show_step false \n" *)
in
let extra_cfiles =
......@@ -852,9 +860,10 @@ class customized_callbacks = object(self)
(String.escaped self#top_extra_env_var_window#extra_includedirs_entry#text) ^ "\"\n")
in
cmd_test_length ^ cmd_draw_nb
cmd_test_length ^ cmd_draw_nb ^ cmd_compute_vol
^ cmd_rif_file ^ cmd_sut ^ cmd_env ^ cmd_oracle ^ cmd_step ^ cmd_seed
^ cmd_draw_inside ^ cmd_draw_edges ^ cmd_draw_vertices ^ cmd_call_sim2chro
^ cmd_draw_inside ^ cmd_draw_edges ^ cmd_draw_vertices
^ cmd_draw_all_formula ^ cmd_call_sim2chro
^ cmd_display_local ^ cmd_verbose ^ cmd_show_step ^ cmd_sut_compiler
^ cmd_oracle_compiler ^ extra_cfiles ^ extra_libs ^ extra_libdirs
^ extra_includedirs
......@@ -1015,11 +1024,11 @@ class customized_callbacks = object(self)
method save_session () =
output_string oc ("pack " ^ self#top_xlurette#saved_session_file#text ^ " \n");
flush oc;
prerr_endline "save session ...";
()
(* method save_session () = *)
(* output_string oc ("pack " ^ self#top_xlurette#saved_session_file#text ^ " \n"); *)
(* flush oc; *)
(* prerr_endline "save session ..."; *)
(* () *)
method get_env () =
......@@ -1077,20 +1086,20 @@ class customized_callbacks = object(self)
self#top_xlurette#draw_nb#set_text (string_of_int i)
method get_draw_inside () =
method get_draw_inside_nb () =
int_of_string self#top_xlurette#inside_nb#text
method set_draw_inside i =
method set_draw_inside_nb i =
self#top_xlurette#inside_nb#set_text (string_of_int i)
method get_draw_edges () =
method get_draw_edges_nb () =
int_of_string self#top_xlurette#edges_nb#text
method set_draw_edges i =
method set_draw_edges_nb i =
self#top_xlurette#edges_nb#set_text (string_of_int i)
method get_draw_vertices () =
method get_draw_vertices_nb () =
int_of_string self#top_xlurette#vertices_nb#text
method set_draw_vertices i =
self#top_xlurette#inside_nb#set_text (string_of_int i)
method set_draw_vertices_nb i =
self#top_xlurette#vertices_nb#set_text (string_of_int i)
......@@ -1099,10 +1108,10 @@ class customized_callbacks = object(self)
method set_rif_file_basename str =
self#top_xlurette#rif_file_basename#set_text str
method get_restore () =
self#top_xlurette#saved_session_file#text
method set_restore str =
self#top_xlurette#saved_session_file#set_text str
(* method get_restore () = *)
(* self#top_xlurette#saved_session_file#text *)
(* method set_restore str = *)
(* self#top_xlurette#saved_session_file#set_text str *)
......@@ -1169,6 +1178,13 @@ class customized_callbacks = object(self)
| [< 'Genlex.Ident "set_test_length" ; 'Genlex.Int i >] ->
self#set_test_length i
| [< 'Genlex.Ident "set_draw_inside" ; 'Genlex.Int i >] ->
self#set_draw_inside_nb i
| [< 'Genlex.Ident "set_draw_edges" ; 'Genlex.Int i >] ->
self#set_draw_edges_nb i
| [< 'Genlex.Ident "set_draw_vertices" ; 'Genlex.Int i >] ->
self#set_draw_vertices_nb i
| [< 'Genlex.Ident "set_draw_nb" ; 'Genlex.Int i >] ->
self#set_draw_nb i
......@@ -1177,6 +1193,23 @@ class customized_callbacks = object(self)
self#top_xlurette#radiobutton_user_seed#set_active true ;
self#set_seed i
| [< 'Genlex.Ident "set_compute_volume"; 'Genlex.Ident id >] ->
if id = "true"
then self#top_xlurette#radiobutton_fair_draw#set_active true
else self#top_xlurette#radiobutton_efficient_draw#set_active true
| [< 'Genlex.Ident "set_draw_all_formula"; 'Genlex.Ident id >] ->
if id = "true"
then self#top_xlurette#radiobutton_draw_all_formula#set_active true
else self#top_xlurette#radiobutton_draw_one_formula#set_active true
| [< 'Genlex.Ident "set_draw_all_vertices"; 'Genlex.Ident id >] ->
if id = "true"
then self#top_xlurette#radiobutton_draw_all_vertices#set_active true
else self#top_xlurette#radiobutton_draw_some_vertices#set_active true
| [< 'Genlex.Ident "set_seed_randomly" >] ->
self#top_xlurette#radiobutton_random_seed#set_active true
......@@ -1201,9 +1234,10 @@ class customized_callbacks = object(self)
else self#top_xlurette#radiobutton_verbose_off#set_active true
| [< 'Genlex.Ident "set_show_step" ; 'Genlex.Ident id >] ->
if id = "true"
then self#top_xlurette#radiobutton_show_step_on#set_active true
else self#top_xlurette#radiobutton_show_step_off#set_active true
()
(* if id = "true" *)
(* then self#top_xlurette#radiobutton_show_step_on#set_active true *)
(* else self#top_xlurette#radiobutton_show_step_off#set_active true *)
| [< 'Genlex.Ident "set_extra_cfiles" ; 'Genlex.String str >] ->
self#top_extra_env_var_window#extra_cfiles_entry#set_text str
......@@ -1277,13 +1311,13 @@ let rec speclist callbacks =
("<int>\t\tat each step (default=" ^
(string_of_int (callbacks#get_draw_nb ())) ^ ").\n");
"--draw-inside", Arg.Int (fun i -> callbacks#set_draw_inside i),
"--draw-inside", Arg.Int (fun i -> callbacks#set_draw_inside_nb i),
"<int>\tDraw on the edges of the convex hull of solutions.";
"--draw-edges", Arg.Int (fun i -> callbacks#set_draw_edges i),