Commit 21b82a82 authored by erwan's avatar erwan

Doc: add a section for the run/in statement

parent 5fc14d2d
LUTINSRC=../../lutin/src
LUT2TEX= $(LURETTE_PATH)/utils/lutintolatex
LUT2TEX=~/rdbg/utils/lutintolatex
SRCS=./commands.tex \
./language.tex \
./objs/lutin.tex ./objs/gnuplotrif.tex ./objs/checkrif.tex \
......@@ -33,13 +33,13 @@ lutin-man.pdf: objs/main.pdf
# XXX ecrire un filtre pour rajouter de la coloration syntaxique !!
./objs/foo.c.tex:
cat ../../examples/lutin/external_code/foo.c > ./objs/foo.c.tex
cat ../../examples/external_code/foo.c > ./objs/foo.c.tex
# XXX idem
./objs/call_external_c_code.lut.tex:../../examples/lutin/external_code/call_external_c_code.lut
$(LUT2TEX) ../../examples/lutin/external_code/call_external_c_code.lut > ./objs/call_external_c_code.lut.tex
./objs/call_external_c_code.lut.tex:../../examples/external_code/call_external_c_code.lut
$(LUT2TEX) ../../examples/external_*sccode/call_external_c_code.lut > ./objs/call_external_c_code.lut.tex
D=../../examples/lutin/up_and_down/$(shell ocamlc -version)
D=../../examples/up_and_down/$(shell ocamlc -version)
objs/ud.rif: $(D)/test.rif.exp
cp $< $@
......@@ -49,13 +49,13 @@ objs/ud.rif: $(D)/test.rif.exp
./objs/polar.lut.tex:
$(LUT2TEX) ../../examples/lutin/external_code/polar.lut > ./objs/polar.lut.tex
$(LUT2TEX) ../../examples/external_code/polar.lut > ./objs/polar.lut.tex
./objs/ud.lut.tex:
$(LUT2TEX) ../../examples/lutin/up_and_down/ud.lut > ./objs/ud.lut.tex
$(LUT2TEX) ../../examples/up_and_down/ud.lut > ./objs/ud.lut.tex
./objs/rabbit.lut.tex:
$(LUT2TEX) ../../examples/lutin/crazy-rabbit/rabbit.lut > ./objs/rabbit.lut.tex
$(LUT2TEX) ../../examples/crazy-rabbit/rabbit.lut > ./objs/rabbit.lut.tex
./objs/gnuplotrif.tex:objs
......
......@@ -277,6 +277,8 @@ execution. This is the solution adopted in the operational semantics
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Exceptions}
......@@ -335,6 +337,8 @@ start; this is the {\em reactivity principle}.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Parallel composition}
\subsubsection{The \ES\ operator}
In order to put in parallel several statements, one can write:\\
\OB \ES \syn{st1} \ES ... \ES \syn{stn} \CB\\
where the first \ES\ can be omitted.
......@@ -351,11 +355,13 @@ If (at least) one branch raises an exception, the whole statement
raises the exception.
\paragraph{Parallelism vs stockastic directives}
\subsubsection{Parallelism versus stockastic directives}
It is impossible to define a parallel composition which is fair
according to the stockastic directive.
\begin{example}
Consider the statement:\\
\OB~\OB \BAR 1000: \syn{X} \BAR \syn{Y} \CB
......@@ -399,8 +405,67 @@ raising are, like stockastic directives, treated in sequence from
left to right.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Calling nodes from nodes: a cheap parallel composition mechanism}
The \key{run}/\key{:=}/\key{in} construct is another way of executing
code in parallel. It is actually the only way of calling Lutin nodes
from other nodes. Nodes are executed, and the result of this
execution is re-injected in the calling nodes (as if an external call
is made).
Let i1, ...., im be m uncontrollable variables, and
o1, ..., on be n controllable ones, then
\key{run} (o1, ..., on) \key{:=} a\_node(i1, ...., im) \key{in} \syn{st}
will execute the node a\_node, and compute values for o1, ..., on that
will be substituted in \syn{st}. In \syn{st} o1, ..., om are therefore
uncontrollable.
Follows a working example that makes use of \key{run} statements:
\begin{example}
\begin{program}
\key{node} N() \key{returns} (\key{y}:int) = y = 0 \key{fby} \key{loop} y = pre y+1 \\
\key{node} incr(x:int) returns (y:\key{int}) = \key{loop} y = x+1 \\
\key{node} use\_run() \key{returns}(x:\key{int}) = \\
~~~ \key{exist} a,b:\key{int in} \\
~~~ \key{run} a := N() \key{in} \\
~~~ \key{run} b := incr(a) \key{in} \\
~~~ \key{run} x := incr(b) \key{in} \\
~~~ \key{loop} true
\end{program}
\end{example}
If the chosen values during a run make a constraint unsatisfiable, no
backtracking occurs. For instance, the following expression is very
likely to deadlock:
\begin{example}
\begin{program}
\key{run} x := within(0,100) \key{in} x = 42
\end{program}
\end{example}
Indeed, if 42 is not chosen during the call to the \key{within} node
(which definition is obvious), the constraint x=42 will fail.
This form of parallelism is cheaper, because contraints are solved
locally. But of course it is less powerful: constraints are not
merged, but solved in sequence (no backtracking). More detail on the
\key{run} semantics is provided in Section~\ref{run-function}.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Some sugared shortcuts}
......
......@@ -85,7 +85,7 @@ set of constraints.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{The run function}
\label{run-function}
The semantics of an execution step is given by a function
taking an environment $e$ and a (trace) expression $t$:
$\RUN(e,t)$.
......
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