Skip to content

GitLab

Commit c3c5f045 authored by Erwan Jahier's avatar Erwan Jahier
Browse files
Options

lurette 0.38 Wed, 06 Mar 2002 10:50:34 +0100 by jahier 

Parent-Version:      0.37
Version-Log:

With this change, lurette is now able to handle numeric variables
over intervals !

Project-Description: Lurette
parent cdeda709
Hide whitespace changes
Inline Side-by-side
Showing with 574 additions and 359 deletions
.lurette.prcs_aux
View file @ c3c5f045
;; This file is automatically generated, editing may cause PRCS to do
;; REALLY bad things.
(Created-By-Prcs-Version 1 3 3)
(test/usager.env 396 1013445149 b/14_usager.env 1.2)
(test/usager.env 439 1015408234 b/14_usager.env 1.3)
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 2789 1015246213 51_env_state. 1.11)
(source/env_state.ml 2795 1015408234 51_env_state. 1.12)
(source/graph.ml 1801 1015250295 14_graph.ml 1.4)
(source/util.ml 9430 1015250295 35_util.ml 1.12)
(source/wtree.ml 9644 1014051154 b/1_wtree.ml 1.8)
(source/solver.ml 18003 1015246213 39_solver.ml 1.12)
(source/solver.ml 18273 1015408234 39_solver.ml 1.13)
(source/command_line.ml 3971 1014048376 b/20_command_li 1.3)
(source/lurette.ml 11540 1015246213 12_lurette.ml 1.23)
(source/lurette.ml 11196 1015408234 12_lurette.ml 1.24)
(source/solver.mli 1059 1015250295 38_solver.mli 1.9)
(source/env.mli 2389 1015250295 15_env.mli 1.9)
(test/heater_float.rif.exp 1577 1015408234 b/30_heater_flo 1.1)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(source/env.ml 8596 1015246213 16_env.ml 1.15)
(source/env.ml 8395 1015408234 16_env.ml 1.16)
(make_lurette 812 1013517738 27_make_luret 1.7)
(test/vrai_tram.lus 453 1007379917 b/6_vrai_tram. 1.1)
(lurette.dep.dot 49 1007651448 b/4_lurette.de 1.2)
(test/passerelle.env 862 1012914629 b/17_passerelle 1.1)
(test/passerelle.env 866 1015408234 b/17_passerelle 1.2)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/rnumsolver.ml 5159 1015246213 b/27_rnumsolver 1.1)
(source/parse_env.mli 954 1015250295 40_parse_env. 1.4)
(source/rnumsolver.ml 7434 1015408234 b/27_rnumsolver 1.2)
(source/parse_env.mli 905 1015408234 40_parse_env. 1.5)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(source/sim2chro.mli 1427 1015250295 b/23_sim2chro.m 1.3)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/eval.ml 8697 1015246213 49_eval.ml 1.7)
(source/gen_stubs.ml 32483 1015250295 24_generate_l 1.18)
(source/parse_env.ml 9616 1015246213 41_parse_env. 1.5)
(test/lurette.rif.exp 4746 1015246213 b/22_lurette.ri 1.6)
(source/eval.ml 7987 1015408234 49_eval.ml 1.8)
(source/gen_stubs.ml 33424 1015408234 24_generate_l 1.19)
(source/parse_env.ml 9431 1015408234 41_parse_env. 1.6)
(interface/TAGS 1956 1007380262 26_TAGS 1.3)
(source/sim2chro.ml 2639 1014132434 b/24_sim2chro.m 1.3)
(source/sim2chro.ml 2669 1015408234 b/24_sim2chro.m 1.4)
(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 1302 1014048376 b/21_command_li 1.3)
(TAGS 9825 1007379917 21_TAGS 1.6)
(source/wtree.mli 2931 1015250295 b/0_wtree.mli 1.6)
(test/porte.env 861 1012914629 b/16_porte.env 1.1)
(source/env_state.mli 3822 1015246213 50_env_state. 1.9)
(test/porte.env 879 1015408234 b/16_porte.env 1.2)
(source/env_state.mli 3644 1015408234 50_env_state. 1.10)
(source/rnumsolver.mli 1909 1015246213 b/26_rnumsolver 1.1)
(source/eval.mli 1645 1015250295 48_eval.mli 1.6)
(source/eval.mli 1665 1015408234 48_eval.mli 1.7)
(README 74 1011881677 10_README 1.2)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(OcamlMakefile 18580 1015250295 17_OcamlMakef 1.19)
(test/tram.env 806 1012914629 b/15_tram.env 1.1)
(OcamlMakefile 19242 1015408234 17_OcamlMakef 1.20)
(test/ControleurPorte.rif.exp 4746 1015408234 b/29_Controleur 1.1)
(test/tram.env 944 1015408234 b/15_tram.env 1.2)
(source/show_env.ml 2961 1014048376 43_show_env.m 1.3)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
(test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
......@@ -54,7 +55,8 @@
(test/vrai_tram.c 3060 1012914629 b/8_vrai_tram. 1.2)
(source/print.mli 597 1014048376 46_print.mli 1.5)
(source/graph.mli 1493 1015250295 13_graph.mli 1.6)
(source/formula.ml 4621 1015250295 45_formula.ml 1.8)
(test/heater_int.rif.exp 785 1015408234 b/28_heater_int 1.1)
(source/formula.ml 4618 1015408234 45_formula.ml 1.9)
(source/lurette.mli 433 1015250295 11_lurette.ml 1.11)
(source/print.ml 5524 1015250295 47_print.ml 1.9)
(test/vrai_tram.h 2468 1012914629 b/7_vrai_tram. 1.2)
OcamlMakefile
View file @ c3c5f045
......@@ -5,7 +5,7 @@
# For updates see:
# http://miss.wu-wien.ac.at/~mottl/ocaml_sources
#
# $Id: OcamlMakefile 1.19 Mon, 04 Mar 2002 14:58:15 +0100 jahier $
# $Id: OcamlMakefile 1.20 Wed, 06 Mar 2002 10:50:34 +0100 jahier $
#
###########################################################################
......@@ -510,7 +510,27 @@ vroum:
test:
$(LURETTE_DIR)/make_lurette ControleurPorte vrai_tram; \
./lurette 100 10 10 tram.env usager.env porte.env passerelle.env -seed 1013219512 -ns2c ;\
diff -u lurette.rif.exp lurette.rif > test.res ; cat test.res
diff -u ControleurPorte.rif.exp lurette.rif > test1.res ;\
\
$(LURETTE_DIR)/make_lurette heater_int vrai_heater; \
./lurette 30 10 10 temp_int.env --no-oracle -seed 1013219512 -ns2c ;\
diff -u heater_int.rif.exp lurette.rif > test2.res ; \
\
$(LURETTE_DIR)/make_lurette heater_float vrai_heater_float; \
./lurette 30 10 10 temp_float.env --no-oracle -seed 1013219512 -ns2c ;\
diff -u heater_float.rif.exp lurette.rif > test3.res ; \
\
cat test1.res ; cat test2.res ; cat test3.res
heater:
$(LURETTE_DIR)/make_lurette heater_int vrai_heater; \
./lurette 30 1 1 temp_int.env --no-oracle
heaterf:
$(LURETTE_DIR)/make_lurette heater_float vrai_heater_float; \
./lurette 30 1 1 temp_float.env --no-oracle
# In order to time profile lurette
gprof:
......
lurette.prj
View file @ c3c5f045
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 37)
(Parent-Version lurette 0 36)
(Version-Log "Various cosmetic changes in comments.")
(Project-Version lurette 0 38)
(Parent-Version lurette 0 37)
(Version-Log "
With this change, lurette is now able to handle numeric variables
over intervals !
")
(New-Version-Log "")
(Checkin-Time "Mon, 04 Mar 2002 14:58:15 +0100")
(Checkin-Time "Wed, 06 Mar 2002 10:50:34 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -17,53 +21,53 @@
;; Sources files
(source/lurette.mli (lurette/11_lurette.ml 1.11 644))
(source/lurette.ml (lurette/12_lurette.ml 1.23 644))
(source/lurette.ml (lurette/12_lurette.ml 1.24 644))
(source/graph.mli (lurette/13_graph.mli 1.6 644))
(source/graph.ml (lurette/14_graph.ml 1.4 644))
(source/env.mli (lurette/15_env.mli 1.9 644))
(source/env.ml (lurette/16_env.ml 1.15 644))
(source/env.ml (lurette/16_env.ml 1.16 644))
(source/util.ml (lurette/35_util.ml 1.12 644))
(source/solver.mli (lurette/38_solver.mli 1.9 644))
(source/solver.ml (lurette/39_solver.ml 1.12 644))
(source/solver.ml (lurette/39_solver.ml 1.13 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.1 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.1 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.2 644))
(source/parse_env.mli (lurette/40_parse_env. 1.4 644))
(source/parse_env.ml (lurette/41_parse_env. 1.5 644))
(source/parse_env.mli (lurette/40_parse_env. 1.5 644))
(source/parse_env.ml (lurette/41_parse_env. 1.6 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.8 644))
(source/formula.ml (lurette/45_formula.ml 1.9 644))
(source/print.mli (lurette/46_print.mli 1.5 644))
(source/print.ml (lurette/47_print.ml 1.9 644))
(source/eval.mli (lurette/48_eval.mli 1.6 644))
(source/eval.ml (lurette/49_eval.ml 1.7 644))
(source/eval.mli (lurette/48_eval.mli 1.7 644))
(source/eval.ml (lurette/49_eval.ml 1.8 644))
(source/env_state.mli (lurette/50_env_state. 1.9 644))
(source/env_state.ml (lurette/51_env_state. 1.11 644))
(source/env_state.mli (lurette/50_env_state. 1.10 644))
(source/env_state.ml (lurette/51_env_state. 1.12 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.6 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.8 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.3 644))
(source/sim2chro.ml (lurette/b/24_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.3 644))
(source/command_line.mli (lurette/b/21_command_li 1.3 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.18 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.19 644))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.19 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.20 644))
(Makefile (lurette/18_Makefile 1.21 644))
(test/Makefile (../Makefile) :symlink)
(interface/Makefile (lurette/25_Makefile 1.6 644))
......@@ -88,10 +92,10 @@
;; Various files used for testing purposes
(test/usager.env (lurette/b/14_usager.env 1.2 644))
(test/tram.env (lurette/b/15_tram.env 1.1 644))
(test/porte.env (lurette/b/16_porte.env 1.1 644))
(test/passerelle.env (lurette/b/17_passerelle 1.1 644))
(test/usager.env (lurette/b/14_usager.env 1.3 644))
(test/tram.env (lurette/b/15_tram.env 1.2 644))
(test/porte.env (lurette/b/16_porte.env 1.2 644))
(test/passerelle.env (lurette/b/17_passerelle 1.2 644))
(test/ControleurPorte.h (lurette/b/18_Controleur 1.1 644))
(test/ControleurPorte.c (lurette/b/19_Controleur 1.1 644))
......@@ -101,7 +105,9 @@
(test/vrai_tram.c (lurette/b/8_vrai_tram. 1.2 644))
(test/tram_simple.h (lurette/b/25_tram_simpl 1.1 644))
(test/lurette.rif.exp (lurette/b/22_lurette.ri 1.6 644))
(test/heater_int.rif.exp (lurette/b/28_heater_int 1.1 644))
(test/ControleurPorte.rif.exp (lurette/b/29_Controleur 1.1 644))
(test/heater_float.rif.exp (lurette/b/30_heater_flo 1.1 644))
)
......
source/env.ml
View file @ c3c5f045
......@@ -29,7 +29,7 @@ let (read_env_state_one_file : string -> node) =
let
(* Reads the content of [file]. *)
Parse_env.Automata(init_node, list_in, list_out, list_loc,
list_pre_expr, list_pre_form, list_arcs) =
list_pre, list_arcs) =
try
Parse_env.parse_automata(
Parse_env.lexer(Stream.of_channel (open_in file)))
......@@ -38,6 +38,7 @@ let (read_env_state_one_file : string -> node) =
flush stdout;
raise e
in
let (list_pre_vn, _) = List.split list_pre in
(* Sets the [graph] field of [env_state]. *)
let node_nb = (List.length (Graph.get_all_nodes env_state.graph)) in
......@@ -53,7 +54,7 @@ let (read_env_state_one_file : string -> node) =
(node_to+node_nb))
in
List.iter (add_arc) list_arcs ;
(* Sets the [node_to_file_name] field of [env_state]. *)
List.iter
(fun node ->
......@@ -63,15 +64,12 @@ let (read_env_state_one_file : string -> node) =
)
(Graph.get_all_nodes env_state.graph);
(* Sets the [var_names], [pre_expr], and [pre_form] fields
of [env_state]. *)
(* Sets the [var_names] and [pre_var_names] fields of [env_state]. *)
Hashtbl.add env_state.var_names file (list_in, list_out, list_loc) ;
env_state.pre_expr <-
(Util.sort_list_string_pair
(List.append list_pre_expr env_state.pre_expr)) ;
env_state.pre_form <-
(Util.sort_list_string_pair
(List.append list_pre_form env_state.pre_form)) ;
List.iter
(fun vn -> env_state.pre_var_names <- (vn::env_state.pre_var_names))
list_pre_vn;
(init_node + node_nb)
......@@ -232,7 +230,6 @@ let _ = assert (
let (env_try: int -> int -> env_in ->
(node list list * env_out * env_loc) list) =
fun n p input ->
let _ = Eval.update_pre env_state.input in
let cn_ll = env_state.current_nodes
and ft = env_state.formula_table
and wtt = env_state.wtree_table
......@@ -263,7 +260,7 @@ let (env_step : node list list -> env_out -> env_loc -> unit) =
fun nodes_to output local ->
env_state.current_nodes <- nodes_to ;
env_state.output <- output ;
env_state.local <- List.append local env_state.local
env_state.local <- local
......
source/env_state.ml
View file @ c3c5f045
......@@ -23,6 +23,7 @@ open Wtree
type env_stateT = {
(* var names and types given file by file *)
mutable var_names: (string, (vnt list * vnt list * vnt list)) Hashtbl.t;
mutable pre_var_names: var_name list;
mutable output_var_names: vnt list;
mutable node_to_file_name: (int, string) Hashtbl.t;
mutable atomic_formula_to_index: ((formula, int) Hashtbl.t);
......@@ -30,12 +31,11 @@ type env_stateT = {
mutable index_cpt: int;
mutable bdd_tbl: (formula, Bdd.t) Hashtbl.t;
mutable snt: (Bdd.t, Util.sol_nb * Util.sol_nb) Hashtbl.t;
mutable pre_expr: vne list;
mutable pre_form: vnf list;
mutable current_nodes: node list list;
mutable graph: (node, arc_info) Graph.t ;
mutable formula_table: Wtree.formula_table ;
mutable wtree_table: Wtree.wtree_table ;
mutable pre: subst list;
mutable input : env_in ;
mutable output: env_out ;
mutable local : env_loc
......@@ -45,6 +45,7 @@ type env_stateT = {
let (env_state:env_stateT) = {
var_names = Hashtbl.create 0 ;
pre_var_names = [];
output_var_names = [];
node_to_file_name = Hashtbl.create 0 ;
atomic_formula_to_index = Hashtbl.create 0 ;
......@@ -52,12 +53,11 @@ let (env_state:env_stateT) = {
index_cpt = 0 ;
bdd_tbl = Hashtbl.create 0;
snt = Hashtbl.create 3;
pre_expr = [] ;
pre_form = [] ;
current_nodes = [];
graph = Graph.create () ;
formula_table = Hashtbl.create 0 ;
wtree_table = Hashtbl.create 0 ;
pre = [] ;
input = Hashtbl.create 0 ;
output = [] ;
local = []
......
source/env_state.mli
View file @ c3c5f045
......@@ -22,6 +22,8 @@ type env_stateT = {
(** Var names and types ([vnt]) of input, output, and local vars,
given module by module. *)
mutable pre_var_names: var_name list;
mutable output_var_names: vnt list;
(** Output var names and types. *)
......@@ -55,14 +57,6 @@ type env_stateT = {
contained in its lhs (then) and rhs (else) branches. Note that
adding those two numbers only give a number of solution that is
relative to which bdd points to it. *)
mutable pre_expr: vne list;
(** In the [.aut] format, expressions under a pre are represented
by a variable name. The correspondance between those variable
names and expressions are given apart; We store this mapping in
this field. *)
mutable pre_form: vnf list;
(** Ditto for formula. *)
mutable current_nodes : node list list;
(** List of the automata node. Nodes belonging to automata that
......@@ -76,6 +70,8 @@ type env_stateT = {
mutable wtree_table : Wtree.wtree_table ;
(** Mapping from nodes to [wtree] (see the doc of the [Wtree] module). *)
mutable pre: subst list;
(** Used to store the values of variables ``under a pre''. *)
mutable input : env_in ;
(** Used to store the values of input vars. *)
mutable output: env_out ;
......
source/eval.ml
View file @ c3c5f045
......@@ -17,17 +17,12 @@ open Wtree
let (lookup: env_in -> var_name -> atomic_expr option) =
fun env_in_tbl v ->
try Some(Hashtbl.find env_in_tbl v)
with Not_found -> None
let (lookup_loc: var_name -> atomic_expr option) =
fun v ->
try
let v = List.assoc v env_state.local in
Some(v)
with Not_found -> None
let (lookup: env_in -> subst list -> var_name -> atomic_expr option) =
fun input pre vn ->
try Some(Hashtbl.find input vn)
with Not_found ->
try Some(List.assoc vn pre)
with Not_found -> None
(****************************************************************************)
......@@ -72,21 +67,13 @@ let rec (eval : formula -> env_in -> formula) =
| False -> False
| Bvar(str) ->
( match (lookup input str) with
( match (lookup input env_state.pre str) with
Some(Bool(bool)) ->
if bool then True else False
| Some(_) ->
print_string (str ^ " is not a boolean!\n");
assert false
| None ->
(match (lookup_loc str) with
Some(Bool(bool)) ->
if bool then True else False
| Some(_) ->
print_string (str ^ " is not a boolean!\n");
assert false
| None -> Bvar(str)
)
| None -> Bvar(str)
)
| Eq(e1, e2) ->
(
......@@ -200,23 +187,14 @@ and
| _ -> Mod(ee1, ee2)
)
| Nvar(str) ->
( match (lookup input str) with
( match (lookup input env_state.pre str) with
Some(Int(i)) -> Ival(i)
| Some(Float(f)) -> Fval(f)
| Some(Bool(f)) ->
print_string ((string_of_bool f)
^ "is a bool, not an int nor of float!\n");
^ "is a bool, not an int nor a float!\n");
assert false
| None ->
( match (lookup_loc str) with
Some(Int(i)) -> Ival(i)
| Some(Float(f)) -> Fval(f)
| Some(Bool(f)) ->
print_string ((string_of_bool f)
^ "is a bool, not an int nor of float!\n");
assert false
| None -> Nvar(str)
)
| None -> Nvar(str)
)
| Ival(i) -> Ival(i)
| Fval(f) -> Fval(f)
......@@ -262,44 +240,35 @@ and
(****************************************************************************)
(* exported *)
let (expr_to_atomic: expr -> atomic_expr) = function
(*
** translates expressions into atomic expressions if possible,
** fails otherwise
*)
Ival(i) -> Int(i)
| Fval(f) -> Float(f)
| _ -> assert false
(* exported *)
let (formula_to_atomic: formula -> atomic_expr) = function
(*
** translates formula into atomic expressions if possible,
** fails otherwise
*)
True -> Bool(true)
| False -> Bool(false)
| _ -> assert false
let (update_pre: env_in -> unit) =
fun input ->
(*
** Computes the values of pre expressions and formula (i.e., updates
** env_state.local).
*)
let new_local0 =
List.fold_left
(fun acc (vn, (e, _)) ->
(vn, (expr_to_atomic (eval_expr e input)))::acc)
[]
env_state.pre_expr ;
in
let new_local =
List.fold_left
(fun acc (vn, (f, _)) ->
(vn, (formula_to_atomic (eval f input)))::acc)
new_local0
env_state.pre_form ;
(* exported *)
let (update_pre: env_in -> env_out -> env_loc -> unit) =
fun input output local ->
let (update_one_pre_var : var_name -> subst) =
fun pre_vn ->
let vn = String.sub pre_vn 4 ((String.length pre_vn) -4) in
let pre_value =
try Hashtbl.find input vn
with Not_found ->
try List.assoc vn output
with Not_found ->
try List.assoc vn local
with Not_found -> assert false
in
(pre_vn, pre_value)
in
env_state.local <- new_local
env_state.pre <- List.map (update_one_pre_var) env_state.pre_var_names
source/eval.mli
View file @ c3c5f045
......@@ -31,9 +31,9 @@ val eval_wtree_list : env_in -> wtree list -> node list list
corresponding to the trees in [wtl] (necessary to get formula
associated to pair of nodes from [env_state.formula_table]). *)
val update_pre: env_in -> unit
val update_pre: env_in -> env_out -> env_loc -> unit
(** Computes the values of pre expressions and formula (i.e.,
updates [env_state.local]). *)
updates [env_state.pre]). *)
val expr_to_atomic: expr -> atomic_expr
......
source/formula.ml
View file @ c3c5f045
......@@ -126,7 +126,7 @@ let (arc_info_to_string : arc_info -> string) =
let (var_type_to_string : var_type -> string) =
fun vt ->
match vt with
BoolT -> "boolean"
BoolT -> "bool"
| IntT(i1, i2) -> "int"
| FloatT(f1, f2) -> "float"
......
source/gen_stubs.ml
View file @ c3c5f045
......@@ -496,7 +496,34 @@ let (get_ml_type2: file -> vn_ct list -> vn_ct list -> vn_ct_mlt_fvn list * vn_c
** sut_in_str be the type of the sut input, and sut_in_list be the list
** of sut_try input vars (in the rigth order!).
*)
let (print_spl : (string * string) list -> unit) =
fun l ->
List.iter (fun (x,y) -> print_string ("(" ^ x ^ "," ^ y ^ ") ")) l
in
let (print_sl : string list -> unit) =
fun l ->
List.iter (fun x -> print_string (x ^ " ")) l
in
let _ =
if (List.length lin <> List.length sut_in_list)
then
(
print_string "*** \t";
print_spl lin;
print_string " does not have the same size as :\n\t";
print_sl sut_in_list;
print_string "\n\n"
);
if (List.length lout <> List.length sut_out_list)
then
(
print_string "*** \t";
print_spl lout;
print_string " does not have the same size as :\n\t";
print_sl sut_out_list;
print_string "\n\n"
);
in
(
(Util.list_map3
(fun (vn, ct) mlt fvn -> (vn, ct, mlt, fvn))
......@@ -596,11 +623,13 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
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
let vn_mltl_in = List.map (fun (w,x,y,z) -> (w,y)) sut_in in
let mltl_in = List.map (fun (w,x,y,z) -> y) sut_in in
let fvnl_in = List.map (fun (w,x,y,z) -> z) sut_in in
let vnl_out = List.map (fun (w,x,y,z) -> w) sut_out in
let vn_ctl_out = List.map (fun (w,x,y,z) -> (w,x)) sut_out in
let vn_mltl_out = List.map (fun (w,x,y,z) -> (w,y)) sut_out in
let mltl_out = List.map (fun (w,x,y,z) -> y) sut_out in
let fvnl_out = List.map (fun (w,x,y,z) -> z) sut_out in
......@@ -808,19 +837,19 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
put " consistent with the ones of the sut and the oracle. \n *) \n\n";
put "let sut_input_var_name_and_type_list = [" ;
( match (List.hd vn_ctl_in) with
( match (List.hd vn_mltl_in) with
(vn, t) -> put ("(\"" ^ vn ^ "\", \"" ^ t ^ "\")") );
List.iter
(fun (vn, t) -> put ("; \n\t (\"" ^ vn ^ "\", \"" ^ t ^ "\") "))
(List.tl vn_ctl_in) ;
(List.tl vn_mltl_in) ;
put "]\n\n" ;
put "let sut_output_var_name_and_type_list = [" ;
( match (List.hd vn_ctl_out) with
( match (List.hd vn_mltl_out) with
(vn, t) -> put ("(\"" ^ vn ^ "\", \"" ^ t ^ "\")")) ;
List.iter
(fun (vn, t) -> put ("; \n\t (\"" ^ vn ^ "\", \"" ^ t ^ "\") "))
(List.tl vn_ctl_out) ;
(List.tl vn_mltl_out) ;
put "]\n\n" ;
......@@ -846,13 +875,13 @@ let (replace_bool_representation: alias list -> alias list) =
("_boolean", "boolean")::(List.remove_assoc "_boolean" ta)
let update_stub new_stub old_stub =
let update_file new_stub old_stub =
(* Replace old_stub by new_stub iff they are different *)
if
not ((Sys.file_exists old_stub)) ||
((Util.readfile old_stub) <> (Util.readfile new_stub))
then
if ((Sys.command ("cp " ^ new_stub ^ " " ^ old_stub)) <> 0)
if ((Sys.command ("mv " ^ new_stub ^ " " ^ old_stub)) <> 0)
then assert false
else print_string ("... " ^ old_stub ^ " successfully created.\n")
......@@ -898,14 +927,16 @@ let main2 sut oracle =
generate_idl oracle_m "oracle" oracle_vi_ord oracle_vo ;
(* Update the stubs iff they have changed to avoid unnecessary re-compilations *)
update_stub "sut_idl_stub.idl.new" "sut_idl_stub.idl" ;
update_stub "sut_stub.c.new" "sut_stub.c" ;
update_file "sut_idl_stub.idl.new" "sut_idl_stub.idl" ;
update_file "sut_stub.c.new" "sut_stub.c" ;
update_stub "oracle_idl_stub.idl.new" "oracle_idl_stub.idl" ;
update_stub "oracle_stub.c.new" "oracle_stub.c" ;
update_file "oracle_idl_stub.idl.new" "oracle_idl_stub.idl" ;