Commit 8e54c847 authored by Erwan Jahier's avatar Erwan Jahier

lurette 0.26 Mon, 11 Feb 2002 17:32:29 +0100 by jahier

Parent-Version:      0.25
Version-Log:

Re-arrange the code so that lurette_stub.ml is not called by all the
modules of lurette to avoid that everything is recompiled each time a
new sut is used. To do that, lurette nows only manipulates list of
substitutuions instead of tuples (as only lurette_stub knows the size
of the tuples).

Also fix two bugs along the way:
    o wtree.ml: Random.int n draw between 0 inclusive and n *exclusive* !
    o wtree.ml: in wtree_product, make sure that I do not unsort list of nodes
    o solver.ml: in draw_in_bdd, I was tossing up the top var of the formula
      instead of tossing up the one of the support

Plus a few cosmetic change:

show_env.ml:
lurette.ml:
    prints the previous nodes in green environment.ps

lurette.ml:
    rename arcs_inputs_loc into nll_inputs_loc.

Project-Description: Lurette
parent e7fce05a
;; This file is automatically generated, editing may cause PRCS to do
;; REALLY bad things.
(Created-By-Prcs-Version 1 3 3)
(test/usager.env 392 1012914629 b/14_usager.env 1.1)
(test/usager.env 396 1013445149 b/14_usager.env 1.2)
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 2183 1012999707 51_env_state. 1.6)
(source/env_state.ml 2145 1013445149 51_env_state. 1.7)
(source/graph.ml 2476 1012914629 14_graph.ml 1.3)
(source/util.ml 4248 1011881677 35_util.ml 1.6)
(source/wtree.ml 9831 1012914629 b/1_wtree.ml 1.5)
(source/solver.ml 11388 1012999707 39_solver.ml 1.6)
(source/util.ml 4367 1013445149 35_util.ml 1.7)
(source/wtree.ml 9842 1013445149 b/1_wtree.ml 1.6)
(source/solver.ml 11461 1013445149 39_solver.ml 1.7)
(source/command_line.ml 3650 1012999707 b/20_command_li 1.1)
(source/lurette.ml 9264 1012999707 12_lurette.ml 1.15)
(source/solver.mli 971 1012914629 38_solver.mli 1.5)
(source/env.mli 2524 1008328137 15_env.mli 1.7)
(source/lurette.ml 9596 1013445149 12_lurette.ml 1.16)
(source/solver.mli 972 1013445149 38_solver.mli 1.6)
(source/env.mli 2506 1013445149 15_env.mli 1.8)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(source/env.ml 9647 1012914629 16_env.ml 1.12)
(source/env.ml 9000 1013445149 16_env.ml 1.13)
(make_lurette 1054 1012914629 27_make_luret 1.6)
(test/vrai_tram.lus 453 1007379917 b/6_vrai_tram. 1.1)
(lurette.dep.dot 49 1007651448 b/4_lurette.de 1.2)
......@@ -22,34 +22,34 @@
(source/parse_env.mli 939 1008328137 40_parse_env. 1.3)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/eval.ml 7978 1012914629 49_eval.ml 1.3)
(source/gen_stubs.ml 32098 1008255910 24_generate_l 1.13)
(source/eval.ml 7903 1013445149 49_eval.ml 1.4)
(source/gen_stubs.ml 31372 1013445149 24_generate_l 1.14)
(source/parse_env.ml 9215 1012914629 41_parse_env. 1.4)
(interface/TAGS 1956 1007380262 26_TAGS 1.3)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
(source/formula.mli 1693 1008328137 44_formula.ml 1.3)
(source/formula.mli 1870 1013445149 44_formula.ml 1.4)
(source/command_line.mli 1154 1012999707 b/21_command_li 1.1)
(TAGS 9825 1007379917 21_TAGS 1.6)
(source/wtree.mli 2860 1008328137 b/0_wtree.mli 1.3)
(source/env_state.mli 3229 1012914629 50_env_state. 1.5)
(source/wtree.mli 2860 1013445149 b/0_wtree.mli 1.4)
(source/env_state.mli 3228 1013445149 50_env_state. 1.6)
(test/porte.env 861 1012914629 b/16_porte.env 1.1)
(interface/sut_idl_stub.ml 338 1006263457 34_sut_idl_st 1.1)
(source/eval.mli 1690 1008328137 48_eval.mli 1.3)
(source/eval.mli 1668 1013445149 48_eval.mli 1.4)
(README 74 1011881677 10_README 1.2)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(OcamlMakefile 16807 1012914629 17_OcamlMakef 1.10)
(source/show_env.ml 3303 1007379917 43_show_env.m 1.1)
(OcamlMakefile 16819 1013445149 17_OcamlMakef 1.11)
(source/show_env.ml 3167 1013445149 43_show_env.m 1.2)
(test/tram.env 806 1012914629 b/15_tram.env 1.1)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
(test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
(interface/Makefile 197 1008255910 25_Makefile 1.6)
(source/show_env.mli 868 1008328137 42_show_env.m 1.2)
(Makefile 1692 1012999707 18_Makefile 1.16)
(source/show_env.mli 929 1013445149 42_show_env.m 1.3)
(Makefile 1703 1013445149 18_Makefile 1.17)
(test/vrai_tram.c 3060 1012914629 b/8_vrai_tram. 1.2)
(source/print.mli 412 1012914629 46_print.mli 1.3)
(source/print.mli 417 1013445149 46_print.mli 1.4)
(source/graph.mli 1417 1012914629 13_graph.mli 1.4)
(source/formula.ml 3118 1012914629 45_formula.ml 1.4)
(source/formula.ml 3689 1013445149 45_formula.ml 1.5)
(source/lurette.mli 396 1012914629 11_lurette.ml 1.10)
(source/print.ml 2680 1012914629 47_print.ml 1.4)
(source/print.ml 2706 1013445149 47_print.ml 1.5)
(test/vrai_tram.h 2468 1012914629 b/7_vrai_tram. 1.2)
......@@ -18,21 +18,22 @@ CLIBS = dd_caml cudd mtr st epd util
SOURCES_C = $(SUT) sut_stub.c sut_idl_stub.idl \
$(ORACLE) oracle_stub.c oracle_idl_stub.idl
SOURCES_OCAML = lurette_stub.ml \
SOURCES_OCAML = \
$(LURETTE_DIR)/source/util.ml \
$(LURETTE_DIR)/source/graph.mli $(LURETTE_DIR)/source/graph.ml \
$(LURETTE_DIR)/source/command_line.mli $(LURETTE_DIR)/source/command_line.ml \
$(LURETTE_DIR)/source/formula.mli $(LURETTE_DIR)/source/formula.ml \
$(LURETTE_DIR)/source/print.mli $(LURETTE_DIR)/source/print.ml \
$(LURETTE_DIR)/source/parse_env.mli $(LURETTE_DIR)/source/parse_env.ml \
$(LURETTE_DIR)/source/env_state.mli $(LURETTE_DIR)/source/env_state.ml \
$(LURETTE_DIR)/source/sim2chro.mli $(LURETTE_DIR)/source/sim2chro.ml \
$(LURETTE_DIR)/source/eval.mli $(LURETTE_DIR)/source/eval.ml \
$(LURETTE_DIR)/source/solver.mli $(LURETTE_DIR)/source/solver.ml \
$(LURETTE_DIR)/source/wtree.mli $(LURETTE_DIR)/source/wtree.ml \
$(LURETTE_DIR)/source/print.mli $(LURETTE_DIR)/source/print.ml \
$(LURETTE_DIR)/source/parse_env.mli $(LURETTE_DIR)/source/parse_env.ml \
$(LURETTE_DIR)/source/env.mli $(LURETTE_DIR)/source/env.ml \
$(LURETTE_DIR)/source/show_env.mli $(LURETTE_DIR)/source/show_env.ml \
$(LURETTE_DIR)/source/command_line.mli $(LURETTE_DIR)/source/command_line.ml \
$(LURETTE_DIR)/source/lurette.mli $(LURETTE_DIR)/source/lurette.ml
$(LURETTE_DIR)/source/eval.mli $(LURETTE_DIR)/source/eval.ml \
$(LURETTE_DIR)/source/sim2chro.mli $(LURETTE_DIR)/source/sim2chro.ml \
$(LURETTE_DIR)/source/env.mli $(LURETTE_DIR)/source/env.ml \
lurette_stub.ml \
$(LURETTE_DIR)/source/lurette.mli $(LURETTE_DIR)/source/lurette.ml
SOURCES = $(SOURCES_C) \
$(SOURCES_OCAML)
......
......@@ -5,7 +5,7 @@
# For updates see:
# http://miss.wu-wien.ac.at/~mottl/ocaml_sources
#
# $Id: OcamlMakefile 1.10 Tue, 05 Feb 2002 14:10:29 +0100 jahier $
# $Id: OcamlMakefile 1.11 Mon, 11 Feb 2002 17:32:29 +0100 jahier $
#
###########################################################################
......@@ -486,8 +486,8 @@ dot:
\rm $(RESULT).dep.ps $(RESULT).dep.dot ; \
touch $(RESULT).depfull.dot ; touch $(RESULT).depfull.ps ; \
\rm $(RESULT).depfull.ps $(RESULT).depfull.dot ; \
ocamldep $(SOURCES) | $(OCAMLDOT) -fullgraph -lr > $(RESULT).depfull.dot ; \
ocamldep $(SOURCES) | $(OCAMLDOT) > $(RESULT).dep.dot ; \
ocamldep $(SOURCES_OCAML) | $(OCAMLDOT) -fullgraph -lr > $(RESULT).depfull.dot ; \
ocamldep $(SOURCES_OCAML) | $(OCAMLDOT) > $(RESULT).dep.dot ; \
dot -Tps $(RESULT).depfull.dot > $(RESULT).depfull.ps ; \
dot -Tps $(RESULT).dep.dot > $(RESULT).dep.ps ; \
cp $(RESULT).dep.ps ../doc ; cp $(RESULT).depfull.ps ../doc ; popd
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 25)
(Parent-Version lurette 0 24)
(Project-Version lurette 0 26)
(Parent-Version lurette 0 25)
(Version-Log "
command_line.ml,mli: (New files)
Re-arrange the code so that lurette_stub.ml is not called by all the
modules of lurette to avoid that everything is recompiled each time a
new sut is used. To do that, lurette nows only manipulates list of
substitutuions instead of tuples (as only lurette_stub knows the size
of the tuples).
Also fix two bugs along the way:
o wtree.ml: Random.int n draw between 0 inclusive and n *exclusive* !
o wtree.ml: in wtree_product, make sure that I do not unsort list of nodes
o solver.ml: in draw_in_bdd, I was tossing up the top var of the formula
instead of tossing up the one of the support
Plus a few cosmetic change:
show_env.ml:
lurette.ml:
Handle options at the lurette command line.
Give better error messages.
prints the previous nodes in green environment.ps
lurette.ml:
rename arcs_inputs_loc into nll_inputs_loc.
")
(New-Version-Log "")
(Checkin-Time "Wed, 06 Feb 2002 13:48:27 +0100")
(Checkin-Time "Mon, 11 Feb 2002 17:32:29 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -23,48 +42,48 @@ lurette.ml:
;; Sources files
(source/lurette.mli (lurette/11_lurette.ml 1.10 644))
(source/lurette.ml (lurette/12_lurette.ml 1.15 644))
(source/lurette.ml (lurette/12_lurette.ml 1.16 644))
(source/graph.mli (lurette/13_graph.mli 1.4 644))
(source/graph.ml (lurette/14_graph.ml 1.3 644))
(source/env.mli (lurette/15_env.mli 1.7 644))
(source/env.ml (lurette/16_env.ml 1.12 644))
(source/env.mli (lurette/15_env.mli 1.8 644))
(source/env.ml (lurette/16_env.ml 1.13 644))
(source/util.ml (lurette/35_util.ml 1.6 644))
(source/util.ml (lurette/35_util.ml 1.7 644))
(source/solver.mli (lurette/38_solver.mli 1.5 644))
(source/solver.ml (lurette/39_solver.ml 1.6 644))
(source/solver.mli (lurette/38_solver.mli 1.6 644))
(source/solver.ml (lurette/39_solver.ml 1.7 644))
(source/parse_env.mli (lurette/40_parse_env. 1.3 644))
(source/parse_env.ml (lurette/41_parse_env. 1.4 644))
(source/show_env.mli (lurette/42_show_env.m 1.2 644))
(source/show_env.ml (lurette/43_show_env.m 1.1 644))
(source/show_env.mli (lurette/42_show_env.m 1.3 644))
(source/show_env.ml (lurette/43_show_env.m 1.2 644))
(source/formula.mli (lurette/44_formula.ml 1.3 644))
(source/formula.ml (lurette/45_formula.ml 1.4 644))
(source/formula.mli (lurette/44_formula.ml 1.4 644))
(source/formula.ml (lurette/45_formula.ml 1.5 644))
(source/print.mli (lurette/46_print.mli 1.3 644))
(source/print.ml (lurette/47_print.ml 1.4 644))
(source/print.mli (lurette/46_print.mli 1.4 644))
(source/print.ml (lurette/47_print.ml 1.5 644))
(source/eval.mli (lurette/48_eval.mli 1.3 644))
(source/eval.ml (lurette/49_eval.ml 1.3 644))
(source/eval.mli (lurette/48_eval.mli 1.4 644))
(source/eval.ml (lurette/49_eval.ml 1.4 644))
(source/env_state.mli (lurette/50_env_state. 1.5 644))
(source/env_state.ml (lurette/51_env_state. 1.6 644))
(source/env_state.mli (lurette/50_env_state. 1.6 644))
(source/env_state.ml (lurette/51_env_state. 1.7 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.3 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.5 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.4 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.6 644))
(source/command_line.ml (lurette/b/20_command_li 1.1 644))
(source/command_line.mli (lurette/b/21_command_li 1.1 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.13 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.14 644))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.10 644))
(Makefile (lurette/18_Makefile 1.16 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.11 644))
(Makefile (lurette/18_Makefile 1.17 644))
(test/Makefile (../Makefile) :symlink)
(interface/Makefile (lurette/25_Makefile 1.6 644))
(make_lurette (lurette/27_make_luret 1.6 744))
......@@ -90,7 +109,7 @@ lurette.ml:
(interface/sut_idl_stub.ml (lurette/34_sut_idl_st 1.1 644))
(test/usager.env (lurette/b/14_usager.env 1.1 644))
(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))
......
......@@ -12,9 +12,11 @@
open List
open Solver
open Formula
open Env_state
(****************************************************************************)
(****************************************************************************)
(* read_env_state *)
......@@ -139,29 +141,10 @@ type nl = node list
type nll = node list list
type sl = subst list
let (tuplise_env_outputs: node list list * subst list * env_loc ->
node list list * env_out * env_loc) =
(** The environement provides a list of substitution whereas
lurette expects tuples of values, where the different variable
values are sorted lexicographically w.r.t. their names. The
transation is done by this function. E.g., [(tuplise_env_outputs
([], [("b", Bool(true)); ("a", Int(1))], []) = ([], (1, true),
[]))].
*)
fun (nll, sl, loc) ->
let (sort_subst: subst list -> subst list) =
fun list ->
(* Sorts substitutions lexicographically w.r.t. to var names. *)
List.sort (fun (n1, v1) (n2, v2) -> compare n1 n2) list
in
let (_, vals) = List.split (sort_subst sl) in
(nll, (Lurette_stub.list_ae_to_sut_in vals), loc)
let (solve_formula_list: int -> node list list ->
(node list list * sl * sl) list -> formula list -> var_name list ->
(node list list * sl * sl) list) =
fun p nll acc fl vars ->
fun p nll acc fl vars_to_gen ->
(*
** Returns [p] solutions for the conjunction of formula contained
** in [fl]; a solution is a triple containing (1) the node list [nll],
......@@ -169,7 +152,9 @@ let (solve_formula_list: int -> node list list ->
** (2) a list of substitutions for output vars, and (3) a list of
** substitutions for local vars.
*)
let sl_sl_l = Solver.solve_formula p fl vars in
let sl_sl_l = Solver.solve_formula p fl vars_to_gen in
let nll_sl_sl_l =
(* Adds the target nodes to the substitutions *)
if acc = [] then
(List.map
(fun (sl1, sl2) ->
......@@ -183,6 +168,8 @@ let (solve_formula_list: int -> node list list ->
sl_sl_l
acc
)
in
nll_sl_sl_l
let (solve_formula_list_list: int -> node list list * formula list list
-> (node list list * sl * sl) list) =
......@@ -197,13 +184,13 @@ let (solve_formula_list_list: int -> node list list * formula list list
let (vars, _) = List.split (List.append out loc) in
List.append vars acc
in
let vars_to_gen_l =
let vars_to_gen_ll =
(* Var names that should be generated for each group of envts. *)
List.map
(fun nl -> List.fold_left get_vars_from_node [] nl) nll
in
let nll_sl_sl_l =
List.fold_left2 (solve_formula_list p nll) [] fll vars_to_gen_l
List.fold_left2 (solve_formula_list p nll) [] fll vars_to_gen_ll
in
assert (p = (List.length nll_sl_sl_l));
nll_sl_sl_l
......@@ -253,8 +240,8 @@ let _ = assert (
(* Exported *)
let (env_try: int -> int -> Lurette_stub.sut_out ->
(node list list * Lurette_stub.sut_in * env_loc) list) =
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
......@@ -263,26 +250,29 @@ let (env_try: int -> int -> Lurette_stub.sut_out ->
in
let wtl = get_wtrees cn_ll wtt in
let fte = Eval.eval_wtree_list input wtl cn_ll in
(* Drawing n formula *)
let nl_fl_ll = map2 (Wtree.choose_n_formula n fte) cn_ll wtl in
let nll_fll_l = merge_lll nl_fl_ll in
(* Drawing p solutions for each of the n formula *)
let nll_sl_sl_ll = List.map (solve_formula_list_list p) nll_fll_l in
let nll_sl_sl_l = flatten nll_sl_sl_ll in
assert (length nll_sl_sl_l = (n*p));
env_state.input <- input;
List.map (tuplise_env_outputs) nll_sl_sl_l
nll_sl_sl_l
(*****************************************************************************)
(*****************************************************************************)
(* env_step *)
(* Exported *)
let (env_step : node list list -> Lurette_stub.sut_in -> env_loc -> unit) =
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.current_nodes <- nodes_to ;
env_state.output <- output ;
env_state.local <- List.append local env_state.local
......
......@@ -23,13 +23,11 @@
*)
open Graph
open Lurette_stub
open Formula
open Env_state
(*---------------------------------------------------------------------*)
val read_env_state : string list list -> unit
(**
[read_env_state files_ll] updates the global variable
......@@ -45,7 +43,7 @@ val read_env_state : string list list -> unit
*)
val env_try : int -> int -> sut_out -> (node list list * sut_in * env_loc) list
val env_try : int -> int -> env_in -> (node list list * env_out * env_loc) list
(**
[env_try n p input] returns a list of [n*p] possible outputs of the
environment with input [input]. This function actually returns a list
......@@ -58,7 +56,7 @@ val env_try : int -> int -> sut_out -> (node list list * sut_in * env_loc) list
val env_step : node list list -> sut_in -> env_loc -> unit
val env_step : node list list -> env_out -> env_loc -> unit
(**
[env_step node_to output local ] modifies the environment state by:
- performing a transition from the current_node to [node_to],
......
......@@ -8,8 +8,6 @@
** Main author: jahier@imag.fr
*)
open Lurette_stub
open Graph
open Formula
open Wtree
......@@ -54,8 +52,8 @@ let (env_state:env_stateT) = {
graph = Graph.create () ;
formula_table = Hashtbl.create 0 ;
wtree_table = Hashtbl.create 0 ;
input = sut_out_init ;
output = sut_in_init ;
input = [] ;
output = [] ;
local = []
}
......
......@@ -15,7 +15,6 @@
open Formula
open Wtree
type env_stateT = {
mutable var_names: (string, (vnt list * vnt list * vnt list)) Hashtbl.t;
(** Var names and types ([vnt]) of input, output, and local vars,
......
......@@ -11,22 +11,23 @@
open Formula
open Env_state
open Lurette_stub
open Wtree
(****************************************************************************)
let (lookup_loc: var_name -> atomic_expr option) =
fun v ->
let (lookup: subst list -> var_name -> atomic_expr option) =
fun sl v ->
try
let v = List.assoc v env_state.local in
let v = List.assoc v sl in
Some(v)
with Not_found -> None
(****************************************************************************)
(****************************************************************************)
let rec (eval : formula -> sut_out -> formula) =
let rec (eval : formula -> env_in -> formula) =
(*
** [eval f input] returns an evaluated version of the formula f. Input
** variables (namely, sut outputs) as well as variables ``under a pre''
......@@ -64,14 +65,14 @@ let rec (eval : formula -> sut_out -> formula) =
| False -> False
| Bvar(str) ->
( match (lookup_sut_out str input) with
( match (lookup input 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
(match (lookup env_state.local str) with
Some(Bool(bool)) ->
if bool then True else False
| Some(_) ->
......@@ -168,7 +169,7 @@ and
| _ -> Mod(ee1, ee2)
)
| Nvar(str) ->
( match (lookup_sut_out str input) with
( match (lookup input str) with
Some(Int(i)) -> Ival(i)
| Some(Float(f)) -> Fval(f)
| Some(Bool(f)) ->
......@@ -176,7 +177,7 @@ and
^ "is a bool, not an int nor of float!\n");
assert false
| None ->
( match (lookup_loc str) with
( match (lookup env_state.local str) with
Some(Int(i)) -> Ival(i)
| Some(Float(f)) -> Fval(f)
| Some(Bool(f)) ->
......@@ -193,7 +194,7 @@ and
(****************************************************************************)
(****************************************************************************)
let rec (eval_wtree_list: sut_out -> wtree list -> node list list ->
let rec (eval_wtree_list: env_in -> wtree list -> node list list ->
formula_table) =
fun input wtl nfll ->
(**
......@@ -209,17 +210,17 @@ let rec (eval_wtree_list: sut_out -> wtree list -> node list list ->
nfll);
ft
and
(eval_wtree : sut_out -> formula_table -> wtree -> node list -> unit) =
(eval_wtree : env_in -> formula_table -> wtree -> node list -> unit) =
fun input ft wt nl ->
List.iter (eval_wnode input ft nl) wt
and
(eval_wnode : sut_out -> formula_table -> node list -> wnode -> unit) =
(eval_wnode : env_in -> formula_table -> node list -> wnode -> unit) =
fun input ft nlf wn ->
match wn with
L(w, nlt) -> List.iter2 (add_formula input ft) (List.sort (-) nlf) (List.sort (-) nlt) (* XXX pas ici te tri !!! *)
L(w, nlt) -> List.iter2 (add_formula input ft) nlf nlt
| N(w, wt) -> (eval_wtree input ft wt nlf)
and
(add_formula : sut_out -> formula_table -> node -> node -> unit) =
(add_formula : env_in -> formula_table -> node -> node -> unit) =
fun input ft nf nt ->
let f = Hashtbl.find env_state.formula_table (nf, nt) in
let fe = eval f input in
......@@ -249,7 +250,7 @@ let (formula_to_atomic: formula -> atomic_expr) = function
| False -> Bool(false)
| _ -> assert false
let (update_pre: sut_out -> unit) =
let (update_pre: env_in -> unit) =
fun input ->
(*
** Computes the values of pre expressions and formula (i.e., updates
......
......@@ -11,10 +11,9 @@
(** Defines functions that evaluate formula or expressions. *)
open Formula
open Lurette_stub
open Wtree
val eval : formula -> sut_out -> formula
val eval : formula -> env_in -> formula
(**
[eval f input] returns an evaluated version of the formula f. Input
variables (namely, sut outputs) as well as variables ``under a pre''
......@@ -22,10 +21,10 @@ val eval : formula -> sut_out -> formula
the formula is simplified; e.g., [true and f] is simplified into [f].
*)
val eval_expr : expr -> sut_out -> expr
val eval_expr : expr -> env_in -> expr
(** Ditto for expressions. *)
val eval_wtree_list : sut_out -> wtree list -> node list list
val eval_wtree_list : env_in -> wtree list -> node list list
-> formula_table
(**
[eval_wtree_list input wtl nfll] returns a table of formula
......@@ -35,7 +34,7 @@ val eval_wtree_list : sut_out -> wtree list -> node list list
associated to pair of nodes from [env_state.formula_table]).
*)
val update_pre: sut_out -> unit
val update_pre: env_in -> unit
(**
Computes the values of pre expressions and formula (i.e., updates
[env_state.local]).
......
......@@ -10,8 +10,6 @@
(****************************************************************************)
open Lurette_stub
type expr =
| Sum of expr * expr
| Diff of expr * expr
......@@ -49,18 +47,23 @@ type arc = node * node
type arc_info = weigth * formula_eps
type atomic_expr =
| Int of int
| Bool of bool
| Float of float
type var_name = string
type subst = (var_name * atomic_expr)
type env_in = sut_out
type env_out = sut_in
type env_loc = subst list
type var_type = string
type vnt = var_name * var_type
type vne = var_name * (expr * expr)
type vnf = var_name * (formula * formula)
type env_in = subst list
type env_out = subst list
type env_loc = subst list
(****************************************************************************)
(****************************************************************************)
......@@ -109,3 +112,24 @@ let (arc_info_to_string : arc_info -> string) =
fun (weigth, formula_eps) ->
((string_of_int weigth) ^ " : " ^ (formula_eps_to_string formula_eps))
let print_atomic_expr e oc =
match e with
Int(i) -> output_string oc (string_of_int i)
| Bool(true) -> output_string oc "t"
| Bool(false) -> output_string oc "f"
| Float(f) -> output_string oc (string_of_float f)
let (print_subst_list : subst list -> out_channel -> unit) =
fun sl oc ->
List.iter
(fun (vn, e) ->
print_string vn ;
print_string "=";
print_atomic_expr e oc;
print_string " "
)
(Util.sort_list_string_pair sl)