Skip to content

Commit

Permalink
Add back Peter's edits and resolve unfinished merge
Browse files Browse the repository at this point in the history
nikklassen committed Feb 24, 2017
1 parent 51b2536 commit 7cc430c
Showing 1 changed file with 3 additions and 70 deletions.
73 changes: 3 additions & 70 deletions body.tex
Original file line number Diff line number Diff line change
@@ -18,18 +18,11 @@ \subsection{Module System}
essential features are outlined in the rest of this section.
The Manifold module system shares the basic features outlined by Cardelli
\cite{Cardelli:1997:PFL:263699.263735}. Each module, in this case a file, can
<<<<<<< HEAD
declare functions and values as \texttt{public}. When a module imports another
module, all of the public exported values in the imported module will be
accessible. Other programming languages, such as Simple ML, feature more exotic module systems, but this complexity
is not currently beneficial to Manifold. Listing~\ref{lst:exports} shows a module that exports several values, as well two
=======
declare functions and values as \texttt{public} --- the exports. When a module imports another
module, all of the exported values in the imported module will be
accessible. Other programming languages, such as Simple ML, feature more exotic module systems, but this
additional complexity is not currently beneficial to Manifold. \autoref{lst:exports} shows a module
that exports several values, as well two
>>>>>>> General edits
electrical nodes that use \texttt{Nil} to denote no input or output.

\begin{lstlisting}[label=lst:exports, caption=Exported values in a Manifold file]
@@ -45,24 +38,13 @@ \subsection{Module System}
resistance = 2;
\end{lstlisting}

<<<<<<< HEAD
Manifold does not compile modules separately. On import, types
are added to the global namespace while values are added to a namespace for the
module they were imported from. Manifold interprets all language constructs as
expressions and imports are no exception. This differs from how imports are
treated as statements in many other
programming languages (even in other functional languages like Haskell and
OCaml, imports do not return a value). In Manifold, import expressions allow module
exports to be scoped by assigning the result of the expression
=======
On import, types are added to the global namespace, and the exported values are returned by the import
expression. In Manifold all language constructs are
expressions, and imports are no exception. This differs from how imports are
treated as statements in many other
programming languages, even in other functional languages like Haskell and
OCaml imports do not return a value. Import expressions allow the
export values of a module to be scoped by assigning the result of the expression
>>>>>>> General edits
to a variable. The imported values are then referenced as properties of that
variable, see \autoref{lst:imports}. A module effectively becomes, and is used as,
a record data type. In the future, it is desirable that Manifold support a
@@ -84,60 +66,32 @@ \subsection{Module System}

\subsection{Type System}

<<<<<<< HEAD
In order to reduce the number of bugs making it through the compilation stage,
Manifold includes a static type checking system. Similar to type-defs in the C
programming language, Manifold allows its users to define or import types,
as well as label variables as being of a certain type. Upon compilation,
Manifold performs static analysis of all typed variables, ensuring that they are
truly of the type they are labeled as, or outputting an error if this is not the
case.
=======
Manifold includes a static type checking system in order to increase the percentage of bugs found during
the compilation stage. Similar to typedefs in the C
programming language, Manifold allows its users to define and import types,
as well as annotate variables with a specific type. Upon compilation,
Manifold performs static analysis of all expression variables, inferring the type of a variable when it
is not explicitly defined.
>>>>>>> General edits

The type system demonstrated in \autoref{lst:types} is Manifold 2.0's structural typing system.
Structural type systems were
created to remove some of the issues with nominal type systems
\cite{Gil:2008:WIS:1449764.1449771}. In a structural
<<<<<<< HEAD
type system, a type A is compatible with another B if for every feature in
=======
type system, a type A is compatible with another type B if for every feature in the
>>>>>>> General edits
type system, a type A is compatible with another type B if for every feature in
A there is a compatible feature in B. Unlike nominal type systems, structural
type systems allow for the supertypes and subtypes of a type to be defined without
modifying the original type. This allows for complex derived types in Manifold that
can extend the different libraries of components.

<<<<<<< HEAD
Manifold allows the assignment of subtype values to a variable whose type is a
supertype of the value's, but not vice-versa, (i.e. a supertype value cannot be
assigned to a subtype variable).
Tuple types are the exception to this rule, being
considered compatible if the signature of the tuples
match. If the value tuple's subfields are assignable to each of the
variable tuple's subfields, then the value tuple can be assigned to the variable
tuple. As Manifold is a descriptive language, it would be an error to allow
the user to hide components and never connect them, so the language will not slice
the fields of a tuple A if you try to assign A to a tuple B with a subset of A's
fields.
=======
Manifold allows the assignment of subtype values to a variable declared with a supertype of that value,
but not vice-versa.
However, tuple types are the exception to this rule. Tuples are
considered compatible if the signatures of two tuples
match, meaning that if the value tuple's subfields are assignable to each of the
match. If the value tuple's subfields are assignable to each of the
other tuple's subfields, then that value can be assigned to that variable.
Some structural typing systems will allow assignment to a type with a subset of the source's fields.
As Manifold is a hardware description language, it would be usually be a logical error to allow
the user to ``drop'' fields in a component.
>>>>>>> General edits

\begin{lstlisting}[label=lst:types,caption=Example of types in a Manifold file]
// Type definitions
@@ -175,11 +129,7 @@ \subsection{Improvements to Tuples}
class. Naming elements means that a programmer can refer an element of a tuple using a
index or the name of that element. Named elements increase the readability of
Manifold and offers a language construct similar to structs in C or record
<<<<<<< HEAD
data types in Haskell. These language features are shown in Listing~\ref{lst:unpacking}.
=======
data types in Haskell. These language features are shown in \autoref{lst:unpacking}.
>>>>>>> General edits

\begin{lstlisting}[label=lst:unpacking, caption=Examples of new tuple features]
and = primitive node (in0: digitalIn, in1: digitalIn) -> (out: digitalOut);
@@ -212,40 +162,24 @@ \subsection{Modelica Code Generation and MapleSim Integration}
Generating Modelica code was of interest because it allows the backend to create simulations of the
synthesized model.
Modelica models are more expressive than SMT2 equations and can simulate how the system will behave with time.
<<<<<<< HEAD
This allows for verification analysis
with respect to the design requirement for parameters that may vary in time.
=======
>>>>>>> General edits

Modelica is open-source and there are many software frontends that support it.
We chose to integrate Manifold with MapleSim, a proprietary simulator developed by MapleSoft.
MapleSim offers a Java API called OpenMaple, allowing it to be called programmatically by Manifold.

Modelica models for MapleSim are straightforward to generate from a Manifold schematic.
<<<<<<< HEAD
A MapleSim model is a list of design components that can be connected to each other using their ports.
The Manifold schematic format has concepts of nodes, ports, and connections, allowing a simple mapping between the two formats.
=======
A MapleSim model is a list of design components that are connected to each other using their ports.
The Manifold schematic format also has concepts of nodes, ports, and connections, allowing a simple mapping
between the two formats.
% I think that this can be removed. We have already said that the mapping is simple so more detail seems cumbersome. If we do decide to keep this lets disambiguate what "nodes" we are talking about (ie we are referring to the nodes in the schematic) and perhaps give a quick example (ie fluid entry component with attributes relating to liquid viscosity?) MP
% TODO(nik): What is CAD, can we explain this acronym?
>>>>>>> General edits
To identify the type of a component, the Manifold microfluidics backend relies on the attributes of the nodes.
On top of the core Modelica code, MapleSim supports annotations that specify the positions of components on a CAD interface and the settings of the simulations.
The Manifold microfluidics backend usually cannot infer the values of these annotations from the schematics
alone and instead tries to fill in the values with reasonable defaults.

<<<<<<< HEAD
A Modelica model can list components and their types (e.g. circular pipes, T-junctions, fluid exit points).
A Modelica model does not contain specific domain knowledge or physical equations that describe how exactly the component works.
=======
A Modelica model can list components and their types (e.g. circular pipes, T-junctions, fluid exit points),
but it does not contain specific domain knowledge or physical equations that describe how exactly these
component works.
>>>>>>> General edits
Instead, the inner workings of components are specified in libraries.
MapleSim has libraries with equations for components in domains fields such as hydraulics and electrical
circuits, both of which have some analogies to microfluidic circuits.
@@ -292,7 +226,7 @@ \subsection{Inferencing with Incomplete Descriptions}

The microfluidics backend will begin the processes of resolving inferred values by generating SMT2 equations
and querying dReal for a solution.
If dReal returns that the system of equations is not satisfiable, Manifold will notify the
If dReal returns that the system of equations is unsatisfiable, Manifold will notify the
user and ask the user to change the design. If dReal is unable to prove the system of equations is unsatisfiable,
it will output a range of values for the inferred variables to be further tested.
The microfluidics backend would parse the dReal output and choose values within the given ranges for the
@@ -324,7 +258,6 @@ \section{Related Work}
framework because the synthesis in Manifold happens using dReal, which is a combinatorial approach
of equation solving using boolean satisfiability. In contrast, Axilog employs a algorithmic and
interactive optimization technique for synthesis.
>>>>>>> General edits

\section{Future Work}

0 comments on commit 7cc430c

Please sign in to comment.