Skip to content

GitLab

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

update lus2lic + minor changes

parent 951ddbcf
Hide whitespace changes
Inline Side-by-side
Makefile.common.source
View file @ fbd316f5
......@@ -255,8 +255,6 @@ LURETTE_SOURCES=\
$(OBJDIR)/graph.mli \
$(OBJDIR)/myGenlex.mli \
$(OBJDIR)/myGenlex.ml \
$(OBJDIR)/gnuplotRif.mli \
$(OBJDIR)/gnuplotRif.ml \
$(OBJDIR)/Ezdl.ml \
$(OBJDIR)/Ezdl.mli \
$(OBJDIR)/type.ml \
......@@ -370,7 +368,6 @@ LUTIN_SOURCES = \
$(OBJDIR)/lutProg.mli \
$(OBJDIR)/lucProg.ml \
$(OBJDIR)/lucProg.mli \
$(OBJDIR)/luciole.ml \
$(OBJDIR)/luc2alice.ml \
$(OBJDIR)/luc2c.mli \
$(OBJDIR)/luc2c.ml \
......
Makefile.version
View file @ fbd316f5
# well, finally, set it manually...
VERSION:=1.56
VERSION:=1.57
#
# When incrementing that version number, please don't forget to
# fill-in the RELEASE-NOTES file (using the git history).
......
source/Lucky/luc2c.ml
View file @ fbd316f5
......@@ -996,7 +996,7 @@ let (main : Exp.var list -> Exp.var list -> Exp.var list -> unit) =
exit 2
);
let var_to_vn_ct v = (Var.name v, Type.to_cstring (Var.typ v)) in
Luciole.gen_stubs false fn
Luciole.gen_stubs fn
(List.map var_to_vn_ct ins)
(List.map var_to_vn_ct outs)
| Scade -> ()
......
source/Lucky/luc2luciole.ml
View file @ fbd316f5
......@@ -138,7 +138,7 @@ let rec (main : unit -> 'a) =
let luciole_outputs = List.sort compare luciole_outputs in
let luciole_inputs = List.sort compare luciole_inputs in
let sut_str = Filename.basename (Filename.chop_extension flag.sut_header) in
Luciole.gen_stubs true sut_str luciole_outputs luciole_inputs
Luciole.gen_stubs sut_str luciole_outputs luciole_inputs
with e ->
......
source/Lurettetop/Makefile.comon
View file @ fbd316f5
......@@ -120,7 +120,7 @@ LUSTRE_SOURCES = \
$(OBJDIR)/licMetaOp.ml \
$(OBJDIR)/ast2lic.mli \
$(OBJDIR)/ast2lic.ml \
$(OBJDIR)/misc.ml \
$(OBJDIR)/lv6Misc.ml \
$(OBJDIR)/l2lCheckKcgKeyWord.ml \
$(OBJDIR)/l2lCheckMemSafe.mli \
$(OBJDIR)/l2lCheckMemSafe.ml \
......@@ -144,8 +144,8 @@ LUSTRE_SOURCES = \
$(OBJDIR)/l2lSplit.ml \
$(OBJDIR)/licTab.ml \
$(OBJDIR)/licTab.mli \
$(OBJDIR)/compile.mli \
$(OBJDIR)/compile.ml \
$(OBJDIR)/lv6Compile.mli \
$(OBJDIR)/lv6Compile.ml \
......
source/Lurettetop/ldbg.ml
View file @ fbd316f5
......@@ -24,7 +24,7 @@ let set_gnuplot b = LtopArg.args.LtopArg.display_gnuplot <- b
let set_sim2chro b = LtopArg.args.LtopArg.display_sim2chro <- b
let run () =
Event.event_nb :=0;
Event.set_nb 0;
RunDirect.start ()
let next e = e.next()
let terminate e = e.terminate
......
source/Lutin/META 0 → 100644
View file @ fbd316f5
version = "1"
description = "an API to call the Lutin interpreter from ocaml"
requires = "str unix num rdbg-plugin"
archive(byte) = "lut4ocaml.cma"
archive(byte, plugin) = "lut4ocaml.cma"
archive(native) = "lut4ocaml.cmxa"
archive(native, plugin) = "lut4ocaml.cmxs"
exists_if = "lut4ocaml.cma"
source/Lutin/Makefile.lutin
View file @ fbd316f5
......@@ -12,8 +12,8 @@ ifneq ($(HOSTTYPE),Darwin-x86_64)
#STATIC=yes
endif
OCAMLFLAGS += -I $(OBJDIR) -I $(OCAMLLIB) -I $(PREFIX)/$(HOSTTYPE)/lib
OCAMLFLAGS += -I +rdbg-plugin
OCAMLFLAGS +=-I $(OBJDIR) -I $(OCAMLLIB) -I $(PREFIX)/$(HOSTTYPE)/lib
OCAMLFLAGS += -I +oUnit2 -I +rdbg-plugin
IDLFLAGS=-nocpp
......@@ -27,7 +27,7 @@ OCAMLLDFLAGS= -cclib -lstdc++ -cclib -I/usr/lib/w32api $(OCAMLOPTFLAG) \
-cclib -l$(POLKA)_caml \
-cclib -l$(POLKA) -cclib -lgmp
endif
OCAMLLDFLAGS += -I +rdbg-plugin
OCAMLLDFLAGS += -I +ounit2 -I +rdbg-plugin
CC= $(GCC) $(DWIN32) -fPIC
......
source/Lutin/lutExe.ml
View file @ fbd316f5
......@@ -551,7 +551,7 @@ let add_to_guard_nc it data (e:CoAlgExp.t) (acc:guard) (si:CoTraceExp.src_info)
let add_to_guard it data (e:CoAlgExp.t) (acc:guard) (si:CoTraceExp.src_info) = (
let res = add_to_guard_nc it data e acc si in
if (check_satisfiablity it res) then res
else raise (Deadlock !Event.event_nb)
else raise (Deadlock (Event.get_nb()))
)
(** Tries to compute a value in a context *)
......@@ -751,660 +751,660 @@ let put_in_para te1 te2 = (
)
let rec genpath
(it : t)
(data : store) (* data env = inputs + pres *)
(x : CoTraceExp.t) (* control = lutin trace *)
= (
(*-------------------------------------------*)
(* Correspondance id de trace -> trace exp
(it : t)
(data : store) (* data env = inputs + pres *)
(x : CoTraceExp.t) (* control = lutin trace *)
= (
(*-------------------------------------------*)
(* Correspondance id de trace -> trace exp
N.B. on traque les récursions ? *)
(*-------------------------------------------*)
(*-------------------------------------------*)
let xenv = it.expanded_code in
let id2trace s =
(Util.hfind (Expand.trace_tab xenv) s).Expand.ti_def_exp
in
(*-------------------------------------------*
* Fonction récursive :
* --------------------------------------------*)
(*-------------------------------------------*
* Fonction récursive :
* --------------------------------------------*)
let rec rec_genpath br = (
let data = br.br_data in
let x = br.br_ctrl in
let acc = br.br_acc in
let cont = br.br_cont in
Verbose.exe ~level:2 ~flag:dbg
(fun _ ->
Printf.fprintf stderr "++REC_GENTRANS:\n" ;
Printf.fprintf stderr "|> CTRL: %s\n" (string_of_control_state br.br_ctrl);
Printf.fprintf stderr " CONT:\n";
List.iter (fun c -> Printf.fprintf stderr " %s;\n" (string_of_cont_mnemo c)) br.br_cont.dbg;
Printf.fprintf stderr "--------\n";
);
(fun _ ->
Printf.fprintf stderr "++REC_GENTRANS:\n" ;
Printf.fprintf stderr "|> CTRL: %s\n" (string_of_control_state br.br_ctrl);
Printf.fprintf stderr " CONT:\n";
List.iter (fun c -> Printf.fprintf stderr " %s;\n" (string_of_cont_mnemo c)) br.br_cont.dbg;
Printf.fprintf stderr "--------\n";
);
match br.br_ctrl with
(** Aliased trace *)
| TE_ref s -> (rec_genpath ({br with br_ctrl = id2trace s}))
(** Leaves: apply cont *)
| TE_raise s -> cont.doit (Raise s)
| TE_eps -> cont.doit Vanish
(** No eps: forbids e to vanish (but not to raise !) *)
| TE_noeps e -> (
let noeps_cont = mk_cont
(fun a ->
Verbose.exe ~flag:dbg
(fun () ->
Printf.printf
"-- noeps_cont (%s)\n in context %s\n"
(string_of_behavior a) (string_of_control_state x));
match a with
| Vanish -> raise (Deadlock !Event.event_nb)
| z -> cont.doit z
(*
(** Aliased trace *)
| TE_ref s -> (rec_genpath ({br with br_ctrl = id2trace s}))
(** Leaves: apply cont *)
| TE_raise s -> cont.doit (Raise s)
| TE_eps -> cont.doit Vanish
(** No eps: forbids e to vanish (but not to raise !) *)
| TE_noeps e -> (
let noeps_cont = mk_cont
(fun a ->
Verbose.exe ~flag:dbg
(fun () ->
Printf.printf
"-- noeps_cont (%s)\n in context %s\n"
(string_of_behavior a) (string_of_control_state x));
match a with
| Vanish -> raise (Deadlock (Event.get_nb()))
| z -> cont.doit z
(*
| Vanish -> raise Deadlock
| _ -> cont a
*)
) (Cnoeps) cont in
rec_genpath ({br with br_ctrl=e; br_cont=noeps_cont})
)
*)
) (Cnoeps) cont in
rec_genpath ({br with br_ctrl=e; br_cont=noeps_cont})
)
(** Constraint: ~same but solve the conjunction first *)
| TE_constraint (ae,si) -> (
let new_acc = add_to_guard it data ae acc si in
ignore(Event.incr_nb ()); (* try *)
ignore(Event.incr_nb ()); (* sat *)
cont.doit (Goto (new_acc, TE_eps))
(* n.b. raise Deadlock if impossible *)
)
(** Sequence *)
| TE_fby (te1, te2) -> (
let fby_cont = mk_cont (fun a ->
Verbose.exe ~flag:dbg
(fun () ->
Printf.printf
"-- fby_cont (%s)\n in context %s\n"
(string_of_behavior a)
(string_of_control_state x));
match a with
| Goto (cl,n) -> cont.doit (Goto (cl, put_in_seq n te2))
| Vanish -> rec_genpath ({br with br_ctrl=te2 })
| Raise _ -> cont.doit a
) (Cfby te2) cont in
rec_genpath ({br with br_ctrl=te1; br_cont=fby_cont})
)
(** Priority:
(** Constraint: ~same but solve the conjunction first *)
| TE_constraint (ae,si) -> (
let new_acc = add_to_guard it data ae acc si in
ignore(Event.incr_nb ()); (* try *)
ignore(Event.incr_nb ()); (* sat *)
cont.doit (Goto (new_acc, TE_eps))
(* n.b. raise Deadlock if impossible *)
)
(** Sequence *)
| TE_fby (te1, te2) -> (
let fby_cont = mk_cont (fun a ->
Verbose.exe ~flag:dbg
(fun () ->
Printf.printf
"-- fby_cont (%s)\n in context %s\n"
(string_of_behavior a)
(string_of_control_state x));
match a with
| Goto (cl,n) -> cont.doit (Goto (cl, put_in_seq n te2))
| Vanish -> rec_genpath ({br with br_ctrl=te2 })
| Raise _ -> cont.doit a
) (Cfby te2) cont in
rec_genpath ({br with br_ctrl=te1; br_cont=fby_cont})
)
(** Priority:
Deadlock is catched HERE
*)
| TE_prio [] -> raise (Deadlock !Event.event_nb)
| TE_prio (te::tel) -> (
try (
rec_genpath ({br with br_ctrl=te})
) with Deadlock _ -> (
*)
| TE_prio [] -> raise (Deadlock (Event.get_nb()))
| TE_prio (te::tel) -> (
try (
rec_genpath ({br with br_ctrl=te})
) with Deadlock _ -> (
ignore( Event.incr_nb ()); (* try *)
ignore( Event.incr_nb ()); (* usat *)
rec_genpath ({br with br_ctrl=(TE_prio tel)})
)
)
(** Try similar to a recurse priority *)
| TE_try (e,eco) -> (
let try_cont = mk_cont (fun a ->
Verbose.exe ~flag:dbg
(fun () ->
Printf.printf
"-- try_cont (%s)\n in context %s\n"
(string_of_behavior a)
(string_of_control_state x));
match a with
| Goto (cl,n) -> cont.doit (Goto (cl, TE_try (n,eco)))
| _ -> cont.doit a
) (Ctry eco) cont in
try (
rec_genpath ({br with br_ctrl=e; br_cont=try_cont})
) with Deadlock _ -> (
)
(** Try similar to a recurse priority *)
| TE_try (e,eco) -> (
let try_cont = mk_cont (fun a ->
Verbose.exe ~flag:dbg
(fun () ->
Printf.printf
"-- try_cont (%s)\n in context %s\n"
(string_of_behavior a)
(string_of_control_state x));
match a with
| Goto (cl,n) -> cont.doit (Goto (cl, TE_try (n,eco)))
| _ -> cont.doit a
) (Ctry eco) cont in
try (
rec_genpath ({br with br_ctrl=e; br_cont=try_cont})
) with Deadlock _ -> (
let ec = match eco with
| Some e' -> e'
| None -> TE_eps
in
rec_genpath ({br with br_ctrl=ec})
)
)
(** INFINITE WEAK LOOP *)
(* must behaves exactly as: (te\eps fby loop te) |> eps *)
| TE_loop te -> (
let e' =
TE_prio [
)
(** INFINITE WEAK LOOP *)
(* must behaves exactly as: (te\eps fby loop te) |> eps *)
| TE_loop te -> (
let e' =
TE_prio [
put_in_seq (TE_noeps te) (TE_loop te)
;
;
TE_eps
]
in
rec_genpath ({br with br_ctrl=e'})
)
(** INFINITE STRONG LOOP *)
(* must behaves exactly as: (te\eps fby omega te) *)
| TE_omega te -> (
let e' = put_in_seq (TE_noeps te) (TE_omega te)
in
rec_genpath ({br with br_ctrl=e'})
)
(** ASSERT *)
(* default assert is WEAK for backward compatibility
in
rec_genpath ({br with br_ctrl=e'})
)
(** INFINITE STRONG LOOP *)
(* must behaves exactly as: (te\eps fby omega te) *)
| TE_omega te -> (
let e' = put_in_seq (TE_noeps te) (TE_omega te)
in
rec_genpath ({br with br_ctrl=e'})
)
(** ASSERT *)
(* default assert is WEAK for backward compatibility
must behave EXACTLY as
trap STOP in (te fby raise STOP) &> omega a
*)
| TE_assert (a, te, si) -> (
let stopid = CoIdent.get_fresh (Expand.ident_space xenv) "Stop_loop" in
let e' = TE_catch (
stopid,
put_in_para
(put_in_seq te (TE_raise stopid))
(TE_omega (TE_constraint (a,si)))
,
None
) in
rec_genpath ({br with br_ctrl=e'})
)
(** STRONG ASSERT *)
(* must behave EXACTLY as
*)
| TE_assert (a, te, si) -> (
let stopid = CoIdent.get_fresh (Expand.ident_space xenv) "Stop_loop" in
let e' = TE_catch (
stopid,
put_in_para
(put_in_seq te (TE_raise stopid))
(TE_omega (TE_constraint (a,si)))
,
None
) in
rec_genpath ({br with br_ctrl=e'})
)
(** STRONG ASSERT *)
(* must behave EXACTLY as
trap STOP in omega a &> (te fby raise STOP)
*)
| TE_strong_assert (a, te, si) -> (
let stopid = CoIdent.get_fresh (Expand.ident_space xenv) "Stop_loop" in
let e' = TE_catch (
stopid,
put_in_para
(TE_omega (TE_constraint (a,si)))
(put_in_seq te (TE_raise stopid))
,
None
) in
rec_genpath ({br with br_ctrl=e'})
)
(** Exist: problem modifies the data and support, and the cont *)
| TE_exist (ectx, te) -> (
let addp inpres (id, eo) = (
match eo with
| None -> inpres
| Some e -> (
(* first translate to lucky ... *)
let v = try compute_exp it data e
with Not_a_constant msg -> raise (Internal_error ("LutExe.add_pres",
("initial value of \""^id^"\" ("^msg^")must be a uncontrolable expression")))
in Value.OfIdent.add inpres (id, v)
*)
| TE_strong_assert (a, te, si) -> (
let stopid = CoIdent.get_fresh (Expand.ident_space xenv) "Stop_loop" in
let e' = TE_catch (
stopid,
put_in_para
(TE_omega (TE_constraint (a,si)))
(put_in_seq te (TE_raise stopid))
,
None
) in
rec_genpath ({br with br_ctrl=e'})
)
(** Exist: problem modifies the data and support, and the cont *)
| TE_exist (ectx, te) -> (
let addp inpres (id, eo) = (
match eo with
| None -> inpres
| Some e -> (
(* first translate to lucky ... *)
let v = try compute_exp it data e
with Not_a_constant msg -> raise (Internal_error ("LutExe.add_pres",
("initial value of \""^id^"\" ("^msg^")must be a uncontrolable expression")))
in Value.OfIdent.add inpres (id, v)
)
) in
let new_pres = List.fold_left addp data.pres ectx in
let new_data = {data with pres=new_pres} in
rec_genpath ({br with br_ctrl=te; br_data = new_data })
)
(** Parallel: at least one ? *)
| TE_para ([]) -> assert false
| TE_para ([e]) -> rec_genpath ({br with br_ctrl = e })
| TE_para (e::el) -> (
(* continuation for the head statement *)
let para_head_cont =
mk_cont
( fun a ->
Verbose.exe ~flag:dbg
(fun () ->
Printf.printf "-- para_head_cont (%s)\n in context %s\n"
(string_of_behavior a) (string_of_control_state x));
match a with
(* 1st raises s: whole raises s *)
| Raise s -> ( cont.doit (Raise s) )
(* 1st vanishes: others continue *)
| Vanish -> (
rec_genpath ({br with br_ctrl = TE_para(el)})
)
) in
let new_pres = List.fold_left addp data.pres ectx in
let new_data = {data with pres=new_pres} in
rec_genpath ({br with br_ctrl=te; br_data = new_data })
)
(** Parallel: at least one ? *)
| TE_para ([]) -> assert false
| TE_para ([e]) -> rec_genpath ({br with br_ctrl = e })
| TE_para (e::el) -> (
(* continuation for the head statement *)
let para_head_cont =
mk_cont
( fun a ->
Verbose.exe ~flag:dbg
(fun () ->
Printf.printf "-- para_head_cont (%s)\n in context %s\n"
(string_of_behavior a) (string_of_control_state x));
match a with
(* 1st raises s: whole raises s *)
| Raise s -> ( cont.doit (Raise s) )
(* 1st vanishes: others continue *)
| Vanish -> (
rec_genpath ({br with br_ctrl = TE_para(el)})
)
(* 1st do a trans ... *)
| Goto (cl,n) -> (
let para_tail_cont =
mk_cont
(fun a ->
match a with
(* others vanish, 1st continue *)
| Vanish -> ( cont.doit (Goto (cl,n)) )
(* others raise -> forbidden *)
| Raise s -> ( raise (Deadlock !Event.event_nb) )
| Goto (tcl, tn) -> (
(* N.B. cl IS ALREADY accumulated in tcl *)
cont.doit (Goto (tcl, put_in_para n tn))
)
) (Cpara_tail (cl, n)) cont in try (
(* N.B. cl CONTAINS incoming acc, thus it becomes the whole rec_acc *)
let tail_acc = cl in
(*** BIG BUG: the other_brs IS NOT THE RIGHT ONE ->
(* 1st do a trans ... *)
| Goto (cl,n) -> (
let para_tail_cont =
mk_cont
(fun a ->
match a with
(* others vanish, 1st continue *)
| Vanish -> ( cont.doit (Goto (cl,n)) )
(* others raise -> forbidden *)
| Raise s -> ( raise (Deadlock (Event.get_nb())) )
| Goto (tcl, tn) -> (
(* N.B. cl IS ALREADY accumulated in tcl *)
cont.doit (Goto (tcl, put_in_para n tn))
)
) (Cpara_tail (cl, n)) cont in try (
(* N.B. cl CONTAINS incoming acc, thus it becomes the whole rec_acc *)
let tail_acc = cl in
(*** BIG BUG: the other_brs IS NOT THE RIGHT ONE ->
SHOULD BE THE ONE REACHED WHEN THE Goto (cl,n) WAS GENERATED !!!
***)
rec_genpath ({br with br_ctrl= TE_para(el); br_acc=tail_acc; br_cont=para_tail_cont})
) with Deadlock nb -> (
(* HERE: nothing to do ? *)
raise (Deadlock nb)
)
)
) (Cpara_head (TE_para el)) cont in
rec_genpath ({br with br_ctrl=e; br_cont=para_head_cont})
)
***)
rec_genpath ({br with br_ctrl= TE_para(el); br_acc=tail_acc; br_cont=para_tail_cont})
) with Deadlock nb -> (
(* HERE: nothing to do ? *)
raise (Deadlock nb)
)
)
) (Cpara_head (TE_para el)) cont in
rec_genpath ({br with br_ctrl=e; br_cont=para_head_cont})
)
(** Catch *)
| TE_catch (i,e,eco) -> (
let catch_cont =
mk_cont
(fun a ->
Verbose.exe ~flag:dbg
(fun () ->
Printf.printf
"-- catch_cont (%s)\n in context %s\n"
(string_of_behavior a) (string_of_control_state x));
match a with
| Goto (cl,n) -> cont.doit (Goto (cl, TE_catch(i, n, eco)))
| Raise x -> (
if ( x == i) then (
match eco with
| None -> cont.doit Vanish
| Some ec -> (
rec_genpath ({br with br_ctrl=ec })
)
) else cont.doit (Raise x)
)
| _ -> cont.doit a
) (Ccatch (i,eco)) cont in
rec_genpath ({br with br_ctrl=e ; br_cont=catch_cont})
)
(** Probabilistic choice
(** Catch *)
| TE_catch (i,e,eco) -> (
let catch_cont =
mk_cont
(fun a ->
Verbose.exe ~flag:dbg
(fun () ->
Printf.printf
"-- catch_cont (%s)\n in context %s\n"
(string_of_behavior a) (string_of_control_state x));
match a with
| Goto (cl,n) -> cont.doit (Goto (cl, TE_catch(i, n, eco)))
| Raise x -> (
if ( x == i) then (
match eco with
| None -> cont.doit Vanish
| Some ec -> (