Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

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

lurette 0.83 Tue, 03 Sep 2002 13:37:10 +0200 by jahier

Parent-Version:      0.82
Version-Log:

source/lurette.ml:
source/lurettetop.ml:
source/command_line.ml, .mli:
source/solver.ml:
source/env_state.ml:
source/rnumsolver.ml:
   Add 2 news options, --draw-edges ans --draw-verteces that makes
   lurette draw among the verteces or on the edges of the convex hull
   of solutons.

Project-Description: Lurette
parent e655b8de
......@@ -3,15 +3,15 @@
(Created-By-Prcs-Version 1 3 3)
(source/command_line_ima_exe.mli 1082 1021651153 b/34_command_li 1.3)
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 19662 1030627155 51_env_state. 1.25)
(source/env_state.ml 20128 1031053030 51_env_state. 1.26)
(source/graph.ml 2563 1027066799 14_graph.ml 1.7)
(bin/Makefile.ima_exe 2013 1027066799 b/41_Makefile.i 1.3)
(source/util.ml 14262 1030614411 35_util.ml 1.24)
(test/time.exp 5577 1030614411 b/48_time.exp 1.3)
(source/solver.ml 24274 1027436332 39_solver.ml 1.25)
(source/solver.ml 24432 1031053030 39_solver.ml 1.26)
(test/test_gen_stubs.h 1818 1020068208 b/45_test_gen_s 1.1)
(source/command_line.ml 4388 1019207707 b/20_command_li 1.7)
(source/lurette.ml 12162 1030614411 12_lurette.ml 1.47)
(source/command_line.ml 4625 1031053030 b/20_command_li 1.8)
(source/lurette.ml 12371 1031053030 12_lurette.ml 1.49)
(source/solver.mli 1003 1027092697 38_solver.mli 1.13)
(source/env.mli 2028 1027349504 15_env.mli 1.15)
(test/heater_float.rif.exp 1453 1028297733 b/30_heater_flo 1.5)
......@@ -22,16 +22,16 @@
(lurette.dep.dot 49 1007651448 b/4_lurette.de 1.2)
(test/porte.ima 1021 1027066799 b/16_porte.env 1.7)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/rnumsolver.ml 10783 1017837703 b/27_rnumsolver 1.6)
(source/rnumsolver.ml 11348 1031053030 b/27_rnumsolver 1.7)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(source/parse_env.mli 1025 1027066799 40_parse_env. 1.9)
(source/sim2chro.mli 1455 1027943375 b/23_sim2chro.m 1.5)
(test/passerelle.ima 972 1027066799 b/17_passerelle 1.7)
(source/ima_exe.ml 11903 1030614411 b/32_ima_exe.ml 1.16)
(source/ima_exe.ml 12067 1030978777 b/32_ima_exe.ml 1.17)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/control.ml 4416 1030975996 c/4_control.ml 1.3)
(source/eval.ml 7755 1027066799 49_eval.ml 1.13)
(source/gen_stubs.ml 33359 1030614411 24_generate_l 1.30)
(source/gen_stubs.ml 33416 1031053030 24_generate_l 1.31)
(source/parse_env.ml 22235 1030975671 41_parse_env. 1.22)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
(source/automata.mli 3397 1027349504 b/46_automata.m 1.2)
......@@ -40,9 +40,9 @@
(source/formula.mli 3638 1027066799 44_formula.ml 1.14)
(test/time.res 5577 1030614411 b/49_time.res 1.6)
(TAGS 9825 1007379917 21_TAGS 1.6)
(source/command_line.mli 1421 1017929190 b/21_command_li 1.6)
(source/env_state.mli 6453 1027092697 50_env_state. 1.21)
(source/rnumsolver.mli 1764 1017335442 b/26_rnumsolver 1.3)
(source/command_line.mli 1442 1031053030 b/21_command_li 1.7)
(source/env_state.mli 6722 1031053030 50_env_state. 1.22)
(source/rnumsolver.mli 1736 1031053030 b/26_rnumsolver 1.4)
(source/ima_exe.mli 447 1016127950 b/31_ima_exe.ml 1.1)
(source/eval.mli 1395 1027066799 48_eval.mli 1.10)
(test/usager.ima 493 1027066799 b/14_usager.env 1.8)
......@@ -69,7 +69,7 @@
(test/heater_float.lus 175 1020068208 b/44_heater_flo 1.1)
(test/vrai_tram.c 3060 1027066799 b/8_vrai_tram. 1.3)
(source/print.mli 773 1027066799 46_print.mli 1.10)
(source/lurettetop.ml 18331 1030975671 c/1_lurettetop 1.5)
(source/lurettetop.ml 19952 1031053030 c/1_lurettetop 1.6)
(test/heater_int.lus 170 1020068208 b/43_heater_int 1.1)
(source/graph.mli 2218 1027066799 13_graph.mli 1.9)
(test/heater_int.rif.exp 860 1028297733 b/28_heater_int 1.6)
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 82)
(Parent-Version lurette 0 81)
(Project-Version lurette 0 83)
(Parent-Version lurette 0 82)
(Version-Log "
source/lurette.ml:
source/ima_exe.ml:
Check that nodes did not changed before redrawing anything
source/lurettetop.ml:
source/command_line.ml, .mli:
source/solver.ml:
source/env_state.ml:
source/rnumsolver.ml:
Add 2 news options, --draw-edges ans --draw-verteces that makes
lurette draw among the verteces or on the edges of the convex hull
of solutons.
also add a <<q>> command to exit from ima_exe more gently.
")
(New-Version-Log "")
(Checkin-Time "Mon, 02 Sep 2002 16:59:37 +0200")
(Checkin-Time "Tue, 03 Sep 2002 13:37:10 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -31,10 +37,10 @@ source/ima_exe.ml:
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.12 644))
(source/lurette.ml (lurette/12_lurette.ml 1.48 644))
(source/lurette.ml (lurette/12_lurette.ml 1.49 644))
(source/command_line.ml (lurette/b/20_command_li 1.7 644))
(source/command_line.mli (lurette/b/21_command_li 1.6 644))
(source/command_line.ml (lurette/b/20_command_li 1.8 644))
(source/command_line.mli (lurette/b/21_command_li 1.7 644))
;; Sources files common to lurette and ima_exe
(source/graph.mli (lurette/13_graph.mli 1.9 644))
......@@ -46,10 +52,10 @@ source/ima_exe.ml:
(source/util.ml (lurette/35_util.ml 1.24 644))
(source/solver.mli (lurette/38_solver.mli 1.13 644))
(source/solver.ml (lurette/39_solver.ml 1.25 644))
(source/solver.ml (lurette/39_solver.ml 1.26 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.3 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.6 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.4 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.7 644))
(source/parse_env.mli (lurette/40_parse_env. 1.9 644))
(source/parse_env.ml (lurette/41_parse_env. 1.22 644))
......@@ -66,8 +72,8 @@ source/ima_exe.ml:
(source/eval.mli (lurette/48_eval.mli 1.10 644))
(source/eval.ml (lurette/49_eval.ml 1.13 644))
(source/env_state.mli (lurette/50_env_state. 1.21 644))
(source/env_state.ml (lurette/51_env_state. 1.25 644))
(source/env_state.mli (lurette/50_env_state. 1.22 644))
(source/env_state.ml (lurette/51_env_state. 1.26 644))
(source/automata.mli (lurette/b/46_automata.m 1.2 644))
(source/automata.ml (lurette/b/47_automata.m 1.3 644))
......@@ -78,8 +84,8 @@ source/ima_exe.ml:
(source/gne.mli (lurette/b/36_gne.mli 1.2 644))
(source/gne.ml (lurette/b/37_gne.ml 1.2 644))
(source/lurettetop.ml (lurette/c/1_lurettetop 1.5 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.30 644))
(source/lurettetop.ml (lurette/c/1_lurettetop 1.6 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.31 644))
(source/control.mli (lurette/c/3_control.ml 1.2 644))
(source/control.ml (lurette/c/4_control.ml 1.3 644))
......
......@@ -25,6 +25,7 @@ type cmd_line_optionT =
Step | NoStep | Help
| DisplayLocalVar | NoDisplayLocalVar
| Sim2chro | NoSim2chro
| Edges | Verteces
(* | CuddHeapInit *)
| Seed | NoOracle | Verbose | Output
......@@ -57,6 +58,9 @@ let (string_to_option: (string * cmd_line_optionT) list) = [
("--do-not-display-local-var", NoDisplayLocalVar);
("-nlv", NoDisplayLocalVar);
("--draw-edges", Edges);
("--draw-verteces", Verteces);
(* ("--init-cudd-heap", CuddHeapInit) *)
]
......@@ -73,6 +77,8 @@ let (option_to_usage: cmd_line_optionT -> string) =
(* | 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 run the oracle.\n "
| Edges -> "Draw on the edges of the convex hull of solutions.\n "
| Verteces -> "Draw among the verteces of the convex hull of solutions.\n "
| Verbose -> "Set on a wordier mode.\n"
| Help -> "Print this message.\n"
......
......@@ -39,6 +39,7 @@ type cmd_line_optionT =
| DisplayLocalVar | NoDisplayLocalVar
| Sim2chro | NoSim2chro
(* | CuddHeapInit *)
| Edges | Verteces
| Seed | NoOracle | Verbose | Output
......
......@@ -16,6 +16,8 @@ open Formula
(****************************************************************************)
type draw_mode = Verteces | Edges | Inside
(*
** The environment is a list of graphs whose arcs are labelled by weighted
** formula.
......@@ -96,6 +98,9 @@ type env_stateT = {
ima flow, e.g., to control the number of times a loop is
executed. *)
mutable draw_mode : draw_mode;
(** Whether we draw on verteces, edges, or inside the convex hull of solution *)
mutable pre: subst list;
(** Stores the values of pre variables. *)
mutable input : env_in ;
......@@ -124,6 +129,7 @@ let (env_state:env_stateT) = {
snt = Hashtbl.create 3;
ce_label = Hashtbl.create 0 ;
ctrl_state = Control.new_state ();
draw_mode = Inside;
bdd_tbl = Hashtbl.create 0;
bdd_tbl_global = Hashtbl.create 0;
atomic_formula_to_index = Hashtbl.create 0;
......@@ -229,6 +235,18 @@ let (set_ctrl_state: Control.state -> unit) =
fun cs ->
env_state.ctrl_state <- cs
(****************************************************************************)
(* Exported *)
let (draw_mode: unit -> draw_mode) =
fun _ ->
env_state.draw_mode
(* Exported *)
let (set_draw_mode: draw_mode -> unit) =
fun dm ->
env_state.draw_mode <- dm
(****************************************************************************)
let (pre: unit -> subst list) =
......
......@@ -14,6 +14,8 @@
open Formula
type draw_mode = Verteces | Edges | Inside
val read_env_state : string list list -> unit
(** [read_env_state files_ll] updates the global variable
[env_state] using the automata defined in the list of list
......@@ -184,6 +186,13 @@ val ctrl_expr : string -> Control.expr
val ctrl_state: unit -> Control.state
val set_ctrl_state: Control.state -> unit
(** Returns and sets a mode of draw, namely, whether the draw
is done among the verteces the the convex hull of sol,
on its edges, or inside it. *)
val draw_mode: unit -> draw_mode
val set_draw_mode: draw_mode -> unit
(** outputs various statistic about the size of env_state tables *)
val dump_env_state_stat : unit -> unit
......@@ -940,6 +940,7 @@ let compile_lustre_program_if_needed lustre_prog =
output_string stderr (" ... No " ^ lustre_prog ^ ".c or no " ^ lustre_prog ^
".h exist(s), so I try to compile " ^ lustre_prog ^
".lus with the lus2ec and ec2c...\n");
let lustre_node = Filename.basename lustre_prog in
let cmd = ("lus2ec " ^ lustre_prog ^ ".lus " ^ lustre_prog)
and cmd2 = ("ec2c " ^ lustre_prog ^ ".ec")
in
......
......@@ -124,6 +124,8 @@ and
| NoOracle -> options.oracle <- false ; (n+1)
| Verbose -> options.verbose <- true ; (n+1)
| Edges -> Env_state.set_draw_mode Env_state.Edges ; (n+1)
| Verteces -> Env_state.set_draw_mode Env_state.Verteces ; (n+1)
| Help -> options.help <- true ; (n+1)
| Output ->
let str = (Sys.argv.(n+1)) in
......@@ -307,7 +309,7 @@ and
then (
(* print inputs and outputs of all wrong tuple *)
output_string stderr ("\n*** An assertion of the oracle has been violated" ^
" at time " ^ (string_of_int t) ^
" at step " ^ (string_of_int t) ^
" with the following values:\n ");
Util.list_iter3
......
......@@ -19,6 +19,7 @@ Type help and/or man at the prompt for more info.
Command line <options> are:
"
type draw_mode = Verteces | Edges | Inside
type flagT = {
mutable sut : string ;
......@@ -27,6 +28,7 @@ type flagT = {
mutable step_nb : int;
mutable formula_nb : int ;
mutable draw_nb : int ;
mutable draw_mode : draw_mode ;
mutable step_by_step : bool ref ;
mutable display_local_var : bool ref ;
mutable display_sim2chro : bool ref;
......@@ -49,6 +51,7 @@ let (flag : flagT) = {
step_nb = 10;
formula_nb = 1 ;
draw_nb = 1 ;
draw_mode = Inside ;
step_by_step = ref false ;
display_local_var = ref true ;
display_sim2chro = ref true ;
......@@ -86,6 +89,13 @@ let rec speclist =
("<int>\t\tat each step (default=" ^
(string_of_int flag.draw_nb) ^ ").\n");
"--draw-edges", Arg.Int (fun _ -> flag.draw_mode <- Edges),
"\t\tDraw on the edges of the convex hull of solutions.\n .";
"--draw-verteces", Arg.Int (fun _ -> flag.draw_mode <- Verteces),
"\t\tDraw among the verteces of the convex hull of solutions.\n .";
"--seed", Arg.Int (fun i -> flag.seed <- Some i),
"<int>\t\tSeed the random engine is init with." ;
"-seed", Arg.Int (fun i -> flag.seed <- Some i), " <int>\n";
......@@ -105,7 +115,7 @@ let rec speclist =
"--restore", Arg.String (fun s -> flag.restore <- Some s),
"<string>\tFile name (without extension) of the package containing"
^ "\t\tthe temporarily files to be restored (cf the pack command).\n";
^ "\n\t\t\tthe temporarily files to be restored (cf the pack command).\n";
"--step", Arg.Set flag.step_by_step, "\t\tRun lurette step by step." ;
"-s", Arg.Set flag.step_by_step, "\n";
......@@ -185,6 +195,11 @@ let (run : string -> int) =
None -> ""
| Some i -> (" -seed " ^ (string_of_int i))
and verb_str = if !(flag.verbose) then " -v" else ""
and draw_mode_str =
match flag.draw_mode with
Inside -> " "
| Edges -> " --draw-edges"
| Verteces -> " --draw-verteces"
and orac_str =
match flag.oracle with
None -> " --no-oracle"
......@@ -200,6 +215,7 @@ let (run : string -> int) =
(string_of_int flag.step_nb) ^ " " ^
(string_of_int flag.formula_nb) ^ " " ^
(string_of_int flag.draw_nb) ^ " " ^
draw_mode_str ^
seed_str ^ verb_str ^ orac_str ^ outp_str ^ step_str ^
sim2_str ^ dlvr_str ^ flag.env
)
......@@ -227,6 +243,9 @@ type cmd =
| Build
| Clean
| Run
| DrawInside
| DrawEdges
| DrawVerteces
| Quit
| Help
| Man
......@@ -245,9 +264,17 @@ let rec
match tok with parser
| [< 'Genlex.Ident "run" >] -> Run
| [< 'Genlex.Ident "r" >] -> Run
| [< 'Genlex.Ident "show" >] -> Show
| [< 'Genlex.Ident "b" >] -> Build
| [< 'Genlex.Ident "build" >] -> Build
| [< 'Genlex.Ident "set_draw_mode" ;'Genlex.Ident id >] ->
(
match id with
"inside" -> DrawInside
| "edges" -> DrawEdges
| "verteces" -> DrawVerteces
| _ -> Error ("Unknown draw mode (" ^ id ^ ")\n")
)
| [< 'Genlex.Ident "show" >] -> Show
| [< 'Genlex.Ident "clean" >] -> Clean
| [< 'Genlex.Ident "set_sut" ; 'Genlex.Ident str >] -> Sut(str)
| [< 'Genlex.Ident "set_oracle" ; 'Genlex.Ident str >] -> Oracle(str)
......@@ -361,6 +388,7 @@ pack <file_name>
show
show of post-script version of the current environment
set_env <env ([x] env)*> (env=<file name without extension>)
to set the environment field (.ima files). Automata of
environments separated by \"x\" are multiplied.
......@@ -395,6 +423,17 @@ set_draw_nb <integer>
to set the number of draw to be done in each formula at each step
Its current value is \"" ^ (string_of_int flag.draw_nb) ^ "\"
set_draw_mode <draw_mode>
set the draw mode, which can be either be inside, edges, or verteces.
- inside : draw inside the convex hull of solutions.
- edges : draw on the edges of the convex hull of solutions.
- verteces : draw among the verteces of the convex hull of solutions.
Its current mode is \"" ^ (match flag.draw_mode with
Inside -> "inside"
| Edges -> "edges"
| Verteces -> "verteces"
) ^ "\".
set_seed <integer>
to set the seed the random engine is initialised with.
Its current value is " ^ (match flag.seed with
......@@ -469,10 +508,19 @@ let rec (main_loop : string -> string -> string -> unit) =
flag.seed <- Some i; true
| Verbose(b) ->
flag.verbose := b; true
| DrawInside ->
flag.draw_mode <- Inside; true
| DrawEdges ->
flag.draw_mode <- Edges; true
| DrawVerteces ->
flag.draw_mode <- Verteces; true
| Output(str) ->
flag.output <- str; true
| Clean ->
let _ = Sys.command "make clean" in
let rm_cmd = ("rm -f " ^ lurette_tmp_dir ^ "/*") in
let _ = Sys.command rm_cmd in
print_string (rm_cmd ^ "\n");
flag.to_build := true;
true
| Build ->
let build_ok = build user_dir lurette_tmp_dir lurette_dir in
......@@ -521,7 +569,9 @@ let rec (main_loop : string -> string -> string -> unit) =
print_string cmd_usage ;
true
in
if continue then main_loop user_dir lurette_tmp_dir lurette_dir else print_string "bye!\n"
if continue
then main_loop user_dir lurette_tmp_dir lurette_dir
else print_string "bye!\n"
......
......@@ -377,14 +377,42 @@ let (draw_inside : store -> Formula.subst list) =
[]
(* exported *)
(* let (draw_edge : store -> int -> Formula.subst list list) =
fun -> *)
(* exported *)
(* let (draw_verteces : store -> int -> Formula.subst list list) =
fun -> *)
let (draw_verteces : store -> Formula.subst list) =
fun store ->
match store with
None -> assert false
| Some(tbl) ->
Hashtbl.fold
(fun vn range acc ->
( match range with
ValI(i) ->
((vn, N(I(i)))::acc)
| RangeI(min, max) ->
let ran = Random.int 2
in
if ran = 0
then ((vn, N(I(min)))::acc)
else ((vn, N(I(max)))::acc)
| ValF(f) ->
((vn, N(F(f)))::acc)
| RangeF(min, max) ->
let ran = Random.int 2 in
if ran = 0
then ((vn, N(F(min)))::acc)
else ((vn, N(F(max)))::acc)
))
tbl
[]
(* exported *)
let (draw_edges : store -> Formula.subst list) =
fun store ->
draw_inside store
(* exported *)
(* let (get_all_verteces : store -> Formula.subst list list) =
fun -> *)
......
......@@ -33,12 +33,12 @@ val draw_inside : store -> Formula.subst list
(** [draw_inside s n] draws [n] points fairly inside the (bounded)
solution hull. *)
(* val draw_edge : store -> Formula.subst list *)
val draw_edges : store -> Formula.subst list
(** [draw_edge s n] draws fairly on the edge of the
(bounded) solution hull. *)
(* val draw_verteces : store -> Formula.subst list *)
(** [draw_vertex s n] draws [n] points fairly among the verteces of
val draw_verteces : store -> Formula.subst list
(** [draw_vertex s n] draws among the verteces of
the (bounded) solution hull. *)
(* val get_all_verteces : store -> Formula.subst list *)
......
......@@ -693,7 +693,12 @@ let (draw : formula -> vnt list -> Bdd.t -> Bdd.t -> subst list * subst list) =
let (bool_subst_l, store) =
draw_in_bdd ([], (new_store num_vnt_to_gen)) bdd comb
in
let num_subst_l = draw_inside store in
let num_subst_l =
match Env_state.draw_mode () with
Env_state.Verteces -> draw_verteces store
| Env_state.Edges -> draw_edges store
| Env_state.Inside -> draw_inside store
in
let subst_l = append bool_subst_l num_subst_l in
let (out_vars, _) = List.split (Env_state.output_var_names ())
in
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment