Manual
UpDown automaton (figure) Changes in the structure: contracts within Section "Syntax and informal semantics"
This commit is contained in:
Gwenal Delaval
parent
bea0c5ac7c
commit
11493f3274
5 changed files with 96 additions and 31 deletions
25
manual/figures/updown-automaton.fig
Normal file
25
manual/figures/updown-automaton.fig
Normal file
|
|
@ -0,0 +1,25 @@
|
|||
#FIG 3.2 Produced by xfig version 3.2.5b
|
||||
Landscape
|
||||
Center
|
||||
Metric
|
||||
A4
|
||||
100.00
|
||||
Single
|
||||
-2
|
||||
1200 2
|
||||
1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 1350 1350 315 315 1350 1350 1350 1665
|
||||
1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 3150 1350 315 315 3150 1350 3150 1665
|
||||
3 0 0 1 0 7 50 -1 -1 0.000 0 1 0 3
|
||||
0 0 1.00 60.00 120.00
|
||||
1575 1125 2250 900 2925 1125
|
||||
0.000 1.000 0.000
|
||||
3 0 0 1 0 7 50 -1 -1 0.000 0 1 0 3
|
||||
0 0 1.00 60.00 120.00
|
||||
2925 1575 2250 1800 1575 1575
|
||||
0.000 1.000 0.000
|
||||
4 1 0 50 -1 0 12 0.0000 6 150 525 3150 1395 Down\001
|
||||
4 0 0 50 -1 0 12 0.0000 6 195 1935 3510 1395 \\lstinline{x = last x - 1}\001
|
||||
4 1 0 50 -1 0 12 0.0000 6 195 255 1350 1395 Up\001
|
||||
4 2 0 50 -1 0 12 0.0000 6 195 1995 990 1395 \\lstinline{x = last x + 1}\001
|
||||
4 1 0 50 -1 0 12 0.0000 6 210 1815 2250 900 $\\mathtt{x} \\geq 10$\001
|
||||
4 1 0 50 -1 0 12 0.0000 6 210 1650 2250 1935 $\\mathtt{x} \\leq 0$\001
|
||||
BIN
manual/figures/updown-automaton.pdf
Normal file
BIN
manual/figures/updown-automaton.pdf
Normal file
Binary file not shown.
24
manual/figures/updown-automaton.tex
Normal file
24
manual/figures/updown-automaton.tex
Normal file
|
|
@ -0,0 +1,24 @@
|
|||
\begin{picture}(0,0)%
|
||||
\includegraphics{figures/updown-automaton}%
|
||||
\end{picture}%
|
||||
\setlength{\unitlength}{4144sp}%
|
||||
%
|
||||
\begingroup\makeatletter\ifx\SetFigFont\undefined%
|
||||
\gdef\SetFigFont#1#2{%
|
||||
\fontsize{#1}{#2pt}%
|
||||
\selectfont}%
|
||||
\fi\endgroup%
|
||||
\begin{picture}(2550,1296)(976,-1174)
|
||||
\put(3151,-556){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}{\color[rgb]{0,0,0}Down}%
|
||||
}}}}
|
||||
\put(3511,-556){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\color[rgb]{0,0,0}\lstinline{x = last x - 1}}%
|
||||
}}}}
|
||||
\put(1351,-556){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}{\color[rgb]{0,0,0}Up}%
|
||||
}}}}
|
||||
\put(991,-556){\makebox(0,0)[rb]{\smash{{\SetFigFont{12}{14.4}{\color[rgb]{0,0,0}\lstinline{x = last x + 1}}%
|
||||
}}}}
|
||||
\put(2251,-61){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}{\color[rgb]{0,0,0}$\mathtt{x} \geq 10$}%
|
||||
}}}}
|
||||
\put(2251,-1096){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}{\color[rgb]{0,0,0}$\mathtt{x} \leq 0$}%
|
||||
}}}}
|
||||
\end{picture}%
|
||||
|
|
@ -462,8 +462,8 @@ activation instant.
|
|||
\paragraph{Example}
|
||||
\label{sec:example}
|
||||
|
||||
The following example gives the node \texttt{updown}. This node is defined by an
|
||||
automaton composed of two states:
|
||||
The following example gives the node \texttt{updown}. This node is defined by the
|
||||
automaton given in Figure~\ref{fig:updown-automaton}, composed of two states:
|
||||
\begin{itemize}
|
||||
\item the state \texttt{Up} gives to \texttt{x} its previous value augmented of 1
|
||||
\item the state \texttt{Down} gives to \texttt{x} its previous value diminued of 1
|
||||
|
|
@ -476,6 +476,13 @@ This automaton comprises two transitions:
|
|||
equal 0.
|
||||
\end{itemize}
|
||||
|
||||
\begin{figure}[htb]
|
||||
\centering
|
||||
\input{figures/updown-automaton}
|
||||
\caption{Automaton of the \texttt{updown} node}
|
||||
\label{fig:updown-automaton}
|
||||
\end{figure}
|
||||
|
||||
\begin{lstlisting}
|
||||
node updown() returns (y:int)
|
||||
var last x:int = 0;
|
||||
|
|
@ -493,9 +500,9 @@ tel
|
|||
\end{lstlisting}
|
||||
|
||||
\[
|
||||
\begin{streams}{14}
|
||||
\text{current state} & Up & Up & Up & Up & Up & Up & Up & Up & Up & Up & Down & Down & Down & \ldots\\\hline
|
||||
\mathtt{y} & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 & 10 & 9 & 8 & 7 & \ldots\\\hline
|
||||
\begin{streams}{9}
|
||||
\text{current state} & Up & Up & \ldots & Up & Up & Down & Down & Down & \ldots\\\hline
|
||||
\mathtt{y} & 1 & 2 & \ldots & 9 & 10 & 9 & 8 & 7 & \ldots\\\hline
|
||||
\end{streams}
|
||||
\]
|
||||
|
||||
|
|
@ -601,9 +608,12 @@ If the backend support parametricity (like in Java), static parameters are kept
|
|||
|
||||
Memory allocation~\cite{Gerard:2012} avoids unnecessary array copies within the nodes automatically (it can be enable with the \texttt{-memalloc} or \texttt{-O} options). In order to avoid copies when calling nodes, the user must add \emph{location annotations}. We will give here only a short introduction, the interested reader can refer to~\cite{Gerard:2012} for more details. They express the fact that a function modifies in-place its argument. For instance, consider this node that swaps two elements in an array:
|
||||
\begin{lstlisting}
|
||||
node swap(i, j:int; t_in:float^100 at r) returns (t_out:float^100 at r)
var t_tmp:float^100 at r;
|
||||
let
t_tmp = [ t_in with [i] = t_in[>j<] ];
|
||||
t_out = [ t_tmp with [j] = t_in[>i<] ];
tel
|
||||
node swap(i, j:int; t_in:float^100 at r) returns (t_out:float^100 at r)
|
||||
var t_tmp:float^100 at r;
|
||||
let
|
||||
t_tmp = [ t_in with [i] = t_in[>j<] ];
|
||||
t_out = [ t_tmp with [j] = t_in[>i<] ];
|
||||
tel
|
||||
\end{lstlisting}
|
||||
The location annotations are introduced by the keyword \lstinline{at} followed by a location name. All the streams with the same location name are guaranteed to be stored together in the generated code, so the function generated for \texttt{swap} will directly modify its argument in-place.
|
||||
|
||||
|
|
@ -613,9 +623,11 @@ Only located variables can be given to a function that expects located arguments
|
|||
\begin{lstlisting}
|
||||
node shuffle(i_arr, j_arr : int^m; q : int) = (v : float)
|
||||
var t, t_prev : float^n at r;
|
||||
let
init<<r>> t_prev = t_0 fby t;
|
||||
let
|
||||
init<<r>> t_prev = t_0 fby t;
|
||||
t = fold<<m>> swap(i_arr, j_arr, t_prev);
|
||||
v = t[>q<];
tel
|
||||
v = t[>q<];
|
||||
tel
|
||||
\end{lstlisting}
|
||||
|
||||
|
||||
|
|
@ -627,11 +639,15 @@ external fun sort(a:int^100) = (o:int^100)
|
|||
\end{lstlisting}
|
||||
The imported function should respect the calling convention given in appendix \ref{sec:app-generated-code}. See the directory \texttt{examples/extern\_C} for a complete example.
|
||||
|
||||
\section{BZR: Contracts for controller synthesis}
|
||||
Interface files can be compiled with \texttt{heptc}, in order to obtain a
|
||||
compiled interface (\texttt{.epci} file), necessary for the subsequent use of
|
||||
the declared types and values in other Heptagon programs.
|
||||
|
||||
\subsection{Contracts for controller synthesis}
|
||||
\label{sec:extens-with-contr}
|
||||
|
||||
Contracts are an extension of the Heptagon language, so as to allow to perform
|
||||
discrete controller synthesis on Heptagon programs. The extended language is
|
||||
discrete controller synthesis (DCS) on Heptagon programs. The extended language is
|
||||
named BZR.
|
||||
|
||||
We associate to each node a \emph{contract}, which is a program associated with
|
||||
|
|
@ -666,7 +682,7 @@ let
|
|||
tel
|
||||
\end{lstlisting}
|
||||
|
||||
\section{BZR Running Example: Multi-task System}
|
||||
\section{Example with Contracts: Multi-task System}
|
||||
\label{sec:multi-task-system}
|
||||
|
||||
\subsection{Delayable Tasks}
|
||||
|
|
@ -708,7 +724,7 @@ node delayable(r,c,e:bool) returns (act:bool)
|
|||
|
||||
The Figure~\ref{fig:n-del-task} shows then a node \texttt{ntasks} where $n$
|
||||
delayable tasks have been put in parallel. The tasks are inlined so as to be
|
||||
able to perform DSC on this node, taking into account the tasks' states. Until
|
||||
able to perform DCS on this node, taking into account the tasks' states. Until
|
||||
now, the only interest of modularity is, from the programmer's point of view, to
|
||||
be able to give once the delayable task code.
|
||||
|
||||
|
|
@ -916,7 +932,7 @@ An example of main C code for the execution of this node would be then:
|
|||
\begin{lstlisting}[language=C]
|
||||
#include "example.h"
|
||||
|
||||
int main(int argc, char * argv[]) \{
|
||||
int main(int argc, char * argv[]) {
|
||||
|
||||
Example__f_m mem;
|
||||
t$_{1}$ x$_{1}$;
|
||||
|
|
@ -927,7 +943,7 @@ int main(int argc, char * argv[]) \{
|
|||
/* initialize memory instance */
|
||||
f_reset(&mem);
|
||||
|
||||
while(1) \{
|
||||
while(1) {
|
||||
/* read inputs */
|
||||
scanf("...", &x$_{1}$, ..., &x$_{n}$);
|
||||
|
||||
|
|
@ -936,8 +952,8 @@ int main(int argc, char * argv[]) \{
|
|||
|
||||
/* write outputs */
|
||||
printf("...", ans.y$_{1}$, ..., ans.y$_{p}$);
|
||||
\}
|
||||
\}
|
||||
}
|
||||
}
|
||||
\end{lstlisting}
|
||||
|
||||
The above code is nearly what is produce for the simulator with the \texttt{-s}
|
||||
|
|
|
|||
|
|
@ -50,8 +50,8 @@
|
|||
|
||||
\lstdefinelanguage{Heptagon}
|
||||
{%
|
||||
keywords={node,returns,let,tel,var,pre,fby,when,whenot,merge,if,then,else,or,not,at,init,map,fold,mapdold,foldi,mapi},%
|
||||
morekeywords=[2]{automaton,state,until,unless,end,present,switch,inlined},%
|
||||
keywords={node,returns,let,tel,var,pre,last,fby,when,whenot,merge,if,then,else,or,not,at,init,map,fold,mapdold,foldi,mapi},%
|
||||
morekeywords=[2]{automaton,state,until,unless,end,present,switch,do,inlined},%
|
||||
morekeywords=[2]{contract,assume,enforce,with},%
|
||||
otherkeywords={->,&},%
|
||||
comment=[n]{(*}{*)},%
|
||||
|
|
@ -62,7 +62,7 @@
|
|||
% morekeywords={link,to},%
|
||||
% }[keywords,comments]
|
||||
|
||||
%% rËgles d'infÈrence
|
||||
%% regles d'inference
|
||||
|
||||
\RequirePackage{mathpartir}
|
||||
|
||||
|
|
@ -96,7 +96,7 @@
|
|||
%\newcommand{\ovfun}[1]{\xrightarrow{#1}}
|
||||
\newcommand{\ovfun}[1]{{\;-\mskip-1.5\thinmuskip\langle{#1}\rangle\!\!\!\rightarrow\;}}
|
||||
|
||||
%% Typage --- gÈnÈral
|
||||
%% Typage --- general
|
||||
|
||||
\DeclareMathOperator{\FV}{FV}
|
||||
\DeclareMathOperator{\FTV}{FTV}
|
||||
|
|
@ -111,7 +111,7 @@
|
|||
|
||||
\newcommand{\mergeenv}{\uplus}
|
||||
|
||||
%% Types de donnÈes
|
||||
%% Types de donnees
|
||||
|
||||
\newcommand{\type}[3]{\ensuremath{#1\vdash#2:#3}}
|
||||
|
||||
|
|
@ -194,7 +194,7 @@
|
|||
|
||||
\newcommand{\subck}{\ensuremath{<:}}
|
||||
|
||||
%% SÈmantique synchrone
|
||||
%% Semantique synchrone
|
||||
|
||||
\newcommand{\clock}[1]{\ensuremath{\langle#1\rangle}}
|
||||
|
||||
|
|
@ -264,7 +264,7 @@
|
|||
\shortcal{Y}
|
||||
\shortcal{Z}
|
||||
|
||||
%% mots-clÈs
|
||||
%% mots-cles
|
||||
|
||||
\newcommand{\m@thspace}{%
|
||||
\ifmmode\ \fi%
|
||||
|
|
@ -309,7 +309,7 @@
|
|||
\newcommand{\unop}[2]{\begkw{#1}{#2}}
|
||||
\newcommand{\funct}[2]{\begkw{#1}{#2}}
|
||||
|
||||
%% Mots-clÈs Lucid Synchrone
|
||||
%% Mots-cles Lucid Synchrone
|
||||
|
||||
\begkw{\Assume}{assume}
|
||||
\begkw{\Automaton}{automaton}
|
||||
|
|
@ -374,7 +374,7 @@
|
|||
|
||||
\newcommand{\Nil}{\ensuremath{\mathit{nil}}}
|
||||
|
||||
%% Mots-clÈs rÈpartition
|
||||
%% Mots-cles repartition
|
||||
|
||||
\midkw{\At}{at}
|
||||
\begkw{\Site}{site}
|
||||
|
|
@ -408,7 +408,7 @@
|
|||
\ |\ \False \rightarrow #3
|
||||
}
|
||||
|
||||
%% ThÈorËmes, dÈfinitions, remarques...
|
||||
%% Theoremes, definitions, remarques...
|
||||
|
||||
\RequirePackage{amsmath}
|
||||
|
||||
|
|
@ -429,7 +429,7 @@
|
|||
\newcommand{\noeuds}{n\oe uds\xspace}
|
||||
\newcommand{\Noeuds}{N\oe uds\xspace}
|
||||
|
||||
%% Macros mathÈmatiques
|
||||
%% Macros mathematiques
|
||||
|
||||
\providecommand{\tonfirst}{}
|
||||
\newcommand{\ton}[1][1]{\renewcommand{\tonfirst}{#1}\tonbis}
|
||||
|
|
@ -465,7 +465,7 @@
|
|||
|
||||
|
||||
|
||||
%% Flots de donnÈes
|
||||
%% Flots de donnees
|
||||
|
||||
\newenvironment{streams}[1]{%
|
||||
\setlength{\arraycolsep}{0.3cm}
|
||||
|
|
@ -495,7 +495,7 @@
|
|||
|
||||
\renewenvironment{amodifier}{}{}
|
||||
|
||||
%% BoÓte-noeud code
|
||||
%% Boite-noeud code
|
||||
|
||||
\RequirePackage{alltt}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue