Skip to content

GitLab

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

lurette 0.17 Mon, 03 Dec 2001 17:54:50 +0100 by jahier 

Parent-Version:      0.16
Version-Log:

Plug sim2cro to the lurette outputs.

Project-Description: Lurette
parent 6d26066c
Hide whitespace changes
Inline Side-by-side
.lurette.prcs_aux
View file @ a330ffbb
......@@ -8,14 +8,14 @@
(source/util.ml 3175 1007379917 35_util.ml 1.2)
(source/wtree.ml 9181 1007379917 b/1_wtree.ml 1.1)
(source/solver.ml 1841 1007379917 39_solver.ml 1.1)
(source/lurette.ml 6270 1007379917 12_lurette.ml 1.9)
(source/lurette.ml 7890 1007398490 12_lurette.ml 1.10)
(source/solver.mli 617 1007379917 38_solver.mli 1.1)
(source/env.mli 2838 1007379917 15_env.mli 1.5)
(test/vrai.lus 65 1006182545 28_vrai.lus 1.1)
(lurette.depfull.dot 1146 1007379917 b/5_lurette.de 1.1)
(test/tram_env_tramway.env 1207 1007379917 b/10_tram_env_t 1.1)
(source/env.ml 7966 1007379917 16_env.ml 1.8)
(make_lurette 1008 1007379917 27_make_luret 1.4)
(make_lurette 1027 1007398490 27_make_luret 1.5)
(test/vrai_tram.lus 453 1007379917 b/6_vrai_tram. 1.1)
(test/edge.c 1693 1006263320 32_edge.c 1.1)
(lurette.dep.dot 485 1007379917 b/4_lurette.de 1.1)
......@@ -25,7 +25,7 @@
(test/edge.h 1052 1006263320 33_edge.h 1.1)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/eval.ml 6238 1007379917 49_eval.ml 1.1)
(source/gen_stubs.ml 31593 1007379917 24_generate_l 1.9)
(source/gen_stubs.ml 31830 1007398490 24_generate_l 1.10)
(source/parse_env.ml 6007 1007379917 41_parse_env. 1.1)
(interface/TAGS 1956 1007380262 26_TAGS 1.3)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
......@@ -50,6 +50,6 @@
(source/graph.mli 1305 1003932490 13_graph.mli 1.2)
(source/formula.ml 3404 1007379917 45_formula.ml 1.1)
(test/vrai.c 1405 1006183551 30_vrai.c 1.1)
(source/lurette.mli 38 1007379917 11_lurette.ml 1.6)
(source/lurette.mli 371 1007398490 11_lurette.ml 1.7)
(source/print.ml 1098 1007379917 47_print.ml 1.1)
(test/vrai_tram.h 2293 1007379917 b/7_vrai_tram. 1.1)
lurette.prj
View file @ a330ffbb
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 16)
(Parent-Version lurette 0 15)
(Project-Version lurette 0 17)
(Parent-Version lurette 0 16)
(Version-Log "
Fix a problem in Ocamlmake")
Plug sim2cro to the lurette outputs.
")
(New-Version-Log "")
(Checkin-Time "Mon, 03 Dec 2001 13:07:25 +0100")
(Checkin-Time "Mon, 03 Dec 2001 17:54:50 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -17,8 +18,8 @@ Fix a problem in Ocamlmake")
;; Sources files
(source/lurette.mli (lurette/11_lurette.ml 1.6 644))
(source/lurette.ml (lurette/12_lurette.ml 1.9 644))
(source/lurette.mli (lurette/11_lurette.ml 1.7 644))
(source/lurette.ml (lurette/12_lurette.ml 1.10 644))
(source/graph.mli (lurette/13_graph.mli 1.2 644))
(source/graph.ml (lurette/14_graph.ml 1.2 644))
......@@ -52,14 +53,14 @@ Fix a problem in Ocamlmake")
(source/wtree.mli (lurette/b/0_wtree.mli 1.1 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.1 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.9 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.10 644))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.4 644))
(Makefile (lurette/18_Makefile 1.9 644))
(test/Makefile (../Makefile) :symlink)
(interface/Makefile (lurette/25_Makefile 1.5 644))
(make_lurette (lurette/27_make_luret 1.4 744))
(make_lurette (lurette/27_make_luret 1.5 744))
;; Documentation
......
make_lurette
View file @ a330ffbb
......@@ -23,7 +23,7 @@ case $# in
############################
echo "... Generating the stub files: gen_stubs $1 $2"
./interface/gen_stubs $1 $2
/home/jahier/lurette/interface/gen_stubs $1 $2
############################
echo "... generates the lurette.in file (which is included in the Makefile) "
......
source/gen_stubs.ml
View file @ a330ffbb
......@@ -602,10 +602,13 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
*)
fun mlt fvn ->
match mlt with
"int" -> put " print_int "; put fvn ; put "; print_string \" \""
| "bool" -> put " print_bool "; put fvn ; put "; print_string \" \""
| "float" -> put " print_float "; put fvn ; put "; print_string \" \""
| _ -> put "print_string \"***\";\n" ;
"int" -> put " output_string oc (string_of_int " ;
put fvn ; put "); output_string oc \" \""
| "bool" -> put " output_string oc (my_string_of_bool ";
put fvn ; put "); output_string oc \" \""
| "float" -> put " output_string oc (string_of_float ";
put fvn ; put "); output_string oc \" \""
| _ -> put "output_string \"***\";\n" ;
in
let vnl_in = List.map (fun (w,x,y,z) -> w) sut_in in
let vn_ctl_in = List.map (fun (w,x,y,z) -> (w,x)) sut_in in
......@@ -817,25 +820,27 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
(*
** Defines print_sut_in and print_sut_out.
*)
put "let (print_sut_in: sut_in -> unit) =\n" ;
put "let my_string_of_bool = function true -> \"t\" | false -> \"f\" \n\n" ;
put "let (print_sut_in: sut_in -> out_channel -> unit) =\n" ;
put " fun (" ;
put (format_string_list ", " fvnl_in) ;
put ") -> \n" ;
put ") oc -> \n" ;
List.iter2
(fun x y -> put_printer x y; put ";\n")
mltl_in
fvnl_in ;
put " flush stdout\n\n" ;
put " flush oc\n\n" ;
put "let (print_sut_out: sut_out -> unit) =\n" ;
put "let (print_sut_out: sut_out -> out_channel -> unit) =\n" ;
put " fun (" ;
put (format_string_list ", " fvnl_out) ;
put ") -> \n" ;
put ") oc -> \n" ;
List.iter2
(fun x y -> put_printer x y; put ";\n")
mltl_out
fvnl_out ;
put " flush stdout\n\n" ;
put " flush oc\n\n" ;
close_out oc
......
source/lurette.ml
View file @ a330ffbb
......@@ -3,7 +3,7 @@
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: lurette.ml
** Main author: jahier@imag.fr
*)
......@@ -17,6 +17,7 @@ open Show_env
open Formula
open Env_state
open List
open Lurette_stub
(*
** [var_decl_are_inconsistent out_env in_sut out_sut] checks the consistency
......@@ -90,6 +91,59 @@ let (read_var_names: string -> vnt list * vnt list) =
(i, o)
(*------------------------------------------------------------------------*)
(*
** To put the values of sut inputs and outputs in a rif file to display
** them using sim2cro.
*)
let (put_var_decl: out_channel -> unit) =
fun rif ->
let put s = output_string rif s in
let put_vt = function
boolean -> put "bool"
| any -> put any
in
let put_vntl = (fun (vn,vt) -> put vn; put ":"; put_vt vt; put "\n") in
let c_type_to_sim2cro_type =
List.map
(fun (vn,vt) ->
let vt2 = match vt with
"true" -> "t"
| "false" -> "f"
| otherwise -> otherwise
in
(vn, vt2)
)
in
put "#program lurette\n"; (* XXX *)
put "#@inputs\n";
List.iter put_vntl Lurette_stub.sut_input_var_name_and_type_list;
put "@#\n#@outputs\n";
List.iter put_vntl Lurette_stub.sut_output_var_name_and_type_list;
put "@#\n"
(* XXX put local vars too ??? *)
let (put_current_step_values: out_channel -> int -> sut_in -> sut_out -> env_loc
-> unit) =
fun rif t input output local ->
let put s = output_string rif s in
put "#step ";
put (string_of_int t);
put "\n";
Lurette_stub.print_sut_in input rif;
put "#outs ";
Lurette_stub.print_sut_out output rif;
put "\n"
(*------------------------------------------------------------------------*)
......@@ -111,6 +165,9 @@ let usage =
"\n`env1', `env2', and `env3' as a product, and `env4' in parallel.\n\n ")
let step_by_step = false
(* XXX set this via an option at command the line !!! *)
let rec (main : unit -> 'a) =
fun _ ->
if (arg_nb < 5) then print_string usage
......@@ -118,9 +175,14 @@ let rec (main : unit -> 'a) =
let s = int_of_string Sys.argv.(1) in
let n = int_of_string Sys.argv.(2) in
let p = int_of_string Sys.argv.(3) in
(* try *)
main2 s n p
(* with Failure(err_msg) -> (print_string err_msg) *)
let res = main2 s n p in
let _ =
if not step_by_step then
Sys.command "sim2chro -ecran -in lurette.rif > /dev/null &"
else 0
in
res
and
(get_env_from_args: int -> string list list -> string list list) =
(*
......@@ -146,23 +208,30 @@ and
fun s n p ->
(* initialises `Env_state.env_state' *)
let () = read_env_state (get_env_from_args (arg_nb-1) []) in
Random.self_init ();
let rif = open_out "lurette.rif" in
var_decl_are_inconsistent sut_input_var_name_and_type_list
sut_output_var_name_and_type_list;
generate_env_graph [] "environment" ;
(* gv ("environment.ps"); *)
if step_by_step then
(
generate_env_graph [] "environment" ;
gv ("environment.ps");
put_var_decl stdout ;
)
else
put_var_decl rif ;
Sut_idl_stub.sut_init ();
Oracle_idl_stub.oracle_init ();
main_loop s n p sut_out_init ;
main_loop 1 s n p rif sut_out_init ;
close_out rif;
and
main_loop s n p output =
main_loop t s n p rif output =
(*
** Generates `n*p' inputs from the environment
*)
......@@ -210,18 +279,26 @@ and
env_step arcs input loc ;
sut_step input ;
oracle_step (input, output) ;
generate_env_graph [] "environment" ;
print_string "\nsut input: ";
print_sut_in input;
print_string "\nsut output: ";
print_sut_out output;
flush stdout ;
(* print_string "\nenvironment local vars: "; *)
(* print_subst_list loc ; *)
print_string "\nOne more loop ? [type any char to stop, `CR' to continue]\n";
let str = read_line () in
if (str = "") then main_loop s n p new_output else ();
(*
**
*)
let str =
if (step_by_step) then
(
generate_env_graph [] "environment" ;
put_current_step_values stdout t input output loc ;
print_string "\nOne more loop ? [type any char to stop, `CR' to continue]\n";
read_line ()
)
else
(
put_current_step_values rif t input output loc ;
""
)
in
if ((str = "") && (s > t)) then main_loop (t+1) s n p rif new_output else ();
;;
......
source/lurette.mli
View file @ a330ffbb
(*-----------------------------------------------------------------------
** Copyright (C) 2001 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: lurette.mli
** Main author: jahier@imag.fr
*)
open Env
......
Supports Markdown
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