Commit 62b3a13b authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.9 Mon, 19 Nov 2001 16:09:05 +0100 by jahier

Parent-Version:      perso.5
Version-Log:

Lurette tourne avec edge.lus vrai.lus et random_bool.aut !

Project-Description: Lurette
parent 0b182b5e
;; This file is automatically generated, editing may cause PRCS to do
;; REALLY bad things.
(Created-By-Prcs-Version 1 3 3)
(env.mli 3428 1003932490 15_env.mli 1.2)
(env.mli 3513 1006182545 15_env.mli 1.3)
(test.aut 644 1003928781 22_test.aut 1.1)
(interface/generate_lurette_interface.mli 2054 1004519854 23_generate_l 1.1)
(Mercury/graph.m 15076 1002205313 7_graph.m 1.1)
(Mercury/lurette.m 4239 1002789994 5_lurette.m 1.5)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(env.ml 21601 1004539865 16_env.ml 1.4)
(env.ml 24522 1006182545 16_env.ml 1.5)
(Mercury/test.aut 1231 1002546062 8_test2.aut 1.1)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(make_lurette 1010 1004969037 27_make_luret 1.1)
(make_lurette 1059 1006182545 27_make_luret 1.2)
(Mercury/Mmakefile 102 1002789994 1_Mmakefile 1.3)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(Makefile 295 1004969037 18_Makefile 1.4)
(interface/generate_lurette_interface.ml 12207 1004969037 24_generate_l 1.5)
(interface/Makefile 132 1004969037 25_Makefile 1.2)
(Makefile 323 1006182545 18_Makefile 1.5)
(interface/Makefile 115 1006182545 25_Makefile 1.3)
(OcamlMakefile 15015 1004519854 17_OcamlMakef 1.2)
(interface/TAGS 608 1004519854 26_TAGS 1.1)
(interface/TAGS 1497 1006182545 26_TAGS 1.2)
(README 0 1002791390 10_README 1.1)
(random_bool.aut 418 1006182545 29_random_boo 1.1)
(Mercury/env.m 9937 1003928781 4_env_automa 1.5)
(interface/gen_stubs.ml 31878 1006182545 24_generate_l 1.6)
(Mercury/dot_automata.m 5814 1002546062 9_dot_automa 1.1)
(vrai.lus 65 1006182545 28_vrai.lus 1.1)
(Mercury/dot.m 3636 1002298322 6_dot.m 1.2)
(Mercury/memory.m 3884 1002196285 3_memory.m 1.1)
(graph.mli 1305 1003932490 13_graph.mli 1.2)
(graph.ml 2397 1003932490 14_graph.ml 1.2)
(lurette.mli 514 1003928781 11_lurette.ml 1.1)
(TAGS 4544 1004547252 21_TAGS 1.4)
(lurette.ml 990 1004547252 12_lurette.ml 1.4)
(lurette.mli 439 1006182545 11_lurette.ml 1.2)
(TAGS 5673 1006182545 21_TAGS 1.5)
(lurette.ml 6688 1006182545 12_lurette.ml 1.5)
......@@ -6,6 +6,7 @@ SOURCES = $(SUT) \
sut_stub.c sut_idl_stub.idl \
$(ORACLE) \
oracle_stub.c oracle_idl_stub.idl \
lurette_stub.ml \
graph.mli graph.ml env.mli env.ml lurette.mli lurette.ml
RESULT = lurette
......
lurette_stub.ml,736
Lurette_stub1,0
type sut_insut_in4,85
type sut_outsut_out6,105
let (sut_trysut_try8,126
let (sut_stepsut_step12,206
let (oracle_tryoracle_try16,288
let (oracle_steporacle_step20,391
let sut_input_var_name_and_type_listsut_input_var_name_and_type_list24,496
let sut_output_var_name_and_type_listsut_output_var_name_and_type_list26,555
type atomic_expratomic_expr28,615
| IntInt29,635
| BoolBool30,650
| FloatFloat31,667
let (lookup_sut_inlookup_sut_in34,688
let (lookup_sut_outlookup_sut_out40,848
let sut_in_initsut_in_init46,1010
let sut_out_initsut_out_init48,1037
let (list_ae_to_sut_inlist_ae_to_sut_in50,1065
let (print_sut_inprint_sut_in56,1207
let (print_sut_outprint_sut_out60,1278
graph.mli,219
Graph1,0
tt16,425
......@@ -21,131 +43,141 @@ let (get_list_of_target_nodesget_list_of_target_nodes58,1608
let (get_all_nodesget_all_nodes70,2116
let (get_all_transget_all_trans77,2242
env.mli,768
env.mli,794
Env1,0
type var_name_and_typevar_name_and_type38,1293
type datedate39,1316
type formula_epsformula_eps40,1326
type formulaformula41,1343
type weigthweigth42,1356
type nodenode44,1375
type arcarc45,1391
type arc_infoarc_info46,1414
type memory_eltmemory_elt47,1451
type substsubst48,1468
type env_inenv_in49,1480
type env_outenv_out50,1505
type env_locenv_loc51,1531
type env_stateTenv_stateT54,1559
mutable current_nodecurrent_node55,1579
mutable graphgraph56,1610
mutable inputinput61,1723
mutable outputoutput62,1750
mutable locallocal63,1778
val read_env_stateread_env_state69,1884
val env__tryenv__try80,2342
val env__stepenv__step90,2776
val generate_env_graphgenerate_env_graph99,3044
val gvgv112,3405
type var_typevar_type40,1312
type var_namevar_name41,1335
type var_name_and_typevar_name_and_type42,1358
type datedate43,1403
type formula_epsformula_eps44,1413
type formulaformula45,1430
type weigthweigth46,1443
type nodenode48,1462
type arcarc49,1478
type arc_infoarc_info50,1501
type substsubst52,1539
type env_inenv_in54,1552
type env_outenv_out55,1575
type env_locenv_loc56,1597
type env_stateTenv_stateT59,1625
mutable current_nodescurrent_nodes60,1645
mutable graphgraph61,1682
mutable inputinput66,1795
mutable outputoutput67,1822
mutable locallocal68,1850
val read_env_stateread_env_state74,1956
val env_tryenv_try85,2414
val env_stepenv_step95,2853
val generate_env_graphgenerate_env_graph104,3123
val gvgv117,3490
env.ml,3055
env.ml,2931
Env1,0
type weigthweigth16,420
type exprexpr18,439
| SumSum19,452
| DiffDiff20,477
| ProdProd21,502
| QuotQuot22,527
| ModMod23,552
| DivDiv24,577
| VarVar25,602
| ValVal26,620
| Pre_ePre_e27,689
type formulaformula29,708
| AndAnd30,723
| OrOr31,752
| NotNot32,781
| TrueTrue33,800
| FalseFalse34,809
| BoolBool35,819
| EqEq37,869
| GeGe38,901
| GG38,901
| Pre_fPre_f40,965
type formula_epsformula_eps42,989
| EpsEps43,1009
| FF44,1017
type nodenode48,1113
type arcarc50,1130
type arc_infoarc_info52,1154
type var_namevar_name54,1192
type memory_eltmemory_elt55,1215
type memory_elt = BB55,1215
type memory_elt = B of bool | VV55,1215
type memory_elt = B of bool | V of string | UU55,1215
type substsubst56,1261
type env_inenv_in57,1298
type env_outenv_out58,1324
type env_locenv_loc59,1350
type env_stateTenv_stateT62,1378
mutable current_nodecurrent_node63,1398
mutable graphgraph64,1429
mutable inputinput69,1542
mutable outputoutput70,1569
mutable locallocal71,1597
let (env_stateenv_state75,1628
type datedate83,1775
type var_typevar_type88,1878
type var_name_and_typevar_name_and_type89,1901
type read_arcread_arc91,1947
type read_arc = ArcArc91,1947
type read_automataread_automata93,1994
type read_automata = AutomataAutomata93,1994
exception EnvErrorEnvError102,2334
let lexerlexer111,2498
type aut_tokenaut_token117,2688
let rec (parse_automataparse_automata119,2728
and (parse_list_varparse_list_var132,3178
and (parse_list_var_tailparse_list_var_tail138,3418
and (parse_varparse_var144,3683
and (parse_list_arcparse_list_arc150,3855
and (parse_list_arc_tailparse_list_arc_tail156,4055
and (parse_arcparse_arc162,4276
and (parse_arc_infoparse_arc_info168,4524
and (parse_formula_epsparse_formula_eps173,4688
and (parse_formulaparse_formula179,4853
and (parse_more_formulaparse_more_formula190,5461
and (parse_expr_rightparse_expr_right196,5700
and (parse_exprparse_expr208,6088
and (parse_more_addsparse_more_adds212,6221
and (parse_multparse_mult218,6493
and (parse_more_multsparse_more_mults222,6629
and (parse_simpleparse_simple230,7083
let (read_env_stateread_env_state243,7514
let (lookuplookup287,9145
let (lookup_memlookup_mem291,9235
let rec (evaleval299,9396
(eval_pre_formulaeval_pre_formula356,11259
(eval_pre_expreval_pre_expr379,12264
(formula_eps_to_stringformula_eps_to_string431,14111
(formula_to_stringformula_to_string436,14245
(expr_to_stringexpr_to_string449,14890
let (arc_info_to_stringarc_info_to_string461,15562
let rec (gen_listgen_list469,15800
let (env__tryenv__try477,16020
let (env__stepenv__step544,18406
let (gvgv559,18897
let (dump_nodes_listdump_nodes_list566,19104
type transtrans583,19712
let (dump_trans_listdump_trans_list585,19751
let (dump_graphdump_graph601,20338
let (generate_graphgenerate_graph609,20691
let (generate_env_graphgenerate_env_graph624,21221
type weigthweigth17,448
type exprexpr19,467
| SumSum20,480
| DiffDiff21,505
| ProdProd22,530
| QuotQuot23,555
| ModMod24,580
| DivDiv25,605
| VarVar26,630
| Pre_ePre_e27,649
| II28,719
| BB29,732
| FF30,746
type formulaformula32,762
| AndAnd33,777
| OrOr34,806
| NotNot35,835
| TrueTrue36,854
| FalseFalse37,863
| BidBid38,873
| EqEq40,922
| GeGe41,954
| GG41,954
| Pre_fPre_f43,1018
type formula_epsformula_eps45,1042
| EpsEps46,1062
| FormForm47,1070
type nodenode53,1183
type arcarc55,1200
type arc_infoarc_info57,1224
type var_namevar_name59,1262
type substsubst60,1285
type env_inenv_in62,1324
type env_outenv_out63,1347
type env_locenv_loc64,1369
type env_stateTenv_stateT67,1397
mutable current_nodescurrent_nodes68,1417
mutable graphgraph69,1454
mutable inputinput74,1567
mutable outputoutput75,1594
mutable locallocal76,1622
let (env_stateenv_state80,1653
type datedate89,1802
type var_typevar_type94,1905
type var_name_and_typevar_name_and_type95,1928
type read_arcread_arc97,1974
type read_arc = ArcArc97,1974
type read_automataread_automata99,2021
type read_automata = AutomataAutomata99,2021
exception EnvErrorEnvError108,2361
let lexerlexer117,2531
type aut_tokenaut_token123,2728
let rec (parse_automataparse_automata125,2768
and (parse_list_varparse_list_var138,3330
and (parse_list_var_tailparse_list_var_tail144,3570
and (parse_varparse_var150,3842
and (parse_list_arcparse_list_arc156,4049
and (parse_list_arc_tailparse_list_arc_tail162,4249
and (parse_arcparse_arc168,4477
and (parse_arc_infoparse_arc_info174,4774
and (parse_formula_epsparse_formula_eps179,4952
and (parse_formulaparse_formula185,5127
and (parse_more_formulaparse_more_formula196,5797
and (parse_expr_rightparse_expr_right202,6050
and (parse_exprparse_expr214,6459
and (parse_more_addsparse_more_adds218,6592
and (parse_multparse_mult224,6878
and (parse_more_multsparse_more_mults228,7014
and (parse_simpleparse_simple236,7496
let (read_env_stateread_env_state249,7903
let (lookup_loclookup_loc294,9627
let (lookup_prelookup_pre298,9724
let rec (evaleval311,10064
(eval_pre_formulaeval_pre_formula368,11828
(eval_pre_expreval_pre_expr391,12728
(formula_eps_to_stringformula_eps_to_string445,14512
(formula_to_stringformula_to_string450,14649
(expr_to_stringexpr_to_string463,15293
let (arc_info_to_stringarc_info_to_string477,16036
let rec (gen_listgen_list485,16274
let (env_tryenv_try493,16494
let (env_stepenv_step621,21258
let (gvgv636,21758
let (dump_nodes_listdump_nodes_list643,21965
type transtrans660,22602
let (dump_trans_listdump_trans_list662,22641
let (dump_graphdump_graph678,23225
let (generate_graphgenerate_graph686,23592
let (generate_env_graphgenerate_env_graph701,24136
lurette.mli,31
lurette.mli,97
Lurette1,0
val mainmain2,1
val var_decl_are_inconsistentvar_decl_are_inconsistent12,199
val mainmain20,415
lurette.ml,33
lurette.ml,435
Lurette1,0
let (mainmain6,33
let rec (rmrm16,420
let rec (list_is_includedlist_is_included25,666
let (list_are_equalslist_are_equals37,947
let print_var_listprint_var_list51,1351
let (var_decl_are_inconsistentvar_decl_are_inconsistent54,1457
let (read_var_namesread_var_names97,2888
let arg_nbarg_nb121,3543
let rec (mainmain124,3583
(read_list_of_autread_list_of_aut130,3774
(main2main2141,4225
main_loopmain_loop170,5052
This diff is collapsed.
......@@ -31,11 +31,15 @@ d'une variable locale ...
*)
open Graph
open Lurette_stub
(* Ces types doivent ils etre visibles ici ??? *)
type var_name_and_type
type var_type = string
type var_name = string
type var_name_and_type = var_name * var_type
type date
type formula_eps
type formula
......@@ -44,15 +48,16 @@ type weigth = int
type node = int
type arc = node * node
type arc_info = weigth * formula_eps
type memory_elt
type subst
type env_in = subst list
type env_out = subst list
type env_in = sut_out
type env_out = sut_in
type env_loc = subst list
type env_stateT = {
mutable current_node : node;
mutable current_nodes : node list;
mutable graph : (node, arc_info) Graph.t ;
(*
......@@ -71,34 +76,34 @@ val read_env_state : string ->
* var_name_and_type list (* Environment output variable names and types *)
* var_name_and_type list (* Environment local variable names and types *)
(*
** [read_env_state file] initializes the global variable `env_state'
** using the content of file `file'. Also returns the lists
** [read_env_state file] updates the global variable `env_state'
** using the content of file `file'. Also returns the new lists
** of input, output, and local variable names and types.
*)
val env__try : int -> env_in -> (node * env_out * env_loc) list
val env_try : int -> sut_out -> (node list * sut_in * env_loc) list
(*
** [env__try n input] returns a list of `n' possible outputs of the environment
** [env_try n input] returns a list of `n' possible outputs of the environment
** with input `input'. This function actually returns a list of 3-tuple
** `node * env_out * env_loc' because we need to know which arcs produced which
** outputs later (namely, when performing `env__step').
** `node list * env_out * env_loc' because we need to know which arcs produced
** which outputs later (namely, when performing `env_step').
**
** Also sets (side effect) the environment input values to `input'.
*)
val env__step : node -> env_out -> env_loc -> unit
val env_step : node list -> sut_in -> env_loc -> unit
(*
** [env__step node_to output local ] modifies the
** [env_step node_to output local ] modifies the
** environment state by:
** 1 - performing a transition from the current_node to `node_to'
** 2 - updating the memory (using `output' and `local').
*)
val generate_env_graph: arc -> string -> unit
val generate_env_graph: arc list -> string -> unit
(*
** [generate_graph arc file_name] generates in `file_name.dot'
** [generate_graph arcs file_name] generates in `file_name.dot'
** a dot version of the automata describing the current environment
** It also outputs in `file_name.ps' a post-script version of it;
** `arc' and `node' are colored in red.
......
OCAMLMAKEFILE = ../OcamlMakefile
SOURCES = generate_lurette_interface.ml
SOURCES = gen_stubs.ml
RESULT = gen_stubs
LIBS = str
......
generate_lurette_interface.ml,572
Generate_lurette_interface1,0
type file_namefile_name36,1362
type module_namemodule_name37,1386
type var_typevar_type38,1412
type var_namevar_name39,1435
type input_varsinput_vars41,1459
type output_varsoutput_vars42,1505
type pragmaspragmas44,1552
let lexerlexer52,1662
type tokentoken54,1727
(parse_pragmasparse_pragmas58,1774
(parse_module_nameparse_module_name71,2131
(parse_module_name_moreparse_module_name_more82,2412
(parse_varsparse_vars98,2710
let (read_pragma_in_c_fileread_pragma_in_c_file119,3192
let (mainmain155,3850
gen_stubs.ml,1477
Gen_stubs1,0
type filefile41,1592
type module_namemodule_name42,1611
type var_namevar_name44,1638
type c_typec_type45,1661
type ml_typeml_type46,1682
type fresh_var_namefresh_var_name47,1704
type vn_ctvn_ct49,1734
type vn_ct_mlt_fvnvn_ct_mlt_fvn50,1765
type aliasalias52,1832
let (readfilereadfile61,2055
let rec (list_map3list_map377,2566
let rec (list_map4list_map487,2917
let reg_typedefreg_typedef104,3549
let reg_blankreg_blank105,3590
let reg_semicolreg_semicol106,3622
(get_typedef_aliasget_typedef_alias109,3666
(find_typedef_listfind_typedef_list119,3968
(find_next_typedeffind_next_typedef126,4198
let reg_MODreg_MOD139,4867
let reg_INreg_IN140,4906
let reg_OUTreg_OUT141,4940
let reg_crreg_cr142,4976
let rec (get_vn_and_ct_listget_vn_and_ct_list144,5007
(find_module_namefind_module_name179,6405
(find_var_listfind_var_list199,7382
let (replace_ct_by_their_aliasreplace_ct_by_their_alias216,8212
type resres229,8697
type res = OkOk229,8697
type res = Ok | ErrorError229,8697
let (check_var_typecheck_var_type231,8730
let (generate_stub_cgenerate_stub_c277,10042
type sut_or_oraclesut_or_oracle372,12893
let (generate_idlgenerate_idl374,12922
let rec (generate_n_var_namesgenerate_n_var_names433,14529
let (get_ml_typeget_ml_type447,14947
let (generate_lurette_stub_filegenerate_lurette_stub_file547,18611
let main2main2756,26235
let usageusage822,28692
let (mainmain827,28889
This diff is collapsed.
(*-----------------------------------------------------------------------
** Copyright (C) 2001 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: generate_lurette_interface.ml
** Main author: jahier@imag.fr
**
**
** Implements a program that takes as input the string "sut"
** (resp. "oracle") as well as a C header file `<foo>.h' to interface,
** and which outputs stub files named `lurette_sut.h' and
** `lurette_sut.c' (resp. `lurette_oracle.h' and `lurette_oracle.c').
** Those files are used by the lurette Makefile to interface the sut
** (resp. the oracle).
**
** Note that <foo>.h should follows the poc convention (e.g., generated
** by a lustre compiler) Namely, it should contain the following pragmas:
**
** //MODULE: <module name> n m
** // where `n' is the input var number, and `m' the output var one
** //IN: <C type of the first input var> <a C identifier for the first input var>
** .
** .
** .
** //IN: <C type of the nth input var> <a C identifier for the nth input var>
** //OUT: <C type of the first output var> <a C identifier for the first output var>
** .
** .
** .
** //OUT: <C type of the mth output var> <a C identifier for the mth output var>
*)
(****************************************************************************)
(****************************************************************************)
type file_name = string
type module_name = string
type var_type = string
type var_name = string
type input_vars = (var_type * var_name) list
type output_vars = (var_type * var_name) list
type pragmas = module_name * input_vars * output_vars
type typedef_alias = (string * string) list
(****************************************************************************)
(****************************************************************************)
(* XXX to put in util.ml *)
let (readfile: string -> string) =
(*
** [readfile file] outputs the whole contents of the file `file' in a
** string.
*)
let rec (readfile_ic : in_channel -> string -> string) =
fun ic acc ->
let line = try (input_line ic) with End_of_file -> (close_in ic) ; "end_of_file" in
if (line = "end_of_file") then acc else (readfile_ic ic (acc ^ "\n" ^ line))
in
fun file -> readfile_ic (open_in file) ""
(****************************************************************************)
(****************************************************************************)
let reg_typedef = Str.regexp "^typedef"
let reg_blank = Str.regexp " "
let reg_semicol = Str.regexp ";"
let rec
(read_typedef: file_name -> typedef_alias) =
(*
** [read_typedef file] reads `file' and search for typedef C expressions
** and returns the list of (alias_type, C_type) found in `file'.
*)
fun file ->
let str = readfile file in
find_typedef_list str 0 []
and
(find_typedef_list: string -> int -> typedef_alias -> typedef_alias) =
fun str sptr list ->
try
let (alias, sptr1) = find_next_typedef str sptr in
find_typedef_list str sptr1 (alias::list)
with Not_found -> list
and
(find_next_typedef: string -> int -> ((string * string) * int)) =
fun str sptr ->
let sptr1 = Str.search_forward reg_typedef str sptr in
let sptr2 = Str.search_forward reg_blank str (sptr1+1) in
let sptr3 = Str.search_forward reg_blank str (sptr2+1) in
let sptr4 = Str.search_forward reg_semicol str (sptr3+1) in
let c_type = String.sub str (sptr2 + 1) (sptr3 - sptr2 - 1) in
let alias_type = String.sub str (sptr3 + 1) (sptr4 - sptr3 - 1) in
((alias_type, c_type), sptr4)
(****************************************************************************)
(****************************************************************************)
let reg_MOD = Str.regexp "^//MODULE:"
let reg_IN = Str.regexp "^//IN:"
let reg_OUT = Str.regexp "^//OUT:"
(* let reg_ident = Str.regexp "[a-z\|A-Z\|_][a-z\|A-Z\|_\|0-9]*" *)
(* let reg_int = Str.regexp "[0-9]+" *)
let reg_cr = Str.regexp "\n"
let rec (read_pragma_in_c_file: file_name -> module_name * input_vars * output_vars) =
(*
** Parsing the pragmas in C files.
*)
fun file ->
let str = readfile file in
let (mod_name, ni, no, str_ptr1) = find_module_name str in
let (vi, str_ptr2) = find_var_list reg_IN str str_ptr1 [] in
let (vo, _) = find_var_list reg_OUT str str_ptr2 [] in
if (List.length vi = ni && List.length vo = no) then
(mod_name, vi, vo)
else
failwith ("Inconsistent pragmas found in `" ^ file ^
"'. The number of variables is wrong: " ^
(string_of_int ni) ^ " and " ^ (string_of_int no) ^
" were declared whereas " ^ (string_of_int (List.length vi)) ^
" and " ^ (string_of_int (List.length vo)) ^ " were counted")
and
(find_module_name: string -> module_name * int * int * int) =
fun str ->
let beg = Str.search_forward reg_MOD str 0 in
let mod_name_beg = Str.search_forward reg_blank str beg in
let mod_name_end = Str.search_forward reg_blank str (mod_name_beg+1) in
let mod_name = String.sub str (mod_name_beg+1) (mod_name_end - mod_name_beg - 1) in
let vi_nb_end = Str.search_forward reg_blank str (mod_name_end+1) in
let vi_nb_str = String.sub str (mod_name_end+1) (vi_nb_end - mod_name_end - 1) in
let vi_nb =
try (int_of_string vi_nb_str)
with _ -> failwith ("*** `" ^ vi_nb_str ^ "'is not an int")
in
let vo_nb_end = Str.search_forward reg_cr str (vi_nb_end + 1) in
let vo_nb_str = String.sub str (vi_nb_end+1) (vo_nb_end - vi_nb_end - 1) in
let vo_nb =
try(int_of_string vo_nb_str)
with _ -> failwith ("*** `" ^ vo_nb_str ^ "'is not an int")