Commit 922e75a2 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Merge /home/raymond/git/lurette

parents 74f93d6c 8c74d530
LUTINSRC=../../source/Lutin
SRCS=./src/commands.tex \
./src/language.tex \
./src/lutsyntax.tex \
./src/semantics.tex \
./objs/lutyacc.tex \
./objs/version.tex \
./src/main.tex \
all: lutin-man.pdf
lutin-man.pdf: objs/main.pdf
cp $< $@
objs/main.pdf: objs $(SRCS)
cd objs; pdflatex main.tex
objs:
mkdir objs
./objs/lutyacc.tex: ./objs/cleanyacc tokens
mly2bnf $< -t tokens > $@
./objs/cleanyacc : $(LUTINSRC)/lutParser.mly
cat $< | sed -e "s/lut//g" -e "s/TK_EOF//" > $@
./objs/version.tex: $(LUTINSRC)/lutVersion.ml Makefile
cat $< | grep "number.*=" | sed -e "s/^.*number.*\"\([^\"]*\)\"/\\\\newcommand{\\\\version}{\1}/" > $@
cat $< | grep "release.*=" | sed -e "s/^.*release.*\"\([^\"]*\)\"/\\\\newcommand{\\\\release}{\1}/" >> $@
clean:
rm -f ./objs/*
re:
touch $(LUTINSRC)/lutParser.mly
touch src/*
make
%%% mly2bnf customization
%\newcommand{\bnftoken}[1]{{\color{blue2}\bfseries\ttfamily #1}}
\newcommand{\bnftoken}[1]{\mbox{\color{blue2}\bfseries\ttfamily #1}}
\newcommand{\bnfleftident}[1]{{\color{purple4}\itshape #1}}
\newcommand{\bnfrightident}[1]{{\color{purple4}\itshape #1}}
\newcommand{\bnfdef}{\mbox{\color{red}$::=$}}
\newcommand{\bnfor}{\mbox{\color{red3}$|$}}
\newcommand{\bnfopt}[1]{\mbox{\color{red3}$\lbrack$} #1 \mbox{\color{red3}$\rbrack$}}
\newcommand{\bnflist}[1]{\mbox{\color{red3}$\lbrace$} #1 \mbox{\color{red3}$\rbrace$}}
\newcommand{\bnfgroup}[1]{\mbox{\color{red3}$($} #1 \mbox{\color{red3}$)$}}
%short cuts ...
\newcommand{\key}[1]{\mbox{\bnftoken{#1}}}
\newcommand{\prg}[1]{\mbox{\bfseries\ttfamily #1}}
\newcommand{\syn}[1]{\mbox{\bnfrightident{#1}}}
%\newcommand {\key}[1]{\mbox{\texttt{\textbf{#1}}}}
%\newcommand {\key}[1]{\mbox{\tt #1}}
%\newcommand {\syn}[1]{\mbox{\it #1}}
\newcommand {\opt}[1]{\mbox{$[$ #1 $]$}}
\newcommand {\oom}[1]{\mbox{$\{$ #1 $\}^+$}}
\newcommand {\zom}[1]{\mbox{$\{$ #1 $\}^*$}}
\newcommand {\comm}[1]{\framebox{#1}}
\newcommand{\OB}{{\tt \symbol{"7B}}} %{
\newcommand{\CB}{{\tt \symbol{"7D}}} %}
\newcommand{\BAR}{{\tt \symbol{"7C}}} %|
\newcommand{\SBAR}{{\tt \symbol{"7C}\symbol{"3E}}} %|>
\newcommand{\OS}{{\tt \symbol{"5B}}} %[
\newcommand{\CS}{{\tt \symbol{"5D}}} %]
\newcommand{\TI}{{\tt \symbol{"7E}}} %~
\newcommand{\EE}{{\tt \symbol{"26}\symbol{"26}}} %&&
\newcommand{\ES}{{\tt \symbol{"26}\symbol{"3E}}} %&>
\newcommand{\OP}{{\tt \symbol{"28}}} %(
\newcommand{\CP}{{\tt \symbol{"29}}} %)
\newcommand{\LOOPI}[2]{{\tt loop\OS\mbox{#1},\mbox{#2}\CS}}
\newcommand{\LOOPA}[2]{{\tt loop\TI\mbox{#1}:\mbox{#2}}}
\newcommand{\EA}{\key{\symbol{"26}\symbol{"3E}}} %&>
\newenvironment{program}{\tt\vspace{0.0cm}\par \begin{minipage}{\fboxrule}\begin{tabbing} XX \= XX \= XX \= XX \= XX \= XX \= XX \= XX \= XX \= XX \= XX \= XX \= XX \= \+\kill}{\end{tabbing} \end{minipage}\vspace{0.0cm}\rm\noindent\par}
\newenvironment{smallprogram}{\vspace{0.3cm}\par \begin{minipage}{\fboxrule}\small\tt\begin{tabbing} XX \= XX \= XX \= XX \= XX \= XX \= XX \= XX \= XX \= XX \= XX \= \+\kill}{\end{tabbing} \end{minipage}\vspace{0.3cm}\rm\noindent\par}
\newenvironment{tinyprogram}{\tt\footnotesize\hspace{-5mm}\par \begin{minipage}{\fboxrule}\begin{tabbing} X \= X \= X \= X \= X \= X \= X \= X \= X \= X \= X \= \+\kill}{\end{tabbing} \end{minipage}\vspace{0.3cm}\rm\noindent\par}
\newenvironment{example}
{\vspace{1ex}\noindent
\begin{tabular}{|p{15.8cm}|}
{\bfseries $\triangleright$ Example:}
}
{\end{tabular}\vspace{1ex}}
\newenvironment{definition}
{\vspace{1ex}\noindent
\begin{tabular}{||p{15.8cm}||}
{\bfseries $\triangleright$ Definition:}
}
{\end{tabular}\vspace{1ex}}
%\newenvironment{minitemize}{\begin{itemize}
%\renewcommand{\labelitemi}{\mbox{--}}
%\renewcommand{\labelitemii}{\mbox{$\bullet$}}
%\setlength{\itemsep}{0mm}
%\setlength{\topsep}{0mm}
%}{\end{itemize}}
\newenvironment{minitemize}{\begin{itemize}
\setlength{\itemsep}{0mm}
\setlength{\topsep}{0mm}
}{\end{itemize}}
\section{The Lutin language}
\subsection{Introduction}
Lutin is a language designed to program non deterministic
synchronous reactive systems.
Such systems can be useful for describing properties,
requirements, partially known systems (in particular
environments in a test process).
Executing a Lutin program consists in randomly generating
a particular behaviour consistent with its definition.
In order to guide the generation, the language provides
some constructs for controlling the random choices.
\subsection{Nodes (aka systems)}
Nodes are entry points for the simulation,
they are not modular abstraction
and thus they cannot be reused
(i.e. they are ``main'' programs).
N.B. they where called {\em systems} in the earlier versions.
A \key{node} is declared with a set of input and output
variables. Those variables may be seen as classical
locations holding data values; they are called
the {\em support variables}.
During the execution, actual input values are provided
by the environment: they are
{\em uncotrallable variables}. The program reacts by providing
output variables: they are {\em controllable variables}.
\begin{example}
\begin{program}
\key{node} foo(x: bool) \key{returns} (t: real) = \syn{Statement}
\end{program}
\end{example}
\subsection{Constraints}
The \key{node} core is a statement describing how the
support variables are evolving among time. This evolution is defined
by a {\em trace} expression.
An atomic trace is simply a constraint (i.e. a Boolean expression)
on the current value of the support. Intuitively, a constraint is a trace of
length 1.
A constraint may reffer to the previous value of a support
variable: \prg{\key{pre} x}. A \key{pre} variable is uncontrollable:
during the execution, it is inherited from the past and cannot be
modified. This is the {\em non-backtracking principle}.
\begin{example}
\begin{program}
(x \key{and} (t > \key{pre} t) \key{and} (t <= \key{pre} t + 10.0))
\end{program}
describes any valuation of the support where \prg{x} is true
and \prg{t} is comprised between its previous value and
and its previous value plus \prg{10.0}.
\end{example}
Note that, during the execution, \prg{x}, which is incontrollable, may
be false, and then the constraint may be unsatisfiable.
In this case, the constraint dynamically raises a {\em deadlock}
exception.
Handling deadlocks is a keypoint of the language:
most of the language constructs are defined in terms
of deadlock catching, as explained in the sequel.
\subsection{Basic statements}
Atomic statements are combined to describe longer traces.
Basic statements are inspired by regular expressions:
\begin{itemize}
\item Sequence: \syn{st1} \key{fby} \syn{st2}\\
executes \syn{st1}, and, if and when
it terminates, executes \syn{st2}.
If \syn{t1} deadlocks, the whole statement deadlocks.
\item Loop: \key{loop} \syn{st}\\
if \syn{st} deadlocks, terminates {\em normally}, otherwise behaves
as \syn{st} \key{fby} \key{loop} \syn{st}.
Intuitivelly, the meaning is ``loop as far as possible''.
\item Choice: \OB \syn{st1} \BAR ... \BAR \syn{stn} \CB\\
randomly choose one of the {\em startable} statements from
\syn{st1}...\syn{stn} (a statement is startable if it does not
instantaneously deadlock).
If none of them are startable, the whole statement deadlocks.
\item Priority: \OB \syn{st1} \SBAR ... \SBAR \syn{stn} \CB\\
behaves as \syn{st1} if \syn{st1} is startable, otherwise
behaves as \syn{st2} if \syn{st2} is startable, etc.
If none of them are startable, the whole statement deadlocks.
\end{itemize}
\paragraph{Non determinism and deadlocks.}
The general rule is that, if a statement can start, then it must
start; this is the {\em reactivity principle}.
For the time being, this principle concerns only the \BAR\ construct
(both \SBAR\ and \key{loop} are deterministic).
\subsection{Local variables}
Local variables can be declared with:\\
\key{exist} \syn{ident} \key{:} \syn{type} \key{in} \syn{st}\\
In their scope, local variables are equivalent to outputs,
(controllable support variables).
\subsection{Weights}
In a choice, the random selection of a particular startable
statement is uniform. For instance, if $k$ of $n$ statements
are startable, each of them is chosen with a probability of
$1/k$.
This is the reason why the choice is not a binary, associative
statement:\\ \OB \syn{st1} \BAR \OB \syn{st2} \BAR \syn{st3} \CB \CB\\
is not {\em stockastically} equivalent to\\
\OB \OB \syn{st1} \BAR \syn{st2} \CB \BAR \syn{st3} \CB
In order to influence the probabilities, the user may
assign {\em weigths} to the branches of a choice:\\
\OB \syn{st1} \key{weight} \syn{w1} \BAR ...
\BAR \syn{stn} \key{weight} \syn{wn} \CB
Weights may be integer constants, or, more generally,
{\em uncontrollable integer expression}. In other terms,
the environment and the past may influence the probabilities.
Note that weights are not probabilities, but rather
stockastic directives. Even with a huge weigth, a non startable
statement has a null probability to be chosen.
\subsection{Random loops}
Random loops are defined by constraining the number of iterations.
There are actually two predifined kind of random loops:\\
\begin{itemize}
\item Interval: \LOOPI{\syn{min}}{\syn{max}} \\
the number of iteration should be comprized between
the integer constants \syn{min} and \syn{max}
(which must satisfy $0 \leq \syn{min} < \syn{max}$).
\item Average: \LOOPA{\syn{av}}{\syn{sd}}\\
the average number of iteration should be \syn{av},
with a standard deviation \syn{sd}.
The behavior is undefined unless $4*\syn{ec} < \syn{av}$
\end{itemize}
\paragraph{Note.}
Random loops are following the {\em reactivity principle}, which means
that the actual number of loops may significantly differ from the ``expected''
one since looping may sometimes be required or impossible,
according to the satisfiability of constraints. The precise semantics
is given in~\S\ref{semantics}.
\subsection{Note on instantaneous loops}
The execution of nested loops may results on infinite,
instantaneous loops.
\begin{example}
If \syn{c} is a non satisfiable constraint, the statement
\begin{program}
\key{loop} \key{loop} \syn{c}
\end{program}
keeps the control but do nothing.
\end{example}
Programs that generates such instantaneous loops
are {\em incorrect} (this is quite similar to infinite recursion
in classical languages).
Statically checking if a program is free of instantaneous loops
is undecidable. One solution is to adopt a statical criterium
rejecting all incorrect programs, but also some correct ones.
Typically, a program is certainly free of instantaneous loop
if each control branch whitin a loop contains a statement
that ``takes time'' (i.e. a constraint).
\begin{example}
The (potentially) incorrect program:
\begin{program}
\key{loop} \key{loop} \syn{c}
\end{program}
can be safely replaced by:
\begin{program}
\key{loop} \OB \syn{c} \key{fby} \key{loop} \syn{c} \CB
\end{program}
\end{example}
The opposite solution is to accept a priori any programs
and generate a run time error if an instantaneous loops arrises
during the execution.
This is the solution adopted in the reference operationnal
semantics~\S\ref{semantics}.
\subsection{Propagating a constraint}
The statement:\\
\key{assert} \syn{exp} \key{in} \syn{st}\\
distributes the constraint \syn{exp} (a Boolean expression)
all along the statement \syn{st}.
\subsection{Parallel composition}
The statement\\
\OB \syn{st1} \ES ... \ES \syn{stn} \CB\\
executes in parallel all the statements \syn{st1} ... \syn{stn}.
All along the parallel execution each branch produces its
own constraint; the conjuntion of these local constraints
gives the global constraint.
If one branch terminates normally, the other branches continue.
The whole statement terminates if and when the last branches terminates.
If (at least) one branch stops abnormally, the whole statement
stops for the same reason (deadlock or other exception).
\paragraph{Parallelism vs 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 \syn{X} \key{weight} 1000 \BAR \syn{Y} \CB
~\ES~
\OB \syn{A} \key{weight} 1000 \BAR \syn{B} \CB
~\CB\\
where \syn{X}, \syn{A}, \syn{X$\wedge$B}, \syn{A$\wedge$Y} are all
satisfiable, but not \syn{X$\wedge$A}:
\begin{minitemize}
\item the priority can be given to \syn{X$\wedge$B}, which
does not respect the stockastic directive of the second branch,
\item or to \syn{A$\wedge$Y}, which
does not respect the stockastic directive of the first branch.
\end{minitemize}
\end{example}
In order to solve the problem, the stockastic directives are not
treated in parallel, but in {\em sequence}, from left to right:
\begin{minitemize}
\item the first branch makes its choice, according its local
stockastic directives,
\item the second one branch makes its choice, according to what has
been choosen by the first one etc.
\end{minitemize}
In the example, the priority is then given to
\syn{X$\wedge$B}.
Finally, the treatment is:
\begin{itemize}
\item parallel for the constraints (conjunction),
\item but sequential for weights directives.
\end{itemize}
Note that the concrete syntax (\ES) reflects the fact the operation
is not commutative.
\subsection{Catching deadlocks}
A dynamic deadlock can be caught using the statement:\\
\key{try} \syn{st1} \key{do} \syn{st2}\\
If a deadlock is raised during the execution of \syn{st1},
the control passe immediately to \syn{st2}. If \syn{st1}
terminates normally, the whole statement terminates and the control
passes to the sequel.
\subsection{Exceptions}
Global exceptions can be declared outside the main node:\\
\key{exception} \syn{ident}\\
or locally within a statement:\\
\key{exception} \syn{ident} \key{in} \syn{st}\\
In the last case, the classical binding rules hold.
An existing exception \syn{ident} can be raised with the statement:
\key{raise} \syn{ident}\\
An exception can be caught with the statement:\\
\key{catch} \syn{ident} \key{in} \syn{st1} \key{do} \syn{st2}\\
If the exception is raised in \syn{st1}, the control immediatelly
passes to \syn{st2}.
If the ``\key{do}'' part is omitted, the control passes
in sequence.
The following statement:\\
\key{trap} \syn{x} \key{in} \syn{st1} \key{do} \syn{st2}\\
is a shortcut for:
\key{exception} \syn{x} \key{in}
\key{catch} \syn{x} \key{in} \syn{st1} \key{do} \syn{st2}
\paragraph{Parallelism vs exception.}
There is no notion of ``muti-raising'', even when several
statements are executed in parallel.
In a parallel composition, exception raising are, like stockastic directives,
treated in sequence from left to right .
\paragraph{The \key{Deadlock} exception.}
Deaclock can be viewed as the raising of a predefined
\key{Deadlock} exception.
In fact, this exception is internal and cannot be redefined nor
raised by the user.
Te only avalaible usage of \key{Deadlock} is\\
\key{catch} \key{Deadlock} \key{in} \syn{st1} \key{do} \syn{st2}\\
for which we already know the shortcut:\\
\key{try} \syn{st1} \key{do} \syn{st2}\\
\subsection{Modularity}
The modular abstraction is the {\em combinator}.
A combinator is declared with a \key{let} statement:\\
{\tt \key{let} \syn{id} (\syn{Params}) :~\syn{Type} = \syn{St1} \key{in} \syn{St2}}\\
Notes:
\begin{itemize}
\item such a definition may appear at top-level, outside a node, in which case the "{\tt \key{in} \syn{St2}}"
is absent.
\item classical scoping rules apply for \syn{St1}: free variables are first binded to the
\syn{Params} declaration, otherwise they are binded to the scope in which the whole statement
appears.
\item the "{\tt (\syn{Params})}" part is optional; with no paramaters, the declaration simply means that
\syn{id} is an alias for the expression \syn{St1} within \syn{St2}.
\item the "{\tt :~\syn{Type}}" is optional; when absent, the type is deduced from the expression \syn{St1}.
\item the type is either a data-type (Boolean, integer, real) or the special type \key{trace}, meaning that
the expression "\syn{St1}" (and thus the identifier "\syn{id}") denotes a behaviour.
This \key{trace} type is voluntary abstracted, in particular it does not say anything about the support
variables of the denotated behavior.
\end{itemize}
Here is an example of (global) boolean combinator:
\begin{program}
\key{let} within\=(x,~min,~max:~\key{real}):~\key{bool}~= (min <= x) \key{and} (x <= max)
\end{program}
~\\
Here is an example of (global) trace combinator. It takes two traces (behavior)
and "returns" a behavior that:
\begin{itemize}
\item runs the two behavior arguments in parrallel,
\item terminates as soon as the first one terminates.
\end{itemize}
\begin{program}
\key{let} as\_long\_as(X, Y : \key{trace}) : \key{trace} = \\
\> \key{trap} \= Stop \key{in}\\
\> \> X \EA~\OB Y \key{fby} \key{raise} Stop\CB\\
\> \CB
\end{program}
\section{Syntax}
%%% Include yacc syntax
\input{lutyacc.tex}
\subsection{Lexical analysis}
\begin{itemize}
\item
Inline comments start with \key{--} and stop at the the end of the line.
\item
Comments start with \key{(*} and end at the next following \key{*)}.
\item
\bnfrightident{Ident} stands for identifier, followinf the C standard
(\bnftoken{[\_a-zA-Z][\_a-zA-Z0-9]*}),
\item
\bnfrightident{Floating} and \bnfrightident{Integer} stands for decimal floating point and integer
notations, following C standard,
\end{itemize}
\subsection{Syntax notation (EBNF)}
\begin{itemize}
\item Keywords are displayed like that: \bnftoken{keyword}
\item grammatical symbols like that: \bnfleftident{GramaticalSymbol}
\item optional parts like that: \bnfopt{something}
\item list (0 or more) parts like that: \bnflist{something}
\item grouped parts like that: \bnfgroup{something}
\end{itemize}
\subsection{Syntax}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\paragraph{Declarations.}
A lutin file ({\tt .lut}) is a list of item declarations.
At top-level, an item can be a exception, a node (main behaviour)
or a macro declaration (let).\\
\decls
\paragraph{Variable and Parameter Declaration.}
Both are declared with their type. The \bnftoken{ref} type flag may only
appear in parameter declaration. A default value
(\bnftoken{=}\bnfleftident{Exp}) may only appear in variable declaration.
\varparams
\types
\paragraph{Statements.}
A statement is basically an expression of type {\em trace},
by opposition to data expressions (\syn{Exp}). Statements are enclosed
within braces, expressions within parenthesis.
\statements
Note on exceptions:
\begin{itemize}
\item The core statements are the declaration (\key{exception}) and the
\key{catch};
\item ``\key{trap} \syn{id} \key{in} \syn{st}'' is a shortcut for
``\key{exception} \syn{id} \key{in} \key{catch} \syn{id} \key{in} \syn{st}'';
\item ``\key{try} \syn{st}'' is a shortcut for
``\key{catch} \key{DeadLock} \key{in} \syn{st}''.
\end{itemize}
\paragraph{Expression.}
They are almost classical algebraic expressions, except for
the special "operator" \bnftoken{pre} which requires an variable identifier.
\expressions
Priorities are the following, from lower precedence to higher precedence.
In the same level, the default is to group binary operators left-to-right
(note that it may result in type errors).
\begin{itemize}
\item \bnftoken{else},
\item \bnftoken{=>}, logical implication, group {\bf right-to-left},
\item \bnftoken{or},
\item \bnftoken{xor},
\item \bnftoken{and},
\item \bnftoken{=}, \bnftoken{<>},
\item \bnftoken{>}, \bnftoken{<}, \bnftoken{>=}, \bnftoken{<=},
\item \bnftoken{+}, \bnftoken{-} (binary),
\item \bnftoken{*}, \bnftoken{/}, \bnftoken{div}, \bnftoken{mod},
\item \bnftoken{not},
\item \bnftoken{-} (unary).
\end{itemize}
\paragraph{References and Arguments.}
Ident references, with or without arguments, appear in both statements and expressions.
Arguments are statements, which include the case of expressions.
\identref
\documentclass[11pt,a4paper,twoside]{article}
\usepackage{color}
\usepackage[pdftex, backref, colorlinks, linkcolor=blue]{hyperref}
\usepackage{longtable}
\usepackage{tabularx}
\usepackage[pdftex]{graphicx}
\usepackage{bold-extra}
\input{x11colors}
\setlength{\textwidth}{161mm} %21cm - (2 * 1cm)
\setlength{\textheight}{224mm}
\setlength{\oddsidemargin}{0pt}
\setlength{\evensidemargin}{0pt}
%\setlength{\topmargin}{0pt}
%\setlength{\partopsep}{0pt}
\setlength{\parskip}{0pt}
\setlength{\parindent}{0pt}
\input{commands}
\input{version}
\title{Lutin (\version-\release)}
\author{Pascal Raymond}
\begin{document}
\maketitle
\tableofcontents
%\input{lutyacc.tex}
\input{language}
\input{semantics}
\input{lutsyntax}
\end{document}
~
~
\newcommand{\trans}[1]{\mbox{$\stackrel{#1}{\rightarrow}$}}
\newcommand{\vanish}{\raisebox{-0mm}{$\;\rotatebox{90}{$\scriptstyle \hookleftarrow$}$}}