Commit d115d326 authored by Erwan Jahier's avatar Erwan Jahier

lurette 1.21 Fri, 13 Feb 2004 18:25:56 +0100 by jahier

Parent-Version:      1.20
Version-Log:

source/lurette.ml:
source/command_line.ml:
source/command_line.mli:
source/lurettetop.ml:
   Plug the step mode stuff into xlurette.

   Repair the step_by_step mode that was broken under xlurette
   (still do not know why though...).

Project-Description: Lurette
parent b3d4d2c7
......@@ -30,7 +30,7 @@
(demo-xlurette/fault-tolerant-heater/sensors.luc 610 1076684617 h/18_sensors.lu 1.1)
(test/test_losange-10d.lus 108 1065787303 g/41_test_losan 1.1)
(polka/C/internal.h 916 1071844798 e/0_internal.h 1.2)
(source/command_line.ml 4750 1073401581 b/20_command_li 1.18)
(source/command_line.ml 5045 1076693156 b/20_command_li 1.19)
(test/cudd_gc_problem.rif.exp 7882 1053337243 e/30_cudd_gc_pr 1.2)
(test/sparc-scade/libpwlinear.saofdm 1379 1055487917 e/43_libpwlinea 1.1)
(test/cygwin-scade/ConfAnnot.aty 13661 1055926783 g/4_ConfAnnot. 1.1)
......@@ -46,7 +46,7 @@
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
(test/cygwin-scade/Pilot_cst.saofd 788 1055926783 f/38_Pilot_cst. 1.1)
(test/cygwin-scade/lib_pilot.etp 1173 1055926783 f/48_lib_pilot. 1.1)
(source/command_line.mli 1629 1069833150 b/21_command_li 1.14)
(source/command_line.mli 1707 1076693156 b/21_command_li 1.15)
(source/Makefile.lucky 5165 1076684617 b/41_Makefile.i 1.31)
(polka/README 1437 1047029868 e/19_README 1.1)
(README 2875 1076684617 10_README 1.12)
......@@ -87,16 +87,16 @@
(source/print.mli 1135 1069150632 46_print.mli 1.14)
(polka/caml/Makefile 6586 1071844798 d/45_Makefile 1.4)
(test/cygwin-scade/det_mvt_mode.saofd 4184 1055926783 f/51_det_mvt_mo 1.1)
(ihm/xlurette/xlurette_glade_main.ml 49790 1076684617 c/12_xlurette_g 1.34)
(ihm/xlurette/xlurette_glade_main.ml 50217 1076693156 c/12_xlurette_g 1.35)
(TAGS 9825 1007379917 21_TAGS 1.6)
(polka/C/main.tex 1961 1047029868 e/14_main.tex 1.1)
(ihm/xlurette/xlurette.glade 104736 1076684617 c/13_xlurette.g 1.26)
(ihm/xlurette/xlurette.glade 104738 1076693156 c/13_xlurette.g 1.27)
(test/cygwin-scade/MODULE.saofd 3026 1055926783 f/45_MODULE.sao 1.1)
(test/cygwin-scade/Command.saofd 4147 1055926783 g/6_Command.sa 1.1)
(test/cygwin-scade/lib_pilot.err 119 1055926783 f/49_lib_pilot. 1.1)
(test/losange.luc 410 1046768487 d/27_losange.lu 1.2)
(test/gyro.rif.exp 11065 1076684617 e/36_gyro.rif.e 1.10)
(test/time-ecrins.exp 9306 1076684617 d/21_time-ecrin 1.41)
(test/time-ecrins.exp 9314 1076693156 d/21_time-ecrin 1.42)
(source/value.ml 2534 1071235286 c/23_value.ml 1.7)
(source/gne.ml 3468 1076684617 b/37_gne.ml 1.7)
(test/cygwin-scade/Pilot.vsp 2075 1055926783 f/40_Pilot.vsp 1.1)
......@@ -187,7 +187,7 @@
(cuddaux/Makefile 3327 1076684617 c/35_Makefile 1.9)
(polka/C/bit.c 3301 1071844798 e/10_bit.c 1.2)
(source/draw.mli 452 1065787303 f/1_draw.mli 1.2)
(test/time-ossau.exp 9308 1073574172 b/48_time.exp 1.57)
(test/time-ossau.exp 9306 1076693156 b/48_time.exp 1.58)
(polka/caml/polkaIO.ml 1651 1071844798 d/44_polkaIO.ml 1.2)
(mlcuddidl/macros.m4 11392 1071844798 c/49_macros.m4 1.2)
(source/print.ml 5901 1074519403 47_print.ml 1.26)
......@@ -203,7 +203,7 @@
(source/run_aut.ml 23239 1076684617 b/47_automata.m 1.23)
(cuddaux/README 1427 1034006019 c/34_README 1.1)
(mlcuddidl/bdd.ml 11038 1071844798 d/6_bdd.ml 1.2)
(source/lurettetop.ml 48854 1076684617 c/1_lurettetop 1.49)
(source/lurettetop.ml 49660 1076693156 c/1_lurettetop 1.50)
(test/tram/tramway.luc 1015 1073401581 h/2_tramway.lu 1.1)
(source/constraint.ml 3180 1069150632 c/19_constraint 1.10)
(test/structured_type.luc 2308 1076684617 g/32_structured 1.2)
......@@ -212,12 +212,12 @@
(test/test7.rif.exp 381 1076684617 g/12_test7.rif. 1.5)
(test/poly-int/poly.lus 72 1073401581 h/7_poly.lus 1.1)
(source/bddd.ml 18278 1076684617 g/36_bddd.ml 1.8)
(ihm/xlurette/xlurette_glade_interface.ml 80841 1076684617 c/15_xlurette_g 1.24)
(ihm/xlurette/xlurette_glade_interface.ml 80843 1076693156 c/15_xlurette_g 1.25)
(INSTALL 101 1056616700 f/26_INSTALL 1.2)
(test/cygwin-scade/MyConsts.saofd 153 1055926783 f/44_MyConsts.s 1.1)
(test/losange-3d2.luc 355 1076684617 e/32_losange-3d 1.6)
(test/Makefile 3935 1076684617 c/0_Makefile 1.16)
(user-rules 36640 1076684617 c/14_myrules 1.54)
(user-rules 36645 1076693156 c/14_myrules 1.55)
(test/infinite_weight.luc 1113 1076684617 g/13_infinite_w 1.2)
(mlcuddidl/cudd_caml.c 23483 1071844798 d/3_cudd_caml. 1.2)
(polka/C/config.h 78 1071844798 e/13_config.h 1.2)
......@@ -282,7 +282,7 @@
(polka/C/polka.h 1791 1071844798 d/50_polka.h 1.2)
(share/pixmaps/ediff-quit.xpm 494 1055926783 f/20_ediff-quit 1.1)
(test/cygwin-scade/Pilot.saofd 3645 1055926783 f/42_Pilot.saof 1.1)
(test/time-moucherotte.exp 3375 1076684617 e/37_time-mouch 1.18)
(test/time-moucherotte.exp 3690 1076693156 e/37_time-mouch 1.19)
(source/command_line_luc_exe.ml 3790 1076684617 b/33_command_li 1.22)
(source/lurette_exe.c 220 1050421093 e/27_lurette_ex 1.2)
(share/pixmaps/close.xpm 803 1055926783 f/21_close.xpm 1.1)
......@@ -305,7 +305,7 @@
(source/luc_exe.ml 13900 1076684617 b/32_ima_exe.ml 1.46)
(source/gne.mli 1853 1063029729 b/36_gne.mli 1.6)
(test/cygwin-scade/Direction_D1.saofd 1298 1055926783 f/50_Direction_ 1.1)
(source/lurette.ml 20242 1076684617 12_lurette.ml 1.87)
(source/lurette.ml 20566 1076693156 12_lurette.ml 1.88)
(share/lucky.bat.in 584 1063786164 g/28_lucky.bat. 1.1)
(share/lucky.sh.in 106 1063786164 g/27_lucky.sh.i 1.1)
(test/sparc-scade/liblinear.saofdm 1301 1055487917 e/46_liblinear. 1.1)
......@@ -327,4 +327,4 @@
(test/cygwin-scade/Pilot_type.saofd 962 1055926783 f/37_Pilot_type 1.1)
(mlcuddidl/Makefile 7435 1076684617 d/9_Makefile 1.11)
(source/Makefile.show_luc 1506 1076684617 b/40_Makefile.s 1.14)
(test/time-rey.exp 9353 1076684617 h/13_time-rey.e 1.1)
(test/time-rey.exp 9336 1076693156 h/13_time-rey.e 1.2)
......@@ -3322,7 +3322,7 @@ Note that if one of the Draw All Formula (via DF) or Draw All Vertices (via DV)
<widget>
<class>GtkRadioButton</class>
<name>radiobutton_step_mode_inside</name>
<tooltip>Chose a point inside for the step</tooltip>
<tooltip>Choose a point inside for the step</tooltip>
<can_focus>True</can_focus>
<label>Inside</label>
<active>True</active>
......@@ -3353,7 +3353,7 @@ Note that if one of the Draw All Formula (via DF) or Draw All Vertices (via DV)
<widget>
<class>GtkRadioButton</class>
<name>radiobutton_step_mode_vertices</name>
<tooltip>Chose a point among vertices for the step </tooltip>
<tooltip>Choose a point among vertices for the step </tooltip>
<can_focus>True</can_focus>
<label>Vertices</label>
<active>False</active>
......
......@@ -2655,7 +2655,7 @@ let radiobutton_step_mode_inside = GButton.radio_button
()
in
let _ = GtkBase.Widget.set_can_focus radiobutton_step_mode_inside#as_widget true in
let _ = tooltips#set_tip ~text:"Chose a point inside for the step" radiobutton_step_mode_inside#coerce in
let _ = tooltips#set_tip ~text:"Choose a point inside for the step" radiobutton_step_mode_inside#coerce in
let radiobutton_step_mode_edges = GButton.radio_button
~group:radiobutton_step_mode_inside#group
~packing:(hbox45#pack ~padding:0
......@@ -2681,7 +2681,7 @@ let radiobutton_step_mode_vertices = GButton.radio_button
()
in
let _ = GtkBase.Widget.set_can_focus radiobutton_step_mode_vertices#as_widget true in
let _ = tooltips#set_tip ~text:"Chose a point among vertices for the step " radiobutton_step_mode_vertices#coerce in
let _ = tooltips#set_tip ~text:"Choose a point among vertices for the step " radiobutton_step_mode_vertices#coerce in
let hbox9 = GPack.hbox
~spacing:0
~homogeneous:false
......
......@@ -263,7 +263,7 @@ let (lusinfo : string -> string list) =
(** returns the list of files specified by the filter *)
let (get_files_list_filtered : string -> string list -> string list) =
fun filter init ->
let lustre_files_name = Filename.temp_file "xlurette" "filtered_files" in
let lustre_files_name = Filename.temp_file "xlurette" "filtered_files" in
let cmd = ("ls " ^ filter ^ " > " ^ lustre_files_name ^ " 2>/dev/null") in
let _ =
if
......@@ -336,7 +336,7 @@ class customized_callbacks = object(self)
then
display "\n"
else if
str = "One more loop ? [type any char to stop, `CR' to continue]"
str = "One more loop ? [type 's' to stop, `CR' to continue]"
then
display (
"One more loop ?
......@@ -618,7 +618,7 @@ class customized_callbacks = object(self)
if !pid <> 0 then (try Unix.kill (!pid) Sys.sigkill with _ -> () );
exit 0
method on_quit_xlurette_button_clicked () =
method on_quit_xlurette_button_clicked () =
self#top_quit_window#quit_window#show ()
method on_quit_yes_clicked () =
......@@ -659,7 +659,7 @@ class customized_callbacks = object(self)
self#top_set_parameters_window#radiobutton_step_yes#active
then
(
let cmd_stop = (" \n") in
let cmd_stop = ("s\n") in
if debug then (output_string stderr cmd_stop; flush stderr);
output_string oc cmd_stop;
flush oc;
......@@ -667,7 +667,7 @@ class customized_callbacks = object(self)
)
else
self#top_xlurette#output_window#insert
"Stop button unactive because step-by-step mode is off\n"
"Stop button unactive because step-by-step mode is off\n"
method on_delete_rif_button_clicked () =
......@@ -768,7 +768,7 @@ class customized_callbacks = object(self)
let cmd_env = ("set_env \"" ^ env ^ "\"\n") in
let oracle = String.escaped self#top_xlurette#oracle_name#entry#text
and oracle_node = self#top_xlurette#oracle_node#entry#text in
and oracle_node = self#top_xlurette#oracle_node#entry#text in
let cmd_oracle =
("set_oracle \"" ^ oracle ^ "\" \"" ^ oracle_node ^ "\"\n") in
......@@ -808,6 +808,15 @@ class customized_callbacks = object(self)
else ("set_seed " ^ self#top_set_parameters_window#user_seed#text ^ "\n")
in
let cmd_step_mode =
if self#top_set_parameters_window#radiobutton_step_mode_inside#active
then "set_step_mode inside\n" else
if self#top_set_parameters_window#radiobutton_step_mode_edges#active
then "set_step_mode edges\n" else
if self#top_set_parameters_window#radiobutton_step_mode_vertices#active
then "set_step_mode vertices\n" else assert false
in
let cmd_compute_vol =
if self#top_set_parameters_window#radiobutton_fair_draw#active
then "set_compute_volume true\n"
......@@ -881,7 +890,7 @@ class customized_callbacks = object(self)
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_draw_inside ^ cmd_draw_edges ^ cmd_draw_vertices ^ cmd_step_mode
^ cmd_draw_all_formula ^ cmd_call_sim2chro ^ cmd_precision
^ cmd_display_local ^ cmd_verbose ^ cmd_show_step ^ cmd_sut_compiler
^ cmd_oracle_compiler ^ extra_cfiles ^ extra_libs ^ extra_libdirs
......@@ -1044,12 +1053,14 @@ class customized_callbacks = object(self)
let all_cmds = (self#get_all_cmds ()) ^ "run\n" in
let all_cmds = (self#get_all_cmds ()) in
if self#top_set_parameters_window#radiobutton_step_yes#active
then self#top_step_by_step_window#step_by_step_window#show ();
output_string oc all_cmds ;
if debug then (output_string stderr all_cmds; flush stderr) ;
flush oc;
output_string oc "run\n" ;
if debug then (output_string stderr (all_cmds ^ "run\n"); flush stderr) ;
flush oc;
if
self#top_xlurette#env_name#entry#text = ""
......@@ -1066,7 +1077,7 @@ class customized_callbacks = object(self)
self#read_env_files ()
);
self#update_all_combo_boxes ();
self#top_xlurette#rif_file#entry#set_text (get_rif_file ())
self#top_xlurette#rif_file#entry#set_text (get_rif_file ())
method on_env_name_entry_changed () =
self#read_env_files ()
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 1 20)
(Parent-Version lurette 1 19)
(Project-Version lurette 1 21)
(Parent-Version lurette 1 20)
(Version-Log "
source/store.ml:
Fix a bug found by Bertrand where it was necessary to
apply substitutions each time a constraint is added
Maybe it is sometimes overkill, but it is safe,
and performance does not seem to suffer that much.
source/parse_luc.ml:
Do not open the .luc file twice, and keep the whole file
in a string to call the lustre expression parser.
This was an attempt to make the debbuger work again
with big .luc file, but it fails... The Stream lib really
seems to suck AFA ocamldebug is concerned.
Also shout when a wrong flag is used.
source/lurette.ml:
when an assertion is violated, put the corresponding vector
in the .rif file.
source/command_line.ml:
source/command_line.mli:
source/lurettetop.ml:
Plug the step mode stuff into xlurette.
Repair the step_by_step mode that was broken under xlurette
(still do not know why though...).
")
(New-Version-Log ""
)
(Checkin-Time "Fri, 13 Feb 2004 16:03:37 +0100")
(Checkin-Time "Fri, 13 Feb 2004 18:25:56 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -49,10 +35,10 @@ source/lurette.ml:
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.16 644))
(source/lurette.ml (lurette/12_lurette.ml 1.87 644))
(source/lurette.ml (lurette/12_lurette.ml 1.88 644))
(source/command_line.ml (lurette/b/20_command_li 1.18 644))
(source/command_line.mli (lurette/b/21_command_li 1.14 644))
(source/command_line.ml (lurette/b/20_command_li 1.19 644))
(source/command_line.mli (lurette/b/21_command_li 1.15 644))
;; Sources files common to lurette and luc_exe
(source/graph.mli (lurette/13_graph.mli 1.13 644))
......@@ -101,7 +87,7 @@ source/lurette.ml:
(source/gne.mli (lurette/b/36_gne.mli 1.6 644))
(source/gne.ml (lurette/b/37_gne.ml 1.7 644))
(source/lurettetop.ml (lurette/c/1_lurettetop 1.49 644))
(source/lurettetop.ml (lurette/c/1_lurettetop 1.50 644))
(source/draw.mli (lurette/f/1_draw.mli 1.2 644))
(source/draw.ml (lurette/f/2_draw.ml 1.3 644))
......@@ -166,7 +152,7 @@ source/lurette.ml:
(Makefile.common.source (lurette/e/33_Makefile.c 1.11 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.51 644))
(share/Makefile.lurette.in (lurette/b/38_Makefile.l 1.31 644))
(user-rules (lurette/c/14_myrules 1.54 644))
(user-rules (lurette/c/14_myrules 1.55 644))
(share/Makefile.test.in (lurette/c/25_user-rules 1.12 644))
(Makefile (lurette/d/13_Makefile 1.4 644))
......@@ -197,13 +183,13 @@ source/lurette.ml:
(share/gnuplot-rif (lurette/e/34_gnuplot-ri 1.7 744))
(share/plot (lurette/e/35_plot 1.8 744))
(test/time-rey.exp (lurette/h/13_time-rey.e 1.1 644))
(test/time-rey.exp (lurette/h/13_time-rey.e 1.2 644))
(test/time-rey.res (lurette/h/14_time-rey.r 1.1 644))
(test/time-ossau.exp (lurette/b/48_time.exp 1.57 644))
(test/time-ossau.exp (lurette/b/48_time.exp 1.58 644))
(test/time-ossau.res (lurette/b/49_time.res 1.61 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.42 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.41 644))
(test/time-moucherotte.exp (lurette/e/37_time-mouch 1.18 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.42 644))
(test/time-moucherotte.exp (lurette/e/37_time-mouch 1.19 644))
(test/time-moucherotte.res (lurette/e/38_time-mouch 1.19 644))
;; Various files used for testing purposes
......@@ -303,9 +289,9 @@ source/lurette.ml:
(test/Makefile (lurette/c/0_Makefile 1.16 644))
;; xlurette
(ihm/xlurette/xlurette_glade_main.ml (lurette/c/12_xlurette_g 1.34 644))
(ihm/xlurette/xlurette.glade (lurette/c/13_xlurette.g 1.26 644))
(ihm/xlurette/xlurette_glade_interface.ml (lurette/c/15_xlurette_g 1.24 644))
(ihm/xlurette/xlurette_glade_main.ml (lurette/c/12_xlurette_g 1.35 644))
(ihm/xlurette/xlurette.glade (lurette/c/13_xlurette.g 1.27 644))
(ihm/xlurette/xlurette_glade_interface.ml (lurette/c/15_xlurette_g 1.25 644))
(ihm/xlurette/makefile (lurette/c/16_makefile 1.20 644))
......
(*-----------------------------------------------------------------------
** Copyright (C) 2001 - 2003 - Verimag.
** Copyright (C) - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
......@@ -9,6 +9,7 @@
*)
type optionsT = {
mutable step_by_step : bool ;
mutable display_local_var : bool ;
......@@ -22,6 +23,7 @@ type optionsT = {
mutable draw_all_formula : bool;
mutable draw_all_vertices : bool;
mutable compute_volume : bool;
mutable step_mode : Lucky.step_mode;
mutable oracle : bool
}
......@@ -32,7 +34,7 @@ type cmd_line_optionT =
| AllVertices | AllFormula
(* | CuddHeapInit *)
| Seed | Precision | NoOracle | Verbose | ShowStep | Output
| ComputeVolume
| ComputeVolume | StepInside | StepEdges | StepVertices
(* Names of the command line options to override the defaults. *)
let (string_to_option: (string * cmd_line_optionT) list) = [
......@@ -72,6 +74,11 @@ let (string_to_option: (string * cmd_line_optionT) list) = [
("--draw-all-formula", AllFormula);
("--compute-poly-volume", ComputeVolume);
("--step-inside", StepInside);
("--step-edges", StepEdges);
("--step-vertices", StepVertices);
(* ("--init-cudd-heap", CuddHeapInit) *)
......@@ -99,6 +106,9 @@ let (option_to_usage: cmd_line_optionT -> string) =
| ComputeVolume -> (
"Compute the polyhedra volume before drawing: more fair, " ^
"but more expensive.")
| StepInside -> "Step inside\n"
| StepEdges -> "Step at edges\n"
| StepVertices -> "Step at vertices\n"
let (group_common_options: (string * cmd_line_optionT) list ->
(string * cmd_line_optionT) list) =
......
(*-----------------------------------------------------------------------
** Copyright (C) 2001 - 2003 - Verimag.
** Copyright (C) - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
......@@ -12,6 +12,7 @@
printing lurette usage message, handling command line options, etc.
*)
open Lucky
type optionsT = {
mutable step_by_step : bool ;
......@@ -26,6 +27,7 @@ type optionsT = {
mutable draw_all_formula : bool;
mutable draw_all_vertices : bool;
mutable compute_volume : bool;
mutable step_mode : Lucky.step_mode;
mutable oracle : bool
}
......@@ -45,7 +47,7 @@ type cmd_line_optionT =
(* | CuddHeapInit *)
| AllVertices | AllFormula
| Seed | Precision | NoOracle | Verbose | ShowStep | Output
| ComputeVolume
| ComputeVolume | StepInside | StepEdges | StepVertices
val string_to_option: (string * cmd_line_optionT) list
......
......@@ -21,6 +21,8 @@ open Env_state
(*------------------------------------------------------------------------*)
let (options:Command_line.optionsT) = {
step_by_step = false ;
display_local_var = false ;
......@@ -33,6 +35,7 @@ let (options:Command_line.optionsT) = {
draw_all_formula = false;
draw_all_vertices = false;
compute_volume = false;
step_mode = Lucky.StepInside;
oracle = true
}
......@@ -466,6 +469,11 @@ and
| Sim2chro -> options.display_sim2chro <- true ; (n+1)
| NoSim2chro -> options.display_sim2chro <- false ; (n+1)
| StepInside -> options.step_mode <- Lucky.StepInside ; (n+1)
| StepEdges -> options.step_mode <- Lucky.StepEdges ; (n+1)
| StepVertices -> options.step_mode <- Lucky.StepVertices ; (n+1)
| NoOracle -> options.oracle <- false ; (n+1)
| Verbose -> options.verb <- true; (n+1)
| ShowStep -> options.show_step <- true ; (n+1)
......@@ -691,7 +699,7 @@ and
est pris <<inside>>. Il faudrait rajouter une option
qui dit vertice ou edges, comme dans lucky...
*)
let (next_state, (output, loc)) = Lucky.env_step Lucky.StepInside input state in
let (next_state, (output, loc)) = Lucky.env_step (options.step_mode) input state in
let new_input = sut_try output in
let _ = check_oracle [output] [new_input] [loc] state.d.memory t rif next_state in
......@@ -718,7 +726,8 @@ and
sut_o_vntl
sut_i_vntl ;
output_string stdout
"\nOne more loop ? [type any char to stop, `CR' to continue]\n";
(* ZZZ this string it matched in xlurette *)
"\nOne more loop ? [type 's' to stop, `CR' to continue]\n";
read_line ()
)
else (
......@@ -733,7 +742,8 @@ and
flush rif;
(* Decides whether to loop once more *)
if
((str = "" || str = " ") && (s > t))
((str <> "s") && (s > t))
(* ((str = "" || str = " ") && (s > t)) *)
then
main_loop (t+1) s p k1 k2 k3 rif new_input next_state
else
......
......@@ -24,6 +24,21 @@ Command line <options> are:
(* compiler used to compiler sut and oracles *)
type compiler = Verimag | Scade
type step_mode = | Inside | Edges | Vertices
let string_to_step_mode = function
| "inside" -> Inside
| "edges" -> Edges
| "vertices" -> Vertices
| _ ->
print_string "\n Warning: bad step mode. ";
Inside
let step_mode_to_string = function
| Inside -> "--step-inside"
| Edges -> "--step-edges"
| Vertices -> "--step-vertices"
type flagT = {
mutable sut : string ;
mutable sut_node : string ;
......@@ -43,6 +58,8 @@ type flagT = {
mutable all_formula : bool ;
mutable all_vertices : bool ;
mutable step_mode : step_mode;
mutable step_by_step : bool ref ;
mutable display_local_var : bool ref ;
mutable display_sim2chro : bool ref;
......@@ -84,6 +101,7 @@ let (flag : flagT) = {
draw_vertices = 0 ;
all_formula = false ;
all_vertices = false ;
step_mode = Inside ;
step_by_step = ref false ;
show_step = ref false ;
display_local_var = ref true ;
......@@ -618,6 +636,7 @@ let (run : unit -> int) =
and verb_str = if !(flag.verbose) then ["-v"] else []
and show_step_str = if !(flag.show_step) then ["--show-step"] else []
and step_mode_str = [step_mode_to_string flag.step_mode]
and inside_nb_str = [string_of_int flag.draw_inside]
and edges_nb_str = [string_of_int flag.draw_edges]
and vertices_nb_str = [string_of_int flag.draw_vertices]
......@@ -670,7 +689,8 @@ let (run : unit -> int) =
inside_nb_str;
edges_nb_str;
vertices_nb_str;
step_mode_str;
all_formula_str ;
all_vertices_str ;
......@@ -760,6 +780,7 @@ type cmd =
| DrawEdges of int
| DrawVertices of int
| AllFormula of bool
| StepMode of string
| AllVertices of bool
| Quit
| Help
......@@ -804,6 +825,7 @@ let rec
| [< 'Genlex.Ident(_, "build") >] -> Build
| [< 'Genlex.Ident(_, "change_dir") ; 'Genlex.String(_, dir) >] -> ChDir(dir)
| [< 'Genlex.Ident(_, "set_step_mode") ; str = parse_ident_or_string >] -> StepMode(str)
| [< 'Genlex.Ident(_, "set_draw_inside") ; 'Genlex.Int(_, i) >] -> DrawInside(i)
| [< 'Genlex.Ident(_, "set_draw_edges") ; 'Genlex.Int(_, i) >] -> DrawEdges(i)
| [< 'Genlex.Ident(_, "set_draw_vertices") ; 'Genlex.Int(_, i) >] -> DrawVertices(i)
......@@ -1083,6 +1105,9 @@ set_draw_vertices <integer>
edges: \"" ^ (string_of_int flag.draw_edges ) ^ "\"
vertices: \"" ^ (string_of_int flag.draw_vertices ) ^ "\"
set_step_mode {inside|edges|vertices}
set the mode used to perform the step
set_draw_all_formula <Boolean>
to a set Boolean that indicates whether lurette should tries
one or all the formula reachable from the current step.
......@@ -1250,7 +1275,10 @@ let (read_commands : string -> (unit -> string) -> bool) =
);
true
| StepMode(str) ->
let step_mode = string_to_step_mode str in
flag.step_mode <- step_mode; true
(* | MakeOpt(str) -> *)
(* flag.make_opt <- str; true *)
| Env(llist) ->
......
This diff is collapsed.
SunOS moucherotte 5.7 Generic_106541-27 sun4u sparc SUNW,Ultra-5_10
This is Lurette Version V2-1.19
--Pollux Version 2.1
--Pollux Version 2.1
The Pid of lurette is 20777
The Pid of lurette is 25862
The random engine was initialized with the seed 1015403953
......@@ -10,13 +11,14 @@ The random engine was initialized with the seed 1015403953
The Test Thickness average was 1.
The execution lasted 33.94 seconds.
The execution lasted 34.55 seconds.
********************************************************************
rm -rf /tmp/lurette8/
rm -rf /tmp/lurette12/
This is Lurette Version V2-1.19
--Pollux Version 2.1
--Pollux Version 2.1
The Pid of lurette is 20828
The Pid of lurette is 25915
The random engine was initialized with the seed 1015403953
......@@ -24,14 +26,15 @@ The random engine was initialized with the seed 1015403953
The Test Thickness average was 2740.
The execution lasted 6.66 seconds.
The execution lasted 6.78 seconds.
********************************************************************
rm -rf /tmp/lurette8/
rm -rf /tmp/lurette12/
This is Lurette Version V2-1.19
--Pollux Version 2.1
--Pollux Version 2.1
The Pid of lurette is 20879
The Pid of lurette is 25966
The random engine was initialized with the seed 1015403953
......@@ -39,14 +42,15 @@ The random engine was initialized with the seed 1015403953
The Test Thickness average was 1265.
The execution lasted 28.41 seconds.
The execution lasted 28.78 seconds.
********************************************************************
rm -rf /tmp/lurette8/
rm -rf /tmp/lurette12/
This is Lurette Version V2-1.19
--Pollux Version 2.1
--Pollux Version 2.1
The Pid of lurette is 20930
The Pid of lurette is 26019
The random engine was initialized with the seed 1015403953
......@@ -54,14 +58,15 @@ The random engine was initialized with the seed 1015403953
The Test Thickness average was 21.9999
The execution lasted 10.81 seconds.
The execution lasted 10.89 seconds.
********************************************************************
rm -rf /tmp/lurette8/
rm -rf /tmp/lurette12/
This is Lurette Version V2-1.19
--Pollux Version 2.1
--Pollux Version 2.1
The Pid of lurette is 20981
The Pid of lurette is 26072
The random engine was initialized with the seed 1015403953
......@@ -69,14 +74,15 @@ The random engine was initialized with the seed 1015403953
The Test Thickness average was 2190.
The execution lasted 0.79 second.
The execution lasted 0.83 second.
********************************************************************
rm -rf /tmp/lurette8/
rm -rf /tmp/lurette12/
This is Lurette Version V2-1.19
--Pollux Version 2.1
--Pollux Version 2.1
The Pid of lurette is 21032
The Pid of lurette is 26123
The random engine was initialized with the seed 1015403953
......@@ -84,14 +90,15 @@ The random engine was initialized with the seed 1015403953