class_overview.tex

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

\subsection{Must}
\begin{tabular}{lll}
& logic must & real must \\
\hysdel{} source & constraint & aff1 $<=$ aff2 \\
meaning & constraint must be true & (constraint=aff1-aff2) $<= 0$ \\
superclass & \multicolumn{2}{c}{Constraint\_item}\\
class name & \cppclass{Logic\_must\_item} & \cppclass{Cont\_must\_item} \\
attributes & \multicolumn{2}{c}{\tt Expr *constraint}\\
semantical conditions & constraint is logic & constraint is affine
\end{tabular}


\chapter{Semantic Checks}
The syntax of \hysdel{} is defined in the grammar. The parser only
accepts input that is syntactically correct. However, this does
not mean that it is a correct \hysdel{} source. The input also has
to be semantically correct. \footnote{In theory it is possible to
put many semantic checks into the grammar. The grammar would get
very complicated.} Checking this is done immediately after the
parsing step.

Semantic checks are implemented in the methods called {\tt void semantic\_checks()}. The following checks are
performed:
\begin{itemize}
\item in \cppclass{Expr}: \begin{itemize}
    \item operators have the right type (real or Boolean) of arguments
    \item no output variable is used
\end{itemize}
\item in \cppclass{Item}: All the semantic conditions mention in \ref{Item_section}.
\item in \cppclass{Min\_max\_eps}: Minimum, maximum and epsilon must be constant.
\end{itemize}





\section{\cppclass{MLD\_representation}}

Recall than a \MLD{} system can be rewritten in this way:
\MLDsystem{modelpure0}{.} The class \cppclass{MLD\_representation}
holds all the matrices $A_{cc}, A_{cd}, \ldots, E_5$. It also
stores a description of each equality and inequality.

When a single \cppclass{Item} is translated into a \cppclass{MLD\_representation}, most matrices will remain
empty. For this reason the matrix implementation should be optimized for sparse matrices. Once two items are
translated, their \cppclass{MLD\_representation} have to be merged. This is done by
\begin{verbatim}
    void MLD_translation::merge(MLD_translation *from);
\end{verbatim}
For the inequalities, the same left hand side variable must not be defined twice. Otherwise, the merge is just an
addition of the corresponding matrices. For the inequalities, the inequalities from both
\cppclass{MLD\_representation} must be present in the merged representation. This is done by setting
$$
E^{*}_i = \begin{bmatrix} \frac{E^a_i}{E^b_i} \end{bmatrix}  \qquad  \text{ for } i=1, \ldots, 5
$$
where $E^a$ and $E^b$ are merged to $E^*$.

The description of the equalities and inequalities is stored as \cppclass{Row\_information}, which contains a
pointer to the \cppclass{Item} that generated the row. It also holds an integer {\tt subindex}, which gives a
sequential number to each row generated by the same item.




\chapter{Affine Functions and CNF Clauses}

In order to generate the \MLD{} representation, real expressions

The \MLD{} representation is built from affine functions and logic expressions in CNF form.

Affine functions and logic expressions in CNF form can easily be transformed into the \MLD{} matrices. The items
however have their expressions as \cppclass{Expr}. Thus, before filling the \MLD{} matrices, a real expression is
first translated into \cppclass{Affine\_func}, which represents an affine function. Similarly, a boolean
expression is translated into \cppclass{CNF\_clause}, which represents the expression in CNF form. The translation
is done by
\begin{verbatim}
    CNF_clause * Expr::compute_CNF();
    Affine_func * Expr::compute_affine();
\end{verbatim}

\section{\cppclass{CNF\_clause}}

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 \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. For the
leaves the corresponding CNF is either constant (for boolean numbers and parameters) or has just one positive
literal (for variables). Now we need to be able to perform all the boolean operators on CNF

\subsection{AND} If $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$. {\tt
CNF\_clause::log\_and(CNF\_clause *c2)} computes the AND.

\subsection{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,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. {\tt
CNF\_clause::log\_or(CNF\_clause *c2)} computes the OR.

\subsection{NOT} We want to compute $f=\neg a$, where $a=\bigwedge_i c^a_i$. We get
\begin{align}
f&=\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 &= \bigwedge_j \neg l_j
\end{align}
This again is a CNF and we can compute $f$ by computing a number of ORs. {\tt CNF\_clause::log\_not()} computes
the NOT.

\subsection{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{Simplification} If the above rules are applied, the results are correct but probably longer than
necessary. For example if two clauses contain the same literal $l$ and you compute the OR of these clauses, then
in the result $l$ should not appear twice. The function {\tt CNF\_clause::simplify()} simplifies the CNF
representation. It performs the following.....

\section{\cppclass{Affine\_func}}

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 {\tt NULL}. \cppclass{Affine\_func} simply contains a list of
\cppclass{Affine\_addend}. We require that no two \cppclass{Affine\_addend}s 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. 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 child is constant. In this case the
\cppclass{Affine\_func} has just the constant part, namely the child. The linear operators are described next.

\subsection{Addition}
\begin{verbatim}
void Affine_func::add(Affine_func*);
\end{verbatim}
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$.

\subsection{Negation}
\begin{verbatim}
void Affine_func::neg();
\end{verbatim}
Just negate the coefficients of all addends.

\subsection{Subtraction}
\begin{verbatim}
void Affine_func::sub(Affine_func*)
\end{verbatim}
$f=a-b = a+(-b)$. Thus, subtraction is done by negation and addition.

\subsection{Multiplication with a Constant}
\begin{verbatim}
void Affine_func::mult_const(Expr*)
\end{verbatim}
Just multiply the constant to the coefficients of all addends.

\subsection{Simplification} The resulting \cppclass{Affine\_func} will have the minimum number of addends,
however the coefficients will not be as simple as possible. Thus,
simplifying \cppclass{Affine\_func} is done by simplifying all
coefficients. If some coefficient turns out to be zero, the
corresponding \cppclass{Affine\_addend} is removed. Note: check if
is this implemented, if not implement it.