mld_translation.tex

由matlab开发的hybrid系统的描述语言

\chapter{Translation into \MLD{} system}
\label{mld_transl_c}

\section{\MLD{} Representation}

Recall that a \MLD{} system can be written as:
\MLDsystem{modelpure}{.} The class \cppclass{MLD\_representation}
holds all the matrices $A_{rr}, A_{rb}, \ldots, E_5$. It also
stores a description of each equality and inequality as a
\cppclass{Row\_information} (see section~\ref{Rowinfo_s}).

\label{B5D5}An extended \MLD{} representation allows constant
terms on the right hand side of the equalities. This is achieved
by adding a vector $B_5$ to the state update equality and a vector
$D_5$ to the output equality \BDMLDsystem{modelplus}{.} To use the
extended \MLD{} system, specify \cmdop{5} in the command line.

In order to generate the \MLD{} output, each \cppclass{Item} is
separately translated into a \cppclass{MLD\_representation}. The
resulting matrices have but a few entries. Thus, the matrix
implementation should be optimized for sparse matrices. See
section~\ref{Matrix_impl_s} for a description of our
implementation.

Once two items are translated, the method
\method{MLD\_representation}{merge} merges the two
\cppclass{MLD\_representation}. For the equalities the merge is
just an addition of the corresponding matrices.\footnote{Note that
the semantic checks guarantee that any row can have nonzero
entries in only one of the two \cppclass{MLD\_representation}s
being merged.} The inequalities from both \MLD{} representations
must be present in the merged representation. This is done by
appending the $E$ matrices. Finally, merge has to collect the
\cppclass{Row\_information}. \cppclass{Row\_information} is stored
in three \code{STL::map}: for state and output equations and for
the inequalities. The key is the row-number. For the equalities,
merge simply copies the entries. For the inequalities, the
row-number change for one \cppclass{MLD\_representation}, so merge
has to store these \cppclass{Row\_information} with a higher key.
It also has to inform the \cppclass{Row\_information} of the
changed inequality number.

\section{Row\_information}
\label{Rowinfo_s}

An instance of \cppclass{Row\_information} is associated with each
equality and inequality of the \MLD{} system. The class contains a
pointer to the \cppclass{Item} that generated the row. It also
holds an integer \code{subindex}, which gives a sequential number
to each row generated by the same item. Finally, it contains a
reference to the \MLD{} row it is describing. This is either the
number of the inequality or, in case of an equality, the left hand
side variable being defined.

To display the information, \cppclass{Row\_information} relies on
the functionality provided by \cppclass{Item}. For example, at
parse time, each item saves the source code (from the \hysdel{}
input file) it was constructed from. Using the subgroup index, it
is possible to see which item was unrolled from which. Group and
subgroup index are set by \method{Item}{comp\_group\_numbers}. The
method \method{Row\_information}{to\_matlab} prints all
information in \matlab{} readable format.


\section{Matrix Implementation}
\label{Matrix_impl_s}

The class \cppclass{Matrix} stores matrices with elements of type \cppclass{Expr}. It basically is a STL map from
\cppclass{Matrix\_entry\_key} to \cppclass{Expr}. \cppclass{Matrix\_entry\_key} has two fields \code{y} and
\code{x} which give the position of the associated expression. The methods \function{get} and \function{set} are
used to read and write matrix elements. Before printing the matrix, the method \function{check\_dim} must be
called. As arguments is takes the dimension the matrix should have. The function then checks that no element has a
too high index.


\section{Translating the Items}

The only thing needed to implement the translation rules given in
\cite{TB02} is to convert \cppclass{Expr} into CNF (for logic
expressions) and into affine functions (for real expressions). A
CNF is stored as \cppclass{CNF\_clause} and the conversion is done
by \method{Expr}{compute\_CNF}. Affine functions are represented
as \cppclass{Affine\_func} and are computed from an expression via
\method{Expr}{compute\_affine}. Note that both
\cppclass{CNF\_clause} and \cppclass{Affine\_func} are only
introduced for easier translation into \MLD{}, they are not
permanently stored.

\subsection{CNF representation}

Any logic expression f over the variables $x_1,\ldots,x_n$ can be written in CNF:
\begin{align}
&f=\bigwedge_i (\bigvee_j l_{i,j} ) \intertext{where} \
&l_{i,j} = x_k \quad \text{or} \quad l_{i,j} = \neg x_k
\notag \quad \text{for some }k
\end{align}
The $l_i$ are called literals, they are variables or negated variables. A literal is represented as
\cppclass{Logic\_literal}. $ \bigvee_j l_{i,j} $ is called a clause. It is true if any of its literals is true. A
clause is represented as \cppclass{Logic\_or\_clause}, it contains a list of \cppclass{Logic\_literal}. The entire
CNF is represented as \cppclass{CNF\_clause} and contains a list of \cppclass{Logic\_or\_clause}.

Computing the CNF representation from an \cppclass{Expr} is done by traversing the parse tree: Each node first
computes the CNF representation of its children and then performs the operation the node stands for on the CNF of
the arguments. For the leaves the corresponding CNF is either constant (for boolean numbers and parameters) or has
just one positive literal (for variables).

\subsubsection{AND}
Let $f=a \wedge b$, and $a=\bigwedge_i c^a_i$ and $b=\bigwedge_i c^b_i$, where $c^a_i$ and $c^b_i$ are clauses.
Clearly
\begin{align}
f=\bigwedge_i c^a_i \wedge \bigwedge_i c^b_i
\end{align}
Thus, the CNF representation of $f$ contains all the clauses of both $a$ and $b$. \method{CNF\_clause}{log\_and}
computes the AND.

\subsubsection{OR} We want to compute $f=a \vee b$. Let $a=\bigwedge_i c^a_i$ and $b=\bigwedge_i c^b_i$, where
$c^a_i$ and $c^b_i$ are clauses.
\begin{align}
f= (\bigwedge_i c^a_i) \vee (\bigwedge_j c^b_j) = \bigwedge_{i,j}c^a_i \vee c^b_j
\end{align}
The OR of two clauses is the clause containing all the literals from both clauses. \method{CNF\_clause}{log\_or}
computes the OR.

\subsubsection{NOT} We want to compute $f=\neg a$, where $a=\bigwedge_i c^a_i$. We get
\begin{align}
f&= \neg \bigwedge_i c^a_i = \bigvee_i \neg c^a_i
\end{align}
So we need to negate $c^a_i=\bigvee_j l_j$, where $l_j$ are literals. We find that
\begin{align}
\neg c^a_i &= \neg \bigvee_j l_j = \bigwedge_j \neg l_j
\end{align}
This again is a CNF and we can compute $f$ by computing a number of ORs. \method{CNF\_clause}{log\_not} computes
the NOT.

\subsubsection{Implication, Equivalence} All other logic operations can be expressed in terms of AND, OR and NOT.
For the implication we have
\begin{align}
a \rightarrow b &= \neg a \vee b \intertext{and for the equivalence} a \leftrightarrow b &= (a \wedge b) \vee
(\neg a \wedge \neg b)
\end{align}

\subsection{Affine Functions}
\label{affine_func_s}

An affine function in the variables $x_1,\ldots,x_n$ can be written as:
$$
c_0 + c_1 x_1 + c_2 x_2 + \ldots c_n x_n
$$
where $c_i$ are constant coefficients. Each addend is represented as \cppclass{Affine\_addend}, which contains an
\cppclass{Expr} as the coefficient an a \cppclass{Var\_symbol} for the variable. The constant part $c_0$ is an
\cppclass{Affine\_addend} whose variable is \NULL{}. \cppclass{Affine\_func} simply contains a list of
\cppclass{Affine\_addend}. We require that no two addends have the same variable.

Computing the affine representation from an \cppclass{Expr} is done by traversing the parse tree: Each node
computes the \cppclass{Affine\_func} of its children and then performs the operation the node stands for on the
affine representation of its arguments. For the leaves the corresponding \cppclass{Affine\_func} has just one
\cppclass{Affine\_addend}: A constant for boolean numbers and parameters or a variable with coefficient one for
\cppclass{Var\_symbol}. Nonlinear operators (e.g., sin, sqrt) take a shortcut: Such a node can only be an affine
function if its arguments are constant. In this case the \cppclass{Affine\_func} has just the constant part,
namely the node itself. The linear operators are described next.

\subsubsection{Addition} We want to compute $f=a+b$. The only problem with the addition is not to create multiple
addends for the same variable. If a variable $v$ is present in both $a$ and $b$, then in $f$ there is only one
\cppclass{Affine\_addend} for $v$ who's coefficient is the sum of the coefficient of $v$ in $a$ and $b$. Addition
is computed by \method{Affine\_func}{add}.

\subsubsection{Negation}

The method \method{Affine\_func}{neg} negates an affine function by negating the coefficients of all addends.

\subsubsection{Subtraction}
Subtraction can be expressed as a negation and an addition: \begin{equation} f=a-b = a+(-b) \end{equation}

\subsubsection{Multiplication with a Constant}
The method \method{Affine\_func}{mult\_const} multiplies the constant to the coefficients of all addends.