Updates based on masters defense

doc/MastersThesis/Lhs/Appendix.lhs

@@ -1,4 +1,3 @@
-
 \section{Literate Programming}
 
 This dissertation made use of literate programming~\footnote{\href{https://en.wikipedia.org/wiki/Literate_programming}{\textcolor{blue}{Literate Programming}}.}, a concept
@@ -26,4 +25,111 @@ the latest iteration of the Lorenz Attractor example, time step of $0.01$ with t
 commands for Windows when running in a Linux machine and vice-versa, should be ignored.
 \end{itemize}
 
+\section{FFACT's Manual}
+\label{appendix:manual}
+
+This is a concise and pragmatic manual on how to create and run simulations using \texttt{FFACT}. For a deeper and more detailed description
+of the internals of the DSL, including a walkthrough via examples, please consult (and generate via \texttt{literate.sh}) either \texttt{GraduationThesis} (for \texttt{FACT}) or \texttt{MasterThesis} (for \texttt{FFACT}).
+
+\subsection{Models}
+
+A simulation model is defined using \texttt{mdo-notation}  (check
+\href{https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/recursive_do.html}{recursive
+do}) to describe a system of \textit{differential equations}. The current version of \texttt{FFACT} only supports 
+continuous simulations, i.e., discrete or hybrid simulations are future work. Alongside the equations, one must provide \textit{initial conditions} for 
+each individual equation, such as the following:
+
+\begin{purespec}
+lorenzModel :: Model [Double]
+lorenzModel = mdo
+   x <- integ (sigma * (y - x)) 1.0
+   y <- integ (x * (rho - z) - y) 1.0
+   z <- integ (x * y - beta * z) 1.0
+   let sigma = 10.0
+       rho = 28.0
+       beta = 8.0 / 3.0
+   return $ sequence [x, y, z]
+\end{purespec}
+
+In this example, \texttt{lorenzModel} will return the state variables of interest via a list, hence the model having the type \texttt{Model [Double]}.
+Recursive monadic bindings are possible due to \texttt{mdo}, which makes the description of a model in code closer to its mathematical counterpart.
+
+\subsection{Solver}
+
+Solver-specific configurations, e.g., which numerical method should be used and with which \textit{time step}, which solver stage should it start with,
+are configured \textit{separately} from the model and from executing a simulation. This sort of configuration details are set via a separate record, such as the following:
+
+\begin{purespec}
+lorenzSolver = Solver { dt = 1,
+                        method = RungeKutta2,
+                        stage = SolverStage 0
+                      }
+\end{purespec}
+
+Available numerical methods:
+\begin{itemize}
+\item \texttt{Euler}
+\item \texttt{RungeKutta2}
+\item \texttt{RungeKutta4}
+\end{itemize}
+
+\subsection{Simulation}
+
+A model and a record with solver's configuration are some of the \textit{arguments} to a \textit{driver function}. A driver function runs the simulation starting from 0 until
+a provided timestamp (in seconds). Currently, \texttt{runCTFinal} outputs the final result of the system
+at the provided final time and \texttt{runCT} outputs a \textit{list} of intermediate values from the start
+until the provided final time spaced by the time step within the solver's configuration. 
+The type signatures of these functions are the following (\texttt{Double} is the final time of choice):
+
+\begin{purespec}
+runCTFinal :: Model a -> Double -> Solver -> IO a
+runCT :: Model a -> Double -> Solver -> IO [a]
+\end{purespec}
+
+\subsection{Interpolation}
+
+Both \texttt{FACT} and \texttt{FFACT} use \textit{linear interpolation} to approximate results in requested timestamps that are not reachable via the chosen time step within
+the solver's configuration. Driver functions automatically take care of detecting and running interpolations. 
+The type signature of the provided interpolation function (and probably future extensions) is the following:
+
+\begin{purespec}
+interpolate :: CT Double -> CT Double
+\end{purespec}
+
+\subsection{Caching}
+
+Both \texttt{FACT} and \texttt{FFACT} employ a \textit{memoization strategy} for caching, in order to speed up the simulation execution. Without this, simulations recompute previously
+computed values multiple times, due to the recursive nature of the numerical methods available. A table is saved in memory with already calculated values, and lookups
+are done instead of triggering a new computation.
+The type signature of the provided memoization function (and probably future extensions) is the following:
+
+\begin{purespec}
+memo :: UMemo e => (CT e -> CT e) -> CT e -> CT (CT e)
+\end{purespec}
+
+The typeclass \texttt{UMemo} is provided custom typeclass.
+
+\subsection{Example}
+
+Lorenz Attractor complete example:
+
+\begin{purespec}
+lorenzModel :: Model [Double]
+lorenzModel = mdo
+   x <- integ (sigma * (y - x)) 1.0
+   y <- integ (x * (rho - z) - y) 1.0
+   z <- integ (x * y - beta * z) 1.0
+   let sigma = 10.0
+       rho = 28.0
+       beta = 8.0 / 3.0
+   return $ sequence [x, y, z]
+
+lorenzSolver = Solver { dt = 1,
+                        method = RungeKutta2,
+                        stage = SolverStage 0
+                      }
+
+lorenz = runCTFinal lorenzModel 100 lorenzSolver
+\end{purespec}
+
 

doc/MastersThesis/Lhs/Conclusion.lhs

@@ -1,3 +1,6 @@
+Our motivation was to mitigate the high difficulty of modeling
+arbitrary closed feedback loops, using the DSL proposed by Medeiros et al.~\cite{Edil2018}. In their DSL, time-varying signals are abstracted by a function data type that updates the state of the system, and the topology of the system can only be described via a set of composition operators instead of dealing with the signals explicitly. In this work, we tackled this by proposing \texttt{FACT}: a reimplementation of the DSL based on a new implementation abstraction, called \texttt{CT}, whilst maintaining GPAC as the formal inspiration. This new data type holds the state of the system indirectly, thus allowing the user of the DSL to directly manipulate the signals when describing a system of equations. The guiding example used throughout this work, the Lorenz Attractor in Figure~\ref{fig:introExample}, is an example of a system with feedback loops that the former DSL could not express. Despite solving this expressivenness problem, \texttt{FACT} introduced an abstraction leaking, exposing to the users of the DSL internal implementation details. We solved this issue leveraging the monadic fixed-point combinator, resulting \texttt{FFACT} and thus improving the notation and usability. 
+
 Chapter 2 established the foundation of the implementation, introducing
 functional programming (FP) concepts and the necessary types
 to model continuous time simulation --- with continuous time machines (\texttt{CT}) being the main type. Chapter 3 extended its power via
@@ -7,15 +10,9 @@ for it, as well as the available numerical methods for simulation.
 As a follow-up, Chapter 4 raised intuition and practical understanding of \texttt{FACT} via a detailed walkthrough of an example.
 Chapter 5 explained and fixed the mix between different domains in the simulation, e.g., continuous time, discrete time and iterations,
 via an additional linear interpolation when executing a model. Chapter 6 addressed performance concerns via a memoization strategy. Finally,
-Chapter 7 introduced the fixed-point combinator in order to increase conciseness of the HEDSL, bringing more familiarity to systems designers
+Chapter 7 introduced the fixed-point combinator and its monadic counterpart in order to increase conciseness of the HEDSL, bringing more familiarity to systems designers
 experienced with the mathematical descriptions of their systems of interest. This notation enhancement is the defining feature between FACT and FFACT.
 
-\section{Final Thoughts}
-
-When Shannon proposed a formal foundation for the Differential Analyzer~\cite{Shannon}, mathematical abstractions were leveraged to model continuous time. However, after the transistor era, a new set of concepts that lack this formal basis was developed, and some of which crippled our capacity of simulating reality. Later, the need for some formalism made a comeback for modeling physical phenomena with abstractions that take \textit{time} into consideration. Models of computation~\cite{LeeModeling, LeeChallenges, LeeComponent, LeeSangiovanni} and the ForSyDe framework~\cite{Sander2017, Seyed2020} are examples of this change in direction. Nevertheless, Shannon's original idea is now being discussed again with some improvements~\cite{Graca2003, Graca2004, Graca2016} and being transposed to high level programming languages in the hybrid system domain~\cite{Edil2018}.
-
-The \texttt{FACT} EDSL~\footnote{\texttt{FACT} \href{https://github.com/FP-Modeling/fact/releases/tag/3.0}{\textcolor{blue}{source code}}.} follows this path of bringing CPS simulation to the highest level of abstraction, via the Haskell programming language, but still taking into account a formal background inspired by the GPAC model. The software uses advanced functional programming techniques to solve differential equations, mapping the abstractions to FF-GPAC's analog units. Although still limited by the discrete nature of numerical methods, the solution is performant and accurate enough for studies in the cyber-physical domain.
-
 \section{Future Work}
 
 The following subsections describe the three main areas for future improvements in \texttt{FFACT}: formalism, possible extensions, and code refactoring. 

doc/MastersThesis/Lhs/Design.lhs

@@ -35,8 +35,6 @@ Composition rules that restrict how these units can be connected to one another.
   \item Each variable of integration of an integrator is the input \textit{t}.
 \end{itemize}
 
-During the definition of the DSL, parallels will map the aforementioned basic units and composition rules to the implementation. With this strategy, all the mathematical formalism leveraged for analog computers will drive the implementation in the digital computer. Although we do not formally prove a refinement between the GPAC theory, i.e., our specification, and the final implementation of \texttt{FACT}, is an attempt to build a tool with formalism taken into account; one of the most frequent critiques in the CPS domain, as explained in the previous Chapter.
-
 \section{The Shape of Information}
 \label{sec:types}
 

doc/MastersThesis/Lhs/Enlightenment.lhs

@@ -34,7 +34,7 @@ oldLorenzSystem = runCTFinal oldLorenzModel 100 lorenzSolver
 \end{code}
 }
 
-Previously, we presented in detail the latter core type of the implementation, the integrator, as well as why it can model an integral when used with the \texttt{CT} type. This Chapter is a follow-up, and its objectives are threefold: to describe how to map a set of differential equations to an executable model, to reveal which functions execute a given example and to present a guided-example as a proof-of-concept.
+Previously, we presented in detail the latter core type of the implementation, the integrator, as well as why it can model an integral when used with the \texttt{CT} type. This Chapter is a follow-up, and its objectives are threefold: to describe how to map a set of differential equations to an executable model, to reveal which functions execute a given example and to present a guided-example as a proof-of-concept. For a simplified guide on how to use the DSL, check the Appendix~\ref{appendix:manual}.
 
 \section{From Models to Models}