Commit 2b7ecaec authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Remove -seed from lurettetop

Really, it is the job of lutin to set the seed.

Also, unplug the "calling lutin from lustre and C" tests, as they are
actually broken since the move to oasis/ocamlbuild.
parent 9686ab43
......@@ -19,6 +19,7 @@ VERSION:=1.57
# the sha is still automatic tough!
SHA:=`git log -1 --pretty=format:"%h"`
COMMIT_NB:=$(shell git log --pretty=oneline | wc -l)
gen_version:
......@@ -31,6 +32,7 @@ gen_version:
echo "\\\newcommand{\\\version}{$(VERSION)}" > doc/version.tex ; \
echo "\\\newcommand{\\\sha}{$(SHA)}" >> doc/version.tex ; \
echo "\\\newcommand{\\\versionname}{Trilby}" >> doc/version.tex ; \
echo "\\\newcommand{\\\commitnb}{$(COMMIT_NB)}" >> doc/version.tex ; \
echo "\\\newcommand{\\\versiondate}{`date +%d-%m-%y`}" >> doc/version.tex ;\
[ -d doc/lutin-man/objs ] || mkdir doc/lutin-man/objs; \
cp doc/version.tex doc/lutin-man/objs/ ;\
......
......@@ -85,7 +85,7 @@ Library gbddml
Modules: Bdd
Install: true
CSources: gbdd_cml.c, gbdd.c, gbdd.h
CCOpt: -x c++ -g -O0 -fno-operator-names -fPIC -I$pkg_camlidl
CCOpt: -x c++ -g -O2 -fno-operator-names -fPIC -I$pkg_camlidl
CClib: -lstdc++
Library polka
......
include $(LURETTE_PATH)/Makefile.common.source
LUTINSRC=../../source/Lutin
LUTINSRC=../../lutin/src
LUT2TEX= $(LURETTE_PATH)/utils/lutintolatex
SRCS=./commands.tex \
./language.tex \
......@@ -17,7 +17,7 @@ SRCS=./commands.tex \
./objs/ud.lut.tex \
./objs/rabbit.lut.tex \
./objs/ud.jpg \
./main.tex touch.tex
bib.bib ./main.tex touch.tex
all: touch.tex lutin-man.pdf
......@@ -65,7 +65,7 @@ touch.tex:
touch touch.tex
objs/main.pdf: objs $(SRCS)
cd objs; pdflatex main.tex
cd objs; pdflatex main.tex; bibtex main; pdflatex main.tex
objs:
mkdir objs
......
......@@ -79,6 +79,7 @@
\newcommand{\lutin}{{\sc Lutin}\xspace}
\newcommand{\lustre}{{\sc Lustre}\xspace}
\newcommand{\lurette}{{\sc Lurette}\xspace}
\newcommand{\rdbg}{{\sc RDBG}\xspace}
\newcommand{\simtochro}{{\sc Sim2chro}\xspace}
\newcommand{\simtochrogtk}{{\sc Sim2chrogtk}\xspace}
\newcommand{\luciole}{{\sc Luciole}\xspace}
......
......@@ -4,7 +4,7 @@
\label{lutin-section}
Synchronous programs~\cite{esterel,lustre,signal} deterministically
Synchronous programs~\cite{signal,esterel,lustre} deterministically
produce outputs from input values. To be able to compile,
synchronous programs need to be fully deterministic.
However, sometimes, we want to be able to describe synchronous
......@@ -122,8 +122,8 @@ Concurrency (i.e., parallel execution) is a central issue for
reactive systems. The problem of merging sequential and parallel
constructs has been largely studied: classical solutions are
hierarchical automata ``\`a la StateCharts''
\cite{maraninchi92,syncchart96}, or statement-based languages like
Esterel~\cite{esterel:scp}. Our opinion is that deeply merging
\cite{syncchart96,maraninchi92}, or statement-based languages like
Esterel~\cite{esterel}. Our opinion is that deeply merging
sequence and parallelism is a problem of high-level language, and
that it is sufficient to have a notion of global parallelism:
intuitively, local parallelism can always be made global by adding
......@@ -132,3 +132,11 @@ notion in our model: a complete system is a set of concurrent
program, each one producing its own constraints on the resulting
global behaviour.
\subsection{More reading}
Some case studies that use Lutin can be found in \cite{tacas,sies}.
A description of the constraint solving algorithms is done here:
\cite{jahier-cstva06}.
A Lutin tutorial is also available in \href{http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lurette/doc/lutin-tuto/lutin-tuto-html.html}{html} and \href{http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lurette/doc/lutin-tuto/lutin-tuto-pdf.pdf}{pdf}.
......@@ -35,8 +35,7 @@ stand-alone executable.
In order call \lutin from \ocaml, one can use the functions provided in
the \verb+luc4ocaml.mli+ interface file (or cf the ocamlcdoc
\href{http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lurette/doc/luc4ocaml/Luc4ocaml.html}{
generated html files}). A complete example can be found in
\href{http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lurette/doc/luc4ocaml/Luc4ocaml.html}{generated html files}). A complete example can be found in
\verb+examples/lutin/ocaml/+.
......@@ -90,6 +89,9 @@ 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{\rdbg}
Lutin programs can be debugged with \rdbg{} (\url{http://rdbg.forge.imag.fr/}).
\subsubsection{\checkrif}
A tool that performs post-mortem oracle checking using the
......
......@@ -47,8 +47,9 @@
\pagestyle{fancy}
\title{\lutin Reference manual\\ Version \versionname-\version (sha:\sha)}
\title{\lutin Reference manual\\ Version \versionname-\version{}}
\author{Pascal Raymond\\Erwan Jahier}
\date{last commit : \versiondate{} (sha:\sha)}
\begin{document}
......@@ -99,5 +100,8 @@ controlling the random choices.
\newpage
\input{lutin_examples}
\bibliographystyle{abbrv}
\bibliography{bib}
\end{document}
......@@ -41,10 +41,12 @@ test-lutin:
cd lutin/external_code && make test;
cd lutin/luciole && make test ;
cd lutin/crazy-rabbit && make test;
cd lutin/lustre && make test ;
cd lutin/C && make test;
echo "All lutin tests ran correctly."
# XXX Broken !
# cd lutin/lustre && make test ;
# cd lutin/C && make test;
# problem ~
test: test-lutin
......
......@@ -15,7 +15,7 @@ LIBS = lut4c.a liblut4c_stubs.a -lgmp -lm -ldl -lstdc++
LIBS = ../../../_build/lutin/src/lut4c.a ../../../_build/lutin/src/liblut4c_stubs.a \
-lasmrun -lgmp -lm -ldl
LIBS = ../../../_build/lutin/src/liblut4c.a -lgmp -lm -ldl -lstdc++
LIBS = ../../../_build/lutin/src/lut4c.a ../../../_build/lutin/src/lutin.a -lgmp -lm -ldl -lstdc++
#gcc -o test -L. -L"`ocamlc -where`" test.c -Wl,--whole-archive -lhello_world -Wl,--no-whole-archive -lasmrun -lm -ldl
......
......@@ -23,9 +23,9 @@ clean:
test.rif:$(EXPDIR) rabbit.cmxs
rm -f test.rif0 .lurette_rc
$(LURETTETOP) -go --output test.rif0 -seed 34 \
$(LURETTETOP) -go --output test.rif0 \
-rp "sut:ocaml:rabbit.cmxs:" \
-rp 'env:lutin:rabbit.lut:-main:rabbit:-L:libm.so:-loc' && \
-rp 'env:lutin:rabbit.lut:-main:rabbit:-seed:34:-L:libm.so:-loc' && \
grep -v "lurette chronogram" test.rif0 | \
grep -v "lurette Version" | \
grep -v "The execution lasted"| sed -e "s/^M//" > test.rif
......
......@@ -3,10 +3,16 @@ LD = gcc -g
EXE=
CFLAGS = \
-L../../../lib \
-I../../../include
-L `ocamlfind -query lutin` \
-I `ocamlfind -query lutin`
LIBS = -lluc4c_nc -llucky_nc -lgmp -lm -ldl -lstdc++
LIB= `ocamlfind query camlidl -l-format` \
`ocamlfind query lutin-utils -i-format` \
`ocamlfind query lutils -i-format` \
-cclib -lcamlidl -cclib -lgmp
#LIBS = -llut4c_stubs `ocamlfind query lutils -i-format` -lgmp -lm -ldl -lstdc++
LUTIN=../../../bin/lutin
ifneq (,$(findstring $(HOSTTYPE),win32))
......@@ -16,12 +22,12 @@ ifneq (,$(findstring $(HOSTTYPE),win32))
-I../../../include \
-Winline -Wimplicit-function-declaration
LIBS = -lluc4c_nc -llucky_nc -lgmp -lws2_32 -lm -lstdc++
LIBS = -llut4c -llutils -lgmp -lws2_32 -lm -lstdc++
LUTIN=../../../bin/lutin$(EXE)
endif
ifeq ($(HOSTTYPE),mac)
LD = g++ -g
LIBS = -lluc4c_nc -llucky_nc -lgmp -lm -ldl
LIBS = -llut4c -llutils -lgmp -lm -ldl
endif
################################################################
......
LTOP=../../../bin/lurettetop
LDBG=../../../bin/ldbg -I +rdbg-plugin
LURETTETOP=$(LTOP) \
--test-length 100 --thick-draw 1 \
--draw-inside 0 --draw-edges 0 --draw-vertices 0 --draw-all-vertices \
--step-mode Inside --local-var --no-gnuplot --no-sim2chro --seed 3 \
--step-mode Inside --local-var --no-gnuplot --no-sim2chro \
--do-not-show-step
EXPDIR=`$(LTOP) --ocaml-version`
......@@ -20,7 +19,7 @@ test1.rif: heater_control$(EXE) $(EXPDIR)
-rp "sut:ec_exe:./heater_control.ec:" \
-rp "oracle:v6:heater_control.lus:not_a_sauna" \
-rp "oracle:v6:heater_control.lus:not_a_fridge" \
-rp "env:lutin:env.lut:-m:main" && \
-rp "env:lutin:env.lut:-m:main:-seed:3" && \
grep -v "lurette chronogram" test1.rif0 | \
grep -v "This is lurette Version" test1.rif0 | \
grep -v "The execution lasted"| sed -e "s/^M//" > test1.rif
......@@ -40,7 +39,7 @@ test2.rif:
rm -f test2.rif0 .lurette_rc
$(LURETTETOP) -go --output test2.rif0 \
-rp "sut:v6:heater_control.lus:heater_control:" \
-rp "env:lutin:degradable-sensors.lut:-m:main" && \
-rp "env:lutin:degradable-sensors.lut:-m:main:-seed:3" && \
grep -v "lurette chronogram" test2.rif0 | \
grep -v "This is lurette Version" test2.rif0 | \
grep -v "The execution lasted"| sed -e "s/^M//" > test2.rif
......@@ -61,7 +60,7 @@ test3.rif: heater_control.cmxs
rm -f test3.rif0 .lurette_rc
$(LURETTETOP) --luciole -go --output test3.rif0 \
-rp "sut:ocaml:heater_control.cmxs:" \
-rp "env:lutin:degradable-sensors.lut:-m:main" && \
-rp "env:lutin:degradable-sensors.lut:-m:main:-seed:3" && \
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
......@@ -77,8 +76,8 @@ test4.rif: heater_control$(EXE)
rm -f test4.rif0 .lurette_rc
$(LURETTETOP) -go --output test4.rif0 \
-rp "sut:ec_exe:./heater_control.ec:" \
-rp "env:lutin:env.lut:-m:main1" \
-rp "env:lutin:env.lut:-m:main2" && \
-rp "env:lutin:env.lut:-m:main1:-seed:3" \
-rp "env:lutin:env.lut:-m:main2:-seed:3" && \
grep -v "lurette chronogram" test4.rif0 | \
grep -v "This is lurette Version" test4.rif0 | \
grep -v "The execution lasted"| sed -e "s/^M//" > test4.rif
......@@ -93,23 +92,6 @@ endif
[ ! -s test4.res ]
# check that lurettetop and ldbg produce the same rif
test5.rif: heater_control$(EXE)
rm -f test5.rif0 .lurette_rc
$(LDBG) -init test5.ml
grep -v "This is lurette Version" test5.rif0 > test5.rif
test5:test5.rif $(EXPDIR)/
rm -f test5.res
diff -u -i $(EXPDIR)/test5.rif.exp test5.rif > test5.res || true
ifneq (,$(findstring $(HOSTTYPE),win32))
taskkill /F /IM heater_control.exe || true
endif
cat test5.res
[ ! -s test5.res ] && make clean
utest1:test1.rif
cp test1.rif $(EXPDIR)/test1.rif.exp
......@@ -120,13 +102,8 @@ utest2:test2.rif
utest4:test4.rif
cp test4.rif $(EXPDIR)/test4.rif.exp
utest5:test5.rif
cp test5.rif $(EXPDIR)/test5.rif.exp
# nb : pas de utest5 car je me sert du test4 pour vérifier que je genere bien la meme
# trace en mode ldbg !!
utest: utest1 utest2 utest4 utest5
utest: utest1 utest2 utest4
test: test1 test2 test4
......
LTOP=../../../../bin/lurettetop
LURETTETOP=$(LTOP) --precision 2 --seed 3\
LURETTETOP=$(LTOP) --precision 2 \
-rp "sut:v6:heater_control.lus:heater_control" \
-rp "oracle:v6:heater_control.lus:not_a_sauna" \
-rp "env:lutin:env.lut:main" \
-rp "env:lutin:env.lut:-n:main:-seed:3" \
--thick-draw 1 \
--draw-inside 0 --draw-edges 0 --draw-vertices 0 --draw-all-vertices \
--step-mode Inside --local-var --no-gnuplot --no-sim2chro \
......@@ -42,8 +42,8 @@ dontgo:
rm -f test.rif0 .lurette_rc
$(LTOP) --precision 2 \
-rp "sut:v6:heater_control.lus:heater_control" \
-rp "env:lutin:env.lut:main" \
-rp "env:lutin:env.lut:-n:main:-seed:3" \
--thick-draw 1 \
--draw-inside 0 --draw-edges 0 --draw-vertices 0 --draw-all-vertices \
--step-mode Inside --local-var --no-sim2chro --seed 3 \
--step-mode Inside --local-var --no-sim2chro \
--do-not-show-step env.lut --output test.rif
......@@ -291,9 +291,9 @@ install ../utils/simec_trap "$LURETTEPATH/bin/"
install ../utils/read-rif.sh "$LURETTEPATH/bin/"
install -m a+x,a+r,u+w ./lurettetop.sh "$LURETTEPATH/bin/lurettetop"
install -m a+x,a+r,u+w ./ldbg "$LURETTEPATH/bin/ldbg"
install -m a+x,a+r,u+w ./show_luc.sh "$LURETTEPATH/bin/show_luc"
install -m a+x,a+r,u+w ./gen_stubs.sh "$LURETTEPATH/bin/gen_stubs"
# install -m a+x,a+r,u+w ./ldbg "$LURETTEPATH/bin/ldbg"
# install -m a+x,a+r,u+w ./show_luc.sh "$LURETTEPATH/bin/show_luc"
# install -m a+x,a+r,u+w ./gen_stubs.sh "$LURETTEPATH/bin/gen_stubs"
install ./set_env_var "$LURETTEPATH/bin"
......
......@@ -625,11 +625,6 @@ let rec speclist =
"--draw-all-vertices", Arg.Unit (fun _ -> args.all_vertices <- true),
"\tTries all the polyhedra vertices.\n" ;
"--seed", Arg.Int (fun i -> args.seed <- Some i),
"<int>\t\tSeed the random engine is initialised with." ;
"-seed", Arg.Int (fun i -> args.seed <- Some i), " <int>\n";
"--dbg", Arg.Unit (fun () -> args.debug_ltop <- true), " debug mode (to debug lurettetop)\n";
"-ldbg", Arg.Unit (fun () -> args.ldbg <- true), " use the lurette debugger \n";
......
......@@ -445,13 +445,6 @@ and
let local_var_name_and_type_list =
Util.sort_list_string_pair local_var_name_and_type_list_unsorted
in
(* Initialisation of the random engine *)
let seed =
match (options.user_seed) with
None -> random_seed ()
| Some seed -> seed
in
set_luciole_mode_if_necessary init_state sut_i_vntl sut_o_vntl [] [];
Random.init seed ;
output_msg ("\nThe random engine was initialized with the seed "^(soi seed)^"\n");
......
......@@ -480,8 +480,6 @@ let (start : unit -> Event.t) =
Rif.write oc ("# This is lurette Version " ^ Version.str ^
" (\"" ^Version.sha^"\")\n");
Rif.write oc ("# The random engine was initialized with the seed " ^
(string_of_int seed) ^ "\n" );
RifIO.write_interface oc
(luciole_outputs_vars@flat_env_out) flat_sut_out loc (Some oracle_out_l);
Rif.flush oc;
......
......@@ -222,7 +222,7 @@ let (gen_h_file : string -> Exp.var list -> Exp.var list -> Exp.var list -> unit
putln ("#ifndef _" ^ fn ^ "_H_INCLUDED \n");
putln ("#define _" ^ fn ^ "_H_INCLUDED \n");
if not option.use_sockets then
putln "#include <luc4c_stubs.h> \n";
putln "#include <lut4c_stubs.h> \n";
putln "#include <stdio.h>";
putln "//-------- Predefined types ---------";
......@@ -842,7 +842,7 @@ Dynamic allocation of an internal structure
(match option.seed with
| None -> ()
| Some seed ->
putln (" lucky_set_seed("^ (string_of_int seed) ^");")
putln (" set_seed("^ (string_of_int seed) ^");")
);
putln (" ctx = malloc(sizeof("^ fn ^ "_ctx));");
putln " ctx->client_data = cdata;";
......
let str="1.57"
let sha="bf5cb12"
let sha="9686ab4"
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