Skip to content

GitLab

Commit 32f5edd6 authored by Pascal Raymond's avatar Pascal Raymond
Browse files

Merge /home/jahier/lurette

parents b311ed64 826aa62e
Hide whitespace changes
Inline Side-by-side
Makefile
View file @ 32f5edd6
......@@ -24,10 +24,12 @@ build: gen_version
cd source && make clean && make install&& cd ..&&\
ln -sf pre_release/$(HOSTTYPE) && \
cd install && autoconf && cd .. &&\
make lus2lic && \
./RUN_ME
lus2lic:
cp `which lus2lic` $(BIN_INSTALL_DIR)
#
clean:
cd polka; make clean; cd ..
......@@ -54,7 +56,7 @@ amend-a:
amend:
git commit -F log --amend && make gen_version
ci: test
ci:
git commit -F log && make gen_version
......
doc/lutin-man/Makefile
View file @ 32f5edd6
......@@ -10,7 +10,7 @@ SRCS=./commands.tex \
./lutin_examples.tex \
./objs/lutyacc.tex \
./objs/version.tex \
./objs/lutin.tex ./objs/gnuplotrif.tex \
./objs/lutin.tex ./objs/gnuplotrif.tex ./objs/checkrif.tex \
./objs/foo.c.tex \
./objs/call_external_c_code.lut.tex \
./objs/polar.lut.tex \
......@@ -51,7 +51,10 @@ lutin-man.pdf: objs/main.pdf
./objs/gnuplotrif.tex:objs
gnuplot-rif --help 2> $@
gnuplot-rif --help &> $@
./objs/checkrif.tex:objs
check-rif --help &> $@
touch.tex:
......
doc/lutin-man/commands.tex
View file @ 32f5edd6
......@@ -83,6 +83,8 @@
\newcommand{\simtochrogtk}{{\sc Sim2chrogtk}\xspace}
\newcommand{\luciole}{{\sc Luciole}\xspace}
\newcommand{\gnuplotrif}{{\sc Gnuplot-rif}\xspace}
\newcommand{\checkrif}{{\sc check-rif}\xspace}
\newcommand{\ecexe}{{\sc ecexe}\xspace}
\newcommand{\Ocaml}{{\sc Ocaml}\xspace}
\newcommand{\ocaml}{{\sc Ocaml}\xspace}
doc/lutin-man/lutin_toplevel.tex
View file @ 32f5edd6
......@@ -90,6 +90,16 @@ inputs. From a lutin-centric point of view, a \lutin program could use
A complete example can be found in {\tt examples/lutin/xlurette}.
\subsubsection{\checkrif}
A tool that performs post-mortem oracle checking using the
Lustre expanded code (.ec) interpreter \ecexe.
Here is the output of {\tt check-rif --help}:
\begin{alltt}
\input{checkrif}
\end{alltt}
\subsubsection{\simtochro}
\simtochro is a program written par Yann R\'emond that displays
......
examples/lutin/C/test2.rif.exp 0 → 100644
View file @ 32f5edd6
#inputs "a":int "b":bool "c":real
#outputs "x":int "y":bool "z":real
# step 1
1 1 1.000000 #outs -1 1 -1.810000
# step 2
2 0 2.000000 #outs 6 0 5.690000
# step 3
3 1 3.000000 #outs 2 1 7.030000
# step 4
4 0 4.000000 #outs 5 0 2.970000
# step 5
5 1 5.000000 #outs 4 1 9.810000
# step 6
6 0 6.000000 #outs 10 1 1.990000
# step 7
7 1 7.000000 #outs 9 1 4.600000
# step 8
8 0 8.000000 #outs 11 0 4.150000
# step 9
9 1 9.000000 #outs 8 1 5.030000
examples/lutin/up_and_down/ud.lut
View file @ 32f5edd6
let delta= 5.
let between(x, min, max : real) : bool = ((min < x) and (x < max))
let up (x : real ref) : bool = between(x, pre x, pre x + delta)
let down(x : real ref) : bool = between(x, pre x - delta, pre x)
let up (delta:real; x : real ref) : bool = between(x, pre x, pre x + delta)
let down(delta:real; x : real ref) : bool = between(x, pre x - delta, pre x)
node main () returns (x : real) =
let min = 0. in
let max= 100. in
let up_and_down(min, max, delta : real ; x : real ref) : trace =
between(x, min, max)
fby
fby
loop {
| loop { up(delta, x) and pre x < max }
| loop { down(delta, x) and pre x > min }
}
node main () returns (x : real) =
loop {
| loop { up(x) and pre x < max }
| loop { down(x) and pre x > min }
}
\ No newline at end of file
up_and_down(0.0, 100.0, 5.0, x)
examples/lutin/xlurette/Makefile
View file @ 32f5edd6
......@@ -31,7 +31,7 @@ clean:
test_dontgo:
rm -f test.rif0 .lurette_rc
$(LURETTETOP) --output test.rif0 degradable-sensors.luc && \
$(LURETTETOP) --output test.rif0 env.lut && \
grep -v "lurette chronogram" test.rif0 | \
grep -v "The execution lasted"| sed -e "s/^M//" > test.rif &&\
rm -f test.res && diff -B -u -i test.rif.exp test.rif > test.res
......
install/configure.in
View file @ 32f5edd6
......@@ -14,21 +14,7 @@ unset LC_ALL LC_CTYPE LC_COLLATE LC_MESSAGES LC_MONETARY LC_NUMERIC LC_TIME
# Determine the system type
case `./config.guess` in
i*86-pc-linux-*)
case `gcc -dumpversion` in
5.*)
echo "HOST_TYPE=i386-linux-gcc3"
HOST_TYPE=i386-linux-gcc3 ;;
4.*)
echo "HOST_TYPE=i386-linux-gcc3"
HOST_TYPE=i386-linux-gcc3 ;;
3.*)
echo "HOST_TYPE=i386-linux-gcc3"
HOST_TYPE=i386-linux-gcc3 ;;
*)
echo "HOST_TYPE=i386-linux"
HOST_TYPE=i386-linux ;;
esac;;
i*86-pc-linux-*) HOST_TYPE=linux ;;
sparc-sun-solaris2.*) HOST_TYPE=sparc-sun ;;
i*86-*-cygwin) HOST_TYPE=cygwin ;;
i*86-apple*) HOST_TYPE=mac ;;
......@@ -366,9 +352,9 @@ AC_OUTPUT(Makefile.lurette set_env_var xlurette.sh lurettetop.sh show_luc.sh ge
install -D -v ../$HOSTTYPE/bin/* "$LURETTEPATH/bin/"
install -D -v ../$HOSTTYPE/lib/* "$LURETTEPATH/lib/"
install -D -v ../$HOSTTYPE/include/* "$LURETTEPATH/include/"
install -D -v ../$HOST_TYPE/bin/* "$LURETTEPATH/bin/"
install -D -v ../$HOST_TYPE/lib/* "$LURETTEPATH/lib/"
install -D -v ../$HOST_TYPE/include/* "$LURETTEPATH/include/"
install ./Makefile.lurette "$LURETTEPATH/lib/Makefile.lurette"
......
install/set_env_var.in
View file @ 32f5edd6
......@@ -57,7 +57,7 @@ fi
if test -z "$HOSTTYPE" ; then
HOSTTYPE=@HOSTTYPE@
HOSTTYPE=@HOST_TYPE@
export HOSTTYPE
fi
......
source/Gnuplot-rif/gnuplot-rif.ml
View file @ 32f5edd6
......@@ -364,7 +364,7 @@ let gen_plot_file rif_file vars to_hide ttbl file tk =
flush stderr;
put ("
# defaults
set data style steps
set style data steps
set pointsize 0.2
set grid back
set xtics "^xtics^" mirror
......@@ -607,7 +607,7 @@ let (gv: string -> unit) =
(********************************************************************************)
let terminal = ref NoDisplay
let terminal = ref Wxt
let rif_file = ref ""
let plot_file = ref ""
......
source/Lucky/Makefile.luc4c
View file @ 32f5edd6
......@@ -130,6 +130,8 @@ SOURCES = $(SOURCES_C) \
$(OBJDIR)/lucFGen.ml \
$(OBJDIR)/print.mli \
$(OBJDIR)/print.ml \
$(OBJDIR)/rif_base.mli \
$(OBJDIR)/rif_base.ml \
$(OBJDIR)/rif.mli \
$(OBJDIR)/rif.ml \
$(OBJDIR)/sim2chro.mli \
......
source/Lucky/Makefile.luc4ocaml
View file @ 32f5edd6
......@@ -104,6 +104,8 @@ SOURCES_OCAML = \
$(OBJDIR)/lucFGen.ml \
$(OBJDIR)/print.mli \
$(OBJDIR)/print.ml \
$(OBJDIR)/rif_base.mli \
$(OBJDIR)/rif_base.ml \
$(OBJDIR)/rif.mli \
$(OBJDIR)/rif.ml \
$(OBJDIR)/sim2chro.mli \
......
source/Lucky/Makefile.lucky
View file @ 32f5edd6
......@@ -111,6 +111,8 @@ SOURCES_OCAML0:= \
$(OBJDIR)/lucFGen.ml \
$(OBJDIR)/print.mli \
$(OBJDIR)/print.ml \
$(OBJDIR)/rif_base.mli \
$(OBJDIR)/rif_base.ml \
$(OBJDIR)/rif.mli \
$(OBJDIR)/rif.ml \
$(OBJDIR)/sim2chro.mli \
......
source/Lucky/Makefile.show_luc
View file @ 32f5edd6
......@@ -110,6 +110,8 @@ SOURCES_OCAML := \
$(OBJDIR)/lucFGen.ml \
$(OBJDIR)/print.mli \
$(OBJDIR)/print.ml \
$(OBJDIR)/rif_base.mli \
$(OBJDIR)/rif_base.ml \
$(OBJDIR)/rif.mli \
$(OBJDIR)/rif.ml \
$(OBJDIR)/sim2chro.mli \
......
source/Lucky/luc2alice.ml
View file @ 32f5edd6
......@@ -20,6 +20,7 @@ type alice_args = {
env_in_vars : Exp.var list;
env_out_vars : Exp.var list;
use_sockets: bool;
output_dir:string;
}
......@@ -106,14 +107,15 @@ let (gen_alice_var_tab : string -> string -> Exp.var list -> string) =
let (gen_alice_stub : alice_args -> string) =
fun args ->
let alice_name = args.alice_module_name
let alice_full_name = args.alice_module_name
and alice_name = Filename.basename args.alice_module_name
and fn = args.env_name
and in_vars = args.env_in_vars
and out_vars = args.env_out_vars
in
("
#include \""^alice_name^".h\"
#include \""^alice_full_name^".h\"
#include \"float.h\"
#include \"Ims/ImsMessageStack.h\"
......@@ -223,10 +225,14 @@ structTab* "^alice_name^"::Memories() {
")
let my_open_out fn =
prerr_string ("Generating file " ^ fn ^ "\n");
open_out fn
let (gen_alice_stub_c : alice_args -> unit) =
fun args ->
let oc = open_out (args.alice_module_name ^ ".cpp") in
let amn = Filename.basename args.alice_module_name in
let oc = my_open_out (Filename.concat args.output_dir (amn ^ ".cpp")) in
let put s = output_string oc s in
let putln s = output_string oc (s^"\n") in
let rec putlist = function
......@@ -240,15 +246,22 @@ let (gen_alice_stub_c : alice_args -> unit) =
let (gen_alice_stub_h : alice_args -> unit) =
fun args ->
let amn = args.alice_module_name in
let oc = open_out (amn ^ ".h") in
let amn = Filename.basename args.alice_module_name in
let oc = my_open_out (Filename.concat args.output_dir (amn ^ ".h")) in
let amn = Filename.basename args.alice_module_name in
let putln s = output_string oc (s^"\n") in
let fn = args.env_name in
putln (Util.entete "// ");
putln ("
#include \"AlicesCommon.h\"
#define "^amn^"_interface LINKER_EXPORTED
#ifdef BUILD_"^amn^"
#define "^amn^"_interface LINKER_EXPORTED
#else // BUILD_"^amn^"
#define "^amn^"_interface LINKER_IMPORTED
#endif // BUILD_"^amn^"
extern \"C\"
{
......
source/Lucky/luc2c.ml
View file @ 32f5edd6
......@@ -24,36 +24,51 @@ let step_mode_to_str = function
| Vertices -> "step_vertices"
type optionT = {
mutable pp : string option;
mutable env : string list;
mutable main_node : string option; (* Main node *)
mutable boot : bool;
mutable pp : string option; (* Pre-processor *)
mutable output : string option;
mutable rif : string option;
mutable calling_module_name : string;
mutable gen_mode : gen_mode;
mutable use_sockets : bool;
mutable step_mode : step_mode;
mutable seed : int option;
mutable env : string list;
mutable sock_addr : string
mutable precision : int option;
mutable use_sockets : bool;
mutable sock_addr : string;
mutable output_dir : string;
}
let (option : optionT) = {
env = [];
main_node = None;
pp = None;
boot = false;
output = None;
rif = None;
gen_mode = Nop;
use_sockets = false;
calling_module_name = "XXX_SCADE_MODULE_NAME";
step_mode = Inside;
seed = None;
env = [];
sock_addr = "127.0.0.1"
precision = None;
sock_addr = "127.0.0.1";
output_dir = Filename.current_dir_name
}
(****************************************************************************)
let my_open_out fn =
prerr_string ("Generating file " ^ fn ^ "\n");
open_out fn
let (gen_lustre_ext_h : string -> unit) =
fun fn ->
let oc = open_out (option.calling_module_name ^ "_ext.h") in
let fn = Filename.concat option.output_dir (option.calling_module_name ^ "_ext.h") in
let oc = my_open_out fn in
let putln s = output_string oc (s^"\n") in
putln (Util.entete "// ");
putln ("#include \"" ^ option.calling_module_name ^ "_ext_func.h\"");
......@@ -62,7 +77,7 @@ let (gen_lustre_ext_h : string -> unit) =
let (gen_lustre_ext_func_h : string -> Exp.var list -> Exp.var list -> unit) =
fun fn in_vars out_vars ->
let oc = open_out (option.calling_module_name ^ "_ext_func.h") in
let oc = my_open_out (Filename.concat option.output_dir (option.calling_module_name ^ "_ext_func.h")) in
let put s = output_string oc s in
let putln s = output_string oc (s^"\n") in
let rec putlist = function
......@@ -98,7 +113,7 @@ let (gen_lustre_ext_func_h : string -> Exp.var list -> Exp.var list -> unit) =
let (gen_lustre_ext_func_c : string -> Exp.var list -> Exp.var list -> unit) =
fun fn in_vars out_vars ->
let oc = open_out (option.calling_module_name ^ "_ext_func.c") in
let oc = my_open_out (Filename.concat option.output_dir (option.calling_module_name ^ "_ext_func.c")) in
let put s = output_string oc s in
let putln s = output_string oc (s^"\n") in
let rec putlist = function
......@@ -177,10 +192,10 @@ let (gen_lustre_ext_func_c : string -> Exp.var list -> Exp.var list -> unit) =
(****************************************************************************)
let (gen_h_file : string -> Exp.var list -> Exp.var list -> Exp.var list -> unit) =
fun fn in_vars out_vars loc_vars ->
let oc = open_out (fn ^ ".h") in
let oc = my_open_out (Filename.concat option.output_dir (fn ^ ".h")) in
let put s = output_string oc s in
let putln s = output_string oc (s^"\n") in
let max_buff_size =
let max_buff_size =
(* 10 digits per I/O is enough? *)
let in_nb = List.length in_vars in
let out_nb = List.length out_vars in
......@@ -218,9 +233,10 @@ typedef float _float;
#define _true 1
#endif
";
if option.use_sockets then
if option.use_sockets then (
putln ("#define MAX_BUFF_SIZE "^(string_of_int max_buff_size)^"");
putln ("#define MAX_BUFF_SIZE_4 "^(string_of_int (4*max_buff_size))^"");
);
putln "//--------- Pragmas ----------------";
putln ("//MODULE: " ^ fn ^ " " ^ (string_of_int (List.length in_vars))
^ " " ^ (string_of_int (List.length out_vars)));
......@@ -357,6 +373,8 @@ let var_to_cast var =
| Type.UT _ -> assert false
let lutin = Sys.argv.(0)
let put_socket_func put fn in_vars out_vars loc_vars =
let putln str = put (str^"\n") in
put ("
......@@ -394,6 +412,8 @@ Input procedures must be used:
)
in_vars;
let lut_file = (List.hd option.env) (* only work with lutin XXX fixme? *) in
let lut_dir = Filename.dirname lut_file in
putln ("
/*--------
launch the lutin interpreter and init socket stuff
......@@ -411,19 +431,23 @@ launch the lutin interpreter and init socket stuff
struct sockaddr_in serv_addr;
struct sockaddr_in cli_addr;
char portno_str[10];
char buff[MAX_BUFF_SIZE_4];
char *sock_addr = \""^option.sock_addr^"\";
const char *args[] = {
#ifdef _WIN32
\"call-via-socket.exe\", sock_addr, portno_str, \"lutin.exe\",
\"call-via-socket.exe\", sock_addr, portno_str, \""^(String.escaped lutin)^"\",
#else
\"call-via-socket\", sock_addr, portno_str, \"lutin\",
\"call-via-socket\", sock_addr, portno_str, \""^(String.escaped lutin)^"\",
#endif
" ^
(match option.seed with None -> "" | Some i -> ("\"-seed\", \""^(string_of_int i)^"\", "))
^" \""^
(List.hd option.env) (* only work with lutin XXX fixme! *)
^"\", \"-rif\",\""^fn^".rif\", NULL};
" ^ (match option.main_node with None -> "" | Some node -> ("\"-main\", \""^node^"\", "))
^ (match option.seed with None -> "" | Some i -> ("\"-seed\", \""^(string_of_int i)^"\", "))
^ (if option.boot then "-boot, " else "")
^ (match option.precision with None -> "" | Some i -> ("\"-precision\", \""^(string_of_int i)^"\", "))
^" \""^ (String.escaped lut_file) ^"\", \"-rif\",\""^(
match option.rif with
Some rif -> String.escaped rif
| None -> String.escaped (fn^".rif"))
^"\", NULL};
// Socket administration stuff
......@@ -453,7 +477,7 @@ launch the lutin interpreter and init socket stuff
#ifndef _LAUNCH_LUTIN_AUTOMATICALLY
printf(\" >>> Waiting for lutin to connect on %s:%s\\n\", sock_addr, portno_str);
#else
dbg_printf(\"Forking...%i\\n\",portno);
dbg_printf(\"Forking...%d\\n\",portno);
#ifdef _WIN32
_spawnvp(_P_DETACH, args[0], args);
#else
......@@ -473,12 +497,8 @@ launch the lutin interpreter and init socket stuff
newsockfd = accept(sockfd, (struct sockaddr *) &cli_addr, &clilen);
if (newsockfd < 0) printf(\"Error: on accept\");
ctx->sock = newsockfd;
memset(ctx->buff, 0, MAX_BUFF_SIZE);
rc = 0;
while (1) {
rc = recv(ctx->sock, ctx->buff, MAX_BUFF_SIZE, 0);
if (rc > 0) break;
}
rc = recv(ctx->sock, buff, MAX_BUFF_SIZE_4, 0);
if (rc<0) { printf(\"Error: cannot read on socket\\n\"); exit(2); }
dbg_printf(\"Skipping '%s'\\n\", ctx->buff);
memset(ctx->buff, 0, MAX_BUFF_SIZE);
......@@ -527,11 +547,9 @@ in
dbg_printf(\"reading inputs\\n\");
rc = 0;
while (1) {
rc = recv(ctx->sock, ctx->buff, MAX_BUFF_SIZE, 0);
dbg_printf(\"reading '%s'\\n\",ctx->buff);
if (rc > 0) break;
}
rc = recv(ctx->sock, ctx->buff, MAX_BUFF_SIZE, 0);
if (rc<0) { printf(\"Error: cannot read on socket\\n\"); exit(2); }
dbg_printf(\"reading '%s'\\n\",ctx->buff);
sscanf(ctx->buff, \"#step %d #outs " ^
let cpt = ref 0 in
let var_to_adress var =
......@@ -598,13 +616,13 @@ void " ^ fn ^ "_reset(" ^ fn ^ "_ctx* ctx){
let (gen_c_file : string -> Exp.var list -> Exp.var list -> Exp.var list -> unit) =
let (gen_c_file : string -> Exp.var list -> Exp.var list -> Exp.var list -> unit) =
fun fn in_vars out_vars loc_vars ->
let oc =
if option.gen_mode = Scade then
open_out (fn ^ "_fctext.c")
my_open_out (Filename.concat option.output_dir (fn ^ "_fctext.c"))
else
open_out (fn ^ ".c")
my_open_out (Filename.concat option.output_dir (fn ^ ".c"))
in
let put s = output_string oc s in
let putln s = output_string oc (s^"\n") in
......@@ -849,6 +867,7 @@ let (main : unit -> unit) =
Luc2alice.env_in_vars = state.s.in_vars ;
Luc2alice.env_out_vars = state.s.out_vars ;
Luc2alice.use_sockets = option.use_sockets ;
Luc2alice.output_dir = option.output_dir;
}
in
......
source/Lucky/luc2c.mli
View file @ 32f5edd6
......@@ -20,16 +20,21 @@ type gen_mode = Lustre | Scade | Alice | Luciole | Nop
type step_mode = Inside | Edges | Vertices
type optionT = {
mutable env : string list; (* lutin/lucky files *)
mutable main_node : string option; (* Main node *)
mutable boot : bool;
mutable pp : string option; (* Pre-processor *)
mutable output : string option; (* A string used in generated files name *)
mutable rif : string option; (* Name of the rif file used to put generated data *)
mutable calling_module_name : string; (* also used in generated files name *)
mutable gen_mode : gen_mode;
mutable use_sockets : bool; (* For the C stubs file generation: use the lutin interpreter via sockets
instead of the interpreter embedded into the C libraries. *)
mutable step_mode : step_mode;
mutable seed : int option;
mutable env : string list; (* lutin/lucky files *)
mutable sock_addr : string
mutable precision : int option;
mutable use_sockets : bool; (* For the C stubs file generation: use the lutin interpreter via sockets
instead of the interpreter embedded into the C libraries. *)
mutable sock_addr : string;
mutable output_dir : string;
}
val option : optionT
......
source/Lurettetop/cmd.ml
View file @ 32f5edd6
......@@ -620,8 +620,8 @@ let (read : (unit -> string) -> bool) =
args.step_mode <- step_mode; true
(* | MakeOpt(str) -> *)
(* args.make_opt <- str; true *)
| Env(llist) ->
args.env <- llist; true
| Env(str) ->
args.env <- LtopArg.explicit_the_file str; true
| StepNb(i) ->
args.step_nb <- i; true
| DrawNb(i) ->
......
source/Lurettetop/ltopArg.ml
View file @ 32f5edd6
......@@ -474,3 +474,10 @@ let rec speclist =
"-h", Arg.Unit (fun _ -> (Arg.usage speclist usage ; exit 0)),
""
]
let (explicit_the_file : string -> string) =
fun s ->
if Filename.is_implicit s
then (Filename.concat args.sut_dir s)
else s
source/Lutin/Makefile.lutin
View file @ 32f5edd6
......@@ -101,6 +101,8 @@ LURETTE_SOURCES=\
$(OBJDIR)/lucFGen.ml \
$(OBJDIR)/lucky.mli \
$(OBJDIR)/lucky.ml \
$(OBJDIR)/rif_base.mli \
$(OBJDIR)/rif_base.ml \
$(OBJDIR)/rif.mli \
$(OBJDIR)/rif.ml \
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment