\documentclass[a4paper]{report}
\usepackage[english]{babel}
\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{verbatim}
%\usepackage{boxedminipage}
%\usepackage{lscape}
\usepackage{makeidx}
\usepackage{palatino}
\usepackage{euler}

\author{David Kågedal \\ LiTH-IDA-Ex-98/48 ???}
\title{A Natural Semantics specification for the equation-based
  modeling language Modelica}

\makeindex

\renewcommand{\bottomfraction}{0.5}

\newcommand{\code}[1]{\texttt{#1}}
\newcommand{\codebox}[1]{\fbox{\code{#1}}}
\newcommand{\filename}[1]{\texttt{#1}}
\newcommand{\term}[1]{\textit{\bfseries#1}}
\newcommand{\firstref}[1]{\term{#1}\index{#1}}
\newcommand{\note}[1]{[\textsc{#1}]}
\newcommand{\fixme}[1]{\mbox{}\marginpar{$\blacktriangleleft$}\note{#1}}
\newcommand{\unfinished}{\fixme{\ldots}}

\newtheorem{defth}{Definition}[chapter]
\newtheorem{example}{Example}[chapter]

\newenvironment{Def}[1]{\begin{defth}[#1]\index{#1|textbf}}{\end{defth}}

\newcommand{\codefont}{\normalfont\ttfamily\fontsize{7}{8}\selectfont}

\makeatletter

\newcommand{\sourcefile}[2]{%
  \clearpage
  \section{Module \code{#1}}
  \label{src:#1}
  \addcontentsline{stc}{sourcefile}{%
    \protect\numberline{\thesection}\protect\makebox[8em][l]{\code{#1}}#2}}
\newcommand{\listofsources}{\@starttoc{stc}}
\newcommand{\l@sourcefile}{%
  \@dottedtocline{1}{2em}{3em}%
  }

% Some magic from Tommy Pettersson
\def\dedu#1#2{{\setbox0=\hbox{\ensuremath{#1}}\dimen0=\wd0\setbox1=\hbox
    to\dimen0{\hss\ensuremath{#2}\hss}\vbox{\box0\vspace{1mm}\hrule
      width\dimen0\vspace{1mm}\box1}}}

% See the verbatim package for info about this
\def\boxedverbatim{\begingroup%
  \parskip=0pt\topsep=0pt\partopsep=0pt%
  \def\verbatim@processline{%
    \setbox1=\hbox{\the\verbatim@line}%
    \setbox0=\vbox{{\box0}{\box1}}%
    }%
  \def\verbatim@font{%
    \codefont
    \let\do\do@noligs
    \verbatim@nolig@list}
   \verbatim}
\def\endboxedverbatim{\endverbatim\framebox[\linewidth][l]{\box0}%
  \endgroup\vspace{2ex}}

\makeatother
  

\begin{document}

\titlepage
\maketitle{}
\endtitlepage

\begin{abstract}
\label{abs}

Modelica is a new modeling language.  It is an object-oriented,
equation-based languages that is designed to incorporate features from
several previous modeling languages and to form a common ground for
modeling and simulation.  As a part of the design process, the exact
semantics of the language needs to be defined.

Formal descriptions of the syntax of programming languages has long
been accepted as a natural way of describing the syntactical form of a
language. Today everybody expects a BNF-like grammar for a new
language. But that is not the case when it comes to describing the
semantics of languages. Formalisms for the specifications of semantics
have been available for many years, but are not often used by others
than researchers.

One advantage of using a formal description of the semantics is of
course that the specification becomes more strict and unambiguous.
However, there is also the possibility of using the semantic
specification to generate a language translator, or compiler, in an
automatic way.

This report describes a partial formal semantics for Modelica. The
notation used enables it to be passed to a compiler generator that
generates a Modelica translator, which translates a Modelica model
into a simple set of equations.

The language used for the specification is called RML, and is based on
Natural semantics, an operational semantic specification formalism.

\end{abstract}

\tableofcontents

\chapter{Background}
\label{cha:bg}


\section{Introduction}
\label{sec:intro}

This chapter tries to give some background information outlining why
this work was done, and what the basic concepts used are.

\section{Overview of formal semantics}
\label{sec:semoverview}

Any new programming language needs to be described in one way or
another.  The syntax of the language is conveniently described by a
grammar in a common format, such as BNF\cite{drakboken}.  However,
when it comes to the semantics of a programming language, things are
not so straightforward.

The semantics of the language describe what any particular program
written in the language ``means'', i.e. what should happen when the
program is executed, or evaluated in some form.

Most programming language semantic definitions are given by a standard
text written in English which tries to give a complete and unambiguous
specification of the language.  Unfortunately, this is often not
enough.  Natural language is inherently not very exact, and it is hard
to make sure that all special cases are covered.  One of the most
important requirements of a language specification is that two
different language implementors should be able to read the
specification and make implementations that interpret the
specification in the same way.  This implies that the specification
must be exact and unambiguous.

For this reason formalisms for writing formal specifications of
languages have been invented\cite{pagan}.  These formalisms allow for
a mathematical semantic description, which as a consequence is exact,
unambiguous and easy to verify.

Several approaches has been explored as to how the semantics should be
described formally.  See \cite{pi} for a good introduction to the
various approaches.


\section{Natural semantics}
\label{sec:natsem}
\index{foobar}

The formalism that we use is called \firstref{Natural Semantics}.
The ``natural'' in Natural semantics is intended to indicate its
similarities to natural deduction, which is a way of constructing
proofs in formal logic systems.  A specification in Natural semantics
is usually given a proof-theoretic interpretation, meaning that it is
used to construct proofs.

There are many different presentations of Natural semantics in the
literature, and I choose to present the simple form that RML uses.

Natural semantics uses \firstref{inference rules} to describe the
semantics.  These rules consist of a \firstref{consequence} and a
number of \firstref{premises}.

$$
\dedu{ p_1 \Rightarrow q_1 \hspace{1em}
       \ldots \hspace{1em} p_n \Rightarrow q_1 }
     { p \Rightarrow q }
$$

The number of premises may be zero, in which case we say that the rule
is an \firstref{axiom}.

$$
p \Rightarrow q
$$

\subsection{A simple expression evaluator}

The proof construction mechanism is described by a small example,
describing a very basic expression language, with numbers and addition
and multiplication operators.  First, we define the abstract syntax of
the expression language:

\begin{gather}
  n \in \text{Int} \\
  e \in \text{Exp} ::= n \;|\; e + e \;|\; e \cdot e
\end{gather}

Then we give the rules for the evaluation of expressions to integer
values.

\begin{gather}
  \label{eq:int}
  n => n \\
  \label{eq:add}
  \dedu{ e_1 \Rightarrow n_1 \hspace{1em}
         e_2 \Rightarrow n_2 \hspace{1em}
         n = n_1 + n_2 }
       { e_1 + e_2 \Rightarrow n } \\
  \label{eq:mul}
  \dedu{ e_1 \Rightarrow n_1 \hspace{1em}
         e_2 \Rightarrow n_2 \hspace{1em}
         n = n_1 \cdot n_2 }
       { e_1 \cdot e_2 \Rightarrow n }
\end{gather}

If we want to prove, using these rules, that the expression $3 \cdot
(4 + 5)$ has a value, we do this by finding a rule, whose consequence
can be instantiated to match this expression.  Such an instance is
called a \firstref{sequent}.

The only rule that matches is rule \ref{eq:mul}, leading to the
following rule instance, where $3$ is substituted for $e_1$ and $(4 +
5)$ is substituted for $e_2$:

$$
  \dedu{ 3 \Rightarrow n_1 \hspace{1em}
         (4 + 5) \Rightarrow n_2 \hspace{1em}
         n = n_1 \cdot n_2 }
       { 3 \cdot (4 + 5) \Rightarrow n }
$$

This is not a complete proof.  We need to prove the sequent $3
\Rightarrow n_1$, and the only rule matching that is rule
\ref{eq:int}, leading to the following proof tree where $3$ is
substituted for $n_1$:

$$
  \dedu{ 3 \Rightarrow 3 \hspace{1em}
         (4 + 5) \Rightarrow n_2 \hspace{1em}
         n = 3 \cdot n_2 }
       { 3 \cdot (4 + 5) \Rightarrow n }
$$

The sequent labeled with a $3$ also needs to be proved, and this can
be done by instantiating rule \ref{eq:add}.

$$
  \dedu{ 3 \Rightarrow 3 \hspace{1em}
         \dedu{ 4 \Rightarrow n_3 \hspace{1em}
                5 \Rightarrow n_4 \hspace{1em}
                n_2 = n_3 + n_4 }
              { 4 + 5 \Rightarrow n_2} \hspace{1em}
                n = 3 \cdot n_2 }
       { 3 \cdot (4 + 5) \Rightarrow n }
$$

Instantiating rule \ref{eq:int} twice leads to the following proof
tree:

$$
  \dedu{ 3 \Rightarrow 3 \hspace{1em}
         \dedu{ 4 \Rightarrow 4 \hspace{1em}
                5 \Rightarrow 5 \hspace{1em}
                n_2 = 4 + 5 }
              { 4 + 5 \Rightarrow n_2} \hspace{1em}
                n = 3 \cdot n_2 }
       { 3 \cdot (4 + 5) \Rightarrow n }
$$

Now we can substitute $9$ for $n_2$, and consequently $27$ for $n$,
leading to the complete proof tree.

$$
  \dedu{ 3 \Rightarrow 3 \hspace{1em}
         \dedu{ 4 \Rightarrow 4 \hspace{1em}
                5 \Rightarrow 5 \hspace{1em}
                9 = 4 + 5 }
              { 4 + 5 \Rightarrow 9} \hspace{1em}
                27 = 3 \cdot 9 }
       { 3 \cdot (4 + 5) \Rightarrow 27 }
$$

Not only does this prove that the initial expression $3 \cdot (4+5)$
has a value, it also computes the value $27$.

\section{RML}
\label{sec:rml}

One of the nice properties of Natural semantics is that it lends
itself to efficient implementation in a computer.  The semantic
specification can be regarded as an operational description of how a
language is interpreted or translated.

This is what RML\cite{rml,petfrrml,pirml} is all about.  The RML
language provides a simple text syntax for specifying rules and data
types.  This specification can then be compiled into an executable
that can be used to interpret or translate any file in the described
language.


\subsection{RML syntax}
\label{sec:rmlsyn}

The RML syntax borrows elements from languages like SML\cite{sml} to
introduce a strict type system and a module system.  The syntax for
rules looks like the normal Natural semantics rule layout, adjusted
for ASCII text.

The rules are grouped in \firstref{relations}.  A relation is a set of
rules that have the same \firstref{signature}, meaning that they
perform the same operation, but are applicable at different occasions.

The type system includes basic types, such as \code{int}, \code{real}
and \code{bool}.  User-defined algebraic types may be declared in a
SML-like syntax, as in the following example that declares the
expression type used in the previous section.

\begin{boxedverbatim}
  datatype Exp = INT of int | ADD of Exp * Exp | MUL of Exp * Exp
\end{boxedverbatim}

With this type declaration, the expression $1*(2+3)$ is represented as
the RML value \codebox{MUL(INT(1),ADD(INT(2),INT(3)))}.

The signature of a relation can also be described as an RML type,
using the \code{=>} type constructor.  A relation has a name, and each
rule has a number of input arguments on the left side of the arrow,
and a number of output arguments on the right side.  The types of
these arguments form the signature.  The rules in the example above
can be grouped in a relation that we call \code{eval}, with the
following signature:

\begin{boxedverbatim}
  relation eval : Exp => int
\end{boxedverbatim}

The rules are placed inside the relation definition.  It uses the
built-in relations \code{int\_add} and \code{int\_mul} that perform
integer addition an multiplication, respectively.

\begin{boxedverbatim}
  relation eval : Exp => int =

    axiom eval INT(i) => i

    rule  eval e1 => n1  &  eval e2 => n2  &  int_add(n1,n2) => n
          -------------------------------------------------------
          eval ADD(e1,e2) => n

    rule  eval e1 => n1  &  eval e2 => n2  &  int_mul(n1,n2) => n
          -------------------------------------------------------
          eval MUL(e1,e2) => n

  end
\end{boxedverbatim}

\section{Modelica}
\label{sec:modelicabg}

Modelica\cite{modelicawww} is an object-oriented language for modeling
of physical systems for the purpose of efficient simulation.  The
language unifies and generalizes previous object-oriented modeling
languages designed by different companies and research institutions.

Compared with the widespread simulation languages previously
available, this language offers three important advances:

\begin{itemize}
\item Non-causal modeling based on differential and algebraic
  equations.

\item Multi-domain modeling capability, i.e. it is possible to combine
  electrical, mechanical, thermodynamic, hydraulic etc. model
  components within the same application model
  
\item A general type system that unifies object-orientation, multiple
  inheritance, and templates within a single class construct.
\end{itemize}

A Modelica model is defined in terms of classes containing equations
and definitions.  The semantics of such a model is defined via
translation of classes, instances, connections and functions into a
flat set of constants, variables and equations.  Equations are sorted
and converted to assignment statements when possible.  Strongly
connected sets of equations are solved by using a symbolic or numeric
solver.

Most tools that use Modelica will also let users define models and
describe their relations using a graphical tool, with icons
representing the models, and lines representing connections between
them.

This section is not intended to teach Modelica, but to give an
introduction to the basic ideas behind the language.  See
\cite{modelica10} for a more comprehensive introduction to the
language.

\subsection{Object-orientation}

Modelica is an object-oriented modeling language, which means that the
building blocks of a Modelica model are objects which correspond more
or less to real-world object.  When modeling an electrical circuit
with a voltage source and a resistor, it will be built up by one
object representing the voltage source and one representing the
resistor.  There will most likely also be other objects, such as
connectors used for connecting the ``pins'' of the components.

This is a principle that has become very popular in the programming
community, but it is still not very common in the modeling and
simulation world, partly because the mathematical description using
\firstref{hybrid differential algebraic equations}\cite{dae}
(\firstref{hybrid DAE}s) is not very familiar to the engineers who do
the modeling.

\subsection{The class concept}

In Modelica, the basic means of structuring models is the
\firstref{class} concept.  Everything in Modelica is declared as a
class.  There are several keywords in the language that is used for
declaring classes, depending on what kind of class is being defined.
A common kind is \term{model}, which is used for describing the main
objects in a model definition.

\begin{example}[A model]
\label{exa:model}
  The following piece of Modelica code defines a model named
  \code{Resistor}.

\begin{boxedverbatim}
  model Resistor
    parameter Real R(unit = "Ohm");
    Pin n, p;
    Real v, i;
  equation
    v = p.v - n.v;
    i = n.i;
    i = p.i;
    R * i = v;
  end Resistor;
\end{boxedverbatim}

  The definition contains two variables \code{i}, and \code{v}, a
  parameter \code{R}, and two connector components \code{p}, and
  \code{n}, each containing \code{i} and \code{v} variables.
\end{example}

The \code{Pin} in the example above is not defined as as \code{model},
but rather as a \code{connector}, which is a simpler variant of
\code{model}, which is used to define connect models to each other.
The connectors define interfaces (or ports), which connect to each
other using the Modelica \code{connect} clause.  Example
\ref{exa:silly} shows how the model definition \code{Resistor} can be
used to build more complex models, in this case a silly circuit with a
voltage source (\code{ACSource}) and two resistors connected in a
loop.

\begin{example}[A silly circuit]
  \label{exa:silly}
  
\begin{boxedverbatim}
  model SillyCircuit
    Resistor r1(R = 1.0), r2(R = 2.0);
    ACSource ac(V = 10.0);
  equation
    connect(r1.n, r2.p);
    connect(ac.n, r1.p);
    connect(r2.n, ac.p);
  end SillyCircuit;
\end{boxedverbatim}
\end{example}

\subsection{Hierarchical modeling}

The basic principle when building models in Modelica is that of model
reuse, and hierarchical modeling.  This means that complex models are
created by taking previously defined models (and connectors etc) and
combining them into a new model definition that can be used just like
any other model.

Example \ref{exa:model} show an example of this, where the connector
\code{Pin} is reused twice.

\section{The Modelica design group}
\label{sec:designgroup}

The work on designing a new modeling language began in 1996 when a
number of experts formed a group to design a new multi-paradigm
modeling language for hybrid systems.  Since the start, the group has
expanded to include many new members from around Europe.

A first version of the Modelica language definition was finalized in
September 1997, and there was much rejoicing.  But no complete
implementation existed yet, and there was actually a lot more work
needed to make the specification comprehensive enough to be able to
build a implementation for it.

The work on the RML specification of Modelica began in November 1997.


\section{PELAB}
\label{sec:pela}

The Programming Environment Laboratory, PELAB, (under the leadership
of professor Peter Fritzson) is concerned with research in software
engineering, i.e. tools and methods for the specification, development
and maintenance of computer programs. Some examples are: programming
languages, debuggers, incremental programming environments and
compilers, compiler generators, tools for debugging and maintenance of
distributed and real-time systems, compilers and programming
environments for parallel computers, high-level environments and
mathematical modeling languages and systems for scientific computing,
program transformation systems, etc.  The groups view of programming
environment research is rather pragmatic, and the primary interest is
in developing and investigating new methods and tools that have
potential for practical applications, e.g. in support systems for
software specialists. Developing such tools is very important, since
most of the rising cost of computer systems is due to development,
debugging and maintenance of software.

The Modelica language and development tools for Modelica are concrete
examples of research done at PELAB.

\chapter{Motivation and scope of the thesis}
\label{cha:goals}

This chapter describes the goals and the scope of this thesis.

\section{Goal}

The initial assignment was very simple in its formulation: ``Write a
formal semantic specification for Modelica using RML.''  There were at
least three important reasons for doing exactly this.

\subsection{A Modelica specification is needed}

The Modelica design process was, and still is, in dire need of a
formalized description of the language.  The language specification
available at the time (version 1.0 from September
1997)\cite{modelica10} did not contain much about the semantics of the
language.  This meant that nobody knew exactly how the language
worked, and it was not certain that everybody in the design group
agreed on the semantical details, since they were not clearly
described anywhere.

Peter Fritzson is a member of the Modelica design group and there are
several projects at PELAB that concerns Modelica.  This project would
be an important contribution to the Modelica design effort.

\subsection{Gaining experience with RML}

The RML language and compiler were developed at PELAB by Mikael
Pettersson.  They were new, and only a few language specifications had
yet been written using it.  More experience with various language
specifications was desired to gain experience with its advantages and
shortcomings.

\subsection{Natural semantics and equation-based\\ languages}

Modelica is not a programming language, such as C or LISP.  Instead it
is a modeling language, with a different distinction between static
and dynamic semantics.  For this reason it was interesting to see how
a formalism like Natural semantics, and more specifically RML, which
is usually used to specify programming languages, could be applied to
it.


\section{Scope of the thesis}
\label{sec:scope}

The work that forms the basis for this thesis only concerns the formal
specification of the Modelica semantics.  The initial goal was to
write a complete semantic specification for Modelica 1.0.
Unfortunately, Modelica 1.0 was not very well-defined, which means
that considerable effort has been needed to figure out what the
semantics were.  This has been done by taking part of the Modelica
design effort, including participation in design meetings and
electronic discussions.

These discussions lay outside the scope of the thesis, and were not
directly part of the work.  However, it was needed to be able to write
the formal semantics.  Unfortunately, this lead to a chicken-and-egg
problem, because until I had tried to write the specification I didn't
know what the problems with the Modelica semantics were.  These
problems could then be discussed with the design group, leading to new
ideas about how the semantics should have been written in the first
place.

Another goal of the formal specification was to build a usable
Modelica translator, which could be used for real-world applications.
Since this partly conflicts with the desire to produce a clear
semantic description, which not necessarily gives translation
efficiency high priority, a decision needed to be made on what to
focus on.  I chose to concentrate on the semantic description, which
shows in things like describing the semantics of equations between two
matrices as a number of simple equations between the individual
elements of the two matrices.

\section{Limitations of the semantic specification}
\label{sec:limitations}

For the reasons outlined above, the semantic specification is far from
complete.  Even the language Modelica itself is still incomplete, but
much effort is currently being put into making a new and complete
specification of the language.

Most of the work has been put into describing the most important
aspects of instantiation and expression analysis, while other things,
like functions and other algorithmic aspects need more attention.
Also more work is needed to add the polish to fix all details
preventing things like instantiation of partial classes.  But this is
something that should not be done before the overall structure is
fixed.

Below is a list of issues that are currently not covered by the
semantic specification, or were implemented before it was decided how
it should have been done.  The limitations are listed in no particular
order.

\begin{enumerate}

\item Class names can only denote classes, which means that it is not
  possible to define a ``type synonym'' for an array type, as in
  \codebox{type Point = Real[3]}.
  
  This might seem like a very basic feature to support, but it depends
  on properties of the type system which are not completely clear yet.
  
  A type is a property of a piece of data.  Instantiating a class
  gives an object of a certain class, and by examining the class
  definition it is possible to determine what the type will be
  \emph{if the class is instantiated without modifications}.  But the
  class may be modified giving the instance another, slightly
  different, type.  For this reason it is not possible to say that a
  class name denotes a type, but instead it simply denotes a class
  definition.  So the above definition of \code{Point} would not be a
  definition of a new type (in the type system sense, the Modelica
  keyword \code{type} is used for classifying class definitions).  But
  what is it?  It is some sort of ``array of class definitions,'' but
  the semantic problems of this has not fully been brought to the
  attention of the design group.
  
\item Modifying whole array dimensions does not work, as in
  \codebox{AModel a(x[:,2] = [1.0,2.0,3.0])}.  This is simply a
  limitation in the implementation.  When the modifications are
  examined, it is unknown what the size of the component being
  modified is.

\item Array slices are not expanded in array equations.
  
\item The built-in pseudo-functions (size etc.) are not implemented.
  These are not functions in the normal sense, but are constructions
  which must be evaluated at instantiation-time, since they are often
  used to define the type (array sizes) of objects.

\item Actually no evaluation of function calls are performed during
  translation.  This would be needed when the value of a constant (or
  parameter) is defined in terms of a function call.
  
\item Functions are implemented in a too simplistic way.  Simple
  type-checking of arguments and a single return value is performed,
  but it only allows complete types, meaning that the sizes of array
  dimensions in input or output arguments must by fully specified, and
  can not depend on the actual arguments given in each function call.
  
  The function semantics is still uncertain.  There have been
  discussions about a proposal where function calls are defined in
  terms of ``implicit instantiation'', where each function definition
  would be instantiated once for each function call in the model.
  This would make it possible to determine the full type of the
  arguments for each function call.
  
  However, this is currently hard to specify in this semantic
  specification due to RML limitations.  The RML module which performs
  the instantiation is called \code{Inst} (see section
  \ref{src:Inst}).  It needs to do static analysis of expressions, and
  for that purpose it uses the relations in the module \code{Static}.
  But if the \code{Static} module encounters a function call it would
  need to do an implicit instantiation, which would require the use of
  the \code{Inst} module.  Unfortunately, circular dependencies
  between modules are not allowed in RML.  This can be worked around
  in several ways, but all of them would make the specification less
  structured or harder to understand.

\item The checking of component attributes is lacking severely.  For
  instance, it is currently possible to use a variable in an outer
  scope.  This should only be possible with constants, if at all.

\item Modifying class names is done even for non-local class names.
  
\item Unused modifications are simply discarded.  They should probably
  produce an error, although this is not yet clearly defined in the
  language specification.  This is also true for out-of-bounds array
  modifications.
  
\item Redeclarations are not implemented.  This is simply because of
  time restrictions.  It could probably be added without too much
  trouble.

\item The builtin type attributes are not completely implemented.
  This includes things like \code{final}, \code{partial}.

\item Assertions are lost during translation.
  
\item When instantiating an \code{extends} element, the extended class
  definition is instantiated in the scope where the \code{extends}
  element appears.  This means that the extended class may refer to
  elements defined in the extending class, as long as it appears above
  the \code{extends} element.
  
\item There are some remaining bugs with the parts that are specified.
  And some of the most recent design decisions and clarifications of
  the Modelica semantics, such as array constructors, are not
  incorporated into the design.

\end{enumerate}

\chapter{Development environment}
\label{cha:devenv}


\section{Compiling RML}
\label{sec:rmlc}

The RML compiler is currently at version 2.0.  When the work on the
Modelica semantics began, the RML version was at 1.5.  The new
compiler provided much improved error messages and freedom in writing
source files.

Compilation of an RML file is done using the RML compiler driver
\code{rmlc}. The driver first translates the RML specification to a C
program using the \code{rml2c} compiler.  Then it compiles the
generated C file using a C compiler.  We have used the GNU C compiler
(GCC), but most modern C compilers should be usable.

\section{Parser}
\label{sec:parser}

The Modelica parser was generated by the PCCTS\cite{pccts} compiler
generation system.  It generates a parser in C, which is linked with
the RML object files.  The glue between the languages is a special RML
relation \code{parse}, which is implemented in C, rather than RML.

The parser only builds an abstract syntax tree (AST), and leaves the
rest of the transformation logic to the RML code.  Therefore, the
parser itself is not further described in this report.

The parser generator in PCCTS is powerful, but it has a few problems,
and is currently not maintained very actively.  Because of problems
with error handlers, the translator does not deal very well with
syntax errors.  If an error occurs while parsing, an error message
will be printed, but the translator will try to translate the result of
parsing anyway.  Since the resulting AST will be severely broken, this
will fail.

\section{The report}
\label{sec:report}

This report was written using the \LaTeX{}\cite{Lamport86} text
formatting system.

To produce the annotated semantics in appendix \ref{app:formsem} a
small program was written to convert the RML source files with
comments to \LaTeX{} source with the comments converted to ordinary
text. This program is a quick'n'dirty Pike\cite{pike} hack, and is
provided in appendix \ref{app:rmldoc}


\chapter{Some important notions in the Modelica semantics}
\label{cha:semantics}


\section{Introduction}
\label{sec:semintro}

The Modelica 1f specification\cite{modelica1f} contains an informal
description of the intended semantics of the language. Unfortunately,
the description lacks considerably in detail, which means that this
work needed to formalize things not covered by the specification. In
some cases, the semantics was easy to guess, but in other cases,
discussions with the authors and reading of design meeting minutes was
needed to find out what was really intended.

This chapter complements the Modelica specification by filling in some
of the larger holes in the informal language semantics.  It is
intended to help the understanding of the formal semantics in appendix
\ref{app:formsem}.


\section{Terminology}
\label{sec:terminology}

There has been some confusion about the terminology regarding Modelica
language elements, and currently the language definition is not very
strict on this point.  This will hopefully improve, but for now it is
necessary to include a short list of terms here to specify what they
mean.

\begin{Def}{Element}
  The term \term{element} corresponds closely to the non-terminal
  \texttt{element} in the grammar in the Modelica specification, which
  is a part of a class declaration.  It can be either a class
  definition, a component declaration or an extends clause, that
  appears inside a class definition.
\end{Def}

\begin{example}
  The following class definition contains four elements.  One
  \code{extends} statement, one class definition, and two component
  declarations.  Note that the definitions of \code{width} and
  \code{height} are separate elements, but the grammar only needs one
  \code{element} rule to match them.

\begin{boxedverbatim}
  class C
    extends OtherClass;
    type Length = Real(unit = "m");
    Length width, height;
  end C;
\end{boxedverbatim}
\end{example}

The word \term{instantiate} is used in many language descriptions.  In
this specification it is used in two related, but slightly different,
meanings.
  
\begin{Def}{Instantiation}
  Instantiating a class means creating an object (or class instance)
  from the description contained in the class definition, possibly
  modified by any given modifiers.  This instance is not a run-time
  object that needs an allocated piece of memory, as in many dynamic
  object-oriented languages, but the principle is the same.
  
  For every component declaration in the class definition (possibly
  inherited from another class definitions using an \code{extends}
  element), the class of the component declaration is also
  instantiated.

  When instantiating a class all of the elements in the definition of
  that class are also said to be instantiated.  Instantiating an
  element means different things depending of what kind of element is
  instantiated.  Basically it means to add the element to the
  partially instantiated parent (see the Modelica specification for an
  explanation of this).
  \begin{itemize}
  \item Instantiating a class definition simply means adding the class
    definition to the partially instantiated parent.
  \item Instantiating a component declaration means instantiating the
    class of the component and adding that object to the partially
    instantiated parent.
  \item Instantiating an extends element means instantiating all the
    elements in the extended class.
  \end{itemize}
\end{Def}

\begin{example}
  The following Modelica example contains three class definitions.  If
  the last one (\code{C}) is instantiated, it means that the class
  \code{B} needs to be instantiated twice to create the subcomponents
  \code{b1} and \code{b2}.

\begin{boxedverbatim}
  class B
    Real x;
  end B;

  class C
    B b1,b2;
  end C;
\end{boxedverbatim}
\end{example}

\begin{Def}{Component}
  The term \term{Component} refers to a class instance.  Many
  components are composed of several other components.
\end{Def}

\begin{Def}{Immediate Subcomponent}
  If component $A$ is a structure which is composed of other
  components, each of these components is an \term{immediate
    subcomponent} of $A$.
\end{Def}

\begin{Def}{Subcomponent}
  This is a recursive definition of \term{subcomponent}.  A
  subcomponent of a component $A$ is either

  \begin{enumerate}
  \item An immediate subcomponent of $A$.
  \item A subcomponent of an immediate subcomponent of $A$.
  \end{enumerate}
\end{Def}

\begin{example}
  
  Consider the following Modelica model:
  
\begin{boxedverbatim}
  model A
    Real x;
  end A;

  model B
    A a;
    Real y;
  end B;
\end{boxedverbatim}

  If an instance of \code{B} is created under the name, \code{B} will
  contain two subcomponents referred to as \code{B.a.x} and
  \code{B.y}.  Only \code{B.y} will be an immediate subcomponent of
  \code{B}.
  
\end{example}

\begin{Def}{Atomic component}
  A component that is not composed of subcomponent is called an
  \term{atomic component}.
\end{Def}


\section{Types}
\label{sec:types}


\subsection{Overview of the type system in Modelica}
\label{sec:typeoverview}

The type system is based on \firstref{classes}. A class is the basic
unit of modeling. It is used to modularize the model description and
to give the models a hierarchical structure.  Another important
concept in the type system is that of \firstref{arrays}.

The type system used in Modelica is based on a type system described
by Luca Cardelli\cite{cardelli}.

The definition of what a type is has been the subject of discussion in
the Modelica group, but the following definition is used in this
specification.

\begin{Def}{Type}
  A type is a property of components and expressions.  It is defined
  as one of the following:

  \begin{enumerate}
  \item A built-in type (Real, Integer, String or Boolean).  These
    correspond to the Modelica predefined classes \code{RealType},
    \code{IntegerType}, \code{StringType} and \code{BooleanType}.
    
  \item A structured type, containing a set of public components
    $(N,T)$, where $N$ is an identifier and $T$ is a type.  No two
    components in the set can have the same identifier.
    
  \item An array of a type, where the size of the array is either
    unknown or a non-negative integer.
  \end{enumerate}
\end{Def}

Note that there is no special provision for multi-dimensional arrays.
They are regarded as equal to arrays of arrays.  A Modelica
implementation might do it the other way around, regard arrays of
arrays as multidimensional arrays.  The important thing is that they
are the same.  Synonyms for two classes of arrays are used both in
this specification and the Modelica language definition.

\begin{Def}{Array synonyms}
  The term \term{vector}\index{vector} is a synonym for a
  one-dimensional array.  The term \term{matrix}\index{matrix} is a
  synonym for a two-dimensional array.
\end{Def}

\begin{Def}{Incomplete types}
  If a type includes an undefined array size, it is an
  \term{incomplete type}.  If not, it is a \term{complete type}.
\end{Def}

All components must have a complete type.  All expressions also have
complete types.  Incomplete types only appear as the input argument
types of function (see the discussion in section \ref{sec:functions}).

\subsection{Type equivalence and subtypes}
\label{sec:typeq}

The concepts of equivalent types and subtypes appear in several places
in the specification.

\begin{Def}{Subtype}
  A type $T_1$ is a \term{subtype} of another type $T_2$ if and
  only if one of the following hold:
  \begin{enumerate}
  \item $T_1$ and $T_2$ are the same built-in type
  \item $T_1$ and $T_2$ are structured types, where all public
    components in $T_2$ appear in $T_1$.  The type of the component in
    $T_1$ must be a subtype of the type of the corresponding component
    in $T_2$.
  \item $T_1$ is an array of type $T_1'$ and $T_2$ is an array of type
    $T_2'$, where $T_1'$ is a subtype of $T_2'$.  Also either the size
    of $T_2$ is undefined or the size of $T_1$ is equal to the size of
    $T_2$.
  \end{enumerate}
\end{Def}

\begin{Def}{Supertype}
  If $T_1$ is a subtype of $T_2$, then $T_2$ is a \term{supertype}
  of $T_1$.
\end{Def}

\begin{Def}{Equivalent types}
  Two types $T_1$ and $T_2$ are said to be \term{equivalent types}
  if and only if $T_1$ is a subtype of $T_2$ and $T_2$ is a subtype of
  $T_1$.
\end{Def}

\subsection{Class restrictions}
\label{sec:clrestr}

A class can either be declared with the \code{class} keyword, or with
one of its restricted forms, listed below.  The restricted forms are
used to indicate the intended use of the class, and to impose certain
restrictions on what the class definition can contain, and how it can
be used.

\begin{table}[tbp]
  \begin{center}
    \begin{tabular}{lp{8cm}}
      \hline
      \code{record} & No equations are allowed in the definition or in any
      of its components. A \code{record} instance may not be used in
      connections. \\
      \hline
      \code{type}   & May only be declared as derived from one of the
      predefined types, or as a array of a \code{type}. \\
      \hline
      \code{connector} & No equations are allowed in the definition or
      in any of its components. \\
      \hline
      \code{model} & A \code{model} instance may not be used in
      connections. \\
      \hline
      \code{block} & Each public component must be declared with one
      of the modifiers \code{input} or \code{output}. \\
      \hline
      \code{package} & May only contain declarations of classes and
      constants. \\
      \hline
      \code{function} & Each public component must be declared with one
      of the modifiers \code{input} or \code{output}. No equations are
      allowed and only one algorithm section is allowed. \\
      \hline
    \end{tabular}
    \caption{Class restrictions}
    \label{tab:clrestr}
  \end{center}
\end{table}

A goal of the Modelica design is that a valid program can always be
transformed into another valid program by replacing all occurrences of
the restricted class keywords with the keyword \code{class}.  For a
class declared with the keyword \code{class} to be able to be used as
if it was declared with a restricted keyword, it has to adhere to the
restrictions for that keyword.

As an example, this means that if a variable is used in a connection,
its type has to be either a class declared with \code{connector}, or a
class declared with \code{class} which contains no equations.  Another
implication is that an invalid program can be transformed into a valid
program by replacing all restricted keywords with \code{class}, e.g.
when incorrectly trying to use a \code{record} in a connection,
because the keyword \code{record} has the same restrictions as the
\code{connector} keyword, except that \code{record} is explicitly not
allowed in connections, but \code{class} is, as long as it fulfills
the restrictions.

It is currently not known if this goal will be fully met.  In most
cases it could be done, but things like \code{package},
\code{function} and \code{type} might be problematic.

\section{Arrays and matrices}
\label{sec:arrays}

The concept of arrays in Modelica have not been thoroughly examined as
of writing.  Most of the basic properties of the type system should be
clear, but there are some points worth noting.


\subsection{Overloaded array operations}
\label{sec:arrayop}

The exact meaning of multiplication where one or more of the operands
are arrays is currently being defined.  Similarly for other
operations.  The semantics specified here should not be regarded as an
absolute reference to what these operations should mean, but rather as
a description of how the overloading of operators works.


\section{Functions}
\label{sec:functions}

The semantics of functions is yet to be defined.  What is clear is
that it should be possible to use positional arguments that depend on
the order of the \code{input} components of the function definition.
It should also be possible to use named arguments matching against the
names of the components in the definition.  Furthermore, all uses of a
function should be type-checked to some extent.

How all this integrates into the type system and the general semantics
of Modelica is yet to be determined.  For simple cases a very
simplistic semantic description can be used, but for some cases, where
the sizes of array dimensions are unknown and depend of each other,
either an extended type system is needed, or other extensions, such as
that of implicit function instantiation, needs to be introduced.

For the purposes of this specification, a simplistic model where all
formal parameter types need to be fully determinable from the
definition is used.  The algorithmic (runtime) semantics is left
unspecified.


\section{Connections}
\label{sec:connections}

Connections between objects are introduced by the \code{connect}
construct in the equation part of a class declaration.  The
connections are between components called \firstref{connectors}

\begin{Def}{Connector}
  A \term{connector} is an instance of a class defined using the
  \code{connector} keyword.
\end{Def}

The \code{connect} construct takes two references to connectors, each
of which is either an element of the same class as the \code{connect}
construct or an element of one of its components. The connectors are
connected to produce equations according to the rules below.  Each
connector reference has either the syntactic form \code{c}, where
\code{c} is a connector instance in the class containing the
\code{connect} construct, or \code{m.c}, where \code{m} is the name of
a component or an array of components of the class containing the
\code{connect} construct, and \code{c} is the name of a connector
variable in the component \code{m}.


\subsection{Connection sets}
\label{sec:connectsets}

To create equations from the \code{connect} constructs, the connected
variables are collected into \firstref{connection sets}.

\begin{Def}{flow variables}
  A variable can be declared as a \firstref{flow variable}, using the
  prefix \code{flow} in the declaration.  Variables not declared as
  flow variables are called \firstref{non-flow variables}.
\end{Def}

\begin{Def}{Connection sets}
  A connection set is a set $C$ of variables connected by means of
  \code{connect} constructs. A connection set contains either flow or
  non-flow variables, but never both.
\end{Def}

\begin{Def}{Inner and outer connectors}
  In an object $M$, each connector element of that class is called an
  \emph{outer connector} with respect to $M$. Each connector element of
  elements of $M$ is called an \emph{inner connector} with respect to
  $M$.
\end{Def}

When a \code{connect(a,b)} construct is encountered while
instantiating a class \code{C}, the component names \code{a} and
\code{b} are checked to be of the same type (see section
\ref{sec:typeq}). Then \code{a} and \code{b} are decomposed into their
public primitive components. Each subcomponent of \code{a} forms a
connection set with its corresponding subcomponent of \code{b}.

If several \code{connect(a,b)} constructs are encountered during
instantiation of a class, the resulting connection sets are merged to
a collection of connection sets $C$ so that if a component $x$ is in
two different connection sets $S_1$ and $S_2$, the union $S_1 \cup
S_2$ is a subset of one of the sets in $C$. Each component is in
exactly one of the sets in $C$.

\subsection{Equations}
\label{sec:coneq}

Each connection set is used to generate one or more equations. In the
case of variables declared with the \code{flow} type modifier, the
equation generated is a sum-to-zero equation, as in equation
\ref{eq:flow}.  The coefficient $d_v$ is $1$ if the component $v$ was
added to the connection set from an inner connector, and $-1$ if it
was added from an outer connector.

\begin{equation}
  \label{eq:flow}
  \sum_{v \in C} d_v v = 0
\end{equation}

In the case of non-flow components a number of simple equations is
generated. If the connection set contains $n$ components $c_1 \ldots
c_n$, equations to the effect of $c_1=c_2=\cdots=c_n$ are generated,
as in \ref{eqn:nonflow}.

\begin{eqnarray}
  \label{eqn:nonflow}
  c_1     & =      & c_2 \notag\\
  c_2     & =      & c_3 \notag\\
          & \vdots & \notag\\
  c_{n-1} & =      & c_n  
\end{eqnarray}


\subsection{Example}
\label{sec:csetex}

This section contains a short example of the use of connections in
Modelica, and shows the corresponding connection sets and generated
equations.  The Modelica source is shown in figure \ref{fig:csetex1}
and declares a connector \code{C} and models \code{A} and \code{M}.
The model that is instantiated at the top level is \code{M}, as it is
the last model in the file.

\begin{figure}[tbp]
\begin{boxedverbatim}
  connector C
    Real x;
    flow Real y;
  end C;

  model A
    C con1, con2;
  equation
    connect(con1,con2);
  end A;

  model M
    C con;
    A a1, a2;
    Real y;
  equation
    connect(con,a1.con1);
    connect(a1.con1,a2.con1);
    connect(a1.con2,a2.con2);
    y = con.y;
  end M;
\end{boxedverbatim}
  \caption{\code{connect} example}
  \label{fig:csetex1}
\end{figure}

Connection sets are generated at two different levels in this example.
While instantiating the model \code{M}, the three \code{connect}
statements creates the connection sets described in figure
\ref{fig:csetex2}, and the two instances of the model \code{A}
(components \code{a1} and \code{a2} in model \code{M}) create the
connection sets in figure \ref{fig:csetex3}.  Each component in the
sets is marked with a label indicating whether they were added from an
inner or an outer connector.

\newcommand{\couter}[1]{\code{#1}^{\text{outer}}}
\newcommand{\cinner}[1]{\code{#1}^{\text{inner}}}

\begin{figure}[tbp]
  \begin{center}
    $\left\{ \couter{con.x}, \cinner{a1.con1.x}, \cinner{a2.con1.x} \right\}$
    $\left\{ \couter{con.y}, \cinner{a1.con1.y}, \cinner{a2.con1.y} \right\}$
    $\left\{ \cinner{a1.con2.x}, \cinner{a2.con2.x} \right\}$
    $\left\{ \cinner{a1.con2.y}, \cinner{a2.con2.y} \right\}$
    \caption{Connection sets from \code{M}}
    \label{fig:csetex2}
  \end{center}
\end{figure}

\begin{figure}[tbp]
  \begin{center}
    $\left\{ \couter{a1.con1.x}, \couter{a1.con2.x} \right\}$
    $\left\{ \couter{a1.con1.y}, \couter{a1.con2.y} \right\}$
    $\left\{ \couter{a2.con1.x}, \couter{a2.con2.x} \right\}$
    $\left\{ \couter{a2.con1.y}, \couter{a2.con2.y} \right\}$
    \caption{Connection sets from \code{A}}
    \label{fig:csetex3}
  \end{center}
\end{figure}

The equations generated from these connection sets, together with the
last equation in the model \code{M} are shown in figure
\ref{fig:csetex4}.  Since the model connects the same two connectors
several times, the resulting set of equations will of course be
overdetermined.

\begin{figure}[tbp]
  \begin{center}
    \begin{eqnarray*}
      \code{con.x}     &=& \code{a1.con1.x} \\
      \code{a1.con1.x} &=& \code{a2.con1.x} \\
      -\code{con.y} + \code{a1.con1.y} + \code{a2.con1.y} &=& 0 \\
      \code{a1.con2.x} &=& \code{a2.con2.x} \\
      \code{a1.con2.y} + \code{a2.con2.y} &=& 0 \\
      \code{a1.con1.x} &=& \code{a1.con2.x} \\
      -\code{a1.con1.y} - \code{a1.con2.x} &=& 0 \\
      \code{a2.con1.x} &=& \code{a2.con2.x} \\
      -\code{a2.con1.y} - \code{a2.con2.x} &=& 0
    \end{eqnarray*}
    \caption{Equations}
    \label{fig:csetex4}
  \end{center}
\end{figure}


\section{Parameters}
\label{sec:param}

The concept of \term{parameters} is important in simulation, but the
semantics of parameters vs. constants in the modeling language is not
so obvious.

In principle, parameters are constants that the user may modify before
a simulation run is started.  The value of a parameter is constant
throughout the simulation, but it should be possible to change it
before simulation in a simple way.  In description of parameters the
notion of compile-time is often used, indicating that parameters are
not constant during compilation, but constants are.

All this means that it is unclear to what depth the semantic
specification should go.  Should it try to describe the semantics of
a model while the parameters are still unknown?  Or should it assume
some default value for the parameters?

In this work, all parameters are regarded as constants, using the
default value given in the model definition.  In some cases, the
parameters are still possible to change after translation, but in
other cases they are not (see section \ref{sec:strucparam} below).
This means that parameters and constants are treated in the same way
for most practical purposes.  The output still indicates whether they
were declared as parameters or constants.

\subsection{Structural parameters}
\label{sec:strucparam}

When a parameter is used to give variable values, such as the
parameter \code{amplitude} in the example in figure
\ref{fig:nonstrucparam}, there will be no problems changing its value
after translating the model to simple equations.

However, when the parameter is used for more complicated things, such
as defining the size of an array, it is usually not possible to change
its value after translation to simple equations.  Consider the
example in figure \ref{fig:strucparam}.  The size of the array
\code{v} is determined by the parameter \code{levels}.  The equation
section first defines two equations, and then there is a loop which
defines another $\code{levels} - 1$ equations.  This means that the
number of equations in the result of the translation will depend on
the value of the parameter \code{levels}.  Simply changing the value
of \code{levels} after the translation is done will only change the
value, but the number of equations will remain the same, creating an
erroneous model.

\begin{figure}[tbp]
  \begin{center}
\begin{boxedverbatim}
  model SinSource
    parameter Real amplitude;
    Real x;
  equation
    x = amplitude * sin(time);
  end SinSource;
\end{boxedverbatim}
    \caption{Non-structural parameter}
    \label{fig:nonstrucparam}
  \end{center}
\end{figure}

\begin{figure}[tbp]
  \begin{center}
\begin{boxedverbatim}
  model Stack
    parameter Integer levels;
    Real v[levels];
    Real x,y;
  protected
    Integer i;
  equation
    x = v[1];
    y = v[levels];
    for i in 2:levels loop
      v[i-1] = v[i] * 0.8;
    end for;
  end Stack;
\end{boxedverbatim}
    \caption{Structural parameter}
    \label{fig:strucparam}
  \end{center}
\end{figure}

Parameters which change the structure of the equations are called
\term{structural parameters}.  A parameter is a structural parameter
if at least one of the following conditions are fulfilled:

\begin{enumerate}
\item It appears in the dimension size of a array declaration.
\item It is used to index an array in any expression.  
\item It is used in a range expression (\code{a:b} or \code{a:b:c}).
\item Its value is defined in terms of another structural parameter.
\end{enumerate}

The conditions above are not verified to be absolutely correct.  For
instance, the second condition is probably too restrictive.

As this semantic specification treats all parameters as constants,
this distinction between structural and non-structural parameters is
not important.  But for simulation environment implementors, this will
be important.  Most implementations will include a compilation step
before the user gets to set parameters and start the simulation.  The
question is how well these implementations will handle the case when
the user changes the value of a structural parameter.  This is
currently regarded as quality-of-implementation issue, but it might be
worthwhile to examine it further.

\chapter{The Target language: Flat Modelica}
\label{cha:target}

The formal semantic specification in appendix \ref{app:formsem}
specifies the semantics of Modelica by showing how it is translated
into another, simpler, language.  The translation is a sort of
flattening of the object-oriented structure of the model.  This
chapter describes the format of the output of the translator.

\section{Requirements}

There are different requirements that can be placed on the output
format, all of which are not possible to meet simultaneously.

\begin{enumerate}
\item The output should contain all the information gathered from the
  analysis of the Modelica source.
\item The output should be easily read by a human.
\item The output should be easily parsed by a computer.
\item The output should be able to be fed to an existing equation
  solver.
\item The target language needs to be able to express everything that
  can be expressed by the Modelica language
\end{enumerate}



The target language needs to be able to express everything that can be
expressed by the Modelica language, but it may do so in a much less
structured way.  The major part of the translator output consists of a
flat list of equations which are the result of instantiating the main
model of the source file and its subcomponents.


\section{Flat Modelica}
\label{sec:flatform}

The language produced by the translator is similar to Modelica, but
with a few restrictions and extensions.

The following restrictions apply:

\begin{itemize}
  
\item Flat models contain only components of predefined types.
  Predefined attributes, e.g. \code{start}, \code{unit}, \code{min},
  \code{max}, \ldots{} are declared as separate variables.
  
\item A flat model has one declaration section, optionally followed by
  an equation section, which is followed by zero or more algorithm
  sections.
  
\item No modifications are used, i.e. equation modifications made in
  the Modelica source code are stated in the equation section of the
  flat representation.  Redeclarations are taken care of while
  flattening the model.
  
\item No connect statements are used, i.e. the corresponding
  connection equations are stated.
  
\item For loops are not used in equations.  They are unrolled in the
  flat representation.

\end{itemize}

The following extensions are made:

\begin{itemize}
  
\item All array components are declared separately.  If the Modelica
  model contains the declaration

\begin{boxedverbatim}
    Real x[2,3];
\end{boxedverbatim}
  
  the flat model will contain the following declarations:
  
\begin{boxedverbatim}
    Real x[1,1];
    Real x[1,2];
    Real x[1,3];
    Real x[2,1];
    Real x[2,2];
    Real x[2,3];
\end{boxedverbatim}
  
  This means that the brackets in declaration do not denote array
  size, as they do in normal Modelica.
  
  This is a consequence of how the semantic specification looks at the
  components.  Using the simple \codebox{x[2,3]} could be done instead, as it
  is shorter and introduces no ambiguities.
  
\item Identifiers may contain dots (\code{.}) (resulting from
  subcomponents in the originating Modelica code).  Identifiers may
  also contain subscripts, as in \code{x[1]}.  This is a consequence
  of the fact that all array components are declared separately.

\item Automatic type conversions defined in the Modelica semantics,
  e.g.  from an \code{Integer} \code{i} to \code{Real}, are stated
  using the target type name as conversion operator, i.e.
  \code{Real(i)}.
  
\item A new postfix subscripting operator is introduced.  In the flat
  model, it is necessary to be able to subscript expressions, so the
  syntax \code{expression[x]} is allowed.  This is not allowed in
  Modelica.
  
\item A special kind of equation \codebox{ident ::= expression} is
  used to indicate that \code{ident} is not equal to
  \code{expression}, but rather \emph{defined as} \code{expression}.
  
  This is used for splitting equations between two expressions which
  contain subcomponents.  If one of the expressions is not a simple
  name, a temporary name is introduced for that expression, and the
  name is used instead.  If an ordinary equation between the temporary
  name and the expression was introduced, this would not solve the
  problem of defining the semantics of the complex equation, but just
  create a new, similar problem.

  From a mathematical point of view, there is no difference in the
  meaning of \code{::=} and \code{=}.

\item Almost no overloading of operators occurs in the flat Modelica.
  If a model contains an array multiplied by a scalar, the flat model
  does not use the multiplication sign, but an operator that is
  specialized for that particular operation.
  
  The normal integer and real arithmetic operators are still
  overloaded, but they should not, really.
  
\item Due to the extensions a flat model representation is not valid
  Modelica.  Therefore, the class definition in the flat code is
  declared as \code{fclass} to differentiate it from Modelica's
  \code{class}.

\end{itemize}

The output of the translator also has the following properties:

\begin{itemize}

\item The order of equations is undefined.
  
\item The order of statements in each algorithm section is kept
  intact, but the order in which the algorithm sections appear is
  undefined.
  
\end{itemize}

The flat Modelica does not exactly meet the requirements described in
the previous section.

\begin{enumerate}
  
\item Most information gathered from the analysis is included.  Some
  type information is lost, though.  The arithmetic operations on
  scalars and the equality sign are still overloaded.  This is to
  improve readability.  Changing the syntax to include this
  information is very easy.

\item The output looks reasonably much like Modelica, so a person
  knowledgeable of Modelica syntax should have no problem understanding
  the output.
  
\item Parsing of the flat Modelica has not been explored. It should
  possible to write a parser that will accept and understand flat
  Modelica.  One thing that may cause trouble is the extension where
  array subscripting may be allowed on arbitrary expressions.
  
  A modified version of the translator which produces valid Modelica
  is currently being developed.  The output of this version will be
  less readable than the current Flat Modelica, but will allow us to
  feed the output of the translator to another Modelica system.

\item Feeding the output to an equation solver needs either a special
  parser for the solver or a filtering step to rewrite the flat
  Modelica to a syntax understood by the solver.

  
\item Everything in Modelica is expressible in flat Modelica, although
  obviously, structural information is lost.

\end{enumerate}

An example of Flat Modelica can be seen in figure \ref{fig:ex-eq}.

\chapter{Translation overview}
\label{cha:system}


The semantic specification is written as a translation from Modelica
to a target language called flat Modelica (see chapter \ref{cha:target}).  The
translation is performed in several steps, which are outlined in this
chapter.

\begin{figure}[btp]
  \begin{center}
    \input{transfig.tex}
    \centerline{\box\graph}
    \caption{Translation steps}
    \label{fig:transsteps}
  \end{center}
\end{figure}

A schematic view of the translation steps are show in figure
\ref{fig:transsteps}.  The box labeled ``RML'' shows what parts of the
translation are performed and handled by the RML specification.

\section{Lexical analysis and parsing}
\label{sec:laxparse}

The lexical analyzer and parser are not really part of the semantic
specification, and this report will not go into detail about the
parsing of Modelica.  It is based on the Modelica grammar as specified
in the Modelica specification, and is written using a parser generator
called PCCTS\cite{pccts}.  This generates a parser in C, which is
separately compiled and linked with the RML specification.

The Modelica source file being translated is first passed to the
lexical analyzer that scans the source for tokens, which it then
passes on to the parser.  The parser uses its grammar to build an RML
representation of the contents of the source file, which is then used
in the RML specification for further processing.


\section{Abstract syntax}
\label{sec:absyndesign}

The \firstref{abstract syntax} is closely modeled after the syntactic
structure, and is defined in the module \code{Absyn} (section
\ref{src:Absyn}).  It basically defines data structures for
representing the structure of the source file (the \firstref{abstract
  syntax tree}, or \firstref{AST}), which are used by the parser to
build a tree describing the source file.  There is a datatype for
representing a class definition, and the whole file is represented
using the datatype \code{Program}, which is defined as a list of
classes.

\section{Preparing the AST: SCode}
\label{sec:asttoscode}

That the AST keeps the structure of the source file has several
disadvantages when it comes to translating the program, especially if
the translation rules should be easy to read for a human.  To address
this problem, a preparatory transformation pass is introduced which
transforms the AST into an intermediate form, called \firstref{SCode}.
This intermediate form contains no more information than the abstract
syntax, but merely restructures the tree representation in it.
Besides some minor simplifications the SCode structure differs from
the abstract syntax in the following important respects:

\begin{description}
\item[All components are described separately]
  
  In the source and in the abstract syntax several components in a
  class definition can be declared at once, as in \codebox{Real x,
    y[17];}.  In the SCode this is represented as two unrelated
  declarations, as if it had been written \codebox{Real x; Real
    y[17];}.

\item[Class declaration sections]
  In a Modelica class declaration the \code{public}, \code{protected},
  \code{equation} and \code{algorithm} sections may be included in any
  number and in any order, with an implicit \code{public} section
  first.  In the SCode these sections are collected so that all
  \code{public} and \code{protected} sections are combined into one
  section, while keeping the order of the elements.  The information
  about which elements were in a \code{protected} section is stored
  with the element itself.

\item[Modifications]
  Modifications are stored using the data types in the \code{Mod}
  module (section \ref{src:Mod}).
\end{description}

One might have thought that more work could be done at this stage,
such as expression type analysis and name resolution.  But due to the
nature of the Modelica language, the only way to know anything about
how the names will be resolved during instantiation is to do a more or
less full instantiation.  It is possible to analyze a class
declaration and find out what the parts of the declaration would mean
if the class was to be instantiated as-is, but since it is possible to
modify much of the class while instantiating it that analysis would
not be of much use.

\section{Instantiation}
\label{sec:instantiation}

The major part of the translation procedure, as described by the RML
specification is the translation from SCode to hybrid
differential-algebraic equations (hybrid DAEs).

A Modelica source file contains only definitions of models and other
classes, which does not really have any semantic meaning in terms of
equations, since the equations appear when a model definition is
\emph{used} to create an instance of that model.
                                                 
To give a Modelica source file a meaning there is a convention that
the last class, which should be a model, is instantiated as the
top-level model.  In a graphical modeling environment the situation
will of course be different.

To go into detail exactly how the instantiation works here would be
too lengthy, but a brief overview is given below.


\subsection{Instantiation environment}
\label{sec:instenv}

When instantiating a class, certain information is available about
what has been instantiated before, and what set of modifiers are
currently applicable to the class being instantiated.  Modelica uses
lexical scoping (the language specification currently specifies
dynamic scoping, but this will be changed in later versions), which
means that when a class definition is saved in the environment, the
current environment needs to be saved in the environment together with
the class definition.

\subsection{Class instantiation}
\label{sec:eleminst}

Instantiation of a class is done by the relation
\code{Inst.inst\_class}.  It goes through the class definition and
instantiates all its elements, expanding all \code{extends} elements.
The equations are added to the list of equations that are collected as
the result of instantiation.

Before adding anything to the result, all names of components are
converted to globally unique names, using the normal hierarchical
naming scheme with dots between the name parts.  If the topmost model
contains a sub-model named \code{a}, which contains a variable
\code{b}, the global name of this variable will be \code{a.b}.


\section{Static expression analysis}
\label{sec:static}

The module \code{Static} contains relations that perform static
analysis and constant propagation on expressions.  The primary reason
to analyze expressions is to check their types, and make sure that
there are no type errors.  Constant propagation is used whenever the
translator needs to know the actual value of an expression.  The
module is described in section \ref{src:Static}, with the following
highlights.

\begin{itemize}
\item The relation \code{elab\_exp} (\ref{src:Static:elabexp})
  analyzes an expression and produces two results: a new expression
  and a set of properties.  The new expression is of type
  \code{Exp.Exp} (\ref{src:Exp}) and is much more specific than the
  abstract syntax expressions.  For each needed type conversion in the
  expression, an explicit type conversion operation is inserted, and
  the operators that are overloaded in the abstract syntax are
  replaced by non-overloaded counterparts.
  
  The set of properties describes the type of the expression (see
  section \ref{sec:types}), and its \firstref{variability}, which
  basically indicates whether the expression is constant or not.

\item The relation \code{ceval} evaluates an expression and gives the
  result as a \code{Values.Value} (section \ref{src:Values}).  This
  can obviously only be done for constant expressions.
\end{itemize}

\section{Equation transformations}
\label{sec:eqtrans}

An equation in the equation section of a Modelica model can take
several forms, and to describe the semantics of an equation, different
transformations are applied.


\subsection{Subcomponent equation expansion}

\begin{figure}[tbp]
  \begin{center}
\begin{boxedverbatim}
  model M
    real x[3], y[3];
  equation
    x = y;
  end M;
\end{boxedverbatim}
    \caption{Array component equation}
    \label{fig:arreq}
  \end{center}
\end{figure}

\begin{figure}[tbp]
  \begin{center}
\begin{boxedverbatim}
  model M
    real x[3], y[3];
  equation
    x[1] = y[1];
    x[2] = y[2];
    x[3] = y[3];
  end M;
\end{boxedverbatim}
    \caption{Expanded array equations}
    \label{fig:arreqexp}
  \end{center}
\end{figure}

When two arrays are equated, as in figure \ref{fig:arreq}, the
equation has the same meaning as if all the array elements were
equated.  Thus, in the output the equation is split into one equation
for each pair of array elements, as in figure \ref{fig:arreqexp}.

Likewise, if two structured components are equated, the equation is
expanded to one equation for each pair of public components.

These two transformations causes problems in the output if either the
left-hand side or the right-hand side of the equation is a complex
expression and not a name of a component.  The Modelica syntax does
not allow the concept of expression subscripting or of picking
subcomponent from complex expressions.  In the flat Modelica output
(see chapter \ref{cha:target}) this is solved in two different ways.
For arrays, an expression subscripting operator is introduced, which
allows things like \codebox{(A*B)[3,4]}.  For expressions of a
composite type, a new identifier is introduced, which is defined to be
identical to the expression.  Then this name is used to look up
subcomponents.  The name is constructed by concatenating the name
\code{\_\_TMP\_\_} with a unique integer, forming a name that looks
something like \code{\_\_TMP\_\_17}.

\section{Class restriction inference}
\label{sec:classinf}

To be able to determine if a class definition or a variable can be
used under certain circumstances it is necessary to check whether it
adheres the restrictions currently imposed on it. If the class is
declared with one of the restricted keywords listen in table
\ref{tab:clrestr}, it is immediately known, but when the class is
declared using the \code{class} keyword, the definition has to be
scanned to see what restrictions it breaks.

This is done for each variable as it is instantiated, using the state
machine in the file \filename{classinf.rml} (see section
\ref{src:ClassInf}).  While instantiating a class the current state is
kept in a variable of type \code{ClassInf.State}.  It is initialized
with the keyword used to declare the class using the relation
\code{ClassInf.start}.  If the keyword was one of the restricted
forms, the state will be initialized to a state that directly
corresponds to that form, and it will never change to another state.
If the keyword was \code{class}, the state is initialized to
\code{ClassInf.UNKNOWN}.

Transitions in the state machine are triggered by events signaled
during instantiation indicating that some piece of information has been
encountered which affects the class restriction. The defined events
are listed in table \ref{tab:classinfevents}.

\begin{table}[tbp]
  \begin{center}
    \begin{tabular}{lp{8cm}}
      \hline
      \code{FOUND\_EQUATION} & The class is now known to contain at
      least one equation. \\
      \code{NEWDEF} & This class is not derived from another class
      with the \code{class A = B} construct. \\
      \hline
    \end{tabular}
    \caption{Class restriction inference events}
    \label{tab:classinfevents}
  \end{center}
\end{table}

After instantiation of a class is complete, the state of the machine
can be checked against a desired restriction to see if the class
definition fulfills it, using the relation \code{valid}
(\ref{src:ClassInf:valid}).

\section{Representation of types}
\label{sec:typerep}

When instantiating, each component is assigned a type descriptor which
is constructed from the type used in the component declaration
combined with all applicable modifications.

The type descriptors are used in several places in the semantic
specification, but two distinct types of usage can be noted.

\begin{description}
\item[Subcomponent lookup] To look up components inside a component, a
  description of all its subcomponents are needed.  This description
  must contain information about which components are protected.  This
  kind of lookup is usually done in places where all type and
  component attributes are needed to determine such things as what
  components can be connected to each other.
\item[Type checking of expressions] Expressions are checked for type
  incompatibilities, which means that information about the types of
  components has to be known.  In this context less information is
  needed.  Either a component is of one of the built-in types, or it
  is a complex type, but then only the names and types of the public
  subcomponents need to be known.
\end{description}

These two needs could be met by two different data types, and a
previous version of the specification did it this way.  But having two
data types that essentially does the same thing is more confusing than
helpful, so they were reduced to only one.


\section{DAE representation}
\label{sec:dearep}

The DAEs are collected in a data structure defined in the module
\code{DAE} (section \ref{src:DAE}).  This structure is basically a
linear list where each element is either a variable declaration, an
equation or an algorithm.



\section{Output of equations}
\label{sec:output}

As the last stage of the translation the internal representation of
the hybrid DAEs are written out in the format described in chapter
\ref{cha:target}.


\section{An example}

To show how the translation of a Modelica model is done in a more
visual manner, this section gives a small example of a model, and how
it is translated to a flat representation.


\subsection{The model}

The source model is given in figure \ref{fig:modelsource}.  It is a
very simple electrical circuit, with an AC voltage source and two
capacitors.

\begin{figure}[tbp]
  \input{example-1.tex}
  \caption{Model source}
  \label{fig:modelsource}
\end{figure}


\subsection{First transformation}

The first thing the translator does it to transform the abstract
syntax tree representing the model into an SCode representation.  This
mainly effects the \code{Circuit} model definition, giving something
that is described in figure \ref{fig:ex-scode}, using a
pseudo-Modelica representation.

\begin{figure}[tbp]
  \input{example-2.tex}
  \caption{SCode for \code{Circuit}}
  \label{fig:ex-scode}
\end{figure}


\subsection{Flattening}

The main translation step does several things simultaneously.  One
important part is the flattening of the hierarchical structure.  This
means that all composite components are split up in subcomponents, and
all atomic components will receive a new name that identifies it with
a unique identifier in the global name space.  For instance, the
voltage variable in the positive connector in the capacitor named
\code{C2} will get the global name \code{C2.p.v}.

The set of all components is listed with their global names in figure
\ref{fig:ex-flatname}.

\begin{figure}[tbp]
  \input{example-3}
  \caption{Global component names}
  \label{fig:ex-flatname}
\end{figure}


\subsection{Connection equations}

Generating equations from the connections in the model is done by
collecting the connected variables into connection sets (see section
\ref{sec:connectsets}).  There will be one set for each set of
connected voltage variables and one set for each set of connected
current variables, giving the connection sets in figure
\ref{fig:ex-csets}.  All connectors are inner connectors, which means
that the connection sets will generate the equations given in figure
\ref{fig:ex-eq}.

\begin{figure}[tbp]
  \begin{center}
    $\left\{ \code{AC.p.v}, \code{C1.p.v}, \code{C2.p.v} \right\}$
    $\left\{ \code{AC.p.i}, \code{C1.p.i}, \code{C2.p.i} \right\}$
    $\left\{ \code{AC.n.v}, \code{C1.n.v}, \code{C2.n.v} \right\}$
    $\left\{ \code{AC.n.i}, \code{C1.n.i}, \code{C2.n.i} \right\}$
    \caption{Connection sets}
    \label{fig:ex-csets}
  \end{center}
\end{figure}

\subsection{Flat Modelica}

The output of the translator is shown in figure \ref{fig:ex-eq}, which
is the Flat Modelica version of the source model.  All the components
are expanded into their simple components.

\begin{figure}[tbp]
  \begin{center}
    \input{example-4}
    \caption{Flat Modelica output}
    \label{fig:ex-eq}
  \end{center}
\end{figure}


\chapter{Conclusions}
\label{cha:conclusions}

In this chapter, some of the conclusions and experiences from writing
the semantic specification are given.  Also, some suggestions for
future work are proposed.

\section{Result}
\label{sec:result}

The result of this work is an RML semantic specification for Modelica
which is incomplete, but works fairly well for the part of the
language it handles.

Another result of working on the semantic specification is that many
problems and unclear issues in the Modelica semantics have been
resolved.  This has not always lead to progress in the formal
specification, since it sometimes has meant that it had to be
rewritten due to changes in the semantics.  But in a larger
perspective, namely the progress of the Modelica language
specifications, it has implied substantial progress.

\section{Translator usability}

Another goal was to produce a Modelica translator that could be used
in real-world applications.  This has become something of a secondary
goal, but there are some issues worth mentioning.

Some properties of the formal semantic specification makes the output
of the translator not so suitable for real use.  For instance, solving
matrix equations is often best done by keeping them as equations
between matrices, but the translator translates them to one equation
for each of the matrix elements.

There are some hidden options\footnote{The command-line option
  \code{+m} makes the translator produce valid Modelica, \code{+a}
  prevents it from splitting arrays, and \code{+t} excludes type
  information in overloaded operators and implicit type conversions}
in the translator which makes it possible to have it output something
that is easier to pass on to existing solvers and simulation
environments.  This is not complete, and relies on some ugly tricks
with the RML system.  This code is not included in this report.

The performance of the translator has not been fully evaluated,
although a simple performance test was done using a 1049--line
Modelica model, containing 16 repetitions of a simple electrical
circuit model.  The test was performed on a Sun Ultra 1 workstation
running Solaris 2.6.  Running the translation 20 times with the
standard output directed to \filename{/dev/null}, it translated the
file in 0.26 seconds on the average.  This is not a complete test, but
at least it hints that the performance is reasonable.


\section{RML experiences}
\label{sec:rmlexpereince}

For practical purposes, writing an RML specification is very much like
programming in a functional programming language or a logic
programming language, but without the expressive power of those
languages.  This limitations of course make the programming more
cumbersome, but on the upside, the resulting specification will
hopefully be much more readable.

The newest version of the RML compiler works well, and even gives
useful error messages.  However, debugging a specification after it
has passed through the compiler is not very fun.  No debugger is
available, and there is no built-in means of tracing the resolution
process.

\section{Future work}
\label{sec:future}

As already stated, the semantic specifications needs more work before
it can be considered complete.  It is possible that it even needs to
be rewritten in large parts, to accommodate for new developments in the
Modelica design process.

To make the translator usable in a production environment, more work
is needed to allow the translator to be used with existing modeling
tools and equation solvers.

Another important work is the development of a test suite that is used
to test the translator to see that it does what it is supposed to.
There currently exists a test suite that tests most of the features
that are implemented, and some which are not yet implemented.  It
contains over 160 cases, but it needs to be expanded 


\appendix

\chapter{Annotated formal semantics}
\label{app:formsem}

This chapter contains the complete formal semantics of Modelica.  This
includes the RML source files, but the comments in the files have been
converted to more readable text.

\section{Overview}

The specification is separated into a number of files, to modularize
it and to make it easier to maintain and to make the structure more
clear.  Each file contains one module.  The names of the files are the
names of the module it contains, with all letters in lower case, and
with the suffix \code{.rml} appended.

\subsection*{Source modules}

\listofsources

%\begin{landscape}
  
\input{main.tex}
\input{absyn.tex}
\input{exp.tex}
\input{classinf.tex}
\input{types.tex}
\input{explode.tex}
\input{inst.tex}
\input{prefix.tex}
\input{mod.tex}
\input{algorithm.tex}
\input{env.tex}
\input{lookup.tex}
\input{builtin.tex}
\input{connect.tex}
\input{values.tex}
\input{staticexp.tex}
\input{dae.tex}
\input{dump.tex}

%\end{landscape}

\chapter{rmldoc}
\label{app:rmldoc}

{\codefont\verbatiminput{../tools/rmldoc}}

\bibliographystyle{plain}
\bibliography{report}

% \printindex

\end{document}
