From 11493f32744dfd8bcf8b10788dba8f10676adda0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=EBl=20Delaval?= Date: Thu, 5 Jul 2012 17:22:53 +0200 Subject: [PATCH] Manual UpDown automaton (figure) Changes in the structure: contracts within Section "Syntax and informal semantics" --- manual/figures/updown-automaton.fig | 25 +++++++++++++ manual/figures/updown-automaton.pdf | Bin 0 -> 3368 bytes manual/figures/updown-automaton.tex | 24 +++++++++++++ manual/heptagon-manual.tex | 52 ++++++++++++++++++---------- manual/macros.sty | 26 +++++++------- 5 files changed, 96 insertions(+), 31 deletions(-) create mode 100644 manual/figures/updown-automaton.fig create mode 100644 manual/figures/updown-automaton.pdf create mode 100644 manual/figures/updown-automaton.tex diff --git a/manual/figures/updown-automaton.fig b/manual/figures/updown-automaton.fig new file mode 100644 index 0000000..0978eb3 --- /dev/null +++ b/manual/figures/updown-automaton.fig @@ -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 diff --git a/manual/figures/updown-automaton.pdf b/manual/figures/updown-automaton.pdf new file mode 100644 index 0000000000000000000000000000000000000000..2737b3d875d93f522c394877fac5bd3d0fc5ab6d GIT binary patch literal 3368 zcmb_fX;>528m_h$83f7|)VlSEa)W3xGuac92xL(!Q3zPE)MZE}$;c#=P9`QnTen(8 zEG|{7qPVoSYO7U>Vkx$Y*ScISw~JMA*Q<|pt#Yl~RqvS)1i3!8KRkbO@||xz@A=*@ zNy;>sgt$nGB<;B}cQqmd7+~_pBN`2wLAo8B6Ud>&f|@9rBUyl&Xo4dRq?NIeIvwKW zSdwrdfn^_z7_i`kvcmx%vO8v6TQKaekQj{#`b&vO~)I z4%yA|pKbaOE3Y41cJli0h@sOXPIbC^W@W$HTji?qlFE;`z?~&=U8{bZue#Zz=g0(V zUy7vmn6A8J#h%;KH$;!G@hvX>;)4SJr3V|AZ?U@1`TR5L)jO8&IuqmB{^dWYqf3il z7!|bVZYQH}7k&QyfE{I`p4%U^oux+#k>nMz?wSWhXq|G;TTzj-spSWhe+T;|)iD)g zcD4Bg?CJkaT<6%RW1635TedvhYz)kcF?14_1~2$F?tN7ES;KewA11d^T{wSB+7Nj) zs{b8_Sa>Zib>`ptIpbdJSYDd;@$aREcV0=R53ZHfj1)=7FFcb|a3^QpzQpV=-;2ej z3`mIV5Gl<6<=4G&T$kwbw3-ah!5M|o#cwB-oISqo7PYfR{V(U5tbUzJKkd_7S#)Dj zd-~ke+^CB98SQd`VAG=4KOPi}KIf0Gj~{zUW1XG0BdYr!T^pFu&JKZfb?7E#UE!O% zXW7fPuOuRe>J#4nv^dKjIMk)S@`YT}t%F$RicY&O&FFmkKSkE-uN&w07-6`&Y23xr z$1CTkcE)8+?^R~>wXLWb7vcQY*mJ{z3CAktX06RTk<$HS(XPwaYLCt@@&lE2_5K}3yuSm_};>wIK_nIU+Aer#+^341HeK+>hwM&mi6nEX1 zRi5gJugkTJo3*y>vYd2bd{7hLacI3D|B&b9uR8Bux&9qzk?}%_a@>TfuNN`wc1tlm z1`H`tnaWnZ|1)^7YT&d#YAuds>jwAOS=Ie;MmxQG@uq|8qS)A1yNNz8dvDl*#3Sh= zQ&x&kba|zkT3y^{wS0}^M)JM(*F+nO+W&r~+iOYO6_M%-T%vS%_92H;_?2fdDFI4XZ%&RRKBJY(|7J>Ba^n=d6J#Ds;Zd~z`JWCC4llNfKU!zfDWZ>UXX|I8CsCh0DADj=y(fL{IO}+ zQcrLM%{ZD|gflgh9ASeeK-DU=;z|4Fyb*MGrWxQmT{uU+j4*Lp6bNr-X)b{G8a@nN zVN*B+&GzMU{H5laGnxn&m&l|#T^JV4z<`Ia7LXjsCmobqE4cp6cLG4!w1SZ`GiLVa zNhdY9kR`JVhvirc3#=-eV4x1s3?v|$q%c5ug!T|~djaXSY7_OA3{xVn5KsqP9v7?{ z1YES+s}5)dArm#+^I}v0LMmK=R*-AX1RTTA1r!IwB9#ai;*$Qr&Jr%t&#(mm7s&^LJgre=;nxk(CzIFNxm#!XeX_t5XVWY z5Q9solHmkqBQX_5;!Tk}Ei!x}6g+^jB=8F0P7NQf&1WT9tzb}Q1{maIyj){wpcE-^ z0UECSIV1!Td3x;-#&Gc(sG~MBHp(6}z~<43F2`1-C9oqhg~a~?O+19%MKFO4Avkf$+8$uN~z qZjwtSMn$?_fg6mtQD)NpxyESzr-PRxST1y-5?CRUlw=%kLjDJ8bb#Lg literal 0 HcmV?d00001 diff --git a/manual/figures/updown-automaton.tex b/manual/figures/updown-automaton.tex new file mode 100644 index 0000000..39e7e4d --- /dev/null +++ b/manual/figures/updown-automaton.tex @@ -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}% diff --git a/manual/heptagon-manual.tex b/manual/heptagon-manual.tex index 368709f..c0e6fb4 100644 --- a/manual/heptagon-manual.tex +++ b/manual/heptagon-manual.tex @@ -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<> t_prev = t_0 fby t; +let + init<> t_prev = t_0 fby t; t = fold<> 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} diff --git a/manual/macros.sty b/manual/macros.sty index 27c5e47..ea1534c 100644 --- a/manual/macros.sty +++ b/manual/macros.sty @@ -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}