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

lurette 0.63 Tue, 07 May 2002 15:12:50 +0200 by jahier

Parent-Version:      0.62
Version-Log:

Reimplement the rif parsing in ima_exe.ml so that it is correct wrt the BLA-RIF
doc.

Project-Description: Lurette
parent c88a7a6f
......@@ -4,10 +4,10 @@
(test/usager.env 523 1019479246 b/14_usager.env 1.7)
(source/command_line_ima_exe.mli 1045 1020420514 b/34_command_li 1.2)
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 13132 1020420514 51_env_state. 1.18)
(source/env_state.ml 13131 1020777170 51_env_state. 1.19)
(source/graph.ml 1819 1016011748 14_graph.ml 1.5)
(bin/Makefile.ima_exe 1926 1020420514 b/41_Makefile.i 1.2)
(source/util.ml 12274 1020420514 35_util.ml 1.18)
(source/util.ml 12330 1020777170 35_util.ml 1.19)
(source/wtree.ml 11388 1020420514 b/1_wtree.ml 1.11)
(source/solver.ml 24560 1017837703 39_solver.ml 1.21)
(test/test_gen_stubs.h 1818 1020068208 b/45_test_gen_s 1.1)
......@@ -27,13 +27,13 @@
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(source/parse_env.mli 908 1020420514 40_parse_env. 1.7)
(source/sim2chro.mli 1429 1017929190 b/23_sim2chro.m 1.4)
(source/ima_exe.ml 7871 1020432102 b/32_ima_exe.ml 1.7)
(source/ima_exe.ml 9327 1020777170 b/32_ima_exe.ml 1.8)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/eval.ml 7749 1016803757 49_eval.ml 1.12)
(source/gen_stubs.ml 36501 1020420514 24_generate_l 1.24)
(source/gen_stubs.ml 36477 1020777170 24_generate_l 1.25)
(source/parse_env.ml 18485 1020420514 41_parse_env. 1.18)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
(source/sim2chro.ml 2680 1017929190 b/24_sim2chro.m 1.7)
(source/sim2chro.ml 2653 1020777170 b/24_sim2chro.m 1.8)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(source/formula.mli 3646 1020420514 44_formula.ml 1.12)
(TAGS 9825 1007379917 21_TAGS 1.6)
......@@ -46,7 +46,7 @@
(source/eval.mli 1389 1016803757 48_eval.mli 1.9)
(README 74 1011881677 10_README 1.2)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(OcamlMakefile 22160 1020068208 17_OcamlMakef 1.27)
(OcamlMakefile 22285 1020777170 17_OcamlMakef 1.28)
(source/command_line_ima_exe.ml 2665 1020420514 b/33_command_li 1.3)
(test/ControleurPorte.rif.exp 4746 1016803757 b/29_Controleur 1.4)
(test/tram.env 1149 1019479246 b/15_tram.env 1.6)
......@@ -65,7 +65,7 @@
(test/heater_int.lus 170 1020068208 b/43_heater_int 1.1)
(source/graph.mli 1499 1020432102 13_graph.mli 1.7)
(test/heater_int.rif.exp 858 1017837703 b/28_heater_int 1.2)
(source/formula.ml 7330 1020420514 45_formula.ml 1.13)
(source/formula.ml 7348 1020777170 45_formula.ml 1.14)
(source/lurette.mli 448 1016027474 11_lurette.ml 1.12)
(source/print.ml 6587 1020420514 47_print.ml 1.15)
(test/vrai_tram.h 2468 1012914629 b/7_vrai_tram. 1.2)
......
......@@ -5,7 +5,7 @@
# For updates see:
# http://miss.wu-wien.ac.at/~mottl/ocaml_sources
#
# $Id: OcamlMakefile 1.27 Mon, 29 Apr 2002 10:16:48 +0200 jahier $
# $Id: OcamlMakefile 1.28 Tue, 07 May 2002 15:12:50 +0200 jahier $
#
###########################################################################
# Set these variables to the names of the sources to be processed and
......@@ -506,15 +506,15 @@ vroum:
# Non regression test
test:
$(LURETTE_PATH)/make_lurette ControleurPorte; \
$(LURETTE_PATH)/make_lurette ControleurPorte; rm -f tram.rif; touch tram.rif; \
./lurette 100 10 10 -o tram.rif tram.env usager.env porte.env passerelle.env -seed 1013219512 -ns2c ;\
diff -u ControleurPorte.rif.exp tram.rif > test1.res ;\
\
$(LURETTE_PATH)/make_lurette heater_int; \
$(LURETTE_PATH)/make_lurette heater_int; rm -f heater_int.rif; touch heater_int.rif; \
./lurette 30 10 10 temp_int.env --no-oracle -seed 1013219512 -ns2c -o heater_int.rif ;\
diff -u heater_int.rif.exp heater_int.rif > test2.res ; \
\
$(LURETTE_PATH)/make_lurette heater_float; \
$(LURETTE_PATH)/make_lurette heater_float; rm -f heater_float.rif; touch heater_float.rif; \
./lurette 30 10 10 temp_float.env --no-oracle -seed 1013219512 -ns2c -o heater_float.rif;\
diff -u heater_float.rif.exp heater_float.rif > test3.res ; \
\
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 62)
(Parent-Version lurette 0 61)
(Version-Log "
Reorganise things a little bit so that show_ima does not depend on
cudd, etc.
(Project-Version lurette 0 63)
(Parent-Version lurette 0 62)
(Version-Log "
Reimplement the rif parsing in ima_exe.ml so that it is correct wrt the BLA-RIF doc.
")
(New-Version-Log "")
(Checkin-Time "Fri, 03 May 2002 15:21:42 +0200")
(Checkin-Time "Tue, 07 May 2002 15:12:50 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -24,7 +20,7 @@ cudd, etc.
;; 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.7 644))
(source/ima_exe.ml (lurette/b/32_ima_exe.ml 1.8 644))
(source/command_line_ima_exe.ml (lurette/b/33_command_li 1.3 644))
(source/command_line_ima_exe.mli (lurette/b/34_command_li 1.2 644))
......@@ -43,7 +39,7 @@ cudd, etc.
(source/env.mli (lurette/15_env.mli 1.13 644))
(source/env.ml (lurette/16_env.ml 1.25 644))
(source/util.ml (lurette/35_util.ml 1.18 644))
(source/util.ml (lurette/35_util.ml 1.19 644))
(source/solver.mli (lurette/38_solver.mli 1.11 644))
(source/solver.ml (lurette/39_solver.ml 1.21 644))
......@@ -58,7 +54,7 @@ cudd, etc.
(source/show_env.ml (lurette/43_show_env.m 1.7 644))
(source/formula.mli (lurette/44_formula.ml 1.12 644))
(source/formula.ml (lurette/45_formula.ml 1.13 644))
(source/formula.ml (lurette/45_formula.ml 1.14 644))
(source/print.mli (lurette/46_print.mli 1.8 644))
(source/print.ml (lurette/47_print.ml 1.15 644))
......@@ -67,24 +63,24 @@ cudd, etc.
(source/eval.ml (lurette/49_eval.ml 1.12 644))
(source/env_state.mli (lurette/50_env_state. 1.17 644))
(source/env_state.ml (lurette/51_env_state. 1.18 644))
(source/env_state.ml (lurette/51_env_state. 1.19 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.9 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.11 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.4 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.7 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.8 644))
(source/gne.mli (lurette/b/36_gne.mli 1.1 644))
(source/gne.ml (lurette/b/37_gne.ml 1.1 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.24 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.25 644))
; little script that sets env vars and starts the lurette build
(make_lurette (lurette/27_make_luret 1.12 744))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.27 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.28 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.3 644))
(bin/Makefile.show_ima (lurette/b/40_Makefile.s 1.3 644))
......
......@@ -342,7 +342,7 @@ and
Util.merge (build_list_pre [] n vn) acc
let _ = assert ( (add_missing_pre ["_pre3toto"; "_pre2titi"; "_pre2toto"])
= ["_pre2titi"; "_pre1titi"; "_pre3toto"; "_pre2toto"; "_pre1toto"] )
= ["_pre1toto"; "_pre2toto"; "_pre3toto"; "_pre1titi"; "_pre2titi"])
(** Returns the initial node of the automata defined in
......
......@@ -222,10 +222,10 @@ let (var_type_to_string2 : var_type -> string) =
let print_var_value oc e =
match e with
N(I(i)) -> output_string oc (string_of_int i)
| N(F(f)) -> output_string oc (string_of_float f)
| B(true) -> output_string oc "t"
| B(false) -> output_string oc "f"
N(I(i)) -> output_string oc ((string_of_int i) ^ " ")
| N(F(f)) -> output_string oc ((string_of_float f) ^ " ")
| B(true) -> output_string oc "t "
| B(false) -> output_string oc "f "
let (print_subst_list : subst list -> out_channel -> unit) =
......
......@@ -276,7 +276,7 @@ let (generate_stub_c: module_name -> string -> vn_ct list -> vn_ct list -> unit)
(*
** Compiler directive
*)
put ("// Automatically generated from " ^ mod_name ^ ".h by interface/gen_stubs.\n" ^
put ("// Automatically generated from " ^ mod_name ^ ".h by bin/gen_stubs.\n" ^
"#include <stdlib.h>\n" ^
"#include \"" ^ mod_name ^ ".h\" \n" ^
" \n") ;
......@@ -376,7 +376,7 @@ let (generate_idl : module_name -> sut_or_oracle -> vn_ct list -> vn_ct list
let vo_pre = List.tl ov in
put ("// Automatically generated file from " ^ mod_name
^ ".h by interface/gen_stubs.\n") ;
^ ".h by bin/gen_stubs.\n") ;
put "\n" ;
(*
......@@ -670,7 +670,7 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
** e.g., if mltl_in = [int, bool], then fvnl_in = ["N(I(x1))"; "B(x2)"]
*)
put "(* Automatically generated from sut_idl_stub.ml by interface/gen_stubs. *)\n" ;
put "(* Automatically generated from sut_idl_stub.ml by bin/gen_stubs. *)\n" ;
put "open Format\n";
put "open Hashtbl\n";
put "open Formula\n\n";
......@@ -984,7 +984,7 @@ let (gen_a_fake_oracle : string -> unit) =
put "-- Automatically generated from ";
put sut_h ;
put " by interface/gen_stubs. \n" ;
put " by bin/gen_stubs. \n" ;
put "\n";
put "node always_true(";
put (format_string_list "; " vn_lt_str_l) ;
......
......@@ -29,60 +29,126 @@ let (options:Command_line_ima_exe.optionsT) = {
(*------------------------------------------------------------------------*)
(* RIF parsing *)
let lexer = Genlex.make_lexer ["t"; "f"; "#"]
let lexer = Genlex.make_lexer ["#"; "#@"; "@#"]
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 (B(true))
| ((vn, BoolT), Genlex.Kwd "f") -> Hashtbl.add tbl vn (B(false))
| ((vn, BoolT), Genlex.Int 0) -> Hashtbl.add tbl vn (B(false))
| ((vn, BoolT), Genlex.Int 1) -> Hashtbl.add tbl vn (B(true))
| ((vn, IntT(_,_)), Genlex.Int i) -> Hashtbl.add tbl vn (N(I(i)))
| ((vn, FloatT(_,_)), Genlex.Float f) -> Hashtbl.add tbl vn (N(F(f)))
| _ -> failwith ("*** Bad input. A " ^ (var_type_to_string2 vt) ^
" was expected for variable " ^ vn ^ ".\n")
)
vntl
in
tbl
let rif_pragmas = ["inputs"]
(* Which pragmas should be defined ? *)
(* let rif_pragmas = ["outs";"outputs";"program";"inputs";"step";"reset"] *)
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
| _ -> get_inputs vntl stream
(** Reads the environment input values on stdin. It should
follow the rif format. *)
let tbl = Hashtbl.create (List.length vntl) in
if vntl = []
then tbl
else
let line = read_line () in
let stream = lexer(Stream.of_string line) in
parse_rif_stream vntl stream tbl
and (parse_rif_stream : vnt list -> rif_stream -> env_in -> env_in) =
fun vntl stream tbl ->
if vntl = []
then tbl
else
let tok_list = Stream.npeek 2 stream in
match tok_list with
| [Genlex.Kwd "#"; Genlex.Ident id] ->
if List.mem id rif_pragmas
then
(
Stream.junk stream ;
Stream.junk stream ;
parse_rif_stream vntl stream tbl
)
else
(* We skip everything that occurs after a [#] not followed by a
member of [rif_pragmas], until the next eol. *)
(
Stream.junk stream ;
parse_rif_stream vntl (lexer (Stream.of_string (read_line ()))) tbl
)
| (Genlex.Kwd "#")::_
(* Ditto *)
->
Stream.junk stream ;
parse_rif_stream vntl (lexer (Stream.of_string (read_line ()))) tbl
| (Genlex.Kwd "#@")::_ ->
(* Beginning of multi-line comment. Note that here,
unlike the rif format, we ignore multi line pragmas;
namely, we handle them as a lusti-line comment. *)
(
Stream.junk stream ;
ignore_toks_until_end_of_pragmas vntl stream tbl
)
| (Genlex.Float f)::_ ->
(
Stream.junk stream ;
Hashtbl.add tbl (fst (hd vntl)) (N(F(f))) ;
parse_rif_stream (tl vntl) stream tbl
)
| (Genlex.Int i)::_ ->
(
Stream.junk stream ;
if ((var_type_to_string (snd (hd vntl))) = "bool")
then
if i = 0
then Hashtbl.add tbl (fst (hd vntl)) (B(false))
else Hashtbl.add tbl (fst (hd vntl)) (B(true))
else Hashtbl.add tbl (fst (hd vntl)) (N(I(i))) ;
parse_rif_stream (tl vntl) stream tbl
)
| (Genlex.Ident b)::_ ->
(
Stream.junk stream ;
if mem b ["f"; "F";"false"]
then Hashtbl.add tbl (fst (hd vntl)) (B(false))
else if mem b ["t"; "T";"true"]
then Hashtbl.add tbl (fst (hd vntl)) (B(true))
else
failwith ("### parse error. " ^ b ^ " is unknown \n") ;
parse_rif_stream (tl vntl) stream tbl
)
| [] ->
(* Eol is is reached; proceed with the next one *)
parse_rif_stream vntl (lexer (Stream.of_string (read_line ()))) tbl
| _ -> failwith ("### parse error.\n")
and (ignore_toks_until_end_of_pragmas : vnt list -> rif_stream -> env_in
-> env_in) =
fun vntl stream tbl ->
(* ignore all tokens until "@#" is reached *)
let tok_opt = Stream.peek stream in
match tok_opt with
| Some(Genlex.Kwd "@#") ->
(
Stream.junk stream ;
parse_rif_stream vntl stream tbl
)
| Some(_) ->
(
Stream.junk stream ;
ignore_toks_until_end_of_pragmas vntl stream tbl
)
| None ->
(* Eol is is reached; proceed with the next one *)
ignore_toks_until_end_of_pragmas vntl
(lexer (Stream.of_string (read_line ()))) tbl
let (write_rif_output : vnt list -> env_out -> unit) =
fun vntl output ->
......@@ -167,9 +233,6 @@ and
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 =
......
......@@ -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_var_value rif e; put " "))
(fun (_, e) -> (print_var_value rif e))
(Util.sort_list_string_pair input);
put "#outs ";
Hashtbl.iter
(fun _ e -> (print_var_value rif e; put " "))
(fun _ e -> (print_var_value rif e))
output;
if display_local_var then
List.iter
(fun (_, e) -> (print_var_value rif e; put " "))
(fun (_, e) -> (print_var_value rif e))
(Util.sort_list_string_pair local);
put "\n"
......
......@@ -171,8 +171,8 @@ let (sort_list_string_pair: (string * 'a) list -> (string * 'a) list) =
List.sort (fun (vn1, t1) (vn2, t2) -> compare vn1 vn2) var_list
(**
Merges two lists without introducing duplicates.
(** Merges two lists without introducing duplicates, respecting the
original elements ordering.
*)
let rec (merge: 'a list -> 'a list -> 'a list) =
fun list1 list2 ->
......@@ -181,7 +181,7 @@ let rec (merge: 'a list -> 'a list -> 'a list) =
| x1::t1 ->
if (List.mem x1 list2)
then merge t1 list2
else merge t1 (x1::list2)
else merge t1 (List.append list2 [x1])
let _ = assert (list_are_equals (merge [1;2;3;4] [4;1;5;6]) [1;2;3;4;5;6])
let _ = assert (list_are_equals (merge [] [4;1;5;6]) [1;4;5;6])
......
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