Commit 6e170755 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Add include statements in the Lutin syntax + Allow several Lutin

programs to be used from the command line.
parent 3ea8c42d
......@@ -72,3 +72,9 @@ cdiff:
# XXX automate that tag numbering and via a make rule
#tag:
# git tag ``xxx
pull-pascal:
git pull ~raymond/git/lurette
pull-erwan:
git pull ~jahier/lurette
......@@ -352,9 +352,9 @@ LUTIN_FILES = \
$(OBJDIR)/lutLexer.mll \
$(OBJDIR)/reactive.mli \
$(OBJDIR)/reactive.ml \
$(OBJDIR)/syntaxe.ml \
$(OBJDIR)/parsers.ml \
$(OBJDIR)/parsers.mli \
$(OBJDIR)/syntaxe.ml \
$(OBJDIR)/syntaxeDump.ml \
$(OBJDIR)/ckTypeEff.ml \
$(OBJDIR)/ckTypeEff.mli \
......
\label{cov-ann}
\subsubsection{}
Le plus simple est d'illustrer ce format de fichier sur un exemple.
Considérons un système sous test chargé de réguler la température
dans une pièce. Ce système prend en entrée la température fournie
par chacun de 3 capteurs, et retourne un booléan indiquant si le
chauffage doit fonctionner ou pas.
Une exigence fonctionnelle d'un tel système pourrait être que la
température dans la pièce ne franchisse pas certain seuil haut, ou
bas. On peut formaliser ces exigences en Lustre comme dans la Figure
\ref{fig:oracle-cov-exemple}.
\begin{figure}
\caption{2 oracles possibles pour un thermostat redondé en capteur}
\label{fig:oracle-cov-exemple}
\begin{alltt}
node not_a_sauna(T, T1, T2, T3 : real; Heat_on: bool) returns (ok, c1, c2, c3:bool);
let
ok = true -> pre T < TMAX + 1.0 ;
c1 = T> TMAX;
c2 = T= TMAX;
c3 = T< TMAX;
tel
node not_a_fridge(T, T1, T2, T3 : real; Heat_on: bool) returns (ok, c4, c5, c6:bool);
let
ok = true -> pre T > TMIN - 1.0 ;
c4 = T < TMIN;
c5 = T = TMIN;
c6 = T < TMIN;
tel
\end{alltt}
\end{figure}
XXX commenter des 2 oracles
XXX faire remarquer qu'il aurait été judicieux de procéder autrement
; 4 critères suffisaient : T> TMAX, T <= TMAX, T> TMIN, T <= TMIN.
#+CAPTION: un exemple de fichier de couverture associé aux oracles de la Figure \ref{fig:oracle-cov-exemple}.
#+LABEL: fig:cov-exemple
#+BEGIN_EXAMPLE
SUT: v6:heater_control.lus:main
ORACLE: v4:heater_control.lus:not_a_sauna
ORACLE: v6:heater_control.lus:not_a_fridge
RIF: test.rif0 - generated at 16:28:15 the 18/4/2011 on peouvou ; the coverage rate is 50.0%
RIF: test.rif0 - generated at 16:29:20 the 18/4/2011 on peouvou ; the coverage rate is 60.0%
VAR: c1 t
VAR: c2 f
VAR: c3 t
VAR: c4 t
VAR: c5 f
VAR: c6 t
#+END_EXAMPLE
XXX commenter
......@@ -111,48 +111,46 @@ let (make : string -> string -> lucky_process) =
output_string !debug_oc "XXXXXXX\n";
flush !debug_oc;
);
assert (file <> "");
Formula_to_bdd.clear_all ()
assert (file <> "");
Formula_to_bdd.clear_all ()
in
let pp_opt = if pp = "" then None else Some pp in
let state0 = LucProg.make_state pp_opt [file] in
let init_state_dyn = state0.d in
let init_state = {
d = init_state_dyn ;
s = state0.s
d = init_state_dyn ;
s = state0.s
}
in
(* I defined mine because i need to know the seed that has been drawn
by self_init. *)
(* I defined mine because i need to know the seed that has been drawn
by self_init. *)
let random_seed () =
let () = Random.self_init () in
Random.int max_int
let () = Random.self_init () in
Random.int max_int
in
let seed = random_seed () in
let _ =
(* Initialisation of the random engine *)
Random.init seed ;
output_string stderr "#The random engine was initialized with the seed ";
output_string stderr (string_of_int seed);
output_string stderr "\n";
flush stderr ;
(* selecting the draw mode *)
Solver.set_efficient_mode ();
(* Initializing the solution number table *)
!Solver.init_snt ()
(* Initialisation of the random engine *)
Random.init seed ;
output_string stderr "#The random engine was initialized with the seed ";
output_string stderr (string_of_int seed);
output_string stderr "\n";
flush stderr ;
(* selecting the draw mode *)
Solver.set_efficient_mode ();
(* Initializing the solution number table *)
!Solver.init_snt ()
in
let lp = get_new_lucky_process_number () in
add_lp lp init_state;
lp
add_lp lp init_state;
lp
with
Failure msg ->
print_string msg;
flush stdout;
raise MakeError
Failure msg ->
print_string msg;
flush stdout;
raise MakeError
(* exported *)
let (kill_lucky_process : lucky_process -> unit) =
......
......@@ -796,7 +796,7 @@ let (make : string option -> string list -> Prog.t) =
Prog.initial_ctrl_state = luc_prog.initial_ctrl_state ;
Prog.get_wtl = get_wtl luc_prog;
Prog.is_final = List.for_all (List.for_all is_final_atomic);
Prog.is_final = List.for_all (List.for_all is_final_atomic);
Prog.gen_dot = luc_prog.gen_dot;
}
in
......@@ -828,7 +828,7 @@ let rec (make_state : string option -> string list -> Prog.state) =
Some(file,node) ->
print_string ("# Interpreting the lutin file " ^ file ^ " with node " ^ node^ "\n");
flush stdout;
LutProg.make_state file node
LutProg.make_state [file] node
| None ->
(* print_string "Lucky mode !\n"; *)
(* flush stdout; *)
......
......@@ -83,7 +83,7 @@ type reactive_program =
| LustreV6 of string * string
| LustreEc of string
| LustreEcExe of string
| Lutin of string * string
| Lutin of string list * string
| Socket of string * int
| SocketInit of string * int
| Ocaml of string
......@@ -105,7 +105,7 @@ let reactive_program_to_string = function
| LustreV6(f,node) -> "v6:"^f^":"^node
| LustreEc(f) -> "ec:"^f^":"
| LustreEcExe(f) -> "ec_exe:"^f^":"
| Lutin(f,node) -> "lutin:"^f^":"^node
| Lutin(f,node) -> "lutin:"^(String.concat "," f)^":"^node
| Socket(addr,port) -> "socket:"^addr^":"^(string_of_int port)
| SocketInit(addr,port) -> "socket_init:"^addr^":"^(string_of_int port)
......@@ -372,7 +372,7 @@ let (parse_rp_string : string -> unit) =
let l = (Str.split (Str.regexp ":") str) in
let rp =
match List.tl l with
| ["lutin"; prog; node] -> Lutin(prog, node)
| ["lutin"; prog; node] -> Lutin(Str.split (Str.regexp ",") prog, node)
| ["v6"; prog; node] -> LustreV6(prog, node)
| ["ec_exe"; prog] -> LustreEcExe(prog)
| ["ec"; prog] -> LustreEc(prog)
......
......@@ -73,7 +73,7 @@ let (make_rp_list : reactive_program list ->
let add_init init (a,b,c,d) = (a,b,c,d,init,init) in
let aux rp =
match rp with
| Lutin(prog,node) -> add_init [] (make_lut prog node)
| Lutin(prog,node) -> add_init [] (make_lut prog node)
| LustreV6(prog,node) -> add_init [] (LustreRun.make_v6 prog node)
| LustreV4(prog,node) -> add_init [] (LustreRun.make_v4 prog node)
| LustreEc(prog) -> add_init [] (LustreRun.make_ec prog)
......
......@@ -222,8 +222,7 @@ let of_expanded_code (exped: Expand.t) = (
let make ?(libs: string list option = None) infile mnode = (
try (
(** open the file, compile and expand the main node ... *)
let inchannel = open_in infile in
let mainprg = Parsers.read_lut inchannel in
let mainprg = Parsers.read_lut infile in
let tlenv = CheckType.check_pack libs mainprg in
let _ = !Solver.clear_snt (); !Solver.init_snt () in
let mnode = if mnode <> "" then mnode else (
......@@ -236,7 +235,7 @@ let make ?(libs: string list option = None) infile mnode = (
one, but I'm sure that list will be useful in the future... R1.*)
let mnode = if all_nodes = [] then
(* shouldn't that be checked before? *)
raise (Errors.Global_error ("the program "^infile^ " contains no node"))
raise (Errors.Global_error ((String.concat "," infile)^ " contains no node"))
else List.hd all_nodes
in
Verbose.put ~level:1 "# No node is specified: will use %s \n" mnode;
......
......@@ -42,7 +42,7 @@ N.B. dans un premier temps, c'est un step simple qu'on
type t
val make: ?libs:string list option -> string -> string -> t
val make: ?libs:string list option -> string list -> string -> t
(* Misc info *)
val in_var_list: t -> Exp.var list
......
......@@ -50,6 +50,7 @@ Hashtbl.add keywords "real" (function s -> TK_REAL s) ;;
Hashtbl.add keywords "trace" (function s -> TK_TRACE s) ;;
Hashtbl.add keywords "ref" (function s -> TK_REF s) ;;
Hashtbl.add keywords "exception" (function s -> TK_EXCEPTION s) ;;
Hashtbl.add keywords "include" (function s -> TK_INCLUDE s) ;;
Hashtbl.add keywords "pre" (function s -> TK_PRE s) ;;
......@@ -82,7 +83,7 @@ let token_code tk = (
| TK_ERROR lxm -> ( "TK_ERROR" , lxm )
| TK_IDENT lxm -> ("TK_IDENT", lxm)
| TK_STRING lxm -> ("TK_STRING", lxm)
| TK_LET lxm -> ("TK_LET", lxm)
| TK_IN lxm -> ("TK_IN", lxm)
| TK_EXTERN lxm -> ("TK_EXTERN", lxm)
......@@ -112,6 +113,7 @@ let token_code tk = (
| TK_TRACE lxm -> ("TK_TRACE", lxm)
| TK_REF lxm -> ("TK_REF", lxm)
| TK_EXCEPTION lxm -> ("TK_EXCEPTION", lxm)
| TK_INCLUDE lxm -> ("TK_INCLUDE", lxm)
| TK_PRE lxm -> ("TK_PRE", lxm)
| TK_FALSE lxm -> ("TK_FALSE", lxm)
......@@ -206,6 +208,14 @@ rule lexer = parse
handle_lexical_error comment_line lexbuf;
lexer lexbuf
}
(* une chaine quelconque *)
| "\"" [^ '\"']* "\""
{
let lxm = Lexeme.make lexbuf in
TK_STRING (lxm)
}
(* constantes entires et relles *)
| (chiffres)+ { TK_ICONST (Lexeme.make lexbuf ) }
......@@ -252,11 +262,11 @@ rule lexer = parse
(* mot-cl ou identificateur *)
| ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '_' '0'-'9'] *
{
let lxm = Lexeme.make lexbuf in
let x = is_a_keyword ( lxm.str ) in
match x with
None -> TK_IDENT ( lxm )
| Some keyw -> keyw (lxm )
let lxm = Lexeme.make lexbuf in
let x = is_a_keyword ( lxm.str ) in
match x with
None -> TK_IDENT ( lxm )
| Some keyw -> keyw (lxm )
}
| _ { TK_ERROR ( Lexeme.make lexbuf ) }
......
......@@ -16,6 +16,7 @@ let lettab = ref (Hashtbl.create 50)
let nodetab = ref (Hashtbl.create 50)
let excepttab = ref (Hashtbl.create 50)
let deflist = ref []
let included_files_to_handle = ref []
let add_info
(htbl : (string, 'a ) Hashtbl.t)
......@@ -32,16 +33,16 @@ let add_info
let add_except (idl : ident list) = (
let f id = (
match (add_info !excepttab id id) with
None -> deflist := (ExceptDef id) :: !deflist
| Some ei -> raise (
Compile_error ( id.src ,
(sprintf "bad exception declaration, ident already linked %s"
(Errors.lexeme_line_col ei.src)))
)
) in
List.iter f idl
let f id = (
match (add_info !excepttab id id) with
None -> deflist := (ExceptDef id) :: !deflist
| Some ei -> raise (
Compile_error ( id.src ,
(sprintf "bad exception declaration, ident already linked %s"
(Errors.lexeme_line_col ei.src)))
)
) in
List.iter f idl
)
(* N.B. let et extern sont dans le meme espace de nom
......@@ -58,6 +59,12 @@ let add_extern (id : Syntaxe.ident) (ci : let_info) = (
)
)
let (add_include : Lexeme.t -> unit) =
fun file ->
(* remove '"' from string. *)
let f = String.sub file.str 1 ((String.length file.str) - 2) in
included_files_to_handle := (f)::!included_files_to_handle
let add_letdef (id : Syntaxe.ident) (ci : let_info) = (
match ( add_info !lettab id ci) with
None -> deflist := (LetDef id) :: !deflist
......@@ -95,7 +102,8 @@ let parse_end () = (
pck_lettab = !lettab;
pck_nodetab = !nodetab;
pck_excepttab = !excepttab;
pck_deflist = (List.rev !deflist)
pck_deflist = (List.rev !deflist);
pck_included_files_to_handle = !included_files_to_handle
} in
lettab := Hashtbl.create 50;
nodetab := Hashtbl.create 50;
......@@ -120,6 +128,7 @@ let make_val_exp ven lxm = {
%token <Lexeme.t> TK_ERROR
%token <Lexeme.t> TK_IDENT
%token <Lexeme.t> TK_STRING
%token <Lexeme.t> TK_LET
%token <Lexeme.t> TK_IN
......@@ -150,6 +159,7 @@ let make_val_exp ven lxm = {
%token <Lexeme.t> TK_TRACE
%token <Lexeme.t> TK_REF
%token <Lexeme.t> TK_EXCEPTION
%token <Lexeme.t> TK_INCLUDE
%token <Lexeme.t> TK_PRE
%token <Lexeme.t> TK_FALSE
......@@ -272,8 +282,17 @@ lutFile:
{ }
;
lutInclude:
TK_INCLUDE TK_STRING
{ $2 }
;
lutOneDecl:
lutLetDecl
| lutInclude
{ add_include $1 }
| lutLetDecl
{ add_letdef (fst $1) (snd $1) }
| lutExceptDecl
{ add_except $1 }
......
......@@ -564,103 +564,102 @@ Verbose.exe ~level:2 (fun () -> Verbose.put "# <- treat_gtree, done\n");
)
let make ?(libs: string list option = None) infile mnode = (
try (
let inchannel = open_in infile in
let mainprg = Parsers.read_lut inchannel in
let tlenv = CheckType.check_pack libs mainprg in
let mnode = if mnode <> "" then mnode else
let all_nodes =
Hashtbl.fold
(fun n _ acc -> n::acc)
mainprg.Syntaxe.pck_nodetab
[]
in
(* It is not necessary to build to complete list to take the first
one, but I'm sure that list will be useful in the future... R1.*)
let mnode =
if all_nodes = [] then
(* shouldn't that be checked before? *)
raise (Errors.Global_error ("the program "^infile^
" contains no node"))
else
List.hd all_nodes
in
Verbose.put ~level:1 "# No node is specified: will use %s \n" mnode;
mnode
in
let exped = Expand.make tlenv mainprg mnode in
(* Les tables de variables decoulent du exped *)
Verbose.put ~level:3 "#---begin AutoGen.make\n";
(* STUPID ! let auto = AutoGen.make exped in *)
(* HERE : PROBLEM, COUNTER ARE NO LONGER DISCOVERED ??? *)
let auto = AutoGen.init exped in
Verbose.put ~level:3 "#---end AutoGen.make\n";
let zelut = create auto in
let _ = init_vars zelut in
let id2var (id: CoIdent.t) = (
let nme = CoIdent.to_string id in
Hashtbl.find zelut.lucky_var_tab nme
) in
let sort_bool_num k v (blin, nlin) = (
(* Verbose.exe ~level:3 (fun () -> Printf.fprintf stderr "sort_bool_num %s=%s\n" k (Var.to_string v)); *)
match Var.mode v with
| Var.Output
| Var.Local -> (
if (Var.alias v = None) then (
if (Var.typ v = Type.BoolT)
then (v::blin, nlin)
else (blin, v::nlin)
) else (blin, nlin)
)
| _ -> (blin, nlin)
) in
let (bl,nl) = Hashtbl.fold sort_bool_num zelut.lucky_var_tab ([],[]) in
(* let get_all_mems n ve a = (n,ve)::a in *)
(* let get_all_mems n ve a = (Prevar.get_pre_var_name n, ve)::a in *)
let get_all_mems n ve a = (Var.name ve, Hashtbl.find zelut.lucky_var_tab n)::a in
(* la fonction qui dit si c'est final *)
let is_final s = (
match AutoGen.get_state_info zelut.auto s with
| AutoGen.SS_final _ -> true
| _ -> false
) in
(* returns a t AND a Prog.t *)
(zelut,
{
Prog.initial_ctrl_state = [[AutoGen.init_control auto]];
Prog.in_vars = List.map id2var (Expand.input_list exped);
Prog.out_vars = List.map id2var (Expand.output_list exped);
Prog.loc_vars = List.map id2var (Expand.local_out_list exped);
Prog.ext_func_tbl = Util.StringMap.empty;
Prog.memories_names = Hashtbl.fold get_all_mems zelut.lucky_prevar_tab [];
Prog.bool_vars_to_gen = [bl];
Prog.num_vars_to_gen = [nl];
Prog.output_var_names = [Expand.output_list exped];
Prog.reactive = false;
Prog.get_wtl = lut_get_wtl zelut;
Prog.is_final = List.for_all (List.for_all is_final) ;
Prog.gen_dot = (fun _ _ _ -> assert false);
}
try (
let mainprg = Parsers.read_lut infile in
let tlenv = CheckType.check_pack libs mainprg in
let mnode = if mnode <> "" then mnode else
let all_nodes =
Hashtbl.fold
(fun n _ acc -> n::acc)
mainprg.Syntaxe.pck_nodetab
[]
in
(* It is not necessary to build to complete list to take the first
one, but I'm sure that list will be useful in the future... R1.*)
let mnode =
if all_nodes = [] then
(* shouldn't that be checked before? *)
raise (Errors.Global_error ((String.concat "," infile)^
" contains no node"))
else
List.hd all_nodes
in
Verbose.put ~level:1 "# No node is specified: will use %s \n" mnode;
mnode
in
let exped = Expand.make tlenv mainprg mnode in
(* Les tables de variables decoulent du exped *)
Verbose.put ~level:3 "#---begin AutoGen.make\n";
(* STUPID ! let auto = AutoGen.make exped in *)
(* HERE : PROBLEM, COUNTER ARE NO LONGER DISCOVERED ??? *)
let auto = AutoGen.init exped in
Verbose.put ~level:3 "#---end AutoGen.make\n";
let zelut = create auto in
let _ = init_vars zelut in
let id2var (id: CoIdent.t) = (
let nme = CoIdent.to_string id in
Hashtbl.find zelut.lucky_var_tab nme
) in
let sort_bool_num k v (blin, nlin) = (
(* Verbose.exe ~level:3 (fun () -> Printf.fprintf stderr "sort_bool_num %s=%s\n" k (Var.to_string v)); *)
match Var.mode v with
| Var.Output
| Var.Local -> (
if (Var.alias v = None) then (
if (Var.typ v = Type.BoolT)
then (v::blin, nlin)
else (blin, v::nlin)
) else (blin, nlin)
)
) with
Sys_error(s) -> (
prerr_string (s^"\n") ; exit 1
) |
Errors.Global_error s -> (
Errors.print_global_error s ; exit 1
) |
Parsing.Parse_error -> (
Errors.print_compile_error (Lexeme.last_made ()) "syntax error";
exit 1
) |
Errors.Compile_error(lxm,msg) -> (
Errors.print_compile_error lxm msg ; exit 1
) |
Errors.Internal_error (fname,msg) -> (
Errors.print_internal_error fname msg ; exit 1
)
| _ -> (blin, nlin)
) in
let (bl,nl) = Hashtbl.fold sort_bool_num zelut.lucky_var_tab ([],[]) in
(* let get_all_mems n ve a = (n,ve)::a in *)
(* let get_all_mems n ve a = (Prevar.get_pre_var_name n, ve)::a in *)
let get_all_mems n ve a = (Var.name ve, Hashtbl.find zelut.lucky_var_tab n)::a in
(* la fonction qui dit si c'est final *)
let is_final s = (
match AutoGen.get_state_info zelut.auto s with
| AutoGen.SS_final _ -> true
| _ -> false
) in
(* returns a t AND a Prog.t *)
(zelut,
{
Prog.initial_ctrl_state = [[AutoGen.init_control auto]];
Prog.in_vars = List.map id2var (Expand.input_list exped);
Prog.out_vars = List.map id2var (Expand.output_list exped);
Prog.loc_vars = List.map id2var (Expand.local_out_list exped);
Prog.ext_func_tbl = Util.StringMap.empty;
Prog.memories_names = Hashtbl.fold get_all_mems zelut.lucky_prevar_tab [];
Prog.bool_vars_to_gen = [bl];
Prog.num_vars_to_gen = [nl];
Prog.output_var_names = [Expand.output_list exped];
Prog.reactive = false;
Prog.get_wtl = lut_get_wtl zelut;
Prog.is_final = List.for_all (List.for_all is_final) ;
Prog.gen_dot = (fun _ _ _ -> assert false);
}
)
) with
Sys_error(s) -> (
prerr_string (s^"\n") ; exit 1
) |
Errors.Global_error s -> (
Errors.print_global_error s ; exit 1
) |
Parsing.Parse_error -> (
Errors.print_compile_error (Lexeme.last_made ()) "syntax error";
exit 1
) |
Errors.Compile_error(lxm,msg) -> (
Errors.print_compile_error lxm msg ; exit 1
) |
Errors.Internal_error (fname,msg) -> (
Errors.print_internal_error fname msg ; exit 1
)
)
let get_init_state ?(verb_level=0) zelutprog zeprog = (
......
......@@ -3,11 +3,11 @@
type t
(** [make infile mnode] *)
val make : ?libs:string list option -> string -> string -> (t * Prog.t)
val make : ?libs:string list option -> string list -> string -> (t * Prog.t)
val get_init_state : ?verb_level:int -> t -> Prog.t -> Prog.state
(** [make_state infile mnode] *)
val make_state : ?libs:string list option -> ?verb_level:int -> string -> string -> Prog.state