Commit 9e783b64 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Add an example illustration how to plug the C step function of Lustre node from Lurette

Cf examples/lutin/xlurette/.

In  order to  do that,  I rely  on the  ocaml Dynlink  support (.cmxs
files).  The idea is to generate caml code that is able to call the C
code  (as  before)  and to  generate  from  that  a .cmxs  file  that
registers the OcamlRM functions.

I should modify gen_stubs to automate that process.
parent 92968119
......@@ -29,4 +29,5 @@ gen_version:
rm -f version.tex ; \
date +VERSION_DATE=%d-%m-%y > version.tex ; \
echo "\\\newcommand{\\\version}{$(VERSION)}" > doc/version.tex ; \
echo "\\\newcommand{\\\versiondate}{`date +%d-%m-%y`}" >> doc/version.tex
echo "\\\newcommand{\\\versiondate}{`date +%d-%m-%y`}" >> doc/version.tex ;\
cp doc/version.tex doc/lutin-man/objs/
\ No newline at end of file
......@@ -559,7 +559,7 @@ declare in the combinator profile that it is a reference using the
\begin{example}
\begin{program}
\key{node} foo(pt: real \key{ref}) \key{returns} (t: real) = \\
\key{let} foo(pt: real \key{ref}, t: real) : \key{bool} = \\
\> \key{if} \key{pre} pt < pt \key{then} pt < t \key{else} t < pt
\end{program}
\end{example}
......
......@@ -9,25 +9,6 @@ LURETTETOP=$(LTOP) \
--do-not-show-step
test:
rm -f test.rif0 .lurette_rc
$(LURETTETOP) -go --output test.rif0 \
-rp "sut:v4:heater_control.lus:heater_control:" \
-rp "env:lutin:degradable-sensors.lut:-m:main" && \
grep -v "lurette chronogram" test.rif0 | \
grep -v "This is lurette Version" 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 || true
cat test.res
[ ! -s test.res ] && make clean
utest:
cp test.rif test.rif.exp
clean:
rm -rf *.ec *.log *~ .*~ *.o *rif0 *rif Data *.pp_luc *.plot *.gp
......
......@@ -67,8 +67,8 @@ returns(x, y, p1x, p1y, p2x, p2y, p3x, p3y, p4x, p4y: real ; freeze:bool) =
draw_params() fby
try loop {
-- try
-- { draw_params() &> escape() } fby
{ draw_params() and keep_position() } fby
{ draw_params() &> escape() } fby
-- { draw_params() and keep_position() } fby
{
|1: loop [0,40] line() -- forward straigth ahead for a while
|3: loop [0,40] curve() -- forward by turning for a while
......
......@@ -36,6 +36,7 @@ let _ =
(**************************************************************************)
let init _ = ()
let kill _ = ()
type var_type = string
......@@ -151,11 +152,12 @@ let (step : Data.subst list -> Data.subst list)=
);
bounds
let _ =
OcamlRM.add_inputs "rabbit.cmxs" inputs;
OcamlRM.add_outputs "rabbit.cmxs" outputs;
OcamlRM.add_init "rabbit.cmxs" init;
OcamlRM.add_kill "rabbit.cmxs" kill;
OcamlRM.add_step "rabbit.cmxs" step;
OcamlRM.add_mems "rabbit.cmxs" mems_i mems_o
......@@ -23,7 +23,7 @@ let rec main_loop foo_state (a, b, c) cpt =
)
let _ =
let foo_state = Luc4ocaml.make ~seed:1 ["foo.lut::main"] in
let foo_state = Luc4ocaml.make ~seed:1 ["foo.lut"] ~main:(Some "main") in
rif_write_interface oc foo_state false;
main_loop foo_state (0, true, 0.0) 100
LTOP=../../../$(HOSTTYPE)/bin/lurettetop
LURETTETOP=$(LTOP) \
......@@ -39,6 +40,20 @@ test2:
[ ! -s test2.res ] && make clean
# Calling the native step function via a cmxs
test3: heater_control.cmxs
rm -f test3.rif0 .lurette_rc
$(LURETTETOP) -go --output test3.rif0 \
-rp "sut:ocaml:heater_control.cmxs:" \
-rp "env:lutin:degradable-sensors.lut:-m:main" && \
grep -v "lurette chronogram" test3.rif0 | \
grep -v "This is lurette Version" test3.rif0 | \
grep -v "The execution lasted"| sed -e "s/^M//" > test3.rif &&\
rm -f test3.res
diff -B -u -i test3.rif.exp test3.rif > test3.res || true
cat test3.res
[ ! -s test3.res ] && make clean
utest1:
cp test1.rif test1.rif.exp
......@@ -48,13 +63,37 @@ utest2:
utest: utest1 utest2
test:test1 test2
heater_control.ec: heater_control.lus
lus2lic -ec heater_control.lus -n heater_control -o heater_control.ec
%.ec: %.lus
lus2lic -ec $^ -n $* -o $@
heater_control$(EXE): heater_control.ec
ec2c -loop heater_control.ec
gcc heater_control.c heater_control_loop.c -o $@
%.c: %.ec
ec2c -loop $^
LIB=-I ../../../$(HOSTTYPE)/lib graphics.cmxa ocaml2c.cmx ocamlRM.cmx rif_base.cmx
XXX=-I ../../../source/obj-linux/
# XXX
ocaml2c_stubs.c:
camlidl ocaml2c.idl
# XXX modify gen_stubs to generate different names
lurette__sut.c:
gen_stubs heater_control.lus heater_control verimag .
# XXX heater_control_ml.ml should be generated by gen_stubs !!
rm.c:heater_control$(EXE) lurette__sut.c
cat lurette__sut.c | sed -e 's/\"float/\"real/' > rm.c
# lustreRM.ml should be elsewhere
%.cmxs: rm.c %.c lustreRM.ml %_ml.ml ocaml2c_stubs.c
ocamlopt -shared -o $*.cmxs $(XXX) $(LIB) $^
sut:
call-via-socket -addr 127.0.0.1 -port 2000 -server ./not_a_sauna.sh
......@@ -75,3 +114,5 @@ test_dontgo:
[ ! -s test.res ] && make clean
(* to be generated from heater_control.lus *)
(* A partir de la, ca devient spécifique a heater_control *)
let _ =
LustreRM.init ();
OcamlRM.add_inputs "heater_control.cmxs" LustreRM.inputs;
OcamlRM.add_outputs "heater_control.cmxs" LustreRM.outputs;
OcamlRM.add_kill "heater_control.cmxs" LustreRM.kill;
OcamlRM.add_step "heater_control.cmxs" LustreRM.step;
OcamlRM.add_mems "heater_control.cmxs" LustreRM.mems_i LustreRM.mems_o
open Data
open Ocaml2c
let (struct_array_to_pair_list : Ocaml2c.vn_t array -> (string * string) list) =
fun a ->
(Array.fold_right
(fun stru acc -> (stru.var_name, stru.var_type)::acc) a [])
let (inputs :(string * string) list) =
struct_array_to_pair_list
(Ocaml2c.lurette__sut_input_var_name_and_type_array (Ocaml2c.lurette__sut_input_arg_nb()))
let (outputs :(string * string) list) =
struct_array_to_pair_list
(Ocaml2c.lurette__sut_output_var_name_and_type_array (Ocaml2c.lurette__sut_output_arg_nb()))
let sut_input_arg_nb = Ocaml2c.lurette__sut_input_arg_nb()
let sut_output_arg_nb = Ocaml2c.lurette__sut_output_arg_nb()
let sut_i_vntl = inputs
let sut_o_vntl = outputs
let (set_sut_input: Data.subst list -> unit) =
fun input ->
let _ =
(* Printf.eprintf "\n--->set_sut_input"; flush stderr; *)
(List.fold_left
(fun j (vn, t) ->
let value = try (List.assoc vn input) with
Not_found -> (
Printf.fprintf stderr
"Internal error in Sut.set_sut_input\n while searching input \"%s\" value\n" vn;
exit 13
) in
(match value with
B(b) -> Ocaml2c.lurette__sut_set_val_bool j b
| I(i) -> Ocaml2c.lurette__sut_set_val_int j i
| F(f) -> Ocaml2c.lurette__sut_set_val_float j f
);
(j+1)
)
0
sut_i_vntl
)
in
()
let (trie : Data.subst list -> Data.subst list) =
fun input ->
Ocaml2c.lurette__sut_restore_state ();
set_sut_input input;
Ocaml2c.lurette__sut_step () ;
let (_, res) =
(List.fold_left
(fun (j,acc) (vn, t) ->
let value =
match t with
| "bool" -> B (Ocaml2c.lurette__sut_get_val_bool j)
| "int" -> I (Ocaml2c.lurette__sut_get_val_int j)
| "float"
| "real" -> F (Ocaml2c.lurette__sut_get_val_float j)
| _ ->
Printf.fprintf stderr "\nUnsupported type: %s (for %s)\n" t vn;
flush stderr;
assert false
in
let acc = (vn,value)::acc in
(j+1, acc)
)
(0, [])
sut_o_vntl
)
in
res
let (step : Data.subst list -> Data.subst list) =
fun input ->
(* Printf.eprintf "\n--->step\n"; flush stderr; *)
let output = trie input in
Ocaml2c.lurette__sut_save_state ();
output
let init () =
(* Printf.eprintf "\n--->lurette__sut_init"; flush stderr; *)
Ocaml2c.lurette__sut_init()
let kill msg = ()
let mems_i = []
let mems_o = []
......@@ -14,7 +14,7 @@ let (outputs :(string * string) list) = [
let pre_res = ref false
let init _ = ()
let kill _ = ()
let (step : subst list -> subst list)=
fun inputs ->
......@@ -37,6 +37,6 @@ let mems_o = []
let _ =
OcamlRM.add_inputs "heat_ctrl2.cmxs" inputs;
OcamlRM.add_outputs "heat_ctrl2.cmxs" outputs;
OcamlRM.add_init "heat_ctrl2.cmxs" init;
OcamlRM.add_kill "heat_ctrl2.cmxs" kill;
OcamlRM.add_step "heat_ctrl2.cmxs" step;
OcamlRM.add_mems "heat_ctrl2.cmxs" mems_i mems_o
......@@ -13,6 +13,7 @@ test:
-rp "env:lutin:giro.lut:main" \
&&\
grep -v "lurette chronogram" test.rif0 | \
grep -v "This is lurette Version" | \
grep -v "The execution lasted"| sed -e "s/^M//" > test.rif &&\
rm -f test.res && diff -u -i test.rif.exp test.rif > test.res
[ ! -s test.res ] && make clean
......
# This is lurette Version 1.54 (7f9e1c3)
# The random engine was initialized with the seed 1
#inputs "choff4":bool "choff3":bool "choff2":bool "choff1":bool "disc4":bool "disc3":bool "disc2":bool "disc1":bool "inairreset":bool "ongroundreset":bool "xb4":real "xa4":real "xb3":real "xa3":real "xb2":real "xa2":real "xb1":real "xa1":real
#outputs "x":real "debug_localfailure1":bool "debug_localfailure2":bool "debug_localfailure3":bool "debug_localfailure4":bool "debug_cross_failure1":bool "debug_cross_failure2":bool "debug_cross_failure3":bool "debug_cross_failure4":bool "debug_ch_failed1":bool "debug_ch_failed2":bool "debug_ch_failed3":bool "debug_ch_failed4":bool "debug_st1":int "debug_st2":int "debug_st3":int "debug_st4":int
......
......@@ -16,6 +16,7 @@ test:
-rp "env:lutin:degradable-sensors.lut:main" \
&& \
grep -v "lurette chronogram" test.rif0 | \
grep -v "This is lurette Version" | \
grep -v "The execution lasted"| sed -e "s/^M//" > test.rif &&\
rm -f test.res && diff -u -i test.rif.exp test.rif > test.res
[ ! -s test.res ] && make clean
......
# This is lurette Version 1.54 (7f9e1c3)
# The random engine was initialized with the seed 3
#inputs "T":real "T1":real "T2":real "T3":real
#outputs "Heat_on":bool
......
......@@ -20,6 +20,7 @@ test1:
--do-not-show-step -ns2c -go -o test1.rif0 --draw-inside 10 --draw-edges 10 \
-go &&\
grep -v "lurette chronogram" test1.rif0 | \
grep -v "This is lurette Version" | \
grep -v "The execution lasted"| sed -e "s/^M//" \
> test1.rif &&\
$(RM) test1.res && diff -u -i test1.rif.exp test1.rif > test1.res
......@@ -36,6 +37,7 @@ test2:
--do-not-show-step -ns2c -o test2.rif0 --draw-inside 10 --draw-edges 10 \
&&\
grep -v "lurette chronogram" test2.rif0 | \
grep -v "This is lurette Version" | \
grep -v "The execution lasted"| sed -e "s/^M//"\
> test2.rif &&\
$(RM) test2.res && diff -u -i test2.rif.exp test2.rif \
......@@ -49,6 +51,7 @@ test3 :
-rp "env:lutin:window.lut:main" \
--do-not-show-step -ns2c -sut heater_ctrl2.lus -msn heater_ctrl2 -o test3.rif0 &&\
grep -v "lurette chronogram" test3.rif0 | \
grep -v "This is lurette Version" | \
grep -v "The execution lasted"| sed -e "s/^M//" > test3.rif && \
$(RM) test3.res && diff -u -i test3.rif.exp test3.rif > test3.res
[ ! -s test3.res ] && make clean
......
# This is lurette Version 1.54 (7f9e1c3)
# The random engine was initialized with the seed 1
#inputs "U":int
#outputs "Heat_on":bool
......
# This is lurette Version 1.54 (7f9e1c3)
# The random engine was initialized with the seed 1
#inputs "U":real
#outputs "Heat_on":bool
......
# This is lurette Version 1.54 (7f9e1c3)
# The random engine was initialized with the seed 1
#inputs "t":real
#outputs "T":real "On":bool
......
......@@ -87,7 +87,7 @@ int cherni_conversion(matrix_t* con, const int start,
for (i=0; i<nbrows; i++){
vector_product(&ray->p[i][0],ray->p[i],con->p[k.index],nbcols);
if (index_non_zero == nbrows && pkint_sgn(ray->p[i][0])!=0){
index_non_zero = i;
index_non_zero = i;
}
}
......@@ -99,11 +99,11 @@ int cherni_conversion(matrix_t* con, const int start,
/* remove it of lines and put it at index nbline */
nbline--;
if (index_non_zero != nbline)
matrix_exch_rows(ray,index_non_zero,nbline);
matrix_exch_rows(ray,index_non_zero,nbline);
/* compute new lineality space */
for (i=index_non_zero; i<nbline; i++)
if (pkint_sgn(ray->p[i][0]) != 0)
matrix_combine_rows(ray,i,nbline,i,0);
if (pkint_sgn(ray->p[i][0]) != 0)
matrix_combine_rows(ray,i,nbline,i,0);
/* orient the new ray */
if (pkint_sgn(ray->p[nbline][0]) < 0)
......
......@@ -10,46 +10,46 @@ let (f : unit -> int) =
fun () ->
try
let seed_str =
match args.seed with
None -> []
| Some i -> "-seed"::[(string_of_int i)]
match args.seed with
None -> []
| Some i -> "-seed"::[(string_of_int i)]
and precision_str = "-precision"::[string_of_int args.precision]
and compute_volume_str =
if (args.compute_volume) then ["--compute-poly-volume"] else []
if (args.compute_volume) then ["--compute-poly-volume"] else []
and verb_str = ["-v"; (string_of_int (args.verbose))]
and step_mode_str = [step_mode_to_string args.step_mode]
and orac_str =
match args.oracle_cmd with
"" -> []
| str ->
"--oracle"::[(Str.global_replace blank_star "+" str)]
match args.oracle_cmd with
"" -> []
| str ->
"--oracle"::[(Str.global_replace blank_star "+" str)]
and step_nb_str = "-l"::[(string_of_int args.step_nb)]
and dlvr_str =
if (args.display_local_var) then ["-locals"] else []
if (args.display_local_var) then ["-locals"] else []
and env_str =
let lut_list = Util2.string_to_string_list args.env in
lut_list
let lut_list = Util2.string_to_string_list args.env in
lut_list
in
let lutin = "lutin" ^ ExtTools.dot_exe in
let prefix = Util2.string_to_string_list args.prefix in
let arg_list0 =
List.flatten
[
prefix;
[lutin];
["-boot"];
step_nb_str ;
orac_str;
step_mode_str;
seed_str;
precision_str;
compute_volume_str;
verb_str ;
dlvr_str ;
env_str
]
List.flatten
[
prefix;
[lutin];
["-boot"];
step_nb_str ;
orac_str;
step_mode_str;
seed_str;
precision_str;
compute_volume_str;
verb_str ;
dlvr_str ;
env_str
]
in
let prog = if args.prefix = "" then lutin else List.hd prefix in
let arg_list = Util.rm "" arg_list0 in
......@@ -59,16 +59,16 @@ let (f : unit -> int) =
let args_str_sut = args.sut_cmd in
let arg_list_sut0 = Util2.string_to_string_list args_str_sut in
let arg_list_sut =
match arg_list_sut0 with
"ecexe"::tail ->
if
(* force the use of -r with ecexe *)
List.mem "-r" tail
then
arg_list_sut0
else
"ecexe"::"-r"::tail
| _ -> arg_list_sut0
match arg_list_sut0 with
"ecexe"::tail ->
if
(* force the use of -r with ecexe *)
List.mem "-r" tail
then
arg_list_sut0
else
"ecexe"::"-r"::tail
| _ -> arg_list_sut0
in
let prog_sut = List.hd arg_list_sut in
let args_sut = Array.of_list arg_list_sut in
......@@ -86,206 +86,206 @@ let (f : unit -> int) =
let sut_oc = Unix.out_channel_of_descr sut_stdin_out in
let _ =
set_binary_mode_in luc_ic false;
set_binary_mode_in sut_ic false;
set_binary_mode_out luc_oc false;
set_binary_mode_out sut_oc false;
(* XXX won't work under windows with mingw and MVC++ !! *)
Unix.set_nonblock lutin_stdout_in;
Unix.set_nonblock sut_stdout_in
set_binary_mode_in luc_ic false;
set_binary_mode_in sut_ic false;
set_binary_mode_out luc_oc false;
set_binary_mode_out sut_oc false;
(* XXX won't work under windows with mingw and MVC++ !! *)
Unix.set_nonblock lutin_stdout_in;
Unix.set_nonblock sut_stdout_in
in
let rif =
if Filename.is_relative args.output then
open_out (Filename.concat args.sut_dir args.output)
else
open_out args.output
if Filename.is_relative args.output then
open_out (Filename.concat args.sut_dir args.output)
else
open_out args.output
in
let rec (read_ic : in_channel -> string) =
fun ic ->
let rec read_loop acc =
try
let line = (input_line ic) in
let lgt = String.length line in
let line' =
if
lgt < 5 || String.sub line 0 5 <> "#outs"
then
line
else
(* do not send #outs to the sut, because it does not
understand it *)
String.sub line 5 (lgt-5)
in
let new_acc = acc ^ line' ^ "\n" in
if
(args.show_step) && Util.is_substring "# step" line
then
(* For the progress bar *)
(
output_string args.ocr
("--- " ^
(String.sub line 2 ((String.length line) - 2)) ^
":\n");
flush args.ocr
);
if Util.is_substring "The oracle Pid is" line then
(
output_string args.ocr (line ^ "\n");
flush args.ocr
);
fun ic ->
let rec read_loop acc =
try
let line = (input_line ic) in
let lgt = String.length line in
let line' =
if
lgt < 5 || String.sub line 0 5 <> "#outs"
then
line
else
(* do not send #outs to the sut, because it does not
understand it *)
String.sub line 5 (lgt-5)
in
let new_acc = acc ^ line' ^ "\n" in
if
(args.show_step) && Util.is_substring "# step" line
then
(* For the progress bar *)
(
output_string args.ocr
("--- " ^
(String.sub line 2 ((String.length line) - 2)) ^
":\n");
flush args.ocr
);
if Util.is_substring "The oracle Pid is" line then
(
output_string args.ocr (line ^ "\n");
flush args.ocr
);
output_string rif (line ^ "\n");
read_loop new_acc
with Sys_blocked_io -> acc
in
read_loop ""
output_string rif (line ^ "\n");
read_loop new_acc
with Sys_blocked_io -> acc
in
read_loop ""
in
let pid_lutin =
Unix.create_process prog arg_array
lutin_stdin_in lutin_stdout_out (Unix.descr_of_out_channel args.ecr)
Unix.create_process prog arg_array
lutin_stdin_in lutin_stdout_out (Unix.descr_of_out_channel args.ecr)
in
let pid_sut =
Unix.create_process prog_sut args_sut
sut_stdin_in sut_stdout_out (Unix.descr_of_out_channel args.ecr)
Unix.create_process prog_sut args_sut
sut_stdin_in sut_stdout_out (Unix.descr_of_out_channel args.ecr)
in