Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
verimag
synchrone
lutin
Commits
93a3a0ec
Commit
93a3a0ec
authored
May 28, 2010
by
Erwan Jahier
Browse files
Renaming Run_aut into FGen and Parse_luc int LucProg.
parent
bd904a00
Changes
42
Expand all
Hide whitespace changes
Inline
Side-by-side
lurette.prj
deleted
100644 → 0
View file @
bd904a00
This diff is collapsed.
Click to expand it.
source/Makefile.gen_fake_lucky
View file @
93a3a0ec
...
...
@@ -39,8 +39,8 @@ SOURCES = \
$(HERE)
/lustreExp.ml
\
$(HERE)
/parser.mly
\
$(HERE)
/lexer.mll
\
$(HERE)
/
parse_luc
.mli
\
$(HERE)
/
parse_luc
.ml
\
$(HERE)
/
lucProg
.mli
\
$(HERE)
/
lucProg
.ml
\
$(HERE)
/gen_stubs_common.mli
\
$(HERE)
/gen_stubs_common.ml
\
$(HERE)
/parse_c_scade.mli
\
...
...
source/Makefile.gen_stubs
View file @
93a3a0ec
...
...
@@ -40,8 +40,8 @@ SOURCES = \
$(HERE)
/lustreExp.ml
\
$(HERE)
/parser.mly
\
$(HERE)
/lexer.mll
\
$(HERE)
/
parse_luc
.mli
\
$(HERE)
/
parse_luc
.ml
\
$(HERE)
/
lucProg
.mli
\
$(HERE)
/
lucProg
.ml
\
$(HERE)
/gen_stubs_common.mli
\
$(HERE)
/gen_stubs_common.ml
\
\
...
...
source/Makefile.luc2c
View file @
93a3a0ec
...
...
@@ -43,7 +43,7 @@ SOURCES_OCAML = \
$(HERE)
/exp.ml
\
$(HERE)
/lustreExp.mli
$(HERE)
/lustreExp.ml
\
$(HERE)
/parser.mly
$(HERE)
/lexer.mll
\
$(HERE)
/
parse_luc
.mli
$(HERE)
/
parse_luc
.ml
\
$(HERE)
/
lucProg
.mli
$(HERE)
/
lucProg
.ml
\
$(HERE)
/env_state.mli
$(HERE)
/env_state.ml
\
$(HERE)
/luc2c.ml
...
...
source/Makefile.luc2luciole
View file @
93a3a0ec
...
...
@@ -43,7 +43,7 @@ SOURCES_OCAML = \
$(HERE)
/exp.ml
\
$(HERE)
/lustreExp.mli
$(HERE)
/lustreExp.ml
\
$(HERE)
/parser.mly
$(HERE)
/lexer.mll
\
$(HERE)
/
parse_luc
.mli
$(HERE)
/
parse_luc
.ml
\
$(HERE)
/
lucProg
.mli
$(HERE)
/
lucProg
.ml
\
$(HERE)
/gen_stubs_common.mli
\
$(HERE)
/gen_stubs_common.ml
\
$(HERE)
/parse_poc.mli
\
...
...
source/Makefile.luc4c
View file @
93a3a0ec
...
...
@@ -90,8 +90,8 @@ SOURCES = $(SOURCES_C) \
$(HERE)
/lexer.mll
\
$(HERE)
/gne.mli
\
$(HERE)
/gne.ml
\
$(HERE)
/
parse_luc
.mli
\
$(HERE)
/
parse_luc
.ml
\
$(HERE)
/
lucProg
.mli
\
$(HERE)
/
lucProg
.ml
\
$(HERE)
/polyhedron.mli
\
$(HERE)
/polyhedron.ml
\
$(HERE)
/formula_to_bdd.mli
\
...
...
@@ -110,8 +110,8 @@ SOURCES = $(SOURCES_C) \
$(HERE)
/solver.ml
\
$(HERE)
/show_env.mli
\
$(HERE)
/show_env.ml
\
$(HERE)
/
run_aut
.mli
\
$(HERE)
/
run_aut
.ml
\
$(HERE)
/
fGen
.mli
\
$(HERE)
/
fGen
.ml
\
$(HERE)
/print.mli
\
$(HERE)
/print.ml
\
$(HERE)
/sim2chro.mli
\
...
...
source/Makefile.luc4ocaml
View file @
93a3a0ec
...
...
@@ -80,8 +80,8 @@ SOURCES_OCAML = \
$(HERE)
/lexer.mll
\
$(HERE)
/gne.mli
\
$(HERE)
/gne.ml
\
$(HERE)
/
parse_luc
.mli
\
$(HERE)
/
parse_luc
.ml
\
$(HERE)
/
lucProg
.mli
\
$(HERE)
/
lucProg
.ml
\
$(HERE)
/polyhedron.mli
\
$(HERE)
/polyhedron.ml
\
$(HERE)
/env_state.mli
\
...
...
@@ -100,8 +100,8 @@ SOURCES_OCAML = \
$(HERE)
/solver.ml
\
$(HERE)
/show_env.mli
\
$(HERE)
/show_env.ml
\
$(HERE)
/
run_aut
.mli
\
$(HERE)
/
run_aut
.ml
\
$(HERE)
/
fGen
.mli
\
$(HERE)
/
fGen
.ml
\
$(HERE)
/print.mli
\
$(HERE)
/print.ml
\
$(HERE)
/sim2chro.mli
\
...
...
@@ -143,7 +143,7 @@ SOURCES_OCAML := \
$(HERE)
/parser.mly
\
$(HERE)
/lexer.mll
\
$(HERE)
/gne.ml
\
$(HERE)
/
parse_luc
.ml
\
$(HERE)
/
lucProg
.ml
\
$(HERE)
/polyhedron.ml
\
$(HERE)
/env_state.ml
\
$(HERE)
/formula_to_bdd.ml
\
...
...
@@ -153,7 +153,7 @@ SOURCES_OCAML := \
$(HERE)
/fair_bddd.ml
\
$(HERE)
/solver.ml
\
$(HERE)
/show_env.ml
\
$(HERE)
/
run_aut
.ml
\
$(HERE)
/
fGen
.ml
\
$(HERE)
/print.ml
\
$(HERE)
/sim2chro.ml
\
$(HERE)
/lucky.ml
\
...
...
source/Makefile.lucky
View file @
93a3a0ec
...
...
@@ -70,7 +70,7 @@ SOURCES_OCAML = \
$(HERE)
/parser.mly
\
$(HERE)
/lexer.mll
\
$(HERE)
/gne.ml
\
$(HERE)
/
parse_luc
.ml
\
$(HERE)
/
lucProg
.ml
\
$(HERE)
/polyhedron.ml
\
$(HERE)
/env_state.ml
\
$(HERE)
/formula_to_bdd.ml
\
...
...
@@ -80,7 +80,7 @@ SOURCES_OCAML = \
$(HERE)
/fair_bddd.ml
\
$(HERE)
/solver.ml
\
$(HERE)
/show_env.ml
\
$(HERE)
/
run_aut
.ml
\
$(HERE)
/
fGen
.ml
\
$(HERE)
/print.ml
\
$(HERE)
/sim2chro.ml
\
$(HERE)
/lucky.ml
\
...
...
@@ -129,8 +129,8 @@ SOURCES_OCAML := \
$(HERE)
/lexer.mll
\
$(HERE)
/gne.mli
\
$(HERE)
/gne.ml
\
$(HERE)
/
parse_luc
.mli
\
$(HERE)
/
parse_luc
.ml
\
$(HERE)
/
lucProg
.mli
\
$(HERE)
/
lucProg
.ml
\
$(HERE)
/polyhedron.mli
\
$(HERE)
/polyhedron.ml
\
$(HERE)
/formula_to_bdd.mli
\
...
...
@@ -149,8 +149,8 @@ SOURCES_OCAML := \
$(HERE)
/solver.ml
\
$(HERE)
/show_env.mli
\
$(HERE)
/show_env.ml
\
$(HERE)
/
run_aut
.mli
\
$(HERE)
/
run_aut
.ml
\
$(HERE)
/
fGen
.mli
\
$(HERE)
/
fGen
.ml
\
$(HERE)
/print.mli
\
$(HERE)
/print.ml
\
$(HERE)
/sim2chro.mli
\
...
...
source/Makefile.lucky.src
View file @
93a3a0ec
...
...
@@ -51,7 +51,7 @@ SOURCES = \
./parser.mly
\
./lexer.mll
\
./gne.ml
\
./
parse_luc
.ml
\
./
lucProg
.ml
\
./polyhedron.ml
\
./env_state.ml
\
./formula_to_bdd.ml
\
...
...
@@ -61,7 +61,7 @@ SOURCES = \
./fair_bddd.ml
\
./solver.ml
\
./show_env.ml
\
./
run_aut
.ml
\
./
fGen
.ml
\
./print.ml
\
./sim2chro.ml
\
./lucky.ml
\
...
...
@@ -117,8 +117,8 @@ SOURCES := \
./lexer.mll
\
./gne.mli
\
./gne.ml
\
./
parse_luc
.mli
\
./
parse_luc
.ml
\
./
lucProg
.mli
\
./
lucProg
.ml
\
./polyhedron.mli
\
./polyhedron.ml
\
./formula_to_bdd.mli
\
...
...
@@ -137,8 +137,8 @@ SOURCES := \
./solver.ml
\
./show_env.mli
\
./show_env.ml
\
./
run_aut
.mli
\
./
run_aut
.ml
\
./
fGen
.mli
\
./
fGen
.ml
\
./print.mli
\
./print.ml
\
./sim2chro.mli
\
...
...
source/Makefile.lucky2lus
View file @
93a3a0ec
...
...
@@ -35,7 +35,7 @@ SOURCES_OCAML = \
$(LURETTE_PATH)
/source/exp.ml
\
$(LURETTE_PATH)
/source/lustreExp.mli
$(LURETTE_PATH)
/source/lustreExp.ml
\
$(LURETTE_PATH)
/source/parser.mly
$(LURETTE_PATH)
/source/lexer.mll
\
$(LURETTE_PATH)
/source/
parse_luc
.mli
$(LURETTE_PATH)
/source/
parse_luc
.ml
\
$(LURETTE_PATH)
/source/
lucProg
.mli
$(LURETTE_PATH)
/source/
lucProg
.ml
\
$(LURETTE_PATH)
/source/lucky2lus.ml
SOURCES
=
$(SOURCES_OCAML)
...
...
source/Makefile.luckyDraw
View file @
93a3a0ec
...
...
@@ -69,7 +69,7 @@ SOURCES_OCAML = \
$(HERE)
/parser.mly
\
$(HERE)
/lexer.mll
\
$(HERE)
/gne.ml
\
$(HERE)
/
parse_luc
.ml
\
$(HERE)
/
lucProg
.ml
\
$(HERE)
/polyhedron.ml
\
$(HERE)
/formula_to_bdd.ml
\
$(HERE)
/store.ml
\
...
...
@@ -79,7 +79,7 @@ SOURCES_OCAML = \
$(HERE)
/fair_bddd.ml
\
$(HERE)
/solver.ml
\
$(HERE)
/show_env.ml
\
$(HERE)
/
run_aut
.ml
\
$(HERE)
/
fGen
.ml
\
$(HERE)
/print.ml
\
$(HERE)
/sim2chro.ml
\
$(HERE)
/lucky.ml
\
...
...
@@ -129,8 +129,8 @@ SOURCES_OCAML := \
$(HERE)
/lexer.mll
\
$(HERE)
/gne.mli
\
$(HERE)
/gne.ml
\
$(HERE)
/
parse_luc
.mli
\
$(HERE)
/
parse_luc
.ml
\
$(HERE)
/
lucProg
.mli
\
$(HERE)
/
lucProg
.ml
\
$(HERE)
/polyhedron.mli
\
$(HERE)
/polyhedron.ml
\
$(HERE)
/formula_to_bdd.mli
\
...
...
@@ -149,8 +149,8 @@ SOURCES_OCAML := \
$(HERE)
/solver.ml
\
$(HERE)
/show_env.mli
\
$(HERE)
/show_env.ml
\
$(HERE)
/
run_aut
.mli
\
$(HERE)
/
run_aut
.ml
\
$(HERE)
/
fGen
.mli
\
$(HERE)
/
fGen
.ml
\
$(HERE)
/print.mli
\
$(HERE)
/print.ml
\
$(HERE)
/sim2chro.mli
\
...
...
source/Makefile.lurette_debug
View file @
93a3a0ec
...
...
@@ -72,7 +72,7 @@ SOURCES = $(SOURCES_C) \
$(LURETTE_PATH)
/source/fair_bddd.ml
\
$(LURETTE_PATH)
/source/solver.ml
\
$(LURETTE_PATH)
/source/show_env.ml
\
$(LURETTE_PATH)
/source/
run_aut
.ml
\
$(LURETTE_PATH)
/source/
fGen
.ml
\
$(LURETTE_PATH)
/source/print.ml
\
$(LURETTE_PATH)
/source/sim2chro.ml
\
$(LURETTE_PATH)
/source/lucky.ml
\
...
...
source/Makefile.lurette_lib
View file @
93a3a0ec
...
...
@@ -89,8 +89,8 @@ SOURCES = $(SOURCES_C) \
$(HERE)
/lexer.mll
\
$(HERE)
/gne.mli
\
$(HERE)
/gne.ml
\
$(HERE)
/
parse_luc
.mli
\
$(HERE)
/
parse_luc
.ml
\
$(HERE)
/
lucProg
.mli
\
$(HERE)
/
lucProg
.ml
\
$(HERE)
/polyhedron.mli
\
$(HERE)
/polyhedron.ml
\
$(HERE)
/formula_to_bdd.mli
\
...
...
@@ -109,8 +109,8 @@ SOURCES = $(SOURCES_C) \
$(HERE)
/solver.ml
\
$(HERE)
/show_env.mli
\
$(HERE)
/show_env.ml
\
$(HERE)
/
run_aut
.mli
\
$(HERE)
/
run_aut
.ml
\
$(HERE)
/
fGen
.mli
\
$(HERE)
/
fGen
.ml
\
$(HERE)
/print.mli
\
$(HERE)
/print.ml
\
$(HERE)
/sim2chro.mli
\
...
...
source/Makefile.lurette_ocaml_lib
View file @
93a3a0ec
...
...
@@ -72,8 +72,8 @@ SOURCES = $(HERE)/util.ml \
$(HERE)
/lexer.mll
\
$(HERE)
/gne.mli
\
$(HERE)
/gne.ml
\
$(HERE)
/
parse_luc
.mli
\
$(HERE)
/
parse_luc
.ml
\
$(HERE)
/
lucProg
.mli
\
$(HERE)
/
lucProg
.ml
\
$(HERE)
/polyhedron.mli
\
$(HERE)
/polyhedron.ml
\
$(HERE)
/store.mli
\
...
...
@@ -92,8 +92,8 @@ SOURCES = $(HERE)/util.ml \
$(HERE)
/solver.ml
\
$(HERE)
/show_env.mli
\
$(HERE)
/show_env.ml
\
$(HERE)
/
run_aut
.mli
\
$(HERE)
/
run_aut
.ml
\
$(HERE)
/
fGen
.mli
\
$(HERE)
/
fGen
.ml
\
$(HERE)
/print.mli
\
$(HERE)
/print.ml
\
$(HERE)
/sim2chro.mli
\
...
...
source/Makefile.show_luc
View file @
93a3a0ec
...
...
@@ -42,7 +42,7 @@ SOURCES_OCAML = \
$(HERE)
/exp.ml
\
$(HERE)
/lustreExp.mli
$(HERE)
/lustreExp.ml
\
$(HERE)
/parser.mly
$(HERE)
/lexer.mll
\
$(HERE)
/
parse_luc
.mli
$(HERE)
/
parse_luc
.ml
\
$(HERE)
/
lucProg
.mli
$(HERE)
/
lucProg
.ml
\
$(HERE)
/show_env.mli
$(HERE)
/show_env.ml
\
$(HERE)
/show_luc.ml
...
...
source/env_state.ml
View file @
93a3a0ec
...
...
@@ -10,7 +10,7 @@
open
Util
open
List
open
Parse_luc
open
LucProg
open
Exp
...
...
@@ -38,7 +38,7 @@ type static_state_fields = {
type
dynamic_state_fields
=
{
memory
:
Var
.
subst
list
;
ctrl_state
:
Parse_luc
.
ctrl_state
list
;
ctrl_state
:
LucProg
.
ctrl_state
list
;
input
:
Var
.
subst
list
;
verbose
:
int
}
...
...
@@ -52,9 +52,9 @@ type t = {
(****************************************************************************)
open
Parse_luc
open
LucProg
let
(
label_to_node
:
string
->
string
->
Parse_luc
.
node
)
=
let
(
label_to_node
:
string
->
string
->
LucProg
.
node
)
=
fun
file
label
->
(* to avoid node label clashes, prepend the name of the file *)
let
...
...
@@ -220,7 +220,7 @@ let rec (list_insert : int -> ('a list -> 'a list -> 'a list) -> 'a list ->
let
(
read_env_state_one_automaton
:
t
->
Parse_luc
.
automata
->
t
)
=
let
(
read_env_state_one_automaton
:
t
->
LucProg
.
automata
->
t
)
=
fun
state
automata
->
(*
Updates [state] according to the content of automata. I.e., we merge
...
...
@@ -301,9 +301,9 @@ let (read_env_state_one_automaton : t -> Parse_luc.automata -> t) =
(w.r.t. the optionnal parameters) for the following reason :
to be able to type declarations such as
x : int ~default pre x
I create (in
Parse_luc
.parse_options_list) a fake variable
I create (in
LucProg
.parse_options_list) a fake variable
with the rigth name and type, but the wrong optionnal fields
(beurk !!!). Then
Parse_luc
.fill_var_options fix those fields
(beurk !!!). Then
LucProg
.fill_var_options fix those fields
in the exp_var_tbl, but not in the formula !!!
Hence, I do that now (altough it would have been better
...
...
@@ -491,7 +491,7 @@ let (read_env_state_one_automaton : t -> Parse_luc.automata -> t) =
let
_
=
let
all_nodes
=
fold_left
(
fun
acc
(
Parse_luc
.
Arc
(
nf0
,
_
,
nt0
))
->
(
fun
acc
(
LucProg
.
Arc
(
nf0
,
_
,
nt0
))
->
let
nt
=
label_to_node
file
nt0
and
nf
=
label_to_node
file
nf0
in
let
nf_node_info
=
{
...
...
@@ -542,11 +542,11 @@ let (read_env_state_one_automaton : t -> Parse_luc.automata -> t) =
(* updates [g]. *)
let
g'
=
let
(
add_arc
:
(
node
,
arc_info
)
Graph
.
t
->
Parse_luc
.
lucky_arc
->
let
(
add_arc
:
(
node
,
arc_info
)
Graph
.
t
->
LucProg
.
lucky_arc
->
(
node
,
arc_info
)
Graph
.
t
)
=
fun
acc
arc
->
match
arc
with
Parse_luc
.
Arc
(
node_from_str
,
arc_info
,
node_to_str
)
->
LucProg
.
Arc
(
node_from_str
,
arc_info
,
node_to_str
)
->
let
node_from
=
label_to_node
file
(
node_from_str
)
in
let
node_to
=
label_to_node
file
(
node_to_str
)
in
(
Graph
.
add_trans
acc
node_from
...
...
@@ -563,9 +563,9 @@ let (read_env_state_one_automaton : t -> Parse_luc.automata -> t) =
let
_
=
(
match
(
Util
.
no_dup
(
List
.
map
(
fun
(
Parse_luc
.
Arc
(
nf
,
_
,
_
))
->
nf
)
(
List
.
map
(
fun
(
LucProg
.
Arc
(
nf
,
_
,
_
))
->
nf
)
(
List
.
find_all
(
fun
(
Parse_luc
.
Arc
(
_
,
(
_
,
w
,_
)
,_
))
->
w
=
Infinity
)
(
fun
(
LucProg
.
Arc
(
_
,
(
_
,
w
,_
)
,_
))
->
w
=
Infinity
)
list_arcs
)
)
...
...
@@ -618,7 +618,7 @@ let (read_env_state_one_automaton : t -> Parse_luc.automata -> t) =
(* Exported *)
let
rec
(
read_env_state
:
bool
->
Parse_luc
.
automata
list
->
t
)
=
let
rec
(
read_env_state
:
bool
->
LucProg
.
automata
list
->
t
)
=
fun
is_reactive
automata_l
->
let
state0
=
{
...
...
@@ -648,7 +648,7 @@ let rec (read_env_state : bool -> Parse_luc.automata list -> t) =
List
.
fold_left
(
read_env_state_one_automaton
)
state0
automata_l
let
(
is_node_transient
:
Parse_luc
.
node
->
t
->
bool
)
=
let
(
is_node_transient
:
LucProg
.
node
->
t
->
bool
)
=
fun
n
state
->
try
(
Hashtbl
.
find
state
.
s
.
node
n
)
.
node_type
=
Transient
...
...
source/env_state.mli
View file @
93a3a0ec
...
...
@@ -18,7 +18,7 @@
*)
open
Parse_luc
open
LucProg
type
node_info
=
{
file_name
:
string
;
...
...
@@ -47,7 +47,7 @@ type static_state_fields = {
(** the dynamic part changes at each cycle. *)
type
dynamic_state_fields
=
{
memory
:
Var
.
subst
list
;
ctrl_state
:
Parse_luc
.
ctrl_state
list
;
ctrl_state
:
LucProg
.
ctrl_state
list
;
input
:
Var
.
subst
list
;
verbose
:
int
}
...
...
@@ -59,14 +59,14 @@ type t = {
}
val
read_env_state
:
bool
->
Parse_luc
.
automata
list
->
t
val
read_env_state
:
bool
->
LucProg
.
automata
list
->
t
(** [read_env_state is_reactive al] builds the initial state
from the list of parsed automata *)
(**/**)
val
is_node_transient
:
Parse_luc
.
node
->
t
->
bool
val
is_node_transient
:
LucProg
.
node
->
t
->
bool
(** outputs various statistic about the size of env_state tables *)
...
...
source/
run_aut
.ml
→
source/
fGen
.ml
View file @
93a3a0ec
...
...
@@ -4,7 +4,7 @@
** Public License
**-----------------------------------------------------------------------
**
** File:
run_aut
.ml
** File:
fGen
.ml
** Author: jahier@imag.fr
**
*)
...
...
@@ -16,12 +16,12 @@ open Var
open
Type
open
List
open
Util
(* open
Parse_luc
*)
(* open
LucProg
*)
open
Env_state
module
NodeMap
=
struct
include
Map
.
Make
(
struct
type
t
=
Parse_luc
.
node
let
compare
=
compare
end
)
include
Map
.
Make
(
struct
type
t
=
LucProg
.
node
let
compare
=
compare
end
)
end
(****************************************************************************)
...
...
@@ -36,21 +36,21 @@ type dyn_weight = V of int | Infin
*)
type
t
=
|
Cont
of
(
unit
->
t
*
Exp
.
formula
*
Parse_luc
.
ctrl_state
)
|
Cont
of
(
unit
->
t
*
Exp
.
formula
*
LucProg
.
ctrl_state
)
|
Finish
(* no more solutions *)
(** A wt (weigthed tree) is a n-ary tree *)
type
wt
=
children
NodeMap
.
t
*
Parse_luc
.
node
(* the top-level node of the wt *)
LucProg
.
node
(* the top-level node of the wt *)
and
children
=
|
Children
of
(
dyn_weight
*
Parse_luc
.
node
)
list
|
Children
of
(
dyn_weight
*
LucProg
.
node
)
list
|
Leave
of
Exp
.
formula
(** wt is traversed using continuations *)
type
wt_cont
=
|
WCont
of
(
unit
->
wt_cont
*
Exp
.
formula
*
Parse_luc
.
node
)
|
WCont
of
(
unit
->
wt_cont
*
Exp
.
formula
*
LucProg
.
node
)
|
WFinish
(* no more solutions *)
(****************************************************************************)
...
...
@@ -60,17 +60,17 @@ let dyn_weight_to_string =
V
i
->
string_of_int
i
|
Infin
->
"infinity"
let
(
compute_weight
:
Parse_luc
.
weight
->
Var
.
env_in
->
Env_state
.
t
->
dyn_weight
)
=
let
(
compute_weight
:
LucProg
.
weight
->
Var
.
env_in
->
Env_state
.
t
->
dyn_weight
)
=
fun
w
input
state
->
match
w
with
Parse_luc
.
Wint
(
i
)
->
V
i
|
Parse_luc
.
Infinity
->
Infin
|
Parse_luc
.
Wexpr
(
e
)
->
LucProg
.
Wint
(
i
)
->
V
i
|
LucProg
.
Infinity
->
Infin
|
LucProg
.
Wexpr
(
e
)
->
let
gne
=
Formula_to_bdd
.
num_to_gne
input
state
e
in
match
Gne
.
get_constant
gne
with
None
->
print_string
(
"*** The weight expression "
^
(
Parse_luc
.
weight_to_string
w
)
^
"*** The weight expression "
^
(
LucProg
.
weight_to_string
w
)
^
" ougth to depend only on pre and input vars
\n
"
);
exit
2
|
Some
(
Value
.
I
i
)
->
V
i
...
...
@@ -105,7 +105,7 @@ and
(****************************************************************************)
type
static_trans_list
=
(
Parse_luc
.
node
,
Parse_luc
.
arc_info
)
Graph
.
t
type
static_trans_list
=
(
LucProg
.
node
,
LucProg
.
arc_info
)
Graph
.
t
(** Computes the weigthed tree from the static graph
...
...
@@ -117,7 +117,7 @@ type static_trans_list = (Parse_luc.node, Parse_luc.arc_info) Graph.t
That ckeck at the beginning (just after parsing).
*)
let
rec
(
get_wt
:
Var
.
env_in
->
Env_state
.
t
->
Parse_luc
.
node
->
wt
)
=
let
rec
(
get_wt
:
Var
.
env_in
->
Env_state
.
t
->
LucProg
.
node
->
wt
)
=
fun
input
state
n
->
let
_
=
if
debug
then
(
print_string
(
"XXX get_wt "
^
n
^
"
\n
"
);
flush
stdout
)
in
let
g
=
state
.
s
.
graph
in
...
...
@@ -132,7 +132,7 @@ and
nb: it is safe to suppose that node does not begin by "__" because
I have renamed all nodes by adding the module name in parse_luc.
*)
(
rename_node
:
Parse_luc
.
node
->
int
NodeMap
.
t
->
Parse_luc
.
node
*
int
NodeMap
.
t
)
=
(
rename_node
:
LucProg
.
node
->
int
NodeMap
.
t
->
LucProg
.
node
*
int
NodeMap
.
t
)
=
fun
node0
tbl
->
let
node
=
try
get_original_name
node0
with
_
->
assert
false
in
let
res
=
...
...
@@ -148,7 +148,7 @@ and
res
and
(
get_original_name
:
Parse_luc
.
node
->
Parse_luc
.
node
)
=
(
get_original_name
:
LucProg
.
node
->
LucProg
.
node
)
=
fun
n
->
let
res
=
if
String
.
sub
n
0
1
<>
"_"
then
n
else
...
...
@@ -161,7 +161,7 @@ and
res
and
(
get_children
:
Var
.
env_in
->
Env_state
.
t
->
static_trans_list
->
Exp
.
formula
->
bool
->
Parse_luc
.
node
->
children
NodeMap
.
t
*
int
NodeMap
.
t
->
Exp
.
formula
->
bool
->
LucProg
.
node
->
children
NodeMap
.
t
*
int
NodeMap
.
t
->
children
NodeMap
.
t
*
int
NodeMap
.
t
)
=
fun
input
state
g
facc
toplevel
n0
(
tbl0
,
ntbl0
)
->
let
_
=
if
debug
then
(
print_string
(
"XXX get_children
\n
"
);
flush
stdout
)
in
...
...
@@ -224,14 +224,14 @@ and
exception
NoMoreFormula
let
(
call_cont
:
t
->
t
*
formula
*
Parse_luc
.
ctrl_state
)
=
let
(
call_cont
:
t
->
t
*
formula
*
LucProg
.
ctrl_state
)
=
fun
cont
->
let
_
=
if
debug
then
(
print_string
"XXX call_cont
\n
"
;
flush
stdout
)
in
match
cont
with
|
Cont
f
->
f
()
|
Finish
->
raise
NoMoreFormula
let
(
call_wt_cont
:
wt_cont
->
wt_cont
*
formula
*
Parse_luc
.
node
)
=
let
(
call_wt_cont
:
wt_cont
->
wt_cont
*
formula
*
LucProg
.
node
)
=
fun
cont
->
let
_
=
if
debug
then
(
print_string
"XXX call_wt_cont
\n
"
;
flush
stdout
)
in
match
cont
with
...
...
@@ -239,7 +239,7 @@ let (call_wt_cont : wt_cont -> wt_cont * formula * Parse_luc.node) =
|
WFinish
->
WFinish
,
False
,
""
(* exported *)
let
(
choose_one_formula
:
t
->
t
*
Exp
.
formula
*
Parse_luc
.
ctrl_state
)
=
call_cont
let
(
choose_one_formula
:
t
->
t
*
Exp
.
formula
*
LucProg
.
ctrl_state
)
=
call_cont
(****************************************************************************)
...
...
@@ -258,7 +258,7 @@ let (get_all_formula: t -> formula list) =
let
rec
(
wt_list_to_cont
:
Var
.
env_in
->
Env_state
.
t
->
wt_cont
list
->
formula
->
Parse_luc
.
ctrl_state
->
t
->
t
)
=
formula
->
LucProg
.
ctrl_state
->
t
->
t
)
=
fun
input
state
wtl
facc
nl
fgen
->
(* [nl] is the list of nodes that correspond to [facc] *)
let
_
=
if
debug
then
(
print_string
"XXX wt_list_to_cont
\n
"
;
flush
stdout
)
in
...
...
@@ -279,7 +279,7 @@ let rec (wt_list_to_cont : Var.env_in -> Env_state.t -> wt_cont list ->
wt_list_to_cont
input
state
wtl'
f2
(
n
::
nl
)
fgen'
and
(
choose_one_formula_atomic
:
Var
.
env_in
->
Env_state
.
t
->
Exp
.
formula
->
wt_cont
->
wt_cont
*
formula
*
Parse_luc
.
node
)
=
Exp
.
formula
->
wt_cont
->
wt_cont
*
formula
*
LucProg
.
node
)
=
fun
input
state
facc
cont
->
let
_
=
if
debug
then
(
print_string
"XXX choose_one_formula_atomic
\n
"
;
flush
stdout
)
in
if
cont
=
WFinish
then
...
...
@@ -360,7 +360,7 @@ and (wt_to_cont : Var.env_in -> Env_state.t -> wt -> wt_cont -> wt_cont) =
(****************************************************************************)
(* exported *)
let
(
get
:
Var
.
env_in
->
Env_state
.
t
->
Parse_luc
.
ctrl_state
list
->
t
list
)
=
let
(
get
:
Var
.
env_in
->
Env_state
.
t
->
LucProg
.
ctrl_state
list
->
t
list
)
=
fun
input
state
nll
->
let
_
=
if
debug
then
(
print_string
"XXX get
\n
"
;
flush
stdout
)
in
List
.
map
...
...
source/
run_aut
.mli
→
source/
fGen
.mli
View file @
93a3a0ec
...
...
@@ -4,7 +4,7 @@
** Public License
**-----------------------------------------------------------------------
**
** File:
run_aut
.mli
** File:
fGen
.mli
** Author: jahier@imag.fr
*)
...
...
@@ -14,7 +14,7 @@
type
t
(** This abstract datatype is used to hold sub-automaton of the
(static) parsed Lucky automaton (cf the [
Parse_luc
] module). It
(static) parsed Lucky automaton (cf the [
LucProg
] module). It
contains the sub-automaton made of transitions accessible from the
current node, where formulas and weights have been evaluated w.r.t
current inputs and memories. Such automata are recomputed at each
...
...
@@ -57,7 +57,7 @@ type t
*)
val
get
:
Var
.
env_in
->
Env_state
.
t
->
Parse_luc
.
ctrl_state
list
->
t
list
val
get
:
Var
.
env_in
->
Env_state
.
t
->
LucProg
.
ctrl_state
list
->
t
list
(** [get input state ctrl_state] computes the sub-automata of the
global Lucky automaton made of the accessible nodes from nodes in
[ctrl_state]. Automata obtained from inner lists of nodes (in
...
...
@@ -72,7 +72,7 @@ val get : Var.env_in -> Env_state.t -> Parse_luc.ctrl_state list -> t list
(** Raised by choose_one_formula no more transitions can be taken *)
exception
NoMoreFormula