Skip to content

GitLab

Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

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

lurette 0.24 Tue, 05 Feb 2002 14:10:29 +0100 by jahier 

Parent-Version:      0.23
Version-Log:

Make the examples of Yvan work. Fix a bunch of bugs alonf the way...

Project-Description: Lurette
parent 010423f4
Hide whitespace changes
Inline Side-by-side
Showing with 396 additions and 292 deletions
.lurette.prcs_aux
View file @ eb46e24b
;; This file is automatically generated, editing may cause PRCS to do
;; REALLY bad things.
(Created-By-Prcs-Version 1 3 3)
(test/vrai.h 1120 1006183551 31_vrai.h 1.1)
(test/usager.env 392 1012914629 b/14_usager.env 1.1)
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 2268 1011881677 51_env_state. 1.4)
(source/graph.ml 2397 1003932490 14_graph.ml 1.2)
(test/tram_env_porte.env 882 1007638809 b/11_tram_env_p 1.2)
(source/env_state.ml 2347 1012914629 51_env_state. 1.5)
(source/graph.ml 2476 1012914629 14_graph.ml 1.3)
(source/util.ml 4248 1011881677 35_util.ml 1.6)
(source/wtree.ml 9221 1011881677 b/1_wtree.ml 1.4)
(source/solver.ml 11173 1011881677 39_solver.ml 1.4)
(source/lurette.ml 8290 1011881677 12_lurette.ml 1.13)
(source/solver.mli 934 1011881677 38_solver.mli 1.4)
(source/wtree.ml 9831 1012914629 b/1_wtree.ml 1.5)
(source/solver.ml 11387 1012914629 39_solver.ml 1.5)
(source/lurette.ml 8437 1012914629 12_lurette.ml 1.14)
(source/solver.mli 971 1012914629 38_solver.mli 1.5)
(source/env.mli 2524 1008328137 15_env.mli 1.7)
(test/vrai.lus 65 1006182545 28_vrai.lus 1.1)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(test/tram_env_tramway.env 1228 1007638809 b/10_tram_env_t 1.2)
(source/env.ml 9609 1011881677 16_env.ml 1.11)
(make_lurette 1027 1007398490 27_make_luret 1.5)
(source/env.ml 9647 1012914629 16_env.ml 1.12)
(make_lurette 1054 1012914629 27_make_luret 1.6)
(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 49 1007651448 b/4_lurette.de 1.2)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(test/passerelle.env 862 1012914629 b/17_passerelle 1.1)
(source/parse_env.mli 939 1008328137 40_parse_env. 1.3)
(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 7923 1007638809 49_eval.ml 1.2)
(source/eval.ml 7978 1012914629 49_eval.ml 1.3)
(source/gen_stubs.ml 32098 1008255910 24_generate_l 1.13)
(source/parse_env.ml 6537 1008328137 41_parse_env. 1.3)
(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)
(test/tram_env_usager.env 826 1007638809 b/9_tram_env_u 1.2)
(TAGS 9825 1007379917 21_TAGS 1.6)
(source/wtree.mli 2860 1008328137 b/0_wtree.mli 1.3)
(source/env_state.mli 3216 1011881677 50_env_state. 1.4)
(source/env_state.mli 3229 1012914629 50_env_state. 1.5)
(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)
(README 74 1011881677 10_README 1.2)
(OcamlMakefile 16726 1011881677 17_OcamlMakef 1.9)
(OcamlMakefile 16807 1012914629 17_OcamlMakef 1.10)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(source/show_env.ml 3303 1007379917 43_show_env.m 1.1)
(test/tram_simple.c 5627 1006433610 37_tram_simpl 1.1)
(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)
(test/tram_simple.h 1746 1006433610 36_tram_simpl 1.1)
(Makefile 1601 1011881677 18_Makefile 1.14)
(test/vrai_tram.c 2855 1007379917 b/8_vrai_tram. 1.1)
(source/print.mli 339 1011881677 46_print.mli 1.2)
(source/graph.mli 1340 1008328137 13_graph.mli 1.3)
(source/formula.ml 3109 1008328137 45_formula.ml 1.3)
(test/vrai.c 1405 1006183551 30_vrai.c 1.1)
(source/lurette.mli 397 1008328137 11_lurette.ml 1.9)
(source/print.ml 2462 1011881677 47_print.ml 1.3)
(test/vrai_tram.h 2293 1007379917 b/7_vrai_tram. 1.1)
(Makefile 1603 1012914629 18_Makefile 1.15)
(test/vrai_tram.c 3060 1012914629 b/8_vrai_tram. 1.2)
(source/print.mli 412 1012914629 46_print.mli 1.3)
(source/graph.mli 1417 1012914629 13_graph.mli 1.4)
(source/formula.ml 3118 1012914629 45_formula.ml 1.4)
(source/lurette.mli 396 1012914629 11_lurette.ml 1.10)
(source/print.ml 2680 1012914629 47_print.ml 1.4)
(test/vrai_tram.h 2468 1012914629 b/7_vrai_tram. 1.2)
Makefile
View file @ eb46e24b
......@@ -2,7 +2,7 @@ LURETTE_DIR = ..
OCAMLMAKEFILE = $(LURETTE_DIR)/OcamlMakefile
# It seems that there is no speed up with those options... Give it another try.
# OCAMLFLAGS = -noassert -unsafe -inline 10
# OCAMLFLAGS = -noassert -unsafe # -inline 10
-include ./lurette.in
......@@ -25,9 +25,9 @@ SOURCES_OCAML = lurette_stub.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/print.mli $(LURETTE_DIR)/source/print.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 \
......
OcamlMakefile
View file @ eb46e24b
......@@ -5,7 +5,7 @@
# For updates see:
# http://miss.wu-wien.ac.at/~mottl/ocaml_sources
#
# $Id: OcamlMakefile 1.9 Thu, 24 Jan 2002 15:14:37 +0100 jahier $
# $Id: OcamlMakefile 1.10 Tue, 05 Feb 2002 14:10:29 +0100 jahier $
#
###########################################################################
......@@ -494,8 +494,11 @@ dot:
# (R1)
try:
$(LURETTE_DIR)/make_lurette tram_simple vrai_tram; \
./lurette 50 10 10 tram_env_porte.env x tram_env_usager.env tram_env_tramway.env
$(LURETTE_DIR)/make_lurette ControleurPorte vrai_tram; \
# ./lurette 10 2 2 tram.env usager.env porte.env passerelle.env | sim2chro -ecran
./lurette 10 2 2 tram.env usager.env porte.env passerelle.env
# runtest:
dochtml:
ocamldoc -t "Lurette implementation description" -html -d ../doc/html -stars \
......
lurette.prj
View file @ eb46e24b
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 23)
(Parent-Version lurette 0 22)
(Project-Version lurette 0 24)
(Parent-Version lurette 0 23)
(Version-Log "
Add a bdd-based boolean solver to draw inside formula.
Make the examples of Yvan work. Fix a bunch of bugs alonf the way...
Also remove several module opening and use explicit module
qualification instead
lurette.ml:
env_state.ml:
Define a function in env.ml to get the list of input and outputs var names
and use it in lurette.ml
env_state.ml:
Add several fields to the env_state structure:
* node_to_file_name: to be able to retrieve the list of vars that
ougth to be generated from a list of nodes (Indeed, some vars
that should be tossed up do no necessarily appear in formula; and
once the whole bdd has been traversed for the draw, we need to be able
to know what variable are still to be drawn).
* var_name_to_index and index_to_var_name: to index output and local
variable names. Indeed, the bdd library we use manipulates var as int,
not string.
* bdd_tbl: be cause transforming a formula into a bdd is expensive,
we store the result of this transformation in a table.
Define the var_names field as an Hashtbl instead of a list for homogeneity.
Define functions that retrieve the list of input (resp output and local)
vars from env_state to avois code duplication.
env.ml:
Initialize the new fields of env_state.
util.ml:
util.mli:
Add a new function that computes the intersection of 2 lists.
solver.ml:
Implement a real boolean solver using bdds.
")
(New-Version-Log "")
(Checkin-Time "Thu, 24 Jan 2002 15:14:37 +0100")
(Checkin-Time "Tue, 05 Feb 2002 14:10:29 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -55,49 +20,49 @@ solver.ml:
;; Sources files
(source/lurette.mli (lurette/11_lurette.ml 1.9 644))
(source/lurette.ml (lurette/12_lurette.ml 1.13 644))
(source/lurette.mli (lurette/11_lurette.ml 1.10 644))
(source/lurette.ml (lurette/12_lurette.ml 1.14 644))
(source/graph.mli (lurette/13_graph.mli 1.3 644))
(source/graph.ml (lurette/14_graph.ml 1.2 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.11 644))
(source/env.ml (lurette/16_env.ml 1.12 644))
(source/util.ml (lurette/35_util.ml 1.6 644))
(source/solver.mli (lurette/38_solver.mli 1.4 644))
(source/solver.ml (lurette/39_solver.ml 1.4 644))
(source/solver.mli (lurette/38_solver.mli 1.5 644))
(source/solver.ml (lurette/39_solver.ml 1.5 644))
(source/parse_env.mli (lurette/40_parse_env. 1.3 644))
(source/parse_env.ml (lurette/41_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/formula.mli (lurette/44_formula.ml 1.3 644))
(source/formula.ml (lurette/45_formula.ml 1.3 644))
(source/formula.ml (lurette/45_formula.ml 1.4 644))
(source/print.mli (lurette/46_print.mli 1.2 644))
(source/print.ml (lurette/47_print.ml 1.3 644))
(source/print.mli (lurette/46_print.mli 1.3 644))
(source/print.ml (lurette/47_print.ml 1.4 644))
(source/eval.mli (lurette/48_eval.mli 1.3 644))
(source/eval.ml (lurette/49_eval.ml 1.2 644))
(source/eval.ml (lurette/49_eval.ml 1.3 644))
(source/env_state.mli (lurette/50_env_state. 1.4 644))
(source/env_state.ml (lurette/51_env_state. 1.4 644))
(source/env_state.mli (lurette/50_env_state. 1.5 644))
(source/env_state.ml (lurette/51_env_state. 1.5 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.3 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.4 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.5 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.13 644))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.9 644))
(Makefile (lurette/18_Makefile 1.14 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.10 644))
(Makefile (lurette/18_Makefile 1.15 644))
(test/Makefile (../Makefile) :symlink)
(interface/Makefile (lurette/25_Makefile 1.6 644))
(make_lurette (lurette/27_make_luret 1.5 744))
(make_lurette (lurette/27_make_luret 1.6 744))
;; Documentation
......@@ -118,23 +83,20 @@ solver.ml:
;; Various files used for testing purposes
(test/vrai.lus (lurette/28_vrai.lus 1.1 644))
(test/vrai.c (lurette/30_vrai.c 1.1 644))
(test/vrai.h (lurette/31_vrai.h 1.1 644))
(interface/sut_idl_stub.ml (lurette/34_sut_idl_st 1.1 644))
(test/edge.c (lurette/32_edge.c 1.1 640))
(test/edge.h (lurette/33_edge.h 1.1 640))
(test/usager.env (lurette/b/14_usager.env 1.1 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))
(interface/sut_idl_stub.ml (lurette/34_sut_idl_st 1.1 644))
(test/ControleurPorte.h (lurette/b/18_Controleur 1.1 644))
(test/ControleurPorte.c (lurette/b/19_Controleur 1.1 644))
(test/tram_simple.h (lurette/36_tram_simpl 1.1 644))
(test/tram_simple.c (lurette/37_tram_simpl 1.1 644))
(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.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))
(test/vrai_tram.h (lurette/b/7_vrai_tram. 1.2 644))
(test/vrai_tram.c (lurette/b/8_vrai_tram. 1.2 644))
)
(Merge-Parents)
(New-Merge-Parents)
make_lurette
View file @ eb46e24b
......@@ -41,7 +41,7 @@ EOF
############################
echo "... Making lurette: make"
make dc
make dc # XXX pas satisfaisant !!!
;;
*)
echo "$Help"
......
source/env.ml
View file @ eb46e24b
......@@ -33,8 +33,10 @@ let (read_env_state_one_file : string -> int -> int * node) =
try
Parse_env.parse_automata(
Parse_env.lexer(Stream.of_channel (open_in file)))
with _ ->
failwith ("*** Error while parsing the environment file " ^ file ^ "\n")
with e ->
print_string ("*** Error while parsing the environment file " ^ file ^ "\n");
flush stdout;
raise e
in
(* Sets the [var_name_to_index] and [index_to_var_name] fields of
......@@ -58,7 +60,8 @@ let (read_env_state_one_file : string -> int -> int * node) =
fun arc ->
match arc with
Parse_env.Arc(node_from, arc_info, node_to) ->
(Graph.add_trans
(Graph.add_trans
(-)
env_state.graph
(node_from+node_nb)
arc_info
......@@ -145,14 +148,14 @@ let (tuplise_env_outputs: node list list * subst list * env_loc ->
([], [("b", Bool(true)); ("a", Int(1))], []) = ([], (1, true),
[]))].
*)
fun (nl, sl, loc) ->
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
(nl, (Lurette_stub.list_ae_to_sut_in vals), loc)
(nll, (Lurette_stub.list_ae_to_sut_in vals), loc)
let (solve_formula_list: int -> node list list ->
......
source/env_state.ml
View file @ eb46e24b
......@@ -40,8 +40,11 @@ type env_stateT = {
mutable local : env_loc
}
(* Initializing Bdd libs. XXX Where should I do that ? *)
let _ = Dd.initialize 0 1
(* Initializing Bdd libs.
XXX Where should I do that ?
55 marche le mieux avec la passerelle. bertrand dit entre 20 et 30...
*)
let _ = Dd.initialize 0 55
let (env_state:env_stateT) = {
......
source/env_state.mli
View file @ eb46e24b
......@@ -59,7 +59,7 @@ type env_stateT = {
mutable graph : (node, arc_info) Graph.t ;
(** The automata is stored in a Graph.t *)
mutable formula_table : Wtree.formula_table ;
mutable formula_table : (node * node, formula) Hashtbl.t ;
(** Mapping from pair of nodes to formula. *)
mutable wtree_table : Wtree.wtree_table ;
(** Mapping from nodes to [wtree] (see the doc of the [Wtree] module). *)
......
source/eval.ml
View file @ eb46e24b
......@@ -196,11 +196,11 @@ and
let rec (eval_wtree_list: sut_out -> wtree list -> node list list ->
formula_table) =
fun input wtl nfll ->
(*
** returns a table of formula appearing in `wtl'; the formula are
** evaluated w.r.t. `input'. `nfll' is the list of list of origin nodes
** corresponding to the trees in `wtl' (necessary to get formula associated
** to pair of nodes from env_state.formula_table).
(**
Returns a table of formula appearing in `wtl'; the formula are
evaluated w.r.t. `input'. `nfll' is the list of list of origin nodes
corresponding to the trees in `wtl' (necessary to get formula associated
to pair of nodes from env_state.formula_table).
*)
let ft = (Hashtbl.create (List.length wtl)) in
(List.iter2
......@@ -216,7 +216,7 @@ and
(eval_wnode : sut_out -> formula_table -> node list -> wnode -> unit) =
fun input ft nlf wn ->
match wn with
L(w, nlt) -> List.iter2 (add_formula input ft) nlf nlt
L(w, nlt) -> List.iter2 (add_formula input ft) (List.sort (-) nlf) (List.sort (-) nlt) (* XXX pas ici te tri !!! *)
| N(w, wt) -> (eval_wtree input ft wt nlf)
and
(add_formula : sut_out -> formula_table -> node -> node -> unit) =
......
source/formula.ml
View file @ eb46e24b
......@@ -81,13 +81,13 @@ and
(formula_to_string f2) ^ ")")
| Or(f1, f2) -> ("(" ^ (formula_to_string f1) ^ " or " ^
(formula_to_string f2) ^ ")")
| Not(f1) -> "not(" ^ (formula_to_string f1) ^ ")"
| Not(f1) -> ("not(" ^ (formula_to_string f1) ^ ")")
| True -> "true"
| False -> "false"
| Bvar(str) -> str
| Eq(e1, e2) -> (expr_to_string e1) ^ " = " ^ (expr_to_string e2)
| Ge(e1, e2) -> (expr_to_string e1) ^ " >= " ^ (expr_to_string e2)
| G(e1, e2) -> (expr_to_string e1) ^ " > " ^ (expr_to_string e2)
| Eq(e1, e2) -> ((expr_to_string e1) ^ " = " ^ (expr_to_string e2))
| Ge(e1, e2) -> ((expr_to_string e1) ^ " >= " ^ (expr_to_string e2))
| G(e1, e2) -> ((expr_to_string e1) ^ " > " ^ (expr_to_string e2))
and
(expr_to_string: expr -> string) =
fun e -> match e with
......@@ -107,5 +107,5 @@ and
let (arc_info_to_string : arc_info -> string) =
fun (weigth, formula_eps) ->
(string_of_int weigth) ^ " : " ^ (formula_eps_to_string formula_eps)
((string_of_int weigth) ^ " : " ^ (formula_eps_to_string formula_eps))
source/graph.ml
View file @ eb46e24b
......@@ -34,38 +34,38 @@ let (create: unit -> ('a, 'b) t) =
trans = []
}
let (add_trans: ('a, 'b) t -> 'a -> 'b -> 'a -> unit) =
let (get_list_of_target_nodes: ('a, 'b) t -> 'a -> ('a * 'b) list) =
(*
** [get_list_of_target_nodes g node] returns the list of target nodes
** starting from `node_from' in the graph `g'. Actually, it does not only
** return a list of nodes but a list of pairs `(node_to, arc_label)' where
** `arc_label' is the arc label of the arc from `node_from' to `node_to'.
*)
fun g node ->
try Hashtbl.find g.table node
with Not_found -> []
let (add_trans: ('a -> 'a -> int) -> ('a, 'b) t -> 'a -> 'b -> 'a -> unit) =
(*
** [add_trans g node_from arc_info node_to] adds a transition from `node_from'
** to `node_to' with arc label `arc_info' to the graph `g'.
** [add_trans sort g node_from arc_info node_to] adds a transition from `node_from'
** to `node_to' with arc label `arc_info' to the graph `g'. [sort] is a comparison
** function used to sort nodes.
*)
fun g node_from arc_info node_to ->
fun sort g node_from arc_info node_to ->
let l = g.nodes in
let l1 = if (List.mem node_from l) then l else (List.append l [node_from]) in
let l2 = if (List.mem node_to l1) then l1 else (List.append l1 [node_to]) in
if (Hashtbl.mem g.table node_from) then
let list = Hashtbl.find g.table node_from in
Hashtbl.replace g.table node_from ((node_to, arc_info)::list)
let list = ((node_to, arc_info)::(Hashtbl.find g.table node_from)) in
let list_sorted = List.sort (fun (n1,a1) (n2,a2) -> (sort n1 n2)) list in
Hashtbl.replace g.table node_from list_sorted
else
Hashtbl.add g.table node_from [(node_to, arc_info)] ;
g.nodes <- l2 ;
g.trans <- (List.append g.trans [(node_from, arc_info, node_to)])
exception GraphError of string
let (get_list_of_target_nodes: ('a, 'b) t -> 'a -> ('a * 'b) list) =
(*
** [get_list_of_target_nodes g node] returns the list of target nodes
** starting from `node_from' in the graph `g'. Actually, it does not only
** return a list of nodes but a list of pairs `(node_to, arc_label)' where
** `arc_label' is the arc label of the arc from `node_from' to `node_to'.
*)
fun g node ->
try Hashtbl.find g.table node
with Not_found -> raise (GraphError "This node does not have any transition.")
let (get_all_nodes: ('a, 'b) t -> 'a list) =
(*
......
source/graph.mli
View file @ eb46e24b
......@@ -23,10 +23,11 @@ val create: unit -> ('a, 'b) t
*)
val add_trans: ('a, 'b) t -> 'a -> 'b -> 'a -> unit
val add_trans: ('a -> 'a -> int) -> ('a, 'b) t -> 'a -> 'b -> 'a -> unit
(**
[add_trans g node_from arc_info node_to] adds a transition from `node_from'
to `node_to' with arc label `arc_info' to the graph `g'.
to `node_to' with arc label `arc_info' to the graph `g'. [sort] is a comparison
function used to sort nodes.
*)
......
source/lurette.ml
View file @ eb46e24b
......@@ -19,8 +19,6 @@ open List
(* XXX set those via an option at command the line !!! *)
let step_by_step = false
let display_local_var = true
let print_vntl vl =
List.iter
......@@ -44,7 +42,9 @@ let (var_decl_are_inconsistent : vnt list -> vnt list -> unit) =
print_vntl out_env;
print_string "\nsut inputs: ";
print_vntl in_sut;
failwith "\n*** env outputs and sut inputs should be the same.\n"
print_string "\n*** env outputs and sut inputs should be the same.\n";
flush stdout ;
assert false
)
else if not(list_are_equals in_env out_sut) then
(
......@@ -52,7 +52,9 @@ let (var_decl_are_inconsistent : vnt list -> vnt list -> unit) =
print_vntl in_env;
print_string "\nsut outputs: ";
print_vntl out_sut;
failwith "\n*** env inputs and sut outputs should be the same.\n"
print_string "\n*** env inputs and sut outputs should be the same.\n";
flush stdout ;
assert false
)
else
()
......@@ -173,7 +175,9 @@ and
)
else Sim2chro.put_var_decl rif display_local_var;
main_loop 1 s n p rif Lurette_stub.sut_out_init ;
try main_loop 1 s n p rif Lurette_stub.sut_out_init
with Failure(errmsg) -> print_string errmsg
| e -> raise e ;
flush stdout;
flush rif;
......@@ -239,7 +243,7 @@ and
flush stdout;
flush rif;
Sim2chro.call_sim2chro ();
failwith ""
assert false
)
else ()
in
......
source/lurette.mli
View file @ eb46e24b
......@@ -13,4 +13,3 @@
open Env
val main : unit -> unit
source/parse_env.ml
View file @ eb46e24b
......@@ -31,132 +31,236 @@ let lexer = Genlex.make_lexer ["automata"; "["; "]"; "("; ")"; ","; ":"; ";";
type aut_token = Genlex.token Stream.t
let print_genlex_token =
fun tok ->
let _ =
match tok with
Genlex.Kwd(str) -> print_string str
| Genlex.Ident(str) -> print_string str
| Genlex.Int(i) -> print_int i
| Genlex.Float(f) -> print_float f
| Genlex.String(str) -> print_string str
| Genlex.Char(c) -> print_char c
in
print_string " "
(*
** Parsing lists
*)
let debug_parsing = false
let print_err_msg tok_list func =
if debug_parsing then
begin
print_string ("* Parse error in " ^ func ^ ".\n\t\t\t\t");
print_string ("The next 10 tokens are:\t``");
List.iter (print_genlex_token) tok_list ;
print_string ("''\n");
flush stdout
end
else ()
(** Parsing lists *)
let rec
(parse_list: (aut_token -> 'a) -> aut_token -> 'a list) =
fun parse tok ->
match tok with parser
[< vnt = parse ; tail = (parse_list_var_tail (parse)) >]
-> vnt :: tail
| [< >] -> [] (* empty list *)
let tok_list = Stream.npeek 10 tok in
try
match tok with parser
[< vnt = parse ; tail = (parse_list_var_tail (parse)) >]
-> vnt :: tail
| [< >] -> [] (* empty list *)
with e ->
print_err_msg tok_list "parse_list";
raise e
and (parse_list_var_tail: (aut_token -> 'a) -> aut_token -> 'a list) =
fun parse tok ->
match tok with parser
| [< 'Genlex.Kwd ";" ; a = parse ;
tail = (parse_list_var_tail (parse)) >]
-> a :: tail
| [< >] -> [] (* end of the list *)
let tok_list = Stream.npeek 10 tok in
try
match tok with parser
| [< 'Genlex.Kwd ";" ; a = parse ;
tail = (parse_list_var_tail (parse)) >]
-> a :: tail
| [< >] -> [] (* end of the list *)
with e ->
print_err_msg tok_list "parse_list_var_tail";
raise e
let rec (parse_automata: aut_token -> read_automata) =
fun tok ->
match tok with parser
[< 'Genlex.Kwd "automata" ;
'Genlex.Kwd "(" ;
'Genlex.Int node_id ; 'Genlex.Kwd "," ;
'Genlex.Kwd "[" ; li = parse_list_var ; 'Genlex.Kwd "]" ;
'Genlex.Kwd "," ;
'Genlex.Kwd "[" ; lo = parse_list_var ; 'Genlex.Kwd "]" ;
'Genlex.Kwd "," ;
'Genlex.Kwd "[" ; ll = parse_list_var ; 'Genlex.Kwd "]" ;
'Genlex.Kwd "," ;
'Genlex.Kwd "[" ; lpe = parse_list_pre_expr ; 'Genlex.Kwd "]" ;
'Genlex.Kwd "," ;
'Genlex.Kwd "[" ; lpf = parse_list_pre_form ; 'Genlex.Kwd "]" ;
'Genlex.Kwd "," ;