jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

User manual for Heptagon+ReaX

Browse source
This commit is contained in:
Gwenaël Delaval 2015-09-17 16:54:10 +02:00
parent 015875b279
commit 8dbb283310
3 changed files with 774 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

BIN
manual/heptreax-manual.pdf Normal file
View file

Binary file not shown.

589
manual/heptreax-manual.tex Normal file
View file

@ -0,0 +1,589 @@
\documentclass[a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[a4paper,margin=2cm]{geometry}
%\usepackage[francais]{babel}
%\usepackage{subfigure}
%\usepackage{fancyvrb}
%\usepackage{fancyhdr}
\usepackage{hyperref}
\usepackage{tabularx}
\usepackage{xcolor}
\usepackage{helvet}
%\usepackage{comment}
%\usepackage{lmodern}
\usepackage{varwidth}
\usepackage{tikz}
\usetikzlibrary{arrows,calc}
\usetikzlibrary{automata}
\usepackage{tikz-timing}
%\usetikzlibrary{matrix}
%\usetikzlibrary{shapes}
%\usetikzlibrary{positioning}
\usepackage{macros}
\usepackage{listings}
\usepackage{mathpazo}
% fontes tt avec gras (mots-clés)
\renewcommand{\ttdefault}{txtt}
\definecolor{deepgreen}{rgb}{0.09,0.32,0.09}
\definecolor{deepyellow}{rgb}{0.6,0.6,0}
\definecolor{kwcolor}{rgb}{0.6,0.1,0.1}
\lstset{
language=Heptagon,% numbers=left, numberstyle=\small,
basicstyle=\normalsize\ttfamily,captionpos=b,
keywordstyle=\color{kwcolor},
frame={tb}, rulesep=1pt, columns=fullflexible,
xleftmargin=1cm, xrightmargin=1cm,
mathescape=true
}
\tikzset{>=stealth'}
\tikzset{
format/.style={rectangle,draw,color=blue,fill=blue!10},
tool/.style={rectangle,draw,color=red,fill=red!10,rounded corners}
}
\title{Programming and controller synthesis with Heptagon/BZR and ReaX}
\author{Nicolas Berthier \and Gwenaël Delaval}
\date{}
\begin{document}
\maketitle
\section{Introduction}
Heptagon/BZR\footnote{\url{http://bzr.inria.fr}}\cite{delaval13:bzr_jdeds}
is a reactive language, belonging to the synchronous languages family,
whose main feature is to include discrete controller synthesis within
its compilation.
It is equipped with a behavioral contract mechanisms, where
assumptions can be described, as well as an ``enforce'' property part:
the semantics of this latter is that the property should be enforced
by controlling the behaviour of the node equipped with the
contract. This property will be enforced by an automatically built
controller, which will act on free controllable variables given by the
programmer.
ReaX\footnote{\url{http://reatk.gforge.inria.fr}}\cite{berthier14:_reax}
is a controller synthesis tool, dedicated to the control of
logico-numerical programs.
This report documents the integration of these two tools.
\section{Heptagon/BZR in a (small) nutshell}
Heptagon is a synchronous dataflow language, with a syntax allowing the
expression of control structures (e.g., switch or mode automata).
A typical Heptagon program will take as input a sequence of values,
and will output a sequence of values. Then, variables (inputs, outputs
or locals) as well as constants are actually variable or constant
\emph{streams}. The usual operators (e.g., arithmetic or Boolean
operators) are applied pointwise on these sequences of values.
Heptagon programs are structured in \emph{nodes}, which are provided
with \emph{inputs} and \emph{outputs}, and possibly local variables. A
node is defined by mean of a set of \emph{parallel equations},
defining the local variables and outputs' current values, as functions
of current inputs, other variables' values, and current state.
Figure~\ref{fig:hept-exple} shows a short Heptagon example. It
consists of a two-mode automaton, with a mode \emph{Up} in which the
output is increased by the current input value, and a mode \emph{Down}
in which the output is decreased. The output \texttt{y}'s current
value is defined as the current value of the local variable
\texttt{x}, whose last value is recorded sp as tp be used in the
computation performed on the next step. In the \texttt{Up}
(resp. \texttt{Down}) mode, \texttt{x} is defined as the value of
\texttt{x} at the previous instant, increased (resp. decreased) by the
current value of the input \texttt{v}. The automaton stays in the
\texttt{Up} mode until \texttt{x} is greater or equal 10; meaning that
when this condition is true, the next mode will be the mode
\texttt{Down}.
\begin{figure}[hbp]
\centering
\begin{lstlisting}
node twomodes(v:int) returns (y:int)
var last x : int = 0;
let
y = x;
automaton
state Up
do x = last x + v
until x >= 10 then Down
state Down
do x = last x - v
until x <= 0 then Up
end
tel
\end{lstlisting}
\scalebox{1.5}{
\begin{tikztimingtable}
v & 2D{2} D{1} D{5} D{2} D{1} D{0} D{3}\\
State & 4D{\texttt{Up}} 4D{\texttt{Down}}\\
\texttt{twomodes}(v) & D{2} D{4} D{5} D{10} D{8} 2D{7} D{4}\\
\end{tikztimingtable}
}
\caption{Heptagon short example}
\label{fig:hept-exple}
\end{figure}
The Heptagon/BZR language provides a \emph{contract} construct,
allowing the expression of assumptions on the environment (inputs)
(\texttt{assume} keyword), and guaranteed or enforced properties
(\texttt{enforce} keyword) on the outputs.
For example, the \texttt{twomodes} node given above can be enriched
with a contract, saying that if for every instant, $0 \leq \mathtt{v}
\leq 1$, then the property $0 \leq \mathtt{twomodes(v)} \leq 10$ will always hold (Fig.~\ref{fig:exple-contract}).
\begin{figure}[htbp]
\centering
\begin{lstlisting}
node twomodes (v:int) = (y:int)
contract
assume (v <= 1) & (v >= 0)
enforce (o <= 10) & (o >= 0)
var last x : int = 0;
let
y = x;
automaton
state Up
do x = last x + v
until x >= 10 then Down
state Down
do x = last x - v
until x <= 0 then Up
end
tel
\end{lstlisting}
\caption{Example of contract in Heptagon/BZR}
\label{fig:exple-contract}
\end{figure}
Contracts can also be provided with a declaration of
\emph{controllable variables}: these variables are local to the node,
and their value can be used into it. However, these variables are not
defined by the programmer. Their value will be given, during
execution, by a \emph{controller}, which will be computed offline by a
\emph{controller synthesis tool}.
Figure~\ref{fig:exple-contvar} shows how the \texttt{twomodes} node
can be equipped with a controllable variable \texttt{c}, which will
\emph{control} the transition between the two modes.
\begin{figure}[htbp]
\centering
\begin{lstlisting}
node twomodes (v:int) = (y:int)
contract
assume (v <= 1) & (v >= 0)
enforce (o <= 10) & (o >= 0)
with (c:bool)
var last x : int = 0;
let
y = x;
automaton
state Up
do x = last x + v
until c then Down
state Down
do x = last x - v
until c then Up
end
tel
\end{lstlisting}
\caption{Contract with one controllable variable}
\label{fig:exple-contvar}
\end{figure}
We will see in the following sections how these contracts can be
handled by the ReaX verification and synthesis tool.
\section{Integration of Reax and Heptagon/BZR}
\subsection{Compilation chain}
Figure~\ref{fig:bzreax-compil} describes the full compilation process,
involving the Heptagon/BZR compiler (\texttt{heptc}) and the ReaX
controller synthesis tool.
\begin{figure}
\centering
\begin{tikzpicture}[node distance=2cm]
\node[format] (Heptagon) {\begin{tabular}{c}Heptagon\\\texttt{.ept}\end{tabular}};
\node[tool,below of=Heptagon] (Heptc) {\begin{tabular}{c}Heptagon compiler\\\texttt{heptc}\end{tabular}};
\node[format,below of=Heptc] (Ctrln) {\begin{tabular}{c}Ctrl-n equations\\\texttt{.ctrln}\end{tabular}};
\node[tool,below of=Ctrln] (ReaX) {\begin{tabular}{c}ReaX synthesis tool\\\texttt{reax}\end{tabular}};
\node[format,below of=ReaX] (Controller) {\begin{tabular}{c}Controller function\\\texttt{.ctrlf}\end{tabular}};
\node[tool,below of=Controller] (Ctrl2ept) {\begin{tabular}{c}Controller compiler\\\texttt{ctrl2ept}\end{tabular}};
\node[format,below of=Ctrl2ept] (HeptagonCtrlr) {\begin{tabular}{c}Heptagon\\\texttt{.ept}\end{tabular}};
\node[tool,below of=HeptagonCtrlr] (HeptcCtrlr) {\begin{tabular}{c}Heptagon compiler\\\texttt{heptc}\end{tabular}};
\node[format,below left of=HeptcCtrlr,node distance=3cm] (C) {\begin{tabular}{c}C program\\\texttt{.c}\end{tabular}};
\node[format,below right of=HeptcCtrlr,node distance=3cm] (Java) {\begin{tabular}{c}Java program\\\texttt{.java}\end{tabular}};
\node[tool,below of=C] (Gcc) {\begin{tabular}{c}C compiler\\\texttt{gcc}\end{tabular}};
\node[tool,below of=Java] (Javac) {\begin{tabular}{c}Java compiler\\\texttt{javac}\end{tabular}};
\coordinate (Middle) at ($(Gcc)!0.5!(Javac)$);
\node[format,below of=Middle] (Exec) {Executable program};
\draw[->] (Heptagon) -- (Heptc);
\draw[->] (Heptc) -- node[right]{\texttt{-target ctrln}} (Ctrln);
\draw[->] (Ctrln) -- (ReaX);
\draw[->] (ReaX) -- node[right]{\texttt{--triang}} (Controller);
\draw[->] (Controller) -- (Ctrl2ept);
\draw[->] (Ctrl2ept) -- (HeptagonCtrlr);
\draw[->] (HeptagonCtrlr) -- (HeptcCtrlr);
\draw[->] (HeptcCtrlr) -- (C);
\draw[->] (C) -- (Gcc);
\draw[->] (Gcc) -- (Exec);
\coordinate (A) at ($(C) + (-3,3)$);
\draw[->] (Heptc) -| node[left,pos=0.75]{\texttt{-target c}} (A) -- (C);
\coordinate (B) at ($(Java) + (3,3)$);
\draw[->] (Heptc) -| node[right,pos=0.75]{\texttt{-target java}} (B) -- (Java);
\draw[->] (HeptcCtrlr) -- (Java);
\draw[->] (Java) -- (Javac);
\draw[->] (Javac) -- (Exec);
\end{tikzpicture}
\caption{BZReaX full compilation chain}
\label{fig:bzreax-compil}
\end{figure}
The Heptagon compiler is usually used to generate target code in a
general-purpose language, like C (option \texttt{-target c}) or Java
(option \texttt{-target java}). This generated code is composed of two
functions for each Heptagon:
\begin{itemize}
\item a \emph{reset} function, used to reset the node's state ;
\item a \emph{step} function, which takes as input the current inputs
of the node, update the current state, and computes the current
outputs.
\end{itemize}
If a node is provided with a contract, then the ReaX
verification/synthesis tool can be used. The Heptagon backend towards
Ctrl-n equations (input format for ReaX) is activated with the
\texttt{-target ctrln} option.
The ReaX tool can then be used to synthesize (generate automatically)
a controller which, composed with the initial program, will give
values to the controllable variables so that the ``enforce'' property
stated by the contract is verified.
This controller is initially a Boolean predicate, over the values of
inputs, current state and controllable variable. The ReaX option
\texttt{-triang} allows the obtention of a function (in the same
Ctrl-n input format), giving values to the controllable variables,
functions of values of current inputs and state.
This controller function can then be translated into an Heptagon node
by the \texttt{ctrl2ept} tool. This Heptagon node is composed in
parallel with the initial one, by the technical mean of a node
instanciation. Thus, the generated code of this controller can be
compiled and linked with the code generated from the initial Heptagon
program.
\section{Verification of logico-numerical Heptagon programs with ReaX}
Heptagon/BZR contracts can be used, with the ReaX tool, to verify
logico-numerical programs.
Let us look back at the example given in
Figure~\ref{fig:exple-contract}, and name this program Modes (in a
file named \texttt{modes.ept}).
\begin{lstlisting}
node twomodes (v:int) = (y:int)
contract
assume (v <= 1) & (v >= 0)
enforce (o <= 10) & (o >= 0)
var last x : int = 0;
let
y = x;
automaton
state Up
do x = last x + v
until x >= 10 then Down
state Down
do x = last x - v
until x <= 0 then Up
end
tel
\end{lstlisting}
We now want to check that the property stated by the contract is
guaranteed by the program. We begin then by compiling this program
towards the Ctrl-n input format :
\begin{alltt}
\textcolor{deepgreen}{> heptc -target ctrln modes.ept}
\end{alltt}
We obtain then a Ctrl-n program placed in a file named
\texttt{modes\_ctrln/twomodes.ctrln}. This file can be given as input
to the ReaX tool:
\begin{alltt}
\textcolor{deepgreen}{> reax -a 'sS:d=\{P:D\}' modes_ctrln/twomodes.ctrln}
[0.008 I Main] Reading node from `modes_ctrln/twomodes.ctrln'…
[0.024 I Supra] Variables(bool/num): state=(4/2), i=(0/1), u=(0/1), c=(0/0)
[0.024 I Df2cf] Preprocessing: discrete program
[0.024 I Verif] Forcing selection of power domain.
[0.024 I Synth] logico-numerical synthesis with powerset extension of power
domain over strict convex polyhedra with BDDs:
[0.068 I sB] Building controller…
[0.072 I sB] Computing boundary transtions…
[0.072 I sB] Simplifying controller…
[0.072 I Synth] {\color{red}logico-numerical synthesis with powerset extension of power
domain over strict convex polyhedra with BDDs succeeded.}
[0.072 I Main] Extracting generated controller…
[0.072 I Main] Checking generated controller…
[0.072 I Main] Outputting into `modes_ctrln/twomodes.ctrlr'…
\end{alltt}
The option \texttt{-a} followed by the string \verb+'sS:d={P:D}'+
defines the algorithme used for the verification. The algorithms
available are:
\begin{itemize}
\item \verb+'sB'+ for Boolean verification/synthesis (for Boolean
programs, or whose Boolean abstraction is meaningful)
\item \verb+'sS'+ for verification/synthesis using abstract
interpretation (over-approximation). The option \verb+'d={...}'+
allows the selection of abstract domains :
\begin{itemize}
\item \texttt{I} selects the domain of \emph{intervals}, for
programs with comparisons or operations between variables and
constants ;
\item \texttt{P} selects the domain of \emph{convex polyhedra},
suitable for programs with comparisons or simple operations (sum or
difference)
between variables.
\end{itemize}
The second part (\texttt{\ldots:D}) of this string selects the
\emph{powerset extension} of the power domain over the abstract
domain, suitable for programs with mixed Boolean, modes and
numerical operations on modes.
\end{itemize}
Our program involves operation between a state variable and an input
(\lstinline{last x + v}); thus we need to use the convex polyhedra
domain. Using a less precise domain such as intervals would lead to a
failed verification:
\begin{alltt}
\textcolor{deepgreen}{> reax -a 'sS:d={I:D}' modes_ctrln/twomodes.ctrln}
[0.012 I Main] Reading node from `modes_ctrln/twomodes.ctrln'…
[0.024 I Supra] Variables(bool/num): state=(4/2), i=(0/1), u=(0/1), c=(0/0)
[0.024 I Df2cf] Preprocessing: discrete program
[0.024 I Verif] Forcing selection of power domain.
[0.025 I Synth] logico-numerical synthesis with powerset extension of power
domain over intervals with BDDs:
[0.033 I Synth] {\color{red}logico-numerical synthesis with powerset extension of power
domain over intervals with BDDs failed.}
\end{alltt}
\section{Controller synthesis on logico-numerical Heptagon programs with ReaX}
We add now a controllable variable to our \texttt{twomodes} node. This
controllable variable \texttt{c} will be used to control the
transition between the two modes:
\begin{lstlisting}
node twomodes (v:int) = (y:int)
contract
assume (v <= 1) & (v >= 0)
enforce (o <= 10) & (o >= 0)
with (c:bool)
var last x : int = 0;
let
y = x;
automaton
state Up
do x = last x + v
until not c then Down
state Down
do x = last x - v
until not c then Up
end
tel
\end{lstlisting}
The transition between \texttt{Up} and \texttt{Down} is no longer
defined as a condition on the current value of \texttt{x}, but
controlled by the controller, via the given value of \texttt{c}.
The full compilation of this program consists in:
\begin{enumerate}
\item Heptagon compilation towards C code and Ctrl-n equations; the
\texttt{-s} option selects the simulated node (\texttt{twomodes})
\begin{alltt}
\textcolor{deepgreen}{> heptc -hepts -s twomodes -target c -target ctrln modes.ept}
\end{alltt}
\item Controller synthesis with ReaX (\texttt{--triang} option to
obtain a function)
\begin{alltt}
\textcolor{deepgreen}{> reax -a 'sS:d=\{P:D\}' --triang modes_ctrln/twomodes.ctrln}
[0.008 I Main] Reading node from `modes_ctrln/twomodes.ctrln'…
[0.024 I Supra] Variables(bool/num): state=(4/2), i=(1/1), u=(0/1), c=(1/0)
[0.024 I Df2cf] Preprocessing: discrete program
[0.024 I Verif] Forcing selection of power domain.
[0.024 I Synth] logico-numerical synthesis with powerset extension of power
domain over strict convex polyhedra with BDDs:
[0.072 I sB] Building controller…
[0.072 I sB] Computing boundary transtions…
[0.072 I sB] Simplifying controller…
[0.072 I Synth] logico-numerical synthesis with powerset extension of power
domain over strict convex polyhedra with BDDs succeeded.
[0.092 I t.] Triangulation…ng…
[0.092 I Main] Extracting triangularized controller…
[0.092 I Main] Checking triangularized controller…
[0.092 I Main] Splitting triangularized controller…
[0.092 I Main] Extracting split triangularized controller…
[0.092 I Main] Checking split triangularized controller…
[0.092 I Main] Outputting into `modes_ctrln/twomodes.0.ctrls'…
\end{alltt}
\item Translation of the controller towards Heptagon
\begin{alltt}
\textcolor{deepgreen}{> ctrl2ept -n Modes.twomodes}
\end{alltt}
\item Compilation of the controller towards C
\begin{alltt}
\textcolor{deepgreen}{> heptc -target c modes_controller.ept}
\end{alltt}
\item Compilation and linking of all C files, obtaining an executable
file for the simulation
\begin{alltt}
\textcolor{deepgreen}{> gcc -o sim -I/usr/local/lib/heptagon/c -Imodes_c -Imodes_controller_c
modes_c/_main.c modes_c/modes.c modes_c/modes_types.c
modes_controller_c/modes_controller.c
modes_controller_c/modes_controller_types.c}
\end{alltt}
\end{enumerate}
The program can then be simulated:\\
\begin{tikztimingtable}
v & 2D{0} 4D{1} 2D{0} 8D{1} 3D{0} 10D{1} \\
twomodes(v) & 2D{0}D{1}D{2}D{3} 3D{4}D{5}D{6}D{7}D{8}D{9}D{10}D{9} 4D{8}D{7}D{6}D{5}D{4}D{3}D{2}D{1}D{0}D{1}D{2} \\
\end{tikztimingtable}
\section{Encapsulation: the BZReaX script}
The full compilation chain described in the previous section has been
encapsulated into a script named \texttt{bzreax}, whose scope is
described in Figure~\ref{fig:bzreax}.
\begin{figure}
\centering
\pgfdeclarelayer{background}
\pgfsetlayers{background,main}
\begin{tikzpicture}[node distance=2cm]
\node[format] (Heptagon) {\begin{tabular}{c}Heptagon\\\texttt{.ept}\end{tabular}};
\node[tool,below of=Heptagon] (Heptc) {\begin{tabular}{c}Heptagon compiler\\\texttt{heptc}\end{tabular}};
\node[format,below of=Heptc] (Ctrln) {\begin{tabular}{c}Ctrl-n equations\\\texttt{.ctrln}\end{tabular}};
\node[tool,below of=Ctrln] (ReaX) {\begin{tabular}{c}ReaX synthesis tool\\\texttt{reax}\end{tabular}};
\node[format,below of=ReaX] (Controller) {\begin{tabular}{c}Controller function\\\texttt{.ctrlf}\end{tabular}};
\node[tool,below of=Controller] (Ctrl2ept) {\begin{tabular}{c}Controller compiler\\\texttt{ctrl2ept}\end{tabular}};
\node[format,below of=Ctrl2ept] (HeptagonCtrlr) {\begin{tabular}{c}Heptagon\\\texttt{.ept}\end{tabular}};
\node[tool,below of=HeptagonCtrlr] (HeptcCtrlr) {\begin{tabular}{c}Heptagon compiler\\\texttt{heptc}\end{tabular}};
\node[format,below left of=HeptcCtrlr,node distance=3cm] (C) {\begin{tabular}{c}C program\\\texttt{.c}\end{tabular}};
\node[format,below right of=HeptcCtrlr,node distance=3cm] (Java) {\begin{tabular}{c}Java program\\\texttt{.java}\end{tabular}};
\node[tool,below of=C] (Gcc) {\begin{tabular}{c}C compiler\\\texttt{gcc}\end{tabular}};
\node[tool,below of=Java] (Javac) {\begin{tabular}{c}Java compiler\\\texttt{javac}\end{tabular}};
\coordinate (Middle) at ($(Gcc)!0.5!(Javac)$);
\node[format,below of=Middle] (Exec) {Executable program};
\draw[->] (Heptagon) -- (Heptc);
\draw[->] (Heptc) -- node[right]{\texttt{-target ctrln}} (Ctrln);
\draw[->] (Ctrln) -- (ReaX);
\draw[->] (ReaX) -- node[right]{\texttt{--triang}} (Controller);
\draw[->] (Controller) -- (Ctrl2ept);
\draw[->] (Ctrl2ept) -- (HeptagonCtrlr);
\draw[->] (HeptagonCtrlr) -- (HeptcCtrlr);
\draw[->] (HeptcCtrlr) -- (C);
\draw[->] (C) -- (Gcc);
\draw[->] (Gcc) -- (Exec);
\coordinate (A) at ($(C) + (-3,3)$);
\draw[->] (Heptc) -| node[left,pos=0.75]{\texttt{-target c}} (A) -- (C);
\coordinate (B) at ($(Java) + (3,3)$);
\draw[->] (Heptc) -| node[right,pos=0.75]{\texttt{-target java}} (B) -- (Java);
\draw[->] (HeptcCtrlr) -- (Java);
\draw[->] (Java) -- (Javac);
\draw[->] (Javac) -- (Exec);
\begin{pgfonlayer}{background}
\path[fill=yellow!40,draw=deepyellow]
($(Heptc.north west) + (-0.5,0.5)$)
-- ($(Heptc.north east) + (0.5,0.5)$)
-- ($(HeptcCtrlr.south east) + (0.5,-0.5)$)
-- ($(C.north east) + (0.5,0.5)$)
-- ($(Gcc.south east) + (0.5,-0.5)$)
-- ($(Gcc.south west) + (-0.5,-0.5)$)
-- ($(C.north west) + (-0.5,0.5)$)
|- cycle;
\end{pgfonlayer}
\node[anchor=north west,color=deepyellow] at ($(Heptc.north west) + (-2,0.5)$) {\texttt{bzreax}};
\end{tikzpicture}
\caption{BZReaX script}
\label{fig:bzreax}
\end{figure}
Thus, the full compilation of the program described in pthe previous
section can be obtained by:
\begin{alltt}
\textcolor{deepgreen}{> bzreax modes.ept twomodes -a 'sS:d=\{P:D\}' -s}
[0.008 I Main] Reading node from `modes_ctrln/twomodes.ctrln'…
[0.020 I Supra] Variables(bool/num): state=(4/2), i=(1/1), u=(0/1), c=(1/0)
[0.020 I Df2cf] Preprocessing: discrete program
[0.020 I Verif] Forcing selection of power domain.
[0.020 I Synth] logico-numerical synthesis with powerset extension of power
domain over strict convex polyhedra with BDDs:
[0.056 I sB] Building controller…
[0.060 I sB] Computing boundary transtions…
[0.060 I sB] Simplifying controller…
[0.060 I Synth] logico-numerical synthesis with powerset extension of power
domain over strict convex polyhedra with BDDs succeeded.
[0.072 I t.] Triangulation…ng…
[0.072 I Main] Extracting triangularized controller…
[0.072 I Main] Checking triangularized controller…
[0.072 I Main] Splitting triangularized controller…
[0.072 I Main] Extracting split triangularized controller…
[0.072 I Main] Checking split triangularized controller…
[0.072 I Main] Outputting into `modes_ctrln/twomodes.0.ctrls'…
Info: Loading module of controllers for node Modes.twomodes…
Info: Reading function from `modes_ctrln/twomodes.0.ctrls'…
Info: Outputting into `modes_controller.ept'…
Info: To launch the simulator, run: `hepts -mod Modes -node twomodes -exec ./sim'
\end{alltt}
\bibliographystyle{plain}
\bibliography{manual}
\end{document}

185
manual/manual.bib
View file

@ -55,3 +55,188 @@
month = {September},
year = 2005,
}
@Article{ramadge-wonham:synthcont,
author = {Ramadge, P. J. and Wonham, W. M.},
title = {Supervisory control of a class of discrete event
processes},
journal = {SIAM J. Control Optim.},
volume = 25,
number = 1,
year = 1987,
issn = {0363-0129},
pages = {206--230},
publisher = {Society for Industrial and Applied Mathematics}
}
@article{marchand00c,
Author = {Marchand, H. and Bournai, P. and Le Borgne, M. and
Le Guernic, P.},
Title = {Synthesis of Discrete-Event Controllers based on the
Signal Environment},
Journal = {Discrete Event Dynamic System: Theory and
Applications},
Volume = 10,
Number = 4,
Month = {October},
Year = 2000
}
@Article{bzr_jdeds,
author = {Delaval, Gwena\"{e}l and Rutten, \'{E}ric and
Marchand, Herv\'{e}},
title = {Integrating Discrete Controller Synthesis into a
Reactive Programming Language Compiler},
journal = {Discrete Event Dynamic Systems},
year = {To appear},
key = {me,bzr}
}
@InProceedings{gcm10:_qos_energ_coord_dcs,
author = {{De Palma}, No\"{e}l and Delaval, Gwena\"{e}l and
Rutten, \'{E}ric},
title = {QoS and Energy Management Coordination using
Discrete Controller Synthesis},
key = {me,bzr},
booktitle = {1st International Workshop on Green Computing
Middleware (GCM'2010)},
year = 2010,
address = {Bangalore, India},
month = nov,
abstract = {Green computing is nowadays a major challenge for
most IT organizations. Administrators have to
manage the trade-off between system performances and
energy saving goals. Autonomic computing is a
promising approach to control the QoS and the energy
consumed by a system. This paper precisely
investigates the use of synchronous programming and
discrete controller synthesis to automate the
generation of a controller that enforces the
required coordination between QoS and energy
managers. We illustrate our approach by describing
the coordination between a simple admission
controller and an energy controller.},
pdf =
{http://pop-art.inrialpes.fr/people/delaval/pub/delaval-gcm10.pdf}
}
@InProceedings{delaval08:_modul_distr_applic_discr_contr_synth,
author = {Delaval, G.},
title = {Modular Distribution and Application to Discrete
Controller Synthesis},
key = {me,these},
year = 2008,
booktitle = {International Workshop on Model-driven High-level
Programming of Embedded Systems (SLA++P'08)},
month = apr,
address = {Budapest, Hungary},
abstract = {This paper shows the application of the automatic
distribution of synchronous reactive programs to the
specific problem of discrete controller synthesis of
complex reactive systems. Discrete controller
synthesis is a formal method used to ensure
properties on a flexible system which does not a
priori verify them. However, this method is
efficient only on boolean programs. More complex
embedded systems, comprising complex data types and
structures, cannot be addressed without abstraction
means. We show how such abstractions can be obtained
automatically using a type-directed projection
operation. This operation allows then the safe
recombination of the result of the synthesis with
the original abstracted system, preserving the
ensured properties.},
pdf =
{http://pop-art.inrialpes.fr/people/delaval/pub/slap08.pdf}
}
@InProceedings{delaval10:_contracts_mod_dcs,
author = {Delaval, Gwena\"{e}l and Marchand, Herv\'{e} and
Rutten, \'{E}ric},
title = {Contracts for Modular Discrete Controller Synthesis},
key = {me,bzr},
booktitle = {ACM International Conference on Languages,
Compilers, and Tools for Embedded Systems (LCTES
2010)},
year = 2010,
address = {Stockholm, Sweden},
month = apr,
abstract = {We describe the extension of a reactive programming
language with a behavioral contract construct. It
is dedicated to the programming of reactive control
of applications in embedded systems, and involves
principles of the supervisory control of discrete
event systems. Our contribution is in a language
approach where modular discrete controller synthesis
(DCS) is integrated, and it is concretized in the
encapsulation of DCS into a compilation process.
From transition system specifications of possible
behaviors, DCS automatically produces controllers
that make the controlled system satisfy the property
given as objective. Our language features and
compiling technique provide
correctness-by-construction in that sense, and
enhance reliability and verifiability. Our
application domain is adaptive and reconfigurable
systems: closed-loop adaptation mechanisms enable
flexible execution of functionalities w.r.t.
changing resource and environment conditions. Our
language can serve programming such adaption
controllers. This paper particularly describes the
compilation of the language. We present a method
for the modular application of discrete controller
synthesis on synchronous programs, and its
integration in the BZR language. We consider
structured programs, as a composition of nodes, and
first apply DCS on particular nodes of the program,
in order to reduce the complexity of the controller
computation; then, we allow the abstraction of parts
of the program for this computation; and finally, we
show how to recompose the different controllers
computed from different abstractions for their
correct co-execution with the initial program. Our
work is illustrated with examples, and we present
quantitative results about its implementation.},
pdf =
{http://pop-art.inrialpes.fr/people/delaval/pub/lctes2010.pdf}
}
@inproceedings{gueye12:_coord_energ,
author = {Gueye, Soguy Mak-Kar{\'e} and de Palma, No{\"e}l and
Rutten, Eric},
title = {Coordinating Energy-aware Administration Loops using
Discrete Control},
booktitle = {Proc. of the Eighth International Conference on
Autonomic and Autonomous Systems, ICAS 2012},
year = 2012,
address = {St. Maarten, Netherlands Antilles},
month = mar,
pdf = {pub/icas12_20027.pdf}
}
@InProceedings{berthier14:_reax,
author = {Nicolas Berthier and Herv{\'e} Marchand},
title = {Discrete Controller Synthesis for Infinite State Systems with {ReaX}},
booktitle = {12th International Workshop on Discrete Event Systems},
year = 2014,
doi = {10.3182/20140514-3-FR-4046.00099},
pages = {46--53},
address = {Cachan, France}
}
@article{delaval13:bzr_jdeds,
title = {{Integrating Discrete Controller Synthesis into a Reactive Programming Language Compiler}},
author = {Delaval, Gwena{\"e}l and Rutten, {\'E}ric and Marchand, Herv{\'e}},
url = {https://hal.inria.fr/hal-00863286},
journal = {{Discrete Event Dynamic Systems}},
publisher = {{Springer Verlag (Germany)}},
volume = {23},
number = {4},
pages = {385-418},
year = {2013},
doi = {10.1007/s10626-013-0163-5},
pdf = {https://hal.inria.fr/hal-00863286/file/jdeds.pdf},
hal_id = {hal-00863286},
hal_version = {},
}