Manual: section on compilation and install

Manual: section on compilation, install, required tools and libraries

manual/heptagon-manual.tex

@@ -82,9 +82,77 @@ An execution of the node \texttt{plus} can then be:
 \end{streams}
 \]
 
-\subsection{Compilation}
+\subsection{Required tools}
+\label{sec:required-tools}
+
+The use of the Heptagon compiler by itself does not require any additional
+tools. However, the usual use involves a compiler for the generated code (e.g.,
+\texttt{gcc} for C generated code, or \texttt{javac} for Java).
+
+The tools below are optional or are related to some subparts of Heptagon:
+\begin{itemize}
+\item The graphical display tool \texttt{sim2chro} can be obtained from
+Verimag\footnote{\url{http://www-verimag.imag.fr/~raymond/edu/distrib/}}. It can
+be used together with the graphical simulator \texttt{hepts} (see Section~\ref{sec:simulation}).
+\item The \texttt{Sigali} tool for model-checking and discrete controller
+  synthesis \cite{sigali}
+  \footnote{\url{http://www.irisa.fr/vertecs/Logiciels/sigali.html}} is
+  mandatory for the use of contracts (see
+  Section~\ref{sec:extens-with-contr}). \texttt{Sigali} can be downloaded on the
+  BZR website : \url{http://bzr.inria.fr}.
+\end{itemize}
+
+\subsection{Compilation and installation}
+\label{sec:comp-inst}
+
+\subsubsection{Required libraries and tools for the compilation}
+\label{sec:requ-libr-tools}
+
+The compilation of the Heptagon compiler requires:
+\begin{itemize}
+\item \texttt{OCaml}\footnote{\url{http://caml.inria.fr}} (version $\geq$
+  3.11), and the \texttt{ocamlbuild} and \texttt{ocamlfind} tools
+\item the \texttt{Menhir}\footnote{\url{http://gallium.inria.fr/~fpottier/menhir/}} parser generator
+\item the \texttt{ocamlgraph}\footnote{\url{http://ocamlgraph.lri.fr}} library.
+\end{itemize}
+
+The compilation of the Heptagon simulator (optional) requires the
+\texttt{LablGTK2}\footnote{\url{http://wwwfun.kurims.kyoto-u.ac.jp/soft/lsl/lablgtk.html}}
+library.
+
+
+\subsubsection{Compilation}
 \label{sec:compilation}
 
+Once the compiler is downloaded and untarred, go into the \texttt{heptagon/} and
+type :
+
+\begin{alltt}
+> ./configure && make
+\end{alltt}
+
+This command will build the compiler, optionally the simulator (if the
+\texttt{LablGTK2} library is found), and the standard library.
+
+\subsubsection{Installation}
+\label{sec:installation}
+
+After the compilation, or the download and untar of the binary distribution, go
+into the \texttt{heptagon/} directory and type :
+
+\begin{alltt}
+> make install
+\end{alltt}
+
+By default, this will install the binaries (\texttt{heptc} and \texttt{hepts}) into
+\texttt{/usr/local/bin} and the standard library into
+\texttt{/usr/local/lib}. Consider the \texttt{configure} script options
+(\verb+./configure --help+) for other specific needs.
+
+
+\subsection{Heptagon programs compilation}
+\label{sec:hept-compilation}
+
 The Heptagon compiler is named \texttt{heptc}. Its list of options is available by
 :
 
@@ -449,7 +517,7 @@ The following operators are defined for arrays:
 \item Accessing an element at a constant index: \lstinline{t[4]}
 \item Accessing an element at a dynamic index with a default value: \lstinline{z = t.[x] default v} is a stream defined by $z_i = t_i[x_i]$ if $0 \leq x_i < n$ and $z_i = v_i$ otherwise (where $n$ is the size of \lstinline+t+).
 \item Accessing an element at a truncated index: \lstinline+z = t[>x<]+ is defined by $z_i = t_i[\min(\max(0, x_i), n-1)]$ (where $n$ is the size of \lstinline+t+).
-\item Modifying an element: \lstinline{t' = [ t with [x] = v ]} is a new array equal to \lstinline+t+, except for the element at index \lstinline+x+ which is equal to $v$, that is for all j in $[0, n-1]$ such that $j \neq x_i$, $t'_i[j] = t[j]$ and $t'_i[x_i] = v_i$.
+\item Modifying an element: \lstinline{t' = [ t with [x] = v ]} is a new array equal to \lstinline+t+, except for the element at index \lstinline+x+ which is equal to $v$, that is for all j in $[0, n-1]$ such that $j \neq x_i$, $t'_i[j] = t_i[j]$ and $t'_i[x_i] = v_i$.
 \item Defining an array by copying one value: \lstinline+x^n+ is the array of size \lstinline+n+ whose elements are all equal to \lstinline+x+.
 \item Defining an array explicitely:  \lstinline+[1, x, 3, y, 5]+.
 \item Extracting a slice: \lstinline+t[n..m]+ returns the sub array of \lstinline+t+ of size \lstinline{m-n+1} starting at index \lstinline+n+ and ending at index \lstinline+m+.

manual/macros.sty

@@ -53,7 +53,7 @@
   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},%
   morekeywords=[2]{contract,assume,enforce,with},%
-  otherkeywords={->,&,=},%
+  otherkeywords={->,&},%
   comment=[n]{(*}{*)},%
 }[keywords,comments]
 

manual/manual.bib

@@ -17,3 +17,41 @@
 	Keywords = {synchronous programming; type system},
 	Title = {A Modular Memory Optimization for Synchronous Data-Flow Languages},
 	Year = {2012}}
+
+@Article{sigali,
+  author =	 {H. Marchand and P. Bournai and M. Le Borgne and
+                  P. Le Guernic},
+  title =	 {Synthesis of Discrete-Event Controllers based on the
+                  {Signal} Environment},
+  journal =	 {Discrete Event Dynamic System: Theory and
+                  Applications},
+  year =	 2000,
+  volume =	 10,
+  number =	 4,
+  month =	 oct,
+  annote =	 {Description of the \textsc{Sigali} tool.}
+}
+
+@InProceedings{lctes10,
+  Author       = {Gwena{\"e}l Delaval and Herv{\'e} Marchand and Eric
+                  Rutten},
+  Title        = {Contracts for Modular Discrete Controller Synthesis},
+  Booktitle    = {Proceedings of the ACM SIGPLAN/SIGBED Conference on
+                  Languages, Compilers and Tools for Embedded Systems,
+                  LCTES 2010},
+  address      = {Stockholm, Sweden},
+  Pages        = {57--66},
+  Year         = 2010,
+  month        = apr,
+  Note         = {\url{http://doi.acm.org/10.1145/1755951.1755898}}
+}
+
+@InProceedings{ls-automata,
+  author       = {J.-L. Cola\c{c}o and B. Pagano and M.  Pouzet},
+  title        = {{A Conservative Extension of Synchronous Data-flow
+                  with State Machines}},
+  booktitle    = {ACM Int. Conf. on Embedded Software (EMSOFT'05)},
+  address      = {Jersey city, New Jersey, USA},
+  month        = {September},
+  year         = 2005,
+}