Skip to content

GitLab

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

lurette 0.18 Thu, 06 Dec 2001 12:40:09 +0100 by jahier 

Parent-Version:      0.17
Version-Log:
 Handle pre in formula and expressions. Also add (in
green) the environment local vars in the sim2chro output.

Project-Description: Lurette
parent a330ffbb
Hide whitespace changes
Inline Side-by-side
.lurette.prcs_aux
View file @ e95202e8
......@@ -2,53 +2,53 @@
;; REALLY bad things.
(Created-By-Prcs-Version 1 3 3)
(test/vrai.h 1120 1006183551 31_vrai.h 1.1)
(source/env_state.ml 1378 1007379917 51_env_state. 1.1)
(source/env_state.ml 1514 1007638809 51_env_state. 1.2)
(source/graph.ml 2397 1003932490 14_graph.ml 1.2)
(test/tram_env_porte.env 857 1007379917 b/11_tram_env_p 1.1)
(source/util.ml 3175 1007379917 35_util.ml 1.2)
(test/tram_env_porte.env 882 1007638809 b/11_tram_env_p 1.2)
(source/util.ml 3166 1007638809 35_util.ml 1.3)
(source/wtree.ml 9181 1007379917 b/1_wtree.ml 1.1)
(source/solver.ml 1841 1007379917 39_solver.ml 1.1)
(source/lurette.ml 7890 1007398490 12_lurette.ml 1.10)
(source/solver.ml 1834 1007638809 39_solver.ml 1.2)
(source/lurette.ml 9612 1007638809 12_lurette.ml 1.11)
(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)
(test/tram_env_tramway.env 1228 1007638809 b/10_tram_env_t 1.2)
(source/env.ml 8243 1007638809 16_env.ml 1.9)
(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)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/parse_env.mli 788 1007379917 40_parse_env. 1.1)
(source/parse_env.mli 865 1007638809 40_parse_env. 1.2)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(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 31830 1007398490 24_generate_l 1.10)
(source/parse_env.ml 6007 1007379917 41_parse_env. 1.1)
(source/eval.ml 7923 1007638809 49_eval.ml 1.2)
(source/gen_stubs.ml 32046 1007638809 24_generate_l 1.11)
(source/parse_env.ml 6609 1007638809 41_parse_env. 1.2)
(interface/TAGS 1956 1007380262 26_TAGS 1.3)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(source/formula.mli 1735 1007379917 44_formula.ml 1.1)
(test/tram_env_usager.env 801 1007379917 b/9_tram_env_u 1.1)
(source/formula.mli 1663 1007638809 44_formula.ml 1.2)
(test/tram_env_usager.env 826 1007638809 b/9_tram_env_u 1.2)
(TAGS 9825 1007379917 21_TAGS 1.6)
(source/wtree.mli 2906 1007379917 b/0_wtree.mli 1.1)
(source/env_state.mli 897 1007379917 50_env_state. 1.1)
(source/env_state.mli 957 1007638809 50_env_state. 1.2)
(interface/sut_idl_stub.ml 338 1006263457 34_sut_idl_st 1.1)
(source/eval.mli 498 1007379917 48_eval.mli 1.1)
(source/eval.mli 859 1007638809 48_eval.mli 1.2)
(README 0 1002791390 10_README 1.1)
(OcamlMakefile 15999 1007381245 17_OcamlMakef 1.4)
(OcamlMakefile 15997 1007638809 17_OcamlMakef 1.5)
(source/show_env.ml 3303 1007379917 43_show_env.m 1.1)
(test/tram_simple.c 5627 1006433610 37_tram_simpl 1.1)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
(interface/Makefile 215 1007380262 25_Makefile 1.5)
(source/show_env.mli 848 1007379917 42_show_env.m 1.1)
(test/tram_simple.h 1746 1006433610 36_tram_simpl 1.1)
(Makefile 1176 1007380262 18_Makefile 1.9)
(Makefile 1269 1007638809 18_Makefile 1.10)
(test/vrai_tram.c 2855 1007379917 b/8_vrai_tram. 1.1)
(source/print.mli 108 1007379917 46_print.mli 1.1)
(source/graph.mli 1305 1003932490 13_graph.mli 1.2)
(source/formula.ml 3404 1007379917 45_formula.ml 1.1)
(source/formula.ml 3115 1007638809 45_formula.ml 1.2)
(test/vrai.c 1405 1006183551 30_vrai.c 1.1)
(source/lurette.mli 371 1007398490 11_lurette.ml 1.7)
(source/print.ml 1098 1007379917 47_print.ml 1.1)
......
Makefile
View file @ e95202e8
LURETTE_DIR = /home/jahier/lurette
OCAMLMAKEFILE = $(LURETTE_DIR)/OcamlMakefile
# It seems that there is no speed up with those options...
# OCAMLFLAGS = -noassert -unsafe
-include ./lurette.in
SOURCES = $(SUT) sut_stub.c sut_idl_stub.idl \
......
OcamlMakefile
View file @ e95202e8
......@@ -5,7 +5,7 @@
# For updates see:
# http://miss.wu-wien.ac.at/~mottl/ocaml_sources
#
# $Id: OcamlMakefile 1.4 Mon, 03 Dec 2001 13:07:25 +0100 jahier $
# $Id: OcamlMakefile 1.5 Thu, 06 Dec 2001 12:40:09 +0100 jahier $
#
###########################################################################
......@@ -492,7 +492,7 @@ dot:
#
try:
$(LURETTE_DIR)/make_lurette tram_simple vrai_tram; \
./lurette 10 100 100 tram_env_porte.env x tram_env_usager.env tram_env_tramway.env
./lurette 50 10 10 tram_env_porte.env x tram_env_usager.env tram_env_tramway.env
###########################################################################
......
lurette.prj
View file @ e95202e8
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 17)
(Parent-Version lurette 0 16)
(Version-Log "
Plug sim2cro to the lurette outputs.
(Project-Version lurette 0 18)
(Parent-Version lurette 0 17)
(Version-Log " Handle pre in formula and expressions. Also add (in
green) the environment local vars in the sim2chro output.
")
(New-Version-Log "")
(Checkin-Time "Mon, 03 Dec 2001 17:54:50 +0100")
(Checkin-Time "Thu, 06 Dec 2001 12:40:09 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -19,45 +19,45 @@ Plug sim2cro to the lurette outputs.
;; Sources files
(source/lurette.mli (lurette/11_lurette.ml 1.7 644))
(source/lurette.ml (lurette/12_lurette.ml 1.10 644))
(source/lurette.ml (lurette/12_lurette.ml 1.11 644))
(source/graph.mli (lurette/13_graph.mli 1.2 644))
(source/graph.ml (lurette/14_graph.ml 1.2 644))
(source/env.mli (lurette/15_env.mli 1.5 644))
(source/env.ml (lurette/16_env.ml 1.8 644))
(source/env.ml (lurette/16_env.ml 1.9 644))
(source/util.ml (lurette/35_util.ml 1.2 644))
(source/util.ml (lurette/35_util.ml 1.3 644))
(source/solver.mli (lurette/38_solver.mli 1.1 644))
(source/solver.ml (lurette/39_solver.ml 1.1 644))
(source/solver.ml (lurette/39_solver.ml 1.2 644))
(source/parse_env.mli (lurette/40_parse_env. 1.1 644))
(source/parse_env.ml (lurette/41_parse_env. 1.1 644))
(source/parse_env.mli (lurette/40_parse_env. 1.2 644))
(source/parse_env.ml (lurette/41_parse_env. 1.2 644))
(source/show_env.mli (lurette/42_show_env.m 1.1 644))
(source/show_env.ml (lurette/43_show_env.m 1.1 644))
(source/formula.mli (lurette/44_formula.ml 1.1 644))
(source/formula.ml (lurette/45_formula.ml 1.1 644))
(source/formula.mli (lurette/44_formula.ml 1.2 644))
(source/formula.ml (lurette/45_formula.ml 1.2 644))
(source/print.mli (lurette/46_print.mli 1.1 644))
(source/print.ml (lurette/47_print.ml 1.1 644))
(source/eval.mli (lurette/48_eval.mli 1.1 644))
(source/eval.ml (lurette/49_eval.ml 1.1 644))
(source/eval.mli (lurette/48_eval.mli 1.2 644))
(source/eval.ml (lurette/49_eval.ml 1.2 644))
(source/env_state.mli (lurette/50_env_state. 1.1 644))
(source/env_state.ml (lurette/51_env_state. 1.1 644))
(source/env_state.mli (lurette/50_env_state. 1.2 644))
(source/env_state.ml (lurette/51_env_state. 1.2 644))
(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.10 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.11 644))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.4 644))
(Makefile (lurette/18_Makefile 1.9 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.5 644))
(Makefile (lurette/18_Makefile 1.10 644))
(test/Makefile (../Makefile) :symlink)
(interface/Makefile (lurette/25_Makefile 1.5 644))
(make_lurette (lurette/27_make_luret 1.5 744))
......@@ -93,9 +93,9 @@ Plug sim2cro to the lurette outputs.
(test/vrai_tram.lus (lurette/b/6_vrai_tram. 1.1 644))
(test/vrai_tram.h (lurette/b/7_vrai_tram. 1.1 644))
(test/vrai_tram.c (lurette/b/8_vrai_tram. 1.1 644))
(test/tram_env_usager.env (lurette/b/9_tram_env_u 1.1 644))
(test/tram_env_tramway.env (lurette/b/10_tram_env_t 1.1 644))
(test/tram_env_porte.env (lurette/b/11_tram_env_p 1.1 644))
(test/tram_env_usager.env (lurette/b/9_tram_env_u 1.2 644))
(test/tram_env_tramway.env (lurette/b/10_tram_env_t 1.2 644))
(test/tram_env_porte.env (lurette/b/11_tram_env_p 1.2 644))
)
(Merge-Parents)
......
source/env.ml
View file @ e95202e8
......@@ -30,7 +30,8 @@ let (read_env_state_one_file : string -> node) =
** Also updates the global variable `env_state'.
*)
let cpt = (List.length (get_all_nodes env_state.graph)) in
let Automata(init_node, list_in, list_out, list_loc, list_arcs) =
let Automata(init_node, list_in, list_out, list_loc, list_pre_expr,
list_pre_form, list_arcs) =
try Parse_env.parse_automata(lexer(Stream.of_channel (open_in file)))
with _ -> failwith "*** Error while parsing the environment file.\n"
in
......@@ -46,6 +47,8 @@ let (read_env_state_one_file : string -> node) =
in
List.iter (add_arc) list_arcs ;
env_state.var_names <- (file, (list_in, list_out, list_loc))::env_state.var_names ;
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)) ;
(init_node+cpt)
......@@ -194,16 +197,17 @@ let (env_try : int -> int -> sut_out -> (node list list * sut_in * env_loc) list
let _ = assert (
(* n = 2, env1 x env2 env3 *)
(merge_lll
[[([1;2], [Bool_id("a");Bool_id("b")]);
([4;5], [Bool_id("d");Bool_id("e")])];
[([3], [Bool_id("c")]);
([6], [Bool_id("f")])]])
[[([1;2], [Bvar("a");Bvar("b")]);
([4;5], [Bvar("d");Bvar("e")])];
[([3], [Bvar("c")]);
([6], [Bvar("f")])]])
=
[[[3]; [1; 2]], [[Bool_id "c"]; [Bool_id "a"; Bool_id "b"]];
[[6]; [4; 5]], [[Bool_id "f"]; [Bool_id "d"; Bool_id "e"]]]
[[[3]; [1; 2]], [[Bvar "c"]; [Bvar "a"; Bvar "b"]];
[[6]; [4; 5]], [[Bvar "f"]; [Bvar "d"; Bvar "e"]]]
)
in
let _ = Eval.update_pre env_state.input in
let cn_ll = env_state.current_nodes in
let ft = env_state.formula_table in
let wtt = env_state.wtree_table in
......@@ -216,10 +220,9 @@ let (env_try : int -> int -> sut_out -> (node list list * sut_in * env_loc) list
let nll_sl_sl_l = flatten nll_sl_sl_ll in
let _ = assert (length nll_sl_sl_l = (n*p)) in
env_state.input <- input;
env_state.input <- input;
List.map (tuplise_env_outputs) nll_sl_sl_l
(****************************************************************************)
......@@ -233,7 +236,7 @@ let (env_step : node list list -> sut_in -> env_loc -> unit) =
fun nodes_to output local ->
env_state.current_nodes <- nodes_to ;
env_state.output <- output ;
env_state.local <- local
env_state.local <- List.append local env_state.local
......
source/env_state.ml
View file @ e95202e8
......@@ -22,14 +22,17 @@ open Wtree
** formula.
*)
(* XXX Should they really be mutable ??? *)
type env_stateT = {
(* var names and types given file by file *)
mutable var_names: (string * (vnt list * vnt list * vnt list)) 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_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 ;
(*
** Used to store the values of variables under a pre
......@@ -46,6 +49,8 @@ type env_stateT = {
*)
let (env_state:env_stateT) = {
var_names = [] ;
pre_expr = [] ;
pre_form = [] ;
current_nodes = [];
graph = Graph.create () ;
formula_table = Hashtbl.create 0 ;
......
source/env_state.mli
View file @ e95202e8
......@@ -17,6 +17,8 @@ open Wtree
type env_stateT = {
mutable var_names: (string * (vnt list * vnt list * vnt list)) list;
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 ;
......
source/eval.ml
View file @ e95202e8
......@@ -16,17 +16,12 @@ open Wtree
(****************************************************************************)
let (lookup_loc: var_name -> subst list -> atomic_expr) =
fun v sl ->
List.assoc v sl
let (lookup_pre: var_name -> atomic_expr) =
fun v ->
try Lurette_stub.lookup_sut_in v env_state.output
with Not_found ->
try Lurette_stub.lookup_sut_out v env_state.input
with Not_found -> lookup_loc v env_state.local
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
(****************************************************************************)
(****************************************************************************)
......@@ -37,11 +32,6 @@ let rec (eval : formula -> sut_out -> formula) =
** variables (namely, sut outputs) as well as variables ``under a pre''
** (in the environment memory) are replaced by their values. Then,
** the formula is simplified; e.g., `true and f' is simplified into `f'.
**
** XXX Do we simplify numerical values (e.g., `3 > 5') here or do we let
** the constraint solver do that job ??? (this might be an issue if this
** function and the constraint solver do not use the same numerical
** representation).
*)
fun f input -> match f with
And(f1, f2) ->
......@@ -73,97 +63,135 @@ let rec (eval : formula -> sut_out -> formula) =
| True -> True
| False -> False
| Bool_id(str) ->
(try let v = (lookup_sut_out str input) in
( match v with
Bool(bool) -> if bool then True else False
| _ -> assert false
)
with Not_found -> Bool_id(str)
| Bvar(str) ->
( match (lookup_sut_out str input) 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)
)
)
(*
** XXX Do we evaluate expressions here or do we let the constraint solver do
** it ?
*)
| Eq(e1, e2) -> Eq(e1, e2)
| Ge(e1, e2) -> Ge(e1, e2)
| G(e1, e2) -> G(e1, e2)
| Pre_f f -> eval_pre_formula f
and
(eval_pre_formula : formula -> formula) =
function
And(f1, f2) -> And(eval_pre_formula f1, eval_pre_formula f2)
| Or(f1, f2) -> Or(eval_pre_formula f1, eval_pre_formula f2)
| Not(f1) -> Not(eval_pre_formula f1)
| True -> True
| False -> False
| Bool_id(str) ->
(try let v = (lookup_pre str) in
( match v with
Bool(bool) -> if bool then True else False
| _ -> assert false
)
with Not_found -> Bool_id(str)
)
| Pre_f _ -> assert false
(* XXX Do we evaluate expressions here or do we let the constraint solver
do it ? *)
| Eq(e1, e2) -> Eq((eval_pre_expr e1), (eval_pre_expr e2))
| Ge(e1, e2) -> Ge((eval_pre_expr e1), (eval_pre_expr e2))
| G(e1, e2) -> G((eval_pre_expr e1), (eval_pre_expr e2))
and
(eval_pre_expr : expr -> expr) =
function
Sum(e1, e2) -> Sum(eval_pre_expr(e1), eval_pre_expr(e2))
| Diff(e1, e2) -> Diff(eval_pre_expr(e1), eval_pre_expr(e2))
| Prod(e1, e2) -> Prod(eval_pre_expr(e1), eval_pre_expr(e2))
| Quot(e1, e2) -> Quot(eval_pre_expr(e1), eval_pre_expr(e2))
| Mod(e1, e2) -> Mod(eval_pre_expr(e1), eval_pre_expr(e2))
| Div(e1, e2) -> Div(eval_pre_expr(e1), eval_pre_expr(e2))
| Var(str) ->
(try let v = lookup_pre str
in
( match v with
Int(i) -> Int_id(i)
| Float(f) -> Float_id(f)
| Bool(_) -> assert false
)
with Not_found -> Var(str)
| Eq(e1, e2) ->
(
let ee1 = eval_expr e1 input in
let ee2 = eval_expr e2 input in
match (ee1, ee2) with
(Ival(i1), Ival(i2)) -> if (i1 = i2) then True else False
| (Fval(f1), Fval(f2)) ->
if (f1 = f2) then True else False
(* XXX Meaningless with floats ??? *)
| _ -> Eq(ee1, ee2)
)
| Int_id(i) -> Int_id(i)
| Float_id(f) -> Float_id(f)
| Pre_e _ -> assert false
(* XXX mettre pleins d'assertions / tests unitaires ici !!! *)
| Ge(e1, e2) ->
(
let ee1 = eval_expr e1 input in
let ee2 = eval_expr e2 input in
match (ee1, ee2) with
(Ival(i1), Ival(i2)) -> if (i1 >= i2) then True else False
| (Fval(f1), Fval(f2)) ->
if (f1 >= f2) then True else False
(* XXX Meaningless with floats ??? *)
| _ -> Ge(ee1, ee2)
)
| G(e1, e2) ->
(
let ee1 = eval_expr e1 input in
let ee2 = eval_expr e2 input in
match (ee1, ee2) with
(Ival(i1), Ival(i2)) -> if (i1 > i2) then True else False
| (Fval(f1), Fval(f2)) ->
if (f1 > f2) then True else False
| _ -> Ge(ee1, ee2)
)
and
(eval_expr : expr -> env_in -> expr) =
fun e input ->
match e with
Sum(e1, e2) ->
(
let ee1 = eval_expr e1 input in
let ee2 = eval_expr e2 input in
match (ee1, ee2) with
(Ival(i1), Ival(i2)) -> Ival(i1+i2)
| (Ival(i1), Fval(f2)) -> Fval(float_of_int(i1)+.f2)
| (Fval(f1), Ival(i2)) -> Fval(f1+.float_of_int(i2))
| (Fval(f1), Fval(f2)) -> Fval(f1+.f2)
| _ -> Sum(ee1, ee2)
)
| Diff(e1, e2) ->
(
let ee1 = eval_expr e1 input in
let ee2 = eval_expr e2 input in
match (ee1, ee2) with
(Ival(i1), Ival(i2)) -> Ival(i1-i2)
| (Ival(i1), Fval(f2)) -> Fval(float_of_int(i1)-.f2)
| (Fval(f1), Ival(i2)) -> Fval(f1-.float_of_int(i2))
| (Fval(f1), Fval(f2)) -> Fval(f1-.f2)
| _ -> Diff(ee1, ee2)
)
| Prod(e1, e2) ->
(
let ee1 = eval_expr e1 input in
let ee2 = eval_expr e2 input in
match (ee1, ee2) with
(Ival(i1), Ival(i2)) -> Ival(i1*i2)
| (Ival(i1), Fval(f2)) -> Fval(float_of_int(i1)*.f2)
| (Fval(f1), Ival(i2)) -> Fval(f1*.float_of_int(i2))
| (Fval(f1), Fval(f2)) -> Fval(f1*.f2)
| _ -> Prod(ee1, ee2)
)
| Quot(e1, e2) ->
(
let ee1 = eval_expr e1 input in
let ee2 = eval_expr e2 input in
match (ee1, ee2) with
(Ival(i1), Ival(i2)) -> Ival(i1/i2)
| (Fval(f1), Fval(f2)) -> Fval(f1/.f2)
| _ -> Quot(ee1, ee2)
)
| Mod(e1, e2) ->
(
let ee1 = eval_expr e1 input in
let ee2 = eval_expr e2 input in
match (ee1, ee2) with
(Ival(i1), Ival(i2)) -> Ival(i1 mod i2)
| (Fval(f1), Fval(f2)) -> Fval(mod_float f1 f2)
| _ -> Mod(ee1, ee2)
)
| Nvar(str) ->
( match (lookup_sut_out str input) 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 ->
( 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)
)
)
| Ival(i) -> Ival(i)
| Fval(f) -> Fval(f)
(*
** XXX Do we evaluate expressions here or do we let the constraint solver
** do it ?
**
** and
** (eval_expr : expr -> env_in -> expr) =
** fun e input ->
** match e with
** Eq(e1, e2) -> (eval_expr e1) = (eval_expr e2)
** | Ge(e1, e2) -> (eval_expr e1) >= (eval_expr e2)
** | G(e1, e2) -> (eval_expr e1) > (eval_expr e2)
**
** | Sum(e1, e2) -> eval_expr(e1) + eval_expr(e2)
** | Diff(e1, e2) -> eval_expr(e1) - eval_expr(e2)
** | Prod(e1, e2) -> eval_expr(e1) * eval_expr(e2)
** | Quot(e1, e2) -> eval_expr(e1) / eval_expr(e2)
** | Mod(e1, e2) -> eval_expr(e1) mod eval_expr(e2)
** | Div(e1, e2) -> eval_expr(e1) / eval_expr(e2)
**
** | Var(str) -> str
** | Val(str) -> str
*)
(****************************************************************************)
(****************************************************************************)
let rec (eval_wtree_list: sut_out -> wtree list -> node list list ->
formula_table) =
......@@ -197,3 +225,49 @@ and
let fe = eval f input in
Hashtbl.add ft (nf, nt) fe
(****************************************************************************)
(****************************************************************************)
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
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: sut_out -> 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 ;
in
env_state.local <- new_local
source/eval.mli
View file @ e95202e8
......@@ -14,6 +14,22 @@ open Lurette_stub
open Wtree
val eval : formula -> sut_out -> formula
val eval_expr : expr -> sut_out -> expr
val eval_wtree_list : sut_out -> wtree list -> node list list
-> formula_table
val update_pre: sut_out -> unit
(*
** Computes the values of pre expressions and formula (i.e., updates
** env_state.local).