Skip to content

GitLab

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 606164a8 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.47 Thu, 14 Mar 2002 18:45:50 +0100 by jahier 

Parent-Version:      0.46
Version-Log:

Implement an ima_exe that lets one imterprets .env automata offline
via a rif dialogue (e.g., to be used from lulu).

Project-Description: Lurette
parent ee264c20
Hide whitespace changes
Inline Side-by-side
Showing with 482 additions and 29 deletions
.lurette.prcs_aux
View file @ 606164a8
......@@ -2,6 +2,7 @@
;; REALLY bad things.
(Created-By-Prcs-Version 1 3 3)
(test/usager.env 424 1015605037 b/14_usager.env 1.4)
(source/command_line_ima_exe.mli 989 1016127950 b/34_command_li 1.1)
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 2787 1016011748 51_env_state. 1.14)
(source/graph.ml 1819 1016011748 14_graph.ml 1.5)
......@@ -21,28 +22,32 @@
(test/passerelle.env 821 1015605037 b/17_passerelle 1.3)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/rnumsolver.ml 7438 1015514807 b/27_rnumsolver 1.3)
(source/parse_env.mli 905 1015408234 40_parse_env. 1.5)
(source/parse_env.mli 907 1016127950 40_parse_env. 1.6)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(source/sim2chro.mli 1427 1015250295 b/23_sim2chro.m 1.3)
(source/ima_exe.ml 7125 1016127950 b/32_ima_exe.ml 1.1)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/eval.ml 8050 1016011748 49_eval.ml 1.11)
(source/gen_stubs.ml 33424 1015408234 24_generate_l 1.19)
(source/parse_env.ml 11322 1016024020 41_parse_env. 1.9)
(interface/TAGS 1956 1007380262 26_TAGS 1.3)
(source/sim2chro.ml 2669 1015408234 b/24_sim2chro.m 1.4)
(source/sim2chro.ml 2669 1016127950 b/24_sim2chro.m 1.5)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
(source/formula.mli 2161 1015250295 44_formula.ml 1.7)
(source/command_line.mli 1317 1016024341 b/21_command_li 1.4)
(source/formula.mli 2206 1016127950 44_formula.ml 1.8)
(TAGS 9825 1007379917 21_TAGS 1.6)
(test/Makefile_ima_exe 1624 1016127950 b/35_Makefile_i 1.1)
(source/command_line.mli 1317 1016024341 b/21_command_li 1.4)
(source/wtree.mli 2340 1016011748 b/0_wtree.mli 1.7)
(test/porte.env 834 1015605037 b/16_porte.env 1.3)
(source/env_state.mli 3589 1016011748 50_env_state. 1.12)
(source/rnumsolver.mli 1909 1015246213 b/26_rnumsolver 1.1)
(source/ima_exe.mli 447 1016127950 b/31_ima_exe.ml 1.1)
(source/eval.mli 1413 1016011748 48_eval.mli 1.8)
(README 74 1011881677 10_README 1.2)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(OcamlMakefile 19189 1016011748 17_OcamlMakef 1.21)
(OcamlMakefile 19280 1016127950 17_OcamlMakef 1.22)
(source/command_line_ima_exe.ml 2381 1016127950 b/33_command_li 1.1)
(test/ControleurPorte.rif.exp 4746 1016013431 b/29_Controleur 1.3)
(test/tram.env 905 1015605037 b/15_tram.env 1.3)
(source/show_env.ml 2961 1014048376 43_show_env.m 1.3)
......@@ -56,7 +61,7 @@
(source/print.mli 606 1016027474 46_print.mli 1.7)
(source/graph.mli 1493 1015250295 13_graph.mli 1.6)
(test/heater_int.rif.exp 785 1015408234 b/28_heater_int 1.1)
(source/formula.ml 4618 1015408234 45_formula.ml 1.9)
(source/formula.ml 4780 1016127950 45_formula.ml 1.10)
(source/lurette.mli 448 1016027474 11_lurette.ml 1.12)
(source/print.ml 5700 1016027474 47_print.ml 1.12)
(test/vrai_tram.h 2468 1012914629 b/7_vrai_tram. 1.2)
OcamlMakefile
View file @ 606164a8
......@@ -5,7 +5,7 @@
# For updates see:
# http://miss.wu-wien.ac.at/~mottl/ocaml_sources
#
# $Id: OcamlMakefile 1.21 Wed, 13 Mar 2002 10:29:08 +0100 jahier $
# $Id: OcamlMakefile 1.22 Thu, 14 Mar 2002 18:45:50 +0100 jahier $
#
###########################################################################
......@@ -502,6 +502,10 @@ try:
# ./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
yvan:
$(LURETTE_DIR)/make_lurette heater Heater_vrai; \
./lurette 50 1 1 Heater.env \
vroum:
../make_lurette ControleurPorte vrai_tram nc; \
time ./lurette 4500 1 1 tram.env usager.env porte.env passerelle.env -seed 1015403953 -ns2c --no-oracle
......
lurette.prj
View file @ 606164a8
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 46)
(Parent-Version lurette 0 45)
(Project-Version lurette 0 47)
(Parent-Version lurette 0 46)
(Version-Log "
Clean up a little bit lurette.ml
Implement an ima_exe that lets one imterprets .env automata offline
via a rif dialogue (e.g., to be used from lulu).
")
(New-Version-Log "")
(Checkin-Time "Wed, 13 Mar 2002 14:51:14 +0100")
(Checkin-Time "Thu, 14 Mar 2002 18:45:50 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -18,10 +19,21 @@ Clean up a little bit lurette.ml
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Sources files
;; Sources files for ima_exe
(source/ima_exe.mli (lurette/b/31_ima_exe.ml 1.1 644))
(source/ima_exe.ml (lurette/b/32_ima_exe.ml 1.1 644))
(source/command_line_ima_exe.ml (lurette/b/33_command_li 1.1 644))
(source/command_line_ima_exe.mli (lurette/b/34_command_li 1.1 644))
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.12 644))
(source/lurette.ml (lurette/12_lurette.ml 1.28 644))
(source/command_line.ml (lurette/b/20_command_li 1.4 644))
(source/command_line.mli (lurette/b/21_command_li 1.4 644))
;; Sources files common to lurette and ima_exe
(source/graph.mli (lurette/13_graph.mli 1.6 644))
(source/graph.ml (lurette/14_graph.ml 1.5 644))
......@@ -36,14 +48,14 @@ Clean up a little bit lurette.ml
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.1 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.3 644))
(source/parse_env.mli (lurette/40_parse_env. 1.5 644))
(source/parse_env.mli (lurette/40_parse_env. 1.6 644))
(source/parse_env.ml (lurette/41_parse_env. 1.9 644))
(source/show_env.mli (lurette/42_show_env.m 1.5 644))
(source/show_env.ml (lurette/43_show_env.m 1.3 644))
(source/formula.mli (lurette/44_formula.ml 1.7 644))
(source/formula.ml (lurette/45_formula.ml 1.9 644))
(source/formula.mli (lurette/44_formula.ml 1.8 644))
(source/formula.ml (lurette/45_formula.ml 1.10 644))
(source/print.mli (lurette/46_print.mli 1.7 644))
(source/print.ml (lurette/47_print.ml 1.12 644))
......@@ -58,18 +70,15 @@ Clean up a little bit lurette.ml
(source/wtree.ml (lurette/b/1_wtree.ml 1.9 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.3 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.4 644))
(source/command_line.ml (lurette/b/20_command_li 1.4 644))
(source/command_line.mli (lurette/b/21_command_li 1.4 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.5 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.19 644))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.21 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.22 644))
(Makefile (lurette/18_Makefile 1.23 644))
(test/Makefile (../Makefile) :symlink)
(interface/Makefile (lurette/25_Makefile 1.6 644))
(test/Makefile_ima_exe (lurette/b/35_Makefile_i 1.1 644))
(make_lurette (lurette/27_make_luret 1.7 744))
......@@ -109,6 +118,8 @@ Clean up a little bit lurette.ml
(test/heater_float.rif.exp (lurette/b/30_heater_flo 1.2 644))
)
(Merge-Parents)
(New-Merge-Parents)
source/command_line_ima_exe.ml 0 → 100644
View file @ 606164a8
(*-----------------------------------------------------------------------
** Copyright (C) 2001 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: command_line_ima_exe.ml
** Main author: jahier@imag.fr
*)
type optionsT = {
mutable boot : bool ;
mutable user_seed : int
}
type cmd_line_optionT =
Seed | Boot
(* Names of the command line options to override the defaults. *)
let (string_to_option: (string * cmd_line_optionT) list) = [
("-b", Boot);
("--boot", Boot);
("--with-seed", Seed);
("-seed", Seed)
]
let (option_to_usage: cmd_line_optionT -> string) =
fun opt ->
match opt with
Boot -> "The automata starts generating values.\n"
| Seed -> "Set the value of the seed the random engine is initialized with (0 lets the system draw a seed).\n"
let (group_common_options: (string * cmd_line_optionT) list ->
(string * cmd_line_optionT) list) =
fun list ->
List.fold_left
(fun acc (str, opt) ->
match acc with
(str2, opt2)::tail ->
if
(opt = opt2)
then
(((str2 ^ "\n\t\t" ^ str), opt)::tail)
else
((str, opt)::(str2, opt2)::tail)
| [] -> [(str, opt)]
)
[]
list
let usage_options =
List.fold_left
(fun acc (str, opt) -> acc ^ "\n\t\t" ^ str ^ "\n\t\t\t" ^ (option_to_usage opt))
""
(List.rev (group_common_options string_to_option))
let usage =
("\n\nusage: ./ima_exe [options]* <file>.env ([x] <file>.env)* \n" ^
" where: " ^
"\n\t o `<file>.env' contains an environment automata. Environments " ^
"\n\t separated by `x' will executed as if their automata where " ^
"\n\t multiplied (necessary if they have common output variables).\n " ^
"\n\t o `options' is a list of options. The available options are: " ^
usage_options ^ "\n\n" ^
"Example: ./ima_exe env1.env x env2.env x env3.env env4\n\t" ^
"will run the environment `env1', `env2', and `env3' as a product, \n\t" ^
"and `env4' in parallel.\n\n ")
let cmd_line_string_to_int str errmsg =
try
(int_of_string str)
with Failure("int_of_string")
->
print_string usage ;
print_string errmsg ;
flush stdout ;
failwith "\n *** Error when calling ima_exe.\n"
source/command_line_ima_exe.mli 0 → 100644
View file @ 606164a8
(*-----------------------------------------------------------------------
** Copyright (C) 2001 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: command_line_iùa_exe.mli
** Main author: jahier@imag.fr
*)
(** Handles everything that is related to command line calls.
*)
type optionsT = {
mutable boot : bool ;
mutable user_seed : int
}
val usage : string
(** Usage message to be printed if an error occur when ima_exe is called. *)
val cmd_line_string_to_int : string -> string -> int
(** [cmd_line_string_to_int str errmsg] converts a string (of the
command line) into an integer, and prints [errmsg] before aborting if
the convertion failed.
*)
type cmd_line_optionT =
Seed | Boot
val string_to_option: (string * cmd_line_optionT) list
(** Mapping from options string (e.g., "--with_seed") to the cmd_line_optionT
type. *)
source/formula.ml
View file @ 606164a8
......@@ -130,8 +130,15 @@ let (var_type_to_string : var_type -> string) =
| IntT(i1, i2) -> "int"
| FloatT(f1, f2) -> "float"
let (var_type_to_string2 : var_type -> string) =
fun vt ->
match vt with
BoolT -> "bool"
| IntT(i1, i2) -> "int"
| FloatT(f1, f2) -> "real"
let print_atomic_expr e oc =
let print_atomic_expr oc e =
match e with
Int(i) -> output_string oc (string_of_int i)
| Bool(true) -> output_string oc "t"
......@@ -145,7 +152,7 @@ let (print_subst_list : subst list -> out_channel -> unit) =
(fun (vn, e) ->
output_string oc vn ;
output_string oc "=";
print_atomic_expr e oc;
print_atomic_expr oc e;
output_string oc " "
)
(Util.sort_list_string_pair sl)
......@@ -156,7 +163,7 @@ let (print_env_in : env_in -> out_channel -> unit) =
(fun vn e ->
output_string oc vn ;
output_string oc "=";
print_atomic_expr e oc;
print_atomic_expr oc e;
output_string oc " "
)
tbl
......
source/formula.mli
View file @ 606164a8
......@@ -83,6 +83,7 @@ val formula_to_string : formula -> string
val expr_to_string : expr -> string
val arc_info_to_string : arc_info -> string
val var_type_to_string : var_type -> string
val print_atomic_expr : atomic_expr -> out_channel -> unit
val var_type_to_string2 : var_type -> string
val print_atomic_expr : out_channel -> atomic_expr -> unit
val print_subst_list : subst list -> out_channel -> unit
val print_env_in : env_in -> out_channel -> unit
source/ima_exe.ml 0 → 100644
View file @ 606164a8
(*-----------------------------------------------------------------------
** Copyright (C) 2001, 2002 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: ima_exe.ml
** Main author: jahier@imag.fr
*)
(*------------------------------------------------------------------------*)
open Util
open Formula
open Env_state
open List
open Command_line_ima_exe
(*------------------------------------------------------------------------*)
let (options:Command_line_ima_exe.optionsT) = {
user_seed = 0 ;
boot = false
}
(*------------------------------------------------------------------------*)
(* RIF parsing *)
let lexer = Genlex.make_lexer ["t"; "f"; "#"]
type rif_token = Genlex.token
type rif_stream = Genlex.token Stream.t
let (get_inputs : vnt list -> rif_stream -> env_in) =
fun vntl stream ->
(** The first token ougth to be a valid token (namely, rif pragmas have
been filtered out). *)
let tbl = Hashtbl.create (List.length vntl) in
let _ =
List.iter
(fun vnt ->
let new_stream =
match Stream.peek stream with
Some(_) -> stream
| None ->
let line = read_line () in
lexer(Stream.of_string line)
in
let (vn, vt) = vnt in
match (vnt, (Stream.next new_stream)) with
((vn, BoolT), Genlex.Kwd "t") -> Hashtbl.add tbl vn (Bool(true))
| ((vn, BoolT), Genlex.Kwd "f") -> Hashtbl.add tbl vn (Bool(false))
| ((vn, BoolT), Genlex.Int 0) -> Hashtbl.add tbl vn (Bool(false))
| ((vn, BoolT), Genlex.Int 1) -> Hashtbl.add tbl vn (Bool(true))
| ((vn, IntT(_,_)), Genlex.Int i) -> Hashtbl.add tbl vn (Int(i))
| ((vn, FloatT(_,_)), Genlex.Float f) -> Hashtbl.add tbl vn (Float(f))
| _ -> failwith ("*** Bad input. A " ^ (var_type_to_string2 vt) ^
" was expected for variable " ^ vn ^ ".\n")
)
vntl
in
tbl
let rec (read_rif_input : vnt list -> env_in) =
fun vntl ->
(** Reads the environment inputs on stdin. It should respect the rif format. *)
let line = read_line () in
let stream = lexer(Stream.of_string line) in
let tok_list = Stream.npeek 2 stream in
match tok_list with
[Genlex.Kwd "#"; Genlex.Ident "outs"] ->
Stream.junk stream ;
Stream.junk stream ;
get_inputs vntl stream
| [Genlex.Kwd "#"; _] ->
(* Ignore everything after a "#"... if it is not followed by "outs". *)
read_rif_input vntl
| [] -> read_rif_input vntl
| _ -> get_inputs vntl stream
let (write_rif_output : vnt list -> env_out -> unit) =
fun vntl output ->
let ae_l = List.map (fun (vn, _) -> List.assoc vn output) vntl in
List.iter (print_atomic_expr stdout) ae_l
(*------------------------------------------------------------------------*)
let arg_nb = (Array.length Sys.argv)
external random_seed: unit -> int = "sys_random_seed";;
let rec (main : unit -> 'a) =
fun _ ->
try
if (arg_nb < 2)
then print_string usage
else
main2 ()
with
Failure(errmsg) -> print_string errmsg
| e -> raise e
and
(get_ima_exe_options: int -> int) =
fun n ->
try
begin
let opt = List.assoc Sys.argv.(n) Command_line_ima_exe.string_to_option in
match opt with
Boot -> options.boot <- true ; (n+1)
| Seed ->
let str = (Sys.argv.(n+1)) in
options.user_seed <- cmd_line_string_to_int str
("*** Error when calling ima_exe: an " ^
"integer is expected after the " ^
"option --with-seed\n") ;
n+2
end
with Not_found -> n
and
(get_env_from_args: int -> string list list -> string list list) =
fun n file_ll ->
(** Returns the environment file names given at top-level into a
list of list. E.g., if the call [ima_exe env1 x env2 x env3
env4] is done, then [get_env_from_args 10 []] (where 10 is the
arg nb) returns [[["env1"; "env2"; "env3"]; ["env4"]]].
Also set the command line options if any. *)
if (n = arg_nb) then file_ll
else
let m = get_ima_exe_options n in
(* m > n iff Sys.argv.(n) is an option *)
if
(m > n)
then
get_env_from_args m file_ll
else
let arg = Sys.argv.(m) in
if
(arg = "x")
then
match file_ll with
sl::sll ->
let env = Sys.argv.(n+1) in
get_env_from_args (n+2) ((env::sl)::sll)
| [] -> assert false
else
get_env_from_args (n+1) ([arg]::file_ll)
and
(main2 : unit -> 'a) =
fun _ ->
(* Initialisation of `Env_state.env_state' *)
let env_llist = (get_env_from_args 1 []) in
let () = Env.read_env_state env_llist in
let local_var_name_and_type_list_unsorted0 = Env_state.loc_env_unsorted () in
let local_var_name_and_type_list_unsorted =
List.map (fun (vn, vt) -> (vn, (var_type_to_string vt)))
local_var_name_and_type_list_unsorted0
in
let local_var_name_and_type_list =
Util.sort_list_string_pair local_var_name_and_type_list_unsorted
in
(* Initialisation of the random engine *)
let seed =
if (options.user_seed = 0)
then (random_seed ())
else options.user_seed
in
Random.init seed ;
print_string "#The random engine was initialized with the seed ";
print_int seed;
print_string "\n ";
flush stdout ;
env_state.output_var_names <- Env_state.out_env_unsorted () ;
(* Initializing Dd's libs. *)
Manager.disable_autodyn env_state.bdd_manager;
(* Initializing the solution number table *)
Hashtbl.add env_state.snt
(Bdd.dtrue env_state.bdd_manager) (Util.one_sol, Util.zero_sol);
Hashtbl.add env_state.snt
(Bdd.dfalse env_state.bdd_manager) (Util.zero_sol, Util.one_sol);
print_string "#inputs ";
List.iter
(fun (vn,vt) ->
print_string (vn ^ ":" ^ (var_type_to_string2 vt) ^ " ")
)
(Env_state.out_env_unsorted ());
print_string "\n";
flush stdout;
if options.boot
then
let nll_out_loc_list = Env.env_try 1 1 (Hashtbl.create 0) in
let (nll, out, loc) =
match nll_out_loc_list with
[(nll, out, loc)] -> (nll, out, loc)
| _ -> assert false
in
Env.env_step nll out loc ;
Eval.update_pre env_state.input env_state.output env_state.local ;
write_rif_output (Env_state.out_env_unsorted ()) out ;
else ();
main_loop 1 ;
flush stdout
and
main_loop t =
let _ = print_string ("\n# step " ^ (string_of_int t) ^ ":\n"); flush stdout in
let input = read_rif_input (Env_state.in_env_unsorted ()) in
let previous_nodes = env_state.current_nodes in
let nll_out_loc_list = Env.env_try 1 1 input in
let (nll, out, loc) =
match nll_out_loc_list with
[(nll, out, loc)] -> (nll, out, loc)
| _ -> assert false
in
Env.env_step nll out loc ;
Eval.update_pre env_state.input env_state.output env_state.local ;
write_rif_output (Env_state.out_env_unsorted ()) out ;
main_loop (t+1)
;;
main ();;
source/ima_exe.mli 0 → 100644
View file @ 606164a8
(*-----------------------------------------------------------------------
** Copyright (C) 2001, 2002 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: ima_exe.mli
** Main author: jahier@imag.fr
*)
(** ima_exe main module. *)
(* {% \psfig{figure=lurette.dep.ps} %} *)
open Env
val main : unit -> unit
source/parse_env.mli
View file @ 606164a8
......@@ -29,3 +29,5 @@ type read_automata = Automata of
val lexer : char Stream.t -> Genlex.token Stream.t
val parse_automata : aut_token -> read_automata
source/sim2chro.ml
View file @ 606164a8
......@@ -47,16 +47,16 @@ let (put_current_step_values: out_channel -> int -> env_out -> env_in -> env_loc
put "\n";
List.iter
(fun (_, e) -> (print_atomic_expr e rif; put " "))
(fun (_, e) -> (print_atomic_expr rif e; put " "))
(Util.sort_list_string_pair input);
put "#outs ";
Hashtbl.iter
(fun _ e -> (print_atomic_expr e rif; put " "))
(fun _ e -> (print_atomic_expr rif e; put " "))
output;
if display_local_var then
List.iter
(fun (_, e) -> (print_atomic_expr e rif; put " "))
(fun (_, e) -> (print_atomic_expr rif e; put " "))
(Util.sort_list_string_pair local);
put "\n"
......
test/Makefile deleted 120000 → 0
View file @ ee264c20
../Makefile
\ No newline at end of file