Commit 483092d0 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Minor naming change: node list are now called ctrl_state, to look more «abstract».

parent 412ff9e0
......@@ -24,12 +24,18 @@ clean:
.PHONY: test
test:
cd example ; make test
cia: test
cia: test cia_notest
cia_notest:
git commit -a -F log
amend:
git commit -a -F log --amend
ci: test
git commit -F log
......@@ -43,7 +49,7 @@ ldiff:
diff:
git diff HEAD -w > diff.diff
echo "il y a $(shell grep "+" diff.diff | wc -l) + et $(shell grep "-" diff.diff | wc -l) -"
touch:
cd test && make touch
......
......@@ -609,6 +609,11 @@ luc4c-doc:
-html -d $(SYNCHRONE_DIR)/lurette/doc/luc4c/ \
-I ocamldoc -I .. luc4c.mli
##############################################################################"
dot:
make -f Makefile.lucky dot
##############################################################################"
gen_lustre:
make -k nc -f Makefile.gen_lustre OCAMLFLAGS="-noassert -unsafe"
......@@ -800,3 +805,5 @@ test:
cd ../examples && make test
time:
cd ../test && make time
xx:
echo $(SOURCES)
\ No newline at end of file
......@@ -42,10 +42,12 @@ USE_CAMLP4 = yes
HERE=./
SOURCES_OCAML = \
SOURCES_C = \
$(HERE)/liblutin_c.c \
$(HERE)/liblutin.idl \
$(HERE)/Ezdl_c.c \
SOURCES_OCAML = \
$(HERE)/Ezdl.ml \
$(HERE)/error.ml \
$(HERE)/version.ml \
......@@ -89,9 +91,6 @@ SOURCES_OCAML = \
ifndef MLONLY
SOURCES_OCAML := \
$(HERE)/liblutin_c.c \
$(HERE)/liblutin.idl \
$(HERE)/Ezdl_c.c \
$(HERE)/Ezdl.ml \
$(HERE)/Ezdl.mli \
$(HERE)/error.ml \
......@@ -171,7 +170,7 @@ SOURCES_OCAML := \
endif
SOURCES = $(SOURCES_OCAML)
SOURCES = $(SOURCES_C) $(SOURCES_OCAML)
RESULT = lucky
......@@ -186,7 +185,12 @@ src :
cp -rf ../examples/lucky examples
cp -rf ../GBDDML lucky-src/
cp -rf ../polka lucky-src/
cp $(SOURCES_OCAML) lucky-src/source
cp $(SOURCES) lucky-src/source
cp ../OcamlMakefile.orig lucky-src/OcamlMakefile
cp Makefile.lucky.src lucky-src/source/Makefile
tar cvfz lucky-src-$(VERSION).tgz lucky-src
\ No newline at end of file
tar cvfz lucky-src-$(VERSION).tgz lucky-src
dot:
ocamldoc -o lucky.dot -dot -dot-include-all -dot-reduce $(filter %.ml, $(SOURCES_OCAML))
dot -Tpdf lucky.dot > lucky.pdf
......@@ -38,7 +38,7 @@ type static_state_fields = {
type dynamic_state_fields = {
memory : Var.subst list;
current_nodes : node list list ;
ctrl_state : Parse_luc.ctrl_state list;
input : Var.subst list;
verbose : int
}
......@@ -244,7 +244,7 @@ let (read_env_state_one_automaton : t -> Parse_luc.automata -> t) =
and node_tbl = state.s.node
and g = state.s.graph
and current_nodes0 = state.d.current_nodes
and ctrl_state0 = state.d.ctrl_state
in
(* Merge the external function tables *)
......@@ -482,8 +482,8 @@ let (read_env_state_one_automaton : t -> Parse_luc.automata -> t) =
let nvll = list_insert n merge_var nvl_current nvll0 in
let init_node_current = label_to_node file init_node_str in
let current_nodes = list_insert n (Util.merge) [init_node_current]
current_nodes0 in
let ctrl_state = list_insert n (Util.merge) [init_node_current]
ctrl_state0 in
let mnl = rev_append pre_vars mnl0 in
......@@ -596,7 +596,7 @@ let (read_env_state_one_automaton : t -> Parse_luc.automata -> t) =
}
and dsf = {
memory = state.d.memory;
current_nodes = current_nodes;
ctrl_state = ctrl_state;
input = [];
verbose = state.d.verbose
}
......@@ -639,7 +639,7 @@ let rec (read_env_state : bool -> Parse_luc.automata list -> t) =
d =
{
memory = [];
current_nodes = [];
ctrl_state = [];
input = [];
verbose = 0
}
......
......@@ -47,7 +47,7 @@ type static_state_fields = {
(** the dynamic part changes at each cycle. *)
type dynamic_state_fields = {
memory : Var.subst list;
current_nodes : node list list ;
ctrl_state : Parse_luc.ctrl_state list;
input : Var.subst list;
verbose : int
}
......
......@@ -30,7 +30,7 @@ let rec (lookup: Var.env_in -> Env_state.t -> Exp.var -> Value.t option) =
( try
Some(Var.get_val_env_in input (Var.name var))
with _ ->
let cnl = List.flatten state.d.current_nodes in
let cnl = List.flatten state.d.ctrl_state in
let nodes_str = String.concat " " cnl in
let node_msg =
if
......@@ -74,7 +74,7 @@ let rec (lookup: Var.env_in -> Env_state.t -> Exp.var -> Value.t option) =
" is not valid.\n");
exit 2
| None ->
let cnl = List.flatten state.d.current_nodes in
let cnl = List.flatten state.d.ctrl_state in
let nodes_str = String.concat " " cnl in
let node_msg =
if
......
......@@ -109,7 +109,7 @@ let (make : string -> string -> lucky_process) =
let init_state_dyn =
{
memory = state0.d.memory;
current_nodes = state0.d.current_nodes;
ctrl_state = state0.d.ctrl_state;
input = state0.d.input;
verbose = state0.d.verbose
}
......@@ -183,7 +183,7 @@ let (step: lucky_process -> step_mode -> unit) =
);
match state_of_lp lp with
| Some (st0,inp,_outp) ->
let ral = Run_aut.get inp st0 st0.d.current_nodes in
let ral = Run_aut.get inp st0 st0.d.ctrl_state in
let (st, (outs, _locs)) =
try
Lucky.env_step
......@@ -195,7 +195,7 @@ let (step: lucky_process -> step_mode -> unit) =
List.iter
(fun n ->
output_string stdout ("# current node: " ^ n ^ "\n "))
(List.flatten st0.d.current_nodes);
(List.flatten st0.d.ctrl_state);
flush stdout;
raise e
in
......@@ -251,7 +251,7 @@ let (set_verbose : lucky_process -> int -> unit) =
Some (state, inputs, outputs) ->
let dsf = {
memory = state.d.memory;
current_nodes = state.d.current_nodes;
ctrl_state = state.d.ctrl_state;
input = state.d.input;
verbose = v
}
......@@ -269,7 +269,7 @@ let (add_subst_in_inputs : Env_state.t -> Var.subst -> Env_state.t) =
fun st s ->
{ d = {
memory = st.d.memory;
current_nodes = st.d.current_nodes;
ctrl_state = st.d.ctrl_state;
input = s::(st.d.input);
verbose = st.d.verbose
};
......
......@@ -57,7 +57,7 @@ let (make : ?seed:(int) -> ?fair:(bool) -> ?pp:(string) -> ?verbose:(int) ->
let init_state_dyn =
{
memory = state0.d.memory;
current_nodes = state0.d.current_nodes;
ctrl_state = state0.d.ctrl_state;
input = state0.d.input;
verbose = verbose
}
......@@ -131,7 +131,7 @@ let (convert_inputs_back : Var.env_in -> subst list) =
let step ?(mode = StepInside) st0 inputs =
let inp = convert_inputs inputs in
let ral = Run_aut.get inp st0 st0.d.current_nodes in
let ral = Run_aut.get inp st0 st0.d.ctrl_state in
let (st, (outs, locs)) =
try
Lucky.env_step
......@@ -143,7 +143,7 @@ let step ?(mode = StepInside) st0 inputs =
List.iter
(fun n ->
output_string stdout ("# current node: " ^ n ^ "\n "))
(List.flatten st0.d.current_nodes);
(List.flatten st0.d.ctrl_state);
flush stdout;
raise e
in
......
......@@ -185,7 +185,7 @@ and
let init_state_dyn =
{
memory = state0.d.memory;
current_nodes = state0.d.current_nodes;
ctrl_state = state0.d.ctrl_state;
input = state0.d.input;
verbose = options.verb
}
......@@ -250,7 +250,7 @@ and
if options.show_automata then (
if
(Show_env.luc_to_dot (flatten init_state.d.current_nodes) []
(Show_env.luc_to_dot (flatten init_state.d.ctrl_state) []
("automata" ^ (string_of_int (Hashtbl.hash Sys.argv)))
init_state.s.graph) = 0
then
......@@ -273,7 +273,7 @@ and
let next_state =
if options.boot then
let htbl = (Hashtbl.create 0) in
let ral = Run_aut.get htbl init_state init_state.d.current_nodes in
let ral = Run_aut.get htbl init_state init_state.d.ctrl_state in
let (next_state, (out, loc)) =
try
Lucky.env_step options.draw_mode htbl init_state ral
......@@ -282,7 +282,7 @@ and
List.iter
(fun n ->
output_string stdout ("# current node: " ^ (string_of_node n) ^ "\n"))
(List.flatten init_state.d.current_nodes);
(List.flatten init_state.d.ctrl_state);
print_string (
"# No transition is labelled by a satisfiable formula.\n" ^
"# The Lucky automata is blocked.\n");
......@@ -309,7 +309,7 @@ and
and
main_loop t state =
let nl = List.flatten state.d.current_nodes in
let nl = List.flatten state.d.ctrl_state in
let step_str =
(
("#step " ^ (string_of_int t)) ^
......@@ -338,7 +338,7 @@ and
in
let (input, state') = Rif.read stdin state in
let input_list = Hashtbl.fold (fun vn x acc -> (vn,x)::acc) input [] in
let ral = Run_aut.get input state' state.d.current_nodes in
let ral = Run_aut.get input state' state.d.ctrl_state in
let (next_state, (out, loc)) =
try
Lucky.env_step options.draw_mode input state' ral
......@@ -347,7 +347,7 @@ and
List.iter
(fun n ->
output_string stdout ("# current node: " ^ (string_of_node n) ^ "\n"))
(List.flatten state.d.current_nodes);
(List.flatten state.d.ctrl_state);
print_string (
"# No transition is labelled by a satisfiable formula.\n" ^
"# The Lucky automata is blocked.\n");
......@@ -386,10 +386,10 @@ and
print_string "\n";
if options.show_automata then (
if (state.d.current_nodes <> next_state.d.current_nodes) then
if (state.d.ctrl_state <> next_state.d.ctrl_state) then
if
(Show_env.luc_to_dot (flatten next_state.d.current_nodes)
(flatten state.d.current_nodes)
(Show_env.luc_to_dot (flatten next_state.d.ctrl_state)
(flatten state.d.ctrl_state)
("automata" ^ (string_of_int (Hashtbl.hash Sys.argv)))
next_state.s.graph) <> 0
then
......
......@@ -20,21 +20,21 @@ open Env_state
(****************************************************************************)
(****************************************************************************)
type nl = node list
type nll = node list list
type cs = Parse_luc.ctrl_state
type csl = cs list
type sl = subst list
(****************************************************************************)
let (draw_values : Var.env_in -> Env_state.t -> int ->
Thickness.numeric -> Run_aut.t list ->
Run_aut.t list * node list list * (sl * sl) list) =
Run_aut.t list * csl * (sl * sl) list) =
fun input state p num_thickness ral ->
let bool_to_gen_l = state.s.bool_vars_to_gen
and num_to_gen_l = state.s.num_vars_to_gen
in
let rec (draw_values_atomic : int -> Exp.var list -> Exp.var list ->
Run_aut.t -> Run_aut.t * node list * (sl * sl) list) =
Run_aut.t -> Run_aut.t * cs * (sl * sl) list) =
fun p bool_to_gen num_to_gen ra ->
let bool_to_gen_f =
if bool_to_gen = [] then True else
......@@ -43,22 +43,22 @@ let (draw_values : Var.env_in -> Env_state.t -> int ->
(Bvar(hd bool_to_gen))
(tl bool_to_gen)
in
let (ra', f, nl) = Run_aut.choose_one_formula ra in
let (ra', f, cs) = Run_aut.choose_one_formula ra in
match
Solver.solve_formula input state p num_thickness f
bool_to_gen_f num_to_gen
with
| [] -> draw_values_atomic p bool_to_gen num_to_gen ra'
| outs_locs_l -> (ra', nl, outs_locs_l)
| outs_locs_l -> (ra', cs, outs_locs_l)
in
let ra_nl_slsll_l =
let ra_cs_slsll_l =
Util.list_map3 (draw_values_atomic p) bool_to_gen_l num_to_gen_l ral
in
let (ra0 ,nl0, slsl0) = List.hd ra_nl_slsll_l in
let (ral', nll, sl1_sl2_l) =
let (ra0 ,cs0, slsl0) = List.hd ra_cs_slsll_l in
let (ral', csl, sl1_sl2_l) =
(* unknitting ...*)
List.fold_left
(fun (ral, nll, sl1_sl2_l) (ra, nl, slsll) ->
(fun (ral, csl, sl1_sl2_l) (ra, cs, slsll) ->
let sl1_sl2_l' =
List.map2
(fun (slacc1, slacc2) (sl1,sl2) ->
......@@ -67,12 +67,12 @@ let (draw_values : Var.env_in -> Env_state.t -> int ->
sl1_sl2_l
slsll
in
(ra::ral, nl::nll, sl1_sl2_l')
(ra::ral, cs::csl, sl1_sl2_l')
)
([ra0] ,[nl0], slsl0)
(List.tl ra_nl_slsll_l)
([ra0] ,[cs0], slsl0)
(List.tl ra_cs_slsll_l)
in
(List.rev ral', List.rev nll, sl1_sl2_l)
(List.rev ral', List.rev csl, sl1_sl2_l)
(****************************************************************************)
......@@ -149,28 +149,28 @@ let previous_local = ref None
let (env_try_do : Thickness.formula_draw_nb * Thickness.numeric -> env_in ->
Env_state.t -> Run_aut.t list -> (env_out * env_loc) list ->
Run_aut.t list * node list list * (env_out * env_loc) list) =
Run_aut.t list * csl * (env_out * env_loc) list) =
fun (p, num_thickness) input state ral acc ->
let ral', nll', sol = (draw_values input state p num_thickness ral) in
ral', nll', (rev_append acc sol)
let ral', csl', sol = (draw_values input state p num_thickness ral) in
ral', csl', (rev_append acc sol)
(* Exported *)
let (env_try : Thickness.t -> env_in -> Env_state.t -> Run_aut.t list ->
Run_aut.t list * (env_out * env_loc) list) =
fun (bt,nt) input state ral ->
(* let ral = Run_aut.get input state state.d.current_nodes in *)
(* let ral = Run_aut.get input state state.d.ctrl_state in *)
if fst bt then
(* try all formula *)
let rec f ral acc =
try
let ral', _nll, acc' = env_try_do (snd bt,nt) input state ral acc in
let ral', _csl, acc' = env_try_do (snd bt,nt) input state ral acc in
f ral' acc'
with
Run_aut.LuckyEnd -> ral,acc
in
f ral []
else
let (ral', _nll, sol) = env_try_do (snd bt,nt) input state ral [] in
let (ral', _csl, sol) = env_try_do (snd bt,nt) input state ral [] in
ral', sol
(*****************************************************************************)
......@@ -185,11 +185,11 @@ let (env_step : step_mode -> env_in -> Env_state.t -> Run_aut.t list ->
| StepVertices -> (0, 0, Thickness.AtMost 1)
in
try
let (_ral', nll, soll) = env_try_do (1, thick) input state ral [] in
let (_ral', csl, soll) = env_try_do (1, thick) input state ral [] in
let (output, local) = List.hd soll in
let new_state_dyn = {
memory = update_pre input output local state;
current_nodes = nll;
ctrl_state = csl;
input = Var.inputs_to_list input;
verbose = state.d.verbose
}
......
......@@ -265,7 +265,7 @@ let (solve : bool_expr -> solutions_set) =
{
d = {
memory = [];
current_nodes = [] ;
ctrl_state = [] ;
input = [] ;
verbose = 0
} ;
......
......@@ -462,7 +462,7 @@ and
let init_state_dyn =
{
memory = state0.d.memory;
current_nodes = state0.d.current_nodes;
ctrl_state = state0.d.ctrl_state;
input = state0.d.input;
verbose = options.verb
}
......@@ -508,7 +508,7 @@ and
| Some i ->
step_cpt := i; (* so that it stops at the first step *)
if
(Show_env.luc_to_dot (flatten init_state.d.current_nodes) []
(Show_env.luc_to_dot (flatten init_state.d.ctrl_state) []
("environment" ^ (soi (Hashtbl.hash Sys.argv)))
init_state.s.graph) = 0
then
......@@ -705,7 +705,7 @@ and
and
main_loop t s p k1 k2 k3 rif input state write_luciole_inputs read_luciole_outputs luciole_outputs =
let ral = Run_aut.get input state state.d.current_nodes in
let ral = Run_aut.get input state state.d.ctrl_state in
let _ =
if (k1 = 0 && k2 = 0 && k3 = 0 && not(options.draw_all_vertices)) then
()
......@@ -725,7 +725,7 @@ and
List.iter
(fun n ->
output_string stdout ("# current node: " ^ (string_of_node n) ^ "\n "))
(List.flatten state.d.current_nodes);
(List.flatten state.d.ctrl_state);
flush stdout;
lurette_exit 2
in
......@@ -757,7 +757,7 @@ and
List.iter
(fun n ->
output_string stdout ("# current node: " ^ (string_of_node n) ^ "\n "))
(List.flatten state.d.current_nodes);
(List.flatten state.d.ctrl_state);
flush stdout;
lurette_exit 2
in
......@@ -816,7 +816,7 @@ and
List.iter
(fun n ->
output_string stdout ("current node:" ^ (string_of_node n) ^ "\n "))
(List.flatten state.d.current_nodes);
(List.flatten state.d.ctrl_state);
flush stdout
in
let str =
......@@ -824,12 +824,12 @@ and
Some i ->
let skip = (i - !step_cpt > 0) in
if (not skip
(* && state.d.current_nodes <> next_state.d.current_nodes *)
(* && state.d.ctrl_state <> next_state.d.ctrl_state *)
) then
(
let _err_code = (Show_env.luc_to_dot
(flatten next_state.d.current_nodes)
(flatten state.d.current_nodes)
(flatten next_state.d.ctrl_state)
(flatten state.d.ctrl_state)
("environment" ^ (soi (Hashtbl.hash Sys.argv)))
state.s.graph
)
......
......@@ -467,7 +467,7 @@ and
let init_state_dyn =
{
memory = state0.d.memory;
current_nodes = state0.d.current_nodes;
ctrl_state = state0.d.ctrl_state;
input = state0.d.input;
verbose = options.verb
}
......@@ -519,7 +519,7 @@ and
| Some i ->
step_cpt := i; (* so that it stops at the first step *)
if
(Show_env.luc_to_dot (flatten init_state.d.current_nodes) []
(Show_env.luc_to_dot (flatten init_state.d.ctrl_state) []
("environment" ^ (string_of_int (Hashtbl.hash Sys.argv)))
init_state.s.graph) = 0
then
......@@ -586,7 +586,7 @@ and
List.iter
(fun n ->
output_string stdout ("current nodes:" ^ (string_of_node n) ^ "\n "))
(List.flatten state.d.current_nodes);
(List.flatten state.d.ctrl_state);
flush stdout
in
let _ =
......@@ -635,11 +635,11 @@ and
match (options.step_by_step) with
Some i ->
let skip = (i - !step_cpt > 0) in
if (not skip && state.d.current_nodes <> next_state.d.current_nodes) then
if (not skip && state.d.ctrl_state <> next_state.d.ctrl_state) then
(
let err_code = (Show_env.luc_to_dot
(flatten next_state.d.current_nodes)
(flatten state.d.current_nodes)
(flatten next_state.d.ctrl_state)
(flatten state.d.ctrl_state)
("environment" ^ (string_of_int (Hashtbl.hash Sys.argv)))
state.s.graph
)
......
......@@ -467,7 +467,7 @@ and
let init_state_dyn =
{
memory = state0.d.memory;
current_nodes = state0.d.current_nodes;
ctrl_state = state0.d.ctrl_state;
input = state0.d.input;
verbose = options.verb
}
......@@ -519,7 +519,7 @@ and
| Some i ->
step_cpt := i; (* so that it stops at the first step *)
if
(Show_env.luc_to_dot (flatten init_state.d.current_nodes) []
(Show_env.luc_to_dot (flatten init_state.d.ctrl_state) []
("environment" ^ (string_of_int (Hashtbl.hash Sys.argv)))
init_state.s.graph) = 0
then
......@@ -586,7 +586,7 @@ and
List.iter
(fun n ->
output_string stdout ("current nodes:" ^ (string_of_node n) ^ "\n "))
(List.flatten state.d.current_nodes);
(List.flatten state.d.ctrl_state);
flush stdout
in
let _ =
......@@ -636,12 +636,12 @@ and
Some i ->
let skip = (i - !step_cpt > 0) in
if (not skip
(* && state.d.current_nodes <> next_state.d.current_nodes *)
(* && state.d.ctrl_state <> next_state.d.ctrl_state *)
) then
(
let err_code = (Show_env.luc_to_dot
(flatten next_state.d.current_nodes)
(flatten state.d.current_nodes)
(flatten next_state.d.ctrl_state)
(flatten state.d.ctrl_state)
("environment" ^ (string_of_int (Hashtbl.hash Sys.argv)))
state.s.graph
)
......
......@@ -53,6 +53,7 @@ type weight =
type node_type = Transient | Stable | Final
type node = string
type ctrl_state = node list
type arc = node * node
......
......@@ -100,6 +100,7 @@ type source_info = (string * int * int) option
type arc_info = source_info * weight * Exp.formula
type ctrl_state = node list
type lucky_arc = Arc of node * arc_info * node
......
......@@ -16,12 +16,12 @@ open Var
open Type