diff --git a/doc/MastersThesis/Lhs/Appendix.lhs b/doc/MastersThesis/Lhs/Appendix.lhs
index 5274d8f..c1f49e0 100644
--- a/doc/MastersThesis/Lhs/Appendix.lhs
+++ b/doc/MastersThesis/Lhs/Appendix.lhs
@@ -1,8 +1,8 @@
 
 \section{Literate Programming}
 
-This thesis leverages~\footnote{\href{https://en.wikipedia.org/wiki/Literate_programming}{\textcolor{blue}{Literate Programming}}.}, a concept
-introduced by Donald Knuth~\cite{knuth1992}. Hence, this thesis can be executed using the same source files that the \texttt{PDF} is created
+This dissertation made use of literate programming~\footnote{\href{https://en.wikipedia.org/wiki/Literate_programming}{\textcolor{blue}{Literate Programming}}.}, a concept
+introduced by Donald Knuth~\cite{knuth1992}. Hence, this document can be executed using the same source files that the \texttt{PDF} is created
 
 This process requires the following dependencies:
 \begin{itemize}
diff --git a/doc/MastersThesis/Lhs/Caching.lhs b/doc/MastersThesis/Lhs/Caching.lhs
index 54d328c..c750e5f 100644
--- a/doc/MastersThesis/Lhs/Caching.lhs
+++ b/doc/MastersThesis/Lhs/Caching.lhs
@@ -62,11 +62,11 @@ subRunCTFinal m t sl = do
 \end{code}
 }
 
-Chapter 5, \textit{Travelling across Domains}, leveraged a major concern with the proposed software: the solvers don't work in the domain of interest, continuous time. This chapter, \textit{Caching the Speed Pill}, addresses a second problem: the performance in \texttt{FACT}. At the end of it, the simulation will be orders of magnitude faster by using a common modern caching strategy to speed up computing processes: memoization.
+Chapter 5, \textit{Travelling across Domains}, leveraged a major concern with the proposed software: the solvers don't work in the domain of interest, continuous time. This Chapter, \textit{Caching the Speed Pill}, addresses a second problem: the performance in \texttt{FACT}. At the end of it, the simulation will be orders of magnitude faster by using a common modern caching strategy to speed up computing processes: memoization.
 
 \section{Performance}
 
-The simulations executed in \texttt{FACT} take too long to run. For instance, to execute the Lorenz's Attractor example using the second-order Runge-Kutta method with an unrealistic time step size for real simulations (time step of $1$ second), the simulator can take around \textbf{10 seconds} to compute 0 to 5 seconds of the physical system with a testbench using a \texttt{Ryzen 7 5700X} AMD processor and 128GB of RAM. Increasing this interval shows an exponential growth in execution time, as depicted by Table \ref{tab:execTimes} and by Figure \ref{fig:graph1} (values obtained after the interpolation tweak). Although the memory use is also problematic, it is hard to reason about those numbers due to Haskell's \textbf{garbage collector}~\footnote{Garbage Collector \href{https://wiki.haskell.org/GHC/Memory\_Management}{\textcolor{blue}{wiki page}}.}, a memory manager that deals with Haskell's \textbf{immutability}. Thus, the memory values serve just to solidify the notion that \texttt{FACT} is inneficient, showing an exponentinal growth in resource use, which makes it impractical to execute longer simulations and diminishes the usability of the proposed software.
+The simulations executed in \texttt{FACT} take too long to run. For instance, to execute the Lorenz's Attractor example using the second-order Runge-Kutta method with an unrealistic time step size for real simulations (time step of $1$ second), the simulator can take around \textit{10 seconds} to compute 0 to 5 seconds of the physical system with a testbench using a \texttt{Ryzen 7 5700X} AMD processor and 128GB of RAM. Increasing this interval shows an exponential growth in execution time, as depicted by Table \ref{tab:execTimes} and by Figure \ref{fig:graph1} (values obtained after the interpolation tweak). Although the memory use is also problematic, it is hard to reason about those numbers due to Haskell's \textit{garbage collector}~\footnote{Garbage Collector \href{https://wiki.haskell.org/GHC/Memory\_Management}{\textcolor{blue}{wiki page}}.}, a memory manager that deals with Haskell's \textit{immutability}. Thus, the memory values serve just to solidify the notion that \texttt{FACT} is inneficient, showing an exponential growth in resource use, which makes it impractical to execute longer simulations and diminishes the usability of the proposed software.
 
 \begin{table}[H]
 \centering
@@ -91,7 +91,7 @@ Total of Iterations  & Execution Time (milliseconds) & Consumed Memory (KB) \\ \
 
 \section{The Saving Strategy}
 
-Before explaining the solution, it is worth describing \textbf{why} and \textbf{where} this problem arises. First, we need to take a look back onto the solvers' functions, such as the \textit{integEuler} function, introduced in chapter 3, \textit{Effectful Integrals}:
+Before explaining the solution, it is worth describing \textit{why} and \textit{where} this problem arises. First, we need to take a look back onto the solvers' functions, such as the \textit{integEuler} function, introduced in Chapter 3, \textit{Effectful Integrals}:
 
 \begin{spec}
 integEuler :: CT Double
@@ -113,9 +113,9 @@ integEuler diff i y = do
       return v
 \end{spec}
 
-From chapter 3, we know that lines 10 to 13 serve the purpose of creating a new parametric record to execute a new solver step for the \textbf{previous} iteration, in order to calculate the current one. From chapter 4, this code section turned out to be where the implicit recursion came in, because the current iteration needs to calculate the previous one. Effectively, this means that for \textbf{all} iterations, \textbf{all} previous steps from each one needs to be calculated. The problem is now clear: unnecessary computations are being made for all iterations, because the same solvers steps are not being saved for future steps, although these values do \textbf{not} change. In other words, to calculate step 3 of the solver, steps 1 and 2 are the same to calculate step 4 as well, but these values are being lost during the simulation.
+From Chapter 3, we know that lines 10 to 13 serve the purpose of creating a new parametric record to execute a new solver step for the \textit{previous} iteration, in order to calculate the current one. From Chapter 4, this code section turned out to be where the implicit recursion came in, because the current iteration needs to calculate the previous one. Effectively, this means that for \textit{all} iterations, \textit{all} previous steps from each one needs to be calculated. The problem is now clear: unnecessary computations are being made for all iterations, because the same solvers steps are not being saved for future steps, although these values do \textit{not} change. In other words, to calculate step 3 of the solver, steps 1 and 2 are the same to calculate step 4 as well, but these values are being lost during the simulation.
 
-To estimate how this lack of optimization affects performance, we can calculate how many solver steps will be executed to simulate theLorenz's Attractor example used in chapter 4, \textit{Execution Walkthrough}. The Table \ref{tab:solverSteps} shows the total number of solver steps needed per iteration simulating the Lorenz example with the Euler method. In addition, the amount of steps also increase depending on which solver method is being used, given that in the higher order Runge-Kutta methods, multiple stages count as a new step as well.
+To estimate how this lack of optimization affects performance, we can calculate how many solver steps will be executed to simulate theLorenz's Attractor example used in Chapter 4, \textit{Execution Walkthrough}. Table \ref{tab:solverSteps} shows the total number of solver steps needed per iteration simulating the Lorenz example with the Euler method. In addition, the amount of steps also increase depending on which solver method is being used, given that in the higher order Runge-Kutta methods, multiple stages count as a new step as well.
 
 \begin{table}[H]
 \centering
@@ -129,16 +129,16 @@ Iteration & Total Solver Steps \\ \hline
 5         & 15           \\ \hline
 6         & 21           \\ \hline
 \end{tabular}
-\caption{\label{tab:solverSteps}Because the previous solver steps are not saved, the total number of steps \textbf{per iteration} starts to accumullate following the numerical sequence of \textbf{triangular numbers} when using the Euler method.}
+\caption{\label{tab:solverSteps}Because the previous solver steps are not saved, the total number of steps \textit{per iteration} starts to accumullate following the numerical sequence of \textit{triangular numbers} when using the Euler method.}
 \end{table}
 
-This is the cause of the imense hit in performance. However, it also clarifies the solution: if the previous solver steps are saved, the next iterations don't need to re-compute them in order to continue. In the computer domain, the act of saving previous steps that do not change is called \textbf{memoization} and it is one form to execute \textbf{caching}. This optimization technique stores the values in a register or memory region and, instead of the process starts calculating the result again, it consults this region to quickly obtain the answer.
+This is the cause of the imense hit in performance. However, it also clarifies the solution: if the previous solver steps are saved, the next iterations don't need to re-compute them in order to continue. In the computer domain, the act of saving previous steps that do not change is called \textit{memoization} and it is one form to execute \textit{caching}. This optimization technique stores the values in a register or memory region and, instead of the process starts calculating the result again, it consults this region to quickly obtain the answer.
 
 \section{Tweak II: Memoization}
 
-The first tweak, \textit{Memoization}, alters the \texttt{Integrator} type. The integrator will now have a pointer to the memory region that stores the previous computed values, meaning that before executing a new computation, it will consult this region first. Because the process is executed in a \textbf{sequential} manner, it is guaranteed that the previous result will be used. Thus, the accumulation of the solver steps will be addressed, and the amount of steps will be equal to the amount of iterations times how many stages the solver method uses.
+The first tweak, \textit{Memoization}, alters the \texttt{Integrator} type. The integrator will now have a pointer to the memory region that stores the previous computed values, meaning that before executing a new computation, it will consult this region first. Because the process is executed in a \textit{sequential} manner, it is guaranteed that the previous result will be used. Thus, the accumulation of the solver steps will be addressed, and the amount of steps will be equal to the amount of iterations times how many stages the solver method uses.
 
-The \textit{memo} function creates this memory region for storing values, as well as providing read access to it. This is the only function in \texttt{FACT} that uses a \textit{constraint}, i.e., it restricts the parametric types to the ones that have implemented the requirement. In our case, this function requires that the internal type \texttt{CT} dependency has implemented the \texttt{UMemo} typeclass. Because this typeclass is too complicated to be in the scope of this project, we will settle with the following explanation: it is required that the parametric values are capable of being contained inside an \textbf{mutable} array, which is the case for our \texttt{Double} values. As dependencies, the \textit{memo} function receives the computation, as well as the interpolation function that is assumed to be used, in order to attenuate the domain problem described in the previous chapter. This means that at the end, the final result will be piped to the interpolation function. 
+The \textit{memo} function creates this memory region for storing values, as well as providing read access to it. This is the only function in \texttt{FACT} that uses a \textit{constraint}, i.e., it restricts the parametric types to the ones that have implemented the requirement. In our case, this function requires that the internal type \texttt{CT} dependency has implemented the \texttt{UMemo} typeclass. Because this typeclass is too complicated to be in the scope of this project, we will settle with the following explanation: it is required that the parametric values are capable of being contained inside a \textit{mutable} array, which is the case for our \texttt{Double} values. As dependencies, the \textit{memo} function receives the computation as well as the interpolation function that is assumed to be used, in order to attenuate the domain problem described in the previous Chapter. This means that at the end, the final result will be piped to the interpolation function. 
 
 \begin{code}
 memo :: UMemo e => (CT e -> CT e) -> CT e -> CT (CT e)
@@ -182,13 +182,13 @@ memo interpolate m = do
 
 The function starts by getting how many iterations will occur in the simulation, as well as how many stages the chosen method uses (lines 5 to 7). This is used to pre-allocate the minimum amount of memory required for the execution (line 8). This mutable array is two-dimensional and can be viewed as a table in which the number of iterations and stages determine the number of rows and columns. Pointers to iterate accross the table are declared as \textit{nref} and \textit{stref} (lines 9 and 10), to read iteration and stage values respectively. The code block from line 11 to line 36 delimit a procedure or computation that will only be used when needed, and it is being called at the end of the \textit{memo} function (line 37).
 
-The next step is to follow the exection of this internal function. From line 13 to line 17, auxiliar "variables", i.e., labels to read information, are created to facilitate manipulation of the solver (\texttt{sl}), interval (\texttt{iv}), current iteration (\texttt{n}), current stage (\texttt{st}) and the final stage used in a solver step (\texttt{stu}). The definition of \textit{loop}, which starts at line 18 and closes at line 33, uses all the previously created labels. The conditional block (line 19 to 33) will store in the pre-allocated memory region the computed values and, because they are stored in a \textbf{sequential} way, the stop condition of the loop is one of the following: the iteration counter of the loop (\texttt{n'}) surpassed the current iteration \textbf{or} the iteration counter matches the current iteration \textbf{and} the stage counter (\texttt{st'}) reached the ceiling of stages of used solver method (line 19). When the loop stops, it \textbf{reads} from the allocated array the value of interest (line 21), given that it is guaranteed that is already in memory. If this condition is not true, it means that further iterations in the loop need to occur in one of the two axis, iteration or stage.
+The next step is to follow the exection of this internal function. From line 13 to line 17, auxiliar "variables", i.e., labels to read information, are created to facilitate manipulation of the solver (\texttt{sl}), interval (\texttt{iv}), current iteration (\texttt{n}), current stage (\texttt{st}) and the final stage used in a solver step (\texttt{stu}). The definition of \textit{loop}, which starts at line 18 and closes at line 33, uses all the previously created labels. The conditional block (line 19 to 33) will store in the pre-allocated memory region the computed values and, because they are stored in a \textit{sequential} way, the stop condition of the loop is one of the following: the iteration counter of the loop (\texttt{n'}) surpassed the current iteration \textit{or} the iteration counter matches the current iteration \textit{and} the stage counter (\texttt{st'}) reached the ceiling of stages of used solver method (line 19). When the loop stops, it \textit{reads} from the allocated array the value of interest (line 21), given that it is guaranteed that it is already in memory. If this condition is not true, it means that further iterations in the loop need to occur in one of the two axis, iteration or stage.
 
 The first step towards that goal is to save the value of the current iteration and stage into memory. The continuous machine \texttt{m}, received as a dependency in line 3, is used to compute a new result with the current counters for iteration and stage (lines 23 to 26). Then, this new value is written into the array (line 27). The condition in line 28 checks if the current stage already achieved its maximum possible value. In that case, the counters for stage and iteration counters will be reset to the first stage (line 29) of the next iteration (line 30) respectively, and the loop should continue (line 31). Otherwise, we need to advance to the next stage within the same iteration and an updated stage (line 32). The loop should continue with the same iteration counter but with the stage counter incremented (lines 32 and 33).
 
 Lines 34 to 36 are the trigger to the beginning of the loop, with \textit{nref} and \textit{stref} being read. These values set the initial values for the counters used in the \textit{loop} function, and both of their values start at zero (lines 10 and 11).  All computations related to the \textit{loop} function will only be called when the \textit{r} function is called. Further, all of these impure computations (lines 12 to 36) compose the definition of \textit{r} (line 12), which is being returned in line 37 combined with the interpolation function \textit{tr} and being wrapped with an extra \texttt{CT} shell via the \textit{pure} function (provided by the \texttt{Applicative} typeclass).
 
-With this function on-hand, it remains to couple it to the \texttt{Integrator} type, meaning that \textbf{all} integrator functions need to be aware of this new caching strategy. First and foremost, a pointer to this memory region needs to be added to the integrator type itself:
+With this function on-hand, it remains to couple it to the \texttt{Integrator} type, meaning that \textit{all} integrator functions need to be aware of this new caching strategy. First and foremost, a pointer to this memory region needs to be added to the integrator type itself:
 
 \newpage
 
@@ -199,9 +199,9 @@ data Integrator = Integrator { initial :: CT Double,
                              }
 \end{code}
 
-Next, two other functions need to be adapted: \textit{createInteg} and \textit{readInteg}. In the former function, the new pointer will be used, and it points to the region where the mutable array will be allocated. In the latter, instead of reading from the computation itself, the read-only pointer will be looking at the \textbf{cached} version. These differences will be illustrated by using the same integrator and state variables used in the Lorenz's Attractor example, detailed in chapter 4, \textit{Execution Walkthrough}.
+Next, two other functions need to be adapted: \textit{createInteg} and \textit{readInteg}. In the former function, the new pointer will be used, and it points to the region where the mutable array will be allocated. In the latter, instead of reading from the computation itself, the read-only pointer will be looking at the \textit{cached} version. These differences will be illustrated by using the same integrator and state variables used in the Lorenz's Attractor example, detailed in Chapter 4, \textit{Execution Walkthrough}.
 
-The main difference in the updated version of the \textit{createInteg} function is the inclusion of the new pointer that reads the cached memory (lines 4 to 7). The pointer \texttt{computation}, which will be changed by \textit{updateInteg} in a model to the differential equation, is being read in lines 8 to 11 and piped with interpolation and memoization in line 12. This approach maintains the interpolation, justified in the previous chapter, and adds the aforementioned caching strategy. Finally, the final result is written in the memory region pointed by the caching pointer (line 13).
+The main difference in the updated version of the \textit{createInteg} function is the inclusion of the new pointer that reads the cached memory (lines 4 to 7). The pointer \texttt{computation}, which will be changed by \textit{updateInteg} in a model to the differential equation, is being read in lines 8 to 11 and piped with interpolation and memoization in line 12. This approach maintains the interpolation, justified in the previous Chapter, and adds the aforementioned caching strategy. Finally, the final result is written in the memory region pointed by the caching pointer (line 13).
 
 Figure \ref{fig:createInteg} shows that the updated version of the \textit{createInteg} function is similar to the previous implementation. The new field, \texttt{cached}, is a pointer that refers to \texttt{readComp} --- the result of memoization (\texttt{memo}), interpolation (\texttt{interpolate}) and the value obtained by the region pointed by the \texttt{computation} pointer. Given a parametric record \texttt{ps}, \texttt{readComp} gives this record to the value stored in the region pointed by \texttt{computation}. This result is then interpolated via the \texttt{interpolate} block and it is used as a dependency for the \texttt{memo} block.
 
@@ -227,7 +227,7 @@ createInteg i = do
 \begin{center}
   \includegraphics[width=0.95\linewidth]{MastersThesis/img/NewInteg}
 \end{center}
-\caption{The new \textit{createInteg} function relies on interpolation composed with memoization. Also, this combination \textbf{produces} results from the computation located in a different memory region, the one pointed by the \texttt{computation} pointer in the integrator.}
+\caption{The new \textit{createInteg} function relies on interpolation composed with memoization. Also, this combination \textit{produces} results from the computation located in a different memory region, the one pointed by the \texttt{computation} pointer in the integrator.}
 \label{fig:createInteg}
 \end{figure}
 
@@ -241,7 +241,7 @@ readInteg = join . liftIO . readIORef . cache
 \begin{center}
   \includegraphics[width=0.95\linewidth]{MastersThesis/img/ReadInteg}
 \end{center}
-\caption{The function \textbf{reads} information from the caching pointer, rather than the pointer where the solvers compute the results.}
+\caption{The function \textit{reads} information from the caching pointer, rather than the pointer where the solvers compute the results.}
 \label{fig:readInteg}
 \end{figure}
 
@@ -276,9 +276,9 @@ The solver functions, \textit{integEuler}, \textit{integRK2} and \textit{integRK
 
 \section{A change in Perspective}
 
-Before the implementation of the described caching strategy, \textbf{all} the solver methods rely on implicit recursion to get the previous iteration value. Thus, performance was degraded due to this potentially long stack call. After caching, this mechanism is not only faster, but it \textbf{completely} changes how the solvers will get these past values.
+Before the implementation of the described caching strategy, \textit{all} the solver methods rely on implicit recursion to get the previous iteration value. Thus, performance was degraded due to this potentially long stack call. After caching, this mechanism is not only faster, but it \textit{completely} changes how the solvers will get these past values.
 
-For instance, when using the function \textit{runCTFinal} as the driver, the simulation will start by the last iteration. Without caching, the solver would go from the current iteration to the previous ones, until it reaches the base case with the initial condition and starts backtracking the recursive calls to compute the result of the final iteration. On the other hand, with the caching strategy, the \textit{memo} function goes in the \textbf{opposite} direction: it starts from the beginning, with the counters at zero, and then incrementally proceeds until it reaches the desired iteration.
+For instance, when using the function \textit{runCTFinal} as the driver, the simulation will start by the last iteration. Without caching, the solver would go from the current iteration to the previous ones, until it reaches the base case with the initial condition and starts backtracking the recursive calls to compute the result of the final iteration. On the other hand, with the caching strategy, the \textit{memo} function goes in the \textit{opposite} direction: it starts from the beginning, with the counters at zero, and then incrementally proceeds until it reaches the desired iteration.
 
 Figure \ref{fig:memoDirection} depicts this stark difference in approach when using memoization in \texttt{FACT}. Instead of iterating through all iterations two times, one backtracking until the base case and another one to accumulate all computed values, the new version starts from the base case, i.e., at iteration 0, and stops when achieves the desired iteration, saving all the values along the way.
 
@@ -286,7 +286,7 @@ Figure \ref{fig:memoDirection} depicts this stark difference in approach when us
 
 \section{Tweak III: Model and Driver}
 
-The memoization added to \texttt{FACT} needs a second tweak, related to the executable models established in chapter 4. The code bellow is the same example model used in that chapter:
+The memoization added to \texttt{FACT} needs a second tweak, related to the executable models established in Chapter 4. The following code is the same example model used in that Chapter:
 
 \begin{spec}
 exampleModel :: Model Vector
@@ -300,7 +300,7 @@ exampleModel =
      sequence [x, y]
 \end{spec}
 
-The caching strategy assumes that the created mutable array will be available for the entire simulation. However, the proposed models will \textbf{always} discard the table created by the \textit{createInteg} function due to the garbage collector~\footnote{Garbage Collector \href{https://wiki.haskell.org/GHC/Memory\_Management}{\textcolor{blue}{wiki page}}.}, after the \textit{sequence} function. Even worse, the table will be created again each time the model is being called and a parametric record is being provided, which happens when using the driver. Thus, the proposed solution to address this problem is to update the \texttt{Model} alias to a \textbf{function} of the model. This can be achieved by \textbf{wrapping} the state vector with a the \texttt{CT} type, i.e., wrapping the model using the function \textit{pure} or \textit{return}. In this manner, the computation will be "placed" as a side effect of the \texttt{IO} monad and Haskell's memory management system will not remove the table used for caching, in the first computation. So, the following code is the new type alias, alongside the previous example model using the \textit{return} function:
+The caching strategy assumes that the created mutable array will be available for the entire simulation. However, the proposed models will \textit{always} discard the table created by the \textit{createInteg} function due to the garbage collector~\footnote{Garbage Collector \href{https://wiki.haskell.org/GHC/Memory\_Management}{\textcolor{blue}{wiki page}}.}, after the \textit{sequence} function. Even worse, the table will be created again each time the model is being called and a parametric record is being provided, which happens when using the driver. Thus, the proposed solution to address this problem is to update the \texttt{Model} alias to a \textit{function} of the model. This can be achieved by \textit{wrapping} the state vector with a the \texttt{CT} type, i.e., wrapping the model using the function \textit{pure} or \textit{return}. In this manner, the computation will be "placed" as a side effect of the \texttt{IO} monad and Haskell's memory management system will not remove the table used for caching in the first computation. So, the following code is the new type alias, alongside the previous example model using the \textit{return} function:
 
 \begin{spec}
 type Model a = CT (CT a)
@@ -316,7 +316,7 @@ exampleModel =
      return $ sequence [x, y]
 \end{spec}
 
-Due to the new type signature, this change implies changing the driver, i.e., modify the function \textit{runCT} (the changes are analogus to the \textit{runCTFinal} function variant). Further, a new auxiliary function was created, \textit{subRunCT}, to separate the environment into two functions. The \textit{runCT} will execute the mapping with the function \textit{parameterise} and the auxiliary function will address the need for interpolation.
+Due to the new type signature, this change implies changing the driver, i.e., modifying the function \textit{runCT} (the changes are analogus to the \textit{runCTFinal} function variant). Further, a new auxiliary function was created, \textit{subRunCT}, to separate the environment into two functions. The \textit{runCT} will execute the mapping with the function \textit{parameterize} and the auxiliary function will address the need for interpolation.
 
 \begin{code}
 runCT :: Model a -> Double -> Solver -> IO [a]
@@ -354,7 +354,7 @@ The main change is the division of the driver into two: one dedicated to "initia
 
 \section{Results with Caching}
 
-The following table (Table \ref{tab:betterResults}) shows the same Lorenz's Attractor example used in the first section, but with the preceding tweaks in the \texttt{Integrator} type and the integrator functions. It is worth noting that there is an overhead due to the memoization strategy when running fewer iterations (such as 1 in the table), in which
+The following table (Table \ref{tab:betterResults}) shows the same Lorenz's Attractor example used in the first Section, but with the preceding tweaks in the \texttt{Integrator} type and the integrator functions. It is worth noting that there is an overhead due to the memoization strategy when running fewer iterations (such as 1 in the table), in which
 most time is spent preparing the caching setup --- the in-memory data structure, and etc.These modifications allows better and more complicated models to be simulated. For instance, the Lorenz example with a variety of total number of iterations can be checked in Table \ref{tab:masterResults} and in Figure \ref{fig:graph2}.
 
 \begin{table}[H]
@@ -395,6 +395,6 @@ Total of Iterations & Execution Time (milliseconds) & Consumed Memory (MB) \\ \h
 
 \figuraBib{Graph2}{By using a logarithmic scale, we can see that the final implementation is performant with more than 100 million iterations in the simulation}{}{fig:graph2}{width=.97\textwidth}%
 
-The project is currently capable of executing interpolation as well as applying memoization to speed up results. These two drawback solutions, detailed in chapter 5 and 6, adds practicality to \texttt{FACT} as well as makes it more competitive. But we can, however, go even further and adds more familiarity to the DSL. The next chapter, \textit{Fixing Recursion}, will
+The project is currently capable of executing interpolation as well as applying memoization to speed up results. These two drawback solutions, detailed in Chapter 5 and 6, adds practicality to \texttt{FACT} as well as makes it more competitive. But we can, however, go even further and adds more familiarity to the DSL. The next Chapter, \textit{Fixing Recursion}, will
 address this concern.
 
diff --git a/doc/MastersThesis/Lhs/Conclusion.lhs b/doc/MastersThesis/Lhs/Conclusion.lhs
index 1146cd1..9e70d10 100644
--- a/doc/MastersThesis/Lhs/Conclusion.lhs
+++ b/doc/MastersThesis/Lhs/Conclusion.lhs
@@ -1,33 +1,43 @@
-Chapters 2 and 3 explained the relationship between software, FF-GPAC and the mathematical world of differential equations. As a follow-up, Chapter 4 raised intuition and practical understanding of \texttt{FACT} via a detailed walkthrough of an example. Chapters 5, 6, and 7 identified some problems with the current implementation, such as lack of performance, the discrete time issue, DSL's familiarity, and addressed both problems via caching and interpolation. This chapter, \textit{Conclusion}, draws limitations, future improvements that can bring \texttt{FACT} to a higher level of abstraction and some final conclusions about the project.
+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
+the implementation of typeclasses to add functionality for the \texttt{CT} type, such as binary operations and
+numerical representation. Further, it also introduced the \texttt{Integrator}, a CRUD-like interface
+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
+experienced with the mathematical descriptions of their systems of interest. This notation enhancement is the defining feature between FACT and FFACT.
 
-\section{Limitations}
+\section{Final Thoughts}
 
-One of the main concerns is the \textbf{correctness} of \texttt{FACT} between its specification and its final implementation, i.e., refinement. Shannon's GPAC concept acted as the specification of the project, whilst the proposed software attempted to implement it. The criteria used to verify that the software fulfilled its goal were by using it for simulation and via code inspection, both of which are based on human analysis. This connection, however, was \textbf{not} formally verified. Thus, \texttt{FACT} can be a threat to validity if a future formal verification comes up and checks that the parallel between those two can't be guaranteed.
+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}.
 
-Further, there is also an issue to regards to \textbf{validation}. In order to know that the mathematical description of the problem is being correctly mapped onto a model representation some formal work needs to be done. This was not explored, and it was considered out of the scope of the thesis. However, such aspect dictates if the specification for further implementation is actually correct and describes its mathematical counterpart. So, checking for validation is just as important as verifying refinement.
+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.
 
-This lack of formalism extends to the typeclasses as well. The programming language of choice, Haskell, does \textbf{not} provide any proofs that the created types actually follow the typeclasses' properties, even if the requested functions type check. This burden is on the developer to manually write down such proofs, a non-explored aspect of this work.
+\section{Future Work}
 
-As explained in chapters 1 and 2, there are some extensions that increase the capabilities of Shannon's original GPAC model. One of these extensions, FF-GPAC, was the one chosen to be modeled via software. However, there are other extensions that not only expand the types of functions that can be modeled, e.g., hypertranscendental functions, but also explore new properties, such as Turing universitality~\cite{Graca2004, Graca2016}. The proposed software didn't touch on those enhancements and restricted the set of functions to only algebraic functions.
+The following subsections describe the three main areas for future improvements in \texttt{FFACT}: formalism, possible extensions, and code refactoring. 
 
-Finally, there is the language itself, Haskell. Although Haskell's type system allowed a great mapping between the numerical methods and its nuances to created types, its simplicity started to fall apart when impurity came into picture. The side effect overhead makes \texttt{FACT} hard to reason about in terms of maintenance, especially for newcomers that intent to expand the software's functionalities.
+\subsection{Formalism}
 
-\section{Future Improvements}
+One of the main concerns is the \textit{correctness} of \texttt{FACT} between its specification and its final implementation, i.e., refinement. Shannon's GPAC concept acted as the specification of the project, whilst the proposed software attempted to implement it. The criteria used to verify that the software fulfilled its goal were by using it for simulation and via code inspection, both of which are based on human analysis. This connection, however, was \textit{not} formally verified --- no model checking tools were used for its validation. In order to know that the mathematical description of the problem is being correctly mapped onto a model representation some formal work needs to be done. This was not explored, and it was considered out of the scope for this work.
 
-There are solutions to mitigate the problems presented in the previous section. First, to address refinement, the simulation could be assessed by continuous domain specialists. Also, proof-assistant tools, such as Rocq and PVS, could be used to re-write \texttt{FACT} with a proper formal basis, hence establishing a solid map between the mathematical description, specification and implementation. Further, the same tools can leverage the correctness of the typeclasses' implementation, via demonstrating that it assures the axioms and properties demanded by each typeclass. More recent extensions of GPAC should also be explored to simulate an even broader set of functions present in the continuous time domain.
+This lack of formalism extends to the typeclasses as well. The programming language of choice, Haskell, does \textit{not} provide any proofs that the created types actually follow the typeclasses' properties --- something that can be achieved with \textit{dependently typed} languages and/or tools such as Rocq, PVS, Agda, Idris and Lean. In Haskell, this burden is on the developer to manually write down such proofs, a non-explored aspect of this work. Hence, this work can be better understood as a \textit{proof of concept} for FFACT, and one potential improvement would be to port it to more powerful and specialized programming languages, such as the ones mentioned earlier. Because FP is highly encouraged in those languages, such port would not be a major roadblock. Thus, these tools would assure a solid mappping between the mathematical the description of the problem, GPAC's specification and FFACT's implementation, including the
+use of the chosen typeclasses.
 
-In regards to numerical methods, one of the immediate improvements would be to use \textbf{adaptive} size for the solver time step that \textbf{change dynamically} in run time. This strategy controls the errors accumulated when using the derivative by adapting the size of the time step. Hence, it starts backtracking previous steps with smaller time steps until some error threshold is satisfied, thus providing finer and granular control to the numerical methods, coping with approximation errors due to larger time steps.
+\subsection{Extensions}
 
-In terms of the used technology, some ideas come to mind related to abstracting out duplicated \textbf{patterns} across the code base. The proposed software used a mix of high level abstractions, such as algebraic types and typeclasses, with some low level abstractions, e.g., explicit memory manipulation. One potential improvement would be to explore an entirely \textbf{pure} based approach, meaning that all the necessary side effects would be handled \textbf{only} by high-level concepts internally, hence decreasing complexity of the software. For instance, the memory allocated via the \texttt{memo} function acts as a \textbf{state} of the numerical solver. Other Haskell abstractions, such as the \texttt{ST} monad~\footnote{\texttt{ST} Monad \href{https://wiki.haskell.org/State\_Monad}{\textcolor{blue}{wiki page}}.}, could be considered for future improvements towards purity. Going even further, given that \texttt{FACT}
-already uses \texttt{ReaderT}, a combination of monads could be used to better unify all different behavior -- in Haskell, an option would be to use \textit{monad transformers}.
-For instance, if the reader and state monads, something like the \texttt{RWS} monad~\footnote{\texttt{RWS} Monad \href{https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-RWS-Lazy.html}{\textcolor{blue}{hackage documentation}}.}, a monad that combines the monads \texttt{Reader}, \texttt{Writer} and \texttt{ST}, may be the final goal for a completely pure but effective solution.
+As explained in Chapters 1 and 2, there are some extensions that increase the capabilities of Shannon's original GPAC model. One of these extensions, FF-GPAC, was the one chosen to be modeled via software. However, there are other extensions that not only expand the types of functions that can be modeled, e.g., hypertranscendental functions, but also explore new properties, such as Turing universality~\cite{Graca2004, Graca2016}. The proposed software didn't touch on those enhancements and restricted the set of functions to only algebraic functions. More recent extensions of GPAC should also be explored to simulate an even broader set of functions present in the continuous time domain.
 
-Also, there's GPAC and its mapping to Haskell features. As explained previously, some basic units of GPAC are being modeled by the \texttt{Num} typeclass, present in Haskell's \texttt{Prelude} module. By using more specific and customized numerical typeclasses~\footnote{Examples of \href{https://guide.aelve.com/haskell/alternative-preludes-zr69k1hc}{\textcolor{blue}{alternative preludes}}.}, it might be possible to better express these basic units and take advantage of better performance and convenience that these alternatives provide.
+In regards to numerical methods, one of the immediate improvements would be to use \textit{adaptive} size for the solver time step that \textit{change dynamically} in run time. This strategy controls the errors accumulated when using the derivative by adapting the size of the time step. Hence, it starts backtracking previous steps with smaller time steps until some error threshold is satisfied, thus providing finer and granular control to the numerical methods, coping with approximation errors due to larger time steps.
 
-\newpage
+\subsection{Refactoring}
 
-\section{Final Thoughts}
+In terms of the used technology, some ideas come to mind related to abstracting out duplicated \textit{patterns} across the code base. The proposed software used a mix of high level abstractions, such as algebraic types and typeclasses, with some low level abstractions, e.g., explicit memory manipulation. One potential improvement would be to explore an entirely \textit{pure} based approach, meaning that all the necessary side effects would be handled \textit{only} by high-level concepts internally, hence decreasing complexity of the software. For instance, the memory allocated via the \texttt{memo} function acts as a \textit{state} of the numerical solver. Other Haskell abstractions, such as the \texttt{ST} monad~\footnote{\texttt{ST} Monad \href{https://wiki.haskell.org/State\_Monad}{\textcolor{blue}{wiki page}}.}, could be considered for future improvements towards purity. Going even further, given that \texttt{FACT}
+already uses \texttt{ReaderT}, a combination of monads could be used to better unify all different behavior -- in Haskell, an option would be to use \textit{monad transformers}.
+For instance, if the reader and state monads, something like the \texttt{RWS} monad~\footnote{\texttt{RWS} Monad \href{https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-RWS-Lazy.html}{\textcolor{blue}{hackage documentation}}.}, a monad that combines the monads \texttt{Reader}, \texttt{Writer} and \texttt{ST}, may be the final goal for a completely pure but effective solution.
 
-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}.
+Also, there's GPAC and its mapping to Haskell features. As explained previously, some basic units of GPAC are being modeled by the \texttt{Num} typeclass, present in Haskell's \texttt{Prelude} module. By using more specific and customized numerical typeclasses~\footnote{Examples of \href{https://guide.aelve.com/haskell/alternative-preludes-zr69k1hc}{\textcolor{blue}{alternative preludes}}.}, it might be possible to better express these basic units and take advantage of better performance and convenience that these alternatives provide.
 
-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.
diff --git a/doc/MastersThesis/Lhs/Design.lhs b/doc/MastersThesis/Lhs/Design.lhs
index b3df5eb..58ec516 100644
--- a/doc/MastersThesis/Lhs/Design.lhs
+++ b/doc/MastersThesis/Lhs/Design.lhs
@@ -6,14 +6,14 @@ import Control.Monad.Trans.Reader ( ReaderT )
 \end{code}
 }
 
-In the previous chapter, the importance of making a bridge between two different sets of abstractions --- computers and the physical domain --- was established. This chapter will explain the core philosophy behind the implementation of this link, starting with an introduction to GPAC, followed by the type and typeclass systems used in Haskell, as well as understanding how to model the main entities of the problem. At the end, the presented modeling strategy will justify the data types used in the solution, paving the way for the next chapter \textit{Effectful Integrals}.
+In the previous Chapter, the importance of making a bridge between two different sets of abstractions --- computers and the physical domain --- was established. This Chapter will explain the core philosophy behind the implementation of this link, starting with an introduction to GPAC, followed by the type and typeclass systems used in Haskell, as well as understanding how to model the main entities of the problem. At the end, the presented modeling strategy will justify the data types used in the solution, paving the way for the next Chapter \textit{Effectful Integrals}.
 
 \section{Shannon's Foundation: GPAC}
 \label{sec:gpac}
 
 The General Purpose Computer or GPAC is a model for the Differential Analyzer --- a mechanical machine controlled by a human operator~\cite{Graca2016}. This machine is composed by a set of shafts interconnected in such a manner that a given differential equation is expressed by a shaft and other mechanical units transmit their values across the entire machine~\cite{Shannon, Graca2004}. For instance, shafts that represent independent variables directly interact with shafts that depicts dependent variables. The machine is primarily composed by four types of units: gear boxes, adders, integrators and input tables~\cite{Shannon}. These units provide useful operations to the machine, such as multiplication, addition, integration and saving the computed values. The main goal of this machine is to solve ordinary differential equations via numerical solutions.
 
-In order to add a formal basis to the machine, Shannon built the GPAC model, a mathematical model sustained by proofs and axioms~\cite{Shannon}. The end result was a set of rules for which types of equations can be modeled as well as which units are the minimum necessary for modeling them and how they can be combined. All algebraic functions (e.g. quotients of polynomials and irrational algebraic functions) and algebraic-trascendental functions (e.g. exponentials, logarithms, trigonometric, Bessel, elliptic and probability functions) can be modeled using a GPAC circuit~\cite{Edil2018, Shannon}. Moreover, the four preceding mechanical units were renamed and together created the minimum set of \textbf{circuits} for a given GPAC~\cite{Edil2018}. Figure \ref{fig:gpacBasic} portrays these basic units, followed by descriptions of their behaviour, inputs and outputs.
+In order to add a formal basis to the machine, Shannon built the GPAC model, a mathematical model sustained by proofs and axioms~\cite{Shannon}. The end result was a set of rules for which types of equations can be modeled as well as which units are the minimum necessary for modeling them and how they can be combined. All algebraic functions (e.g. quotients of polynomials and irrational algebraic functions) and algebraic-trascendental functions (e.g. exponentials, logarithms, trigonometric, Bessel, elliptic and probability functions) can be modeled using a GPAC circuit~\cite{Edil2018, Shannon}. Moreover, the four preceding mechanical units were renamed and together created the minimum set of \textit{circuits} for a given GPAC~\cite{Edil2018}. Figure \ref{fig:gpacBasic} portrays these basic units, followed by descriptions of their behaviour, inputs and outputs.
 
 \figuraBib{GPACBasicUnits}{The combination of these four basic units compose any GPAC circuit (taken from~\cite{Edil2018} with permission)}{}{fig:gpacBasic}{width=.95\textwidth}%
 
@@ -24,7 +24,7 @@ In order to add a formal basis to the machine, Shannon built the GPAC model, a m
   \item Integrator: Given two inputs --- $u(t)$ and $v(t)$ --- and an initial condition $w_0$ at time $t_0$, the unit generates the output $w(t) = w_0 + \int_{t_0}^{t} u(t) \,dv(t)$, where $u$ is the \textit{integrand} and $v$ is the \textit{variable of integration}.
 \end{itemize}
 
-Composition rules that restrict how these units can be hooked to one another. Shannon established that a valid GPAC is the one in which two inputs and two outputs are not interconnected and the inputs are only driven by either the independent variable $t$ (usually \textit{time}) or by a single unit output~\cite{Edil2018, Graca2003, Shannon}. Daniel's GPAC extension, FF-GPAC~\cite{Graca2003}, added new constraints related to no-feedback GPAC configurations while still using the same four basic units. These structures, so-called \textit{polynomial circuits}~\cite{Edil2018, Graca2004}, are being displayed in Figure \ref{fig:gpacComposition} and they are made by only using constant function units, adders and multipliers. Also, such circuits are \textit{combinational}, meaning that they compute values in a \textit{point-wise} manner between the given inputs. Thus, FF-GPAC's composition rules are the following:
+Composition rules that restrict how these units can be connected to one another. Shannon established that a valid GPAC is the one in which two inputs and two outputs are not interconnected and the inputs are only driven by either the independent variable $t$ (usually \textit{time}) or by a single unit output~\cite{Edil2018, Graca2003, Shannon}. Daniel's GPAC extension, FF-GPAC~\cite{Graca2003}, added new constraints related to no-feedback GPAC configurations while still using the same four basic units. These structures, so-called \textit{polynomial circuits}~\cite{Edil2018, Graca2004}, are being displayed in Figure \ref{fig:gpacComposition} and they are made by only using constant function units, adders and multipliers. Also, such circuits are \textit{combinational}, meaning that they compute values in a \textit{point-wise} manner between the given inputs. Thus, FF-GPAC's composition rules are the following:
 
 \figuraBib{GPACComposition}{Polynomial circuits resembles combinational circuits, in which the circuit respond instantly to changes on its inputs (taken from~\cite{Edil2018} with permission)}{}{fig:gpacComposition}{width=.55\textwidth}%
  
@@ -35,12 +35,12 @@ Composition rules that restrict how these units can be hooked to one another. Sh
   \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 epurespecification, 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.
+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}
 
-Types in programming languages represent the format of information. Figure \ref{fig:simpleTypes} illustrates types with an imaginary representation of their shape and Figure \ref{fig:functions} shows how types can be used to restrain which data can be plumbered into and from a function. In the latter image, function \textit{lessThan10} has the type signature \texttt{Int -> Bool}, meaning that it accepts \texttt{Int} data as input and produces \texttt{Bool} data as the output. These types are used to make constratins and add a safety layer in compile time, given that using data with different types as input, e.g, \texttt{Char} or \texttt{Double}, is regarded as a \textbf{type error}.
+Types in programming languages represent the format of information. Figure \ref{fig:simpleTypes} illustrates types with an imaginary representation of their shape and Figure \ref{fig:functions} shows how types can be used to restrain which data can be plumbered into and from a function. In the latter image, function \textit{lessThan10} has the type signature \texttt{Int -> Bool}, meaning that it accepts \texttt{Int} data as input and produces \texttt{Bool} data as the output. These types are used to make constratins and add a safety layer in compile time, given that using data with different types as input, e.g, \texttt{Char} or \texttt{Double}, is regarded as a \textit{type error}.
 
 \begin{figure}[ht!]
 \centering
@@ -59,9 +59,9 @@ Types in programming languages represent the format of information. Figure \ref{
 \end{minipage}
 \end{figure}
 
-Primitive types, e.g., \texttt{Int}, \texttt{Double} and \texttt{Char}, can be \textbf{composed} to create more powerful data types, capable of modeling complicated data structures. In this context, composition means binding or gluing existent types together to create more sophisticated abstractions, such as recursive structures and records of information. Two \textbf{algebraic data types} are the type composition mechanism provided by Haskell to bind existent types together.
+Primitive types, e.g., \texttt{Int}, \texttt{Double} and \texttt{Char}, can be \textit{composed} to create more powerful data types, capable of modeling complicated data structures. In this context, composition means binding or gluing existent types together to create more sophisticated abstractions, such as recursive structures and records of information. Two \textit{algebraic data types} are the type composition mechanism provided by Haskell to bind existent types together.
 
-The sum type, also known as tagged union in type theory, is an algebraic data type that introduces \textbf{choice} across multiple options using a single label. For instance, a type named \texttt{Parity} can represent the parity of a natural number. It has two options or representatives: \texttt{Even} \textbf{or} \texttt{Odd}, where these are mutually exclusive. When using this type either of them will be of type \texttt{Parity}. A given sum type can have any number of representatives, but only one of them can be used at a given moment. Figure \ref{fig:sumType} depicts examples of sum types with their syntax in the language, in which a given entry of the type can only assume one of the available possibilities. Another use case depicted in the image is the type \texttt{DigitalStates}, which describes the possible states in digital circuits as one of three options: \texttt{High}, \texttt{Low} and \texttt{Z}.
+The sum type, also known as tagged union in type theory, is an algebraic data type that introduces \textit{choice} across multiple options using a single label. For instance, a type named \texttt{Parity} can represent the parity of a natural number. It has two options or representatives: \texttt{Even} \textit{or} \texttt{Odd}, where these are mutually exclusive. When using this type either of them will be of type \texttt{Parity}. A given sum type can have any number of representatives, but only one of them can be used at a given moment. Figure \ref{fig:sumType} depicts examples of sum types with their syntax in the language, in which a given entry of the type can only assume one of the available possibilities. Another use case depicted in the image is the type \texttt{DigitalStates}, which describes the possible states in digital circuits as one of three options: \texttt{High}, \texttt{Low} and \texttt{Z}.
 
 \begin{figure}[ht!]
 \centering
@@ -81,7 +81,7 @@ The sum type, also known as tagged union in type theory, is an algebraic data ty
 \label{fig:sumType}
 \end{figure}
 
-The second type composition mechanism available is the product type, which \textbf{combines} using a type constructor. While the sum type adds choice in the language, this data type requires multiple types to assemble a new one in a mutually inclusive manner. For example, a digital clock composed by two numbers, hours and minutes, can be portrayed by the type \texttt{ClockTime}, which is a combination of two separate numbers combined by the wrapper \texttt{Time}. In order to have any possible time, it is necessary to provide \textbf{both} parts. Effectively, the product type executes a cartesian product with its parts. Figure \ref{fig:productType} illustrates the syntax used in Haskell to create product types as well as another example of combined data, the type \texttt{SpacePosition}. It represents spatial position in three dimensional space, combining spatial coordinates in a single place. 
+The second type composition mechanism available is the product type, which \textit{combines} using a type constructor. While the sum type adds choice in the language, this data type requires multiple types to assemble a new one in a mutually inclusive manner. For example, a digital clock composed by two numbers, hours and minutes, can be portrayed by the type \texttt{ClockTime}, which is a combination of two separate numbers combined by the wrapper \texttt{Time}. In order to have any possible time, it is necessary to provide \textit{both} parts. Effectively, the product type executes a cartesian product with its parts. Figure \ref{fig:productType} illustrates the syntax used in Haskell to create product types as well as another example of combined data, the type \texttt{SpacePosition}. It represents spatial position in three dimensional space, combining spatial coordinates in a single place. 
 
 \begin{figure}[ht!]
 \centering
@@ -101,11 +101,11 @@ The second type composition mechanism available is the product type, which \text
   \centering
   \includegraphics[width=0.95\linewidth]{MastersThesis/img/ProductType}
 \end{minipage}
-\caption{Product types are a combination of different sets, where you pick a representative from each one. Digital clocks' time and objects' coordinates in space are common use cases. In Haskell, a product type can be defined using a \textbf{record} alongside with the constructor, where the labels for each member inside it are explicit.}
+\caption{Product types are a combination of different sets, where you pick a representative from each one. Digital clocks' time and objects' coordinates in space are common use cases. In Haskell, a product type can be defined using a \textit{record} alongside with the constructor, where the labels for each member inside it are explicit.}
 \label{fig:productType}
 \end{figure}
 
-Within algebraic data types, it is possible to abstract the \textbf{structure} out, meaning that the outer shell of the type can be understood as a common pattern changing only the internal content. For instance, if a given application can take advantage of integer values but want to use the same configuration as the one presented in the \texttt{SpacePosition} data type, it's possible to add this customization. This feature is known as \textit{parametric polymorphism}, a powerful tool available in Haskell's type system. An example is presented in Figure \ref{fig:parametricPoly} using the \texttt{SpacePosition} type structure, where its internal types are being parametrized, thus allowing the use of other types internally, such as \texttt{Float}, \texttt{Int} and \texttt{Double}.
+Within algebraic data types, it is possible to abstract the \textit{structure} out, meaning that the outer shell of the type can be understood as a common pattern changing only the internal content. For instance, if a given application can take advantage of integer values but want to use the same configuration as the one presented in the \texttt{SpacePosition} data type, it's possible to add this customization. This feature is known as \textit{parametric polymorphism}, a powerful tool available in Haskell's type system. An example is presented in Figure \ref{fig:parametricPoly} using the \texttt{SpacePosition} type structure, where its internal types are being parametrized, thus allowing the use of other types internally, such as \texttt{Float}, \texttt{Int} and \texttt{Double}.
 
 \begin{figure}[ht!]
 \centering
@@ -127,7 +127,7 @@ Within algebraic data types, it is possible to abstract the \textbf{structure} o
 \label{fig:parametricPoly}
 \end{figure}
 
-In some situations, changing the type of the structure is not the desired property of interest. There are applications where some sort of \textbf{behaviour} is a necessity, e.g., the ability of comparing two instances of a custom type. This nature of polymorphism is known as \textit{ad hoc polymorphism}, which is implemented in Haskell via what is similar to java-like interfaces, so-called \textbf{typeclasses}~\cite{Wadler1989}. However, establishing a contract with a typeclass differs from an interface in a fundamental apurespect: rather than inheritance being given to the type, it has a lawful implementation, meaning that \textbf{mathematical formalism} is assured for it, although the implementer is not obligated to prove its laws on a language level. As an example, the implementation of the typeclass \texttt{Eq} gives to the type all comparable operations ($==$ and $!=$). Figure \ref{fig:adHocPoly} shows the implementation of \texttt{Ord} typeclass for the presented \texttt{ClockTime}, giving it capabilities for sorting instances of such type.
+In some situations, changing the type of the structure is not the desired property of interest. There are applications where some sort of \textit{behaviour} is a necessity, e.g., the ability of comparing two instances of a custom type. This nature of polymorphism is known as \textit{ad hoc polymorphism}, which is implemented in Haskell via what is similar to java-like interfaces, so-called \textit{typeclasses}~\cite{Wadler1989}. However, establishing a contract with a typeclass differs from an interface in a fundamental aspect: rather than inheritance being given to the type, it has a lawful implementation, meaning that \textit{mathematical formalism} is assured for it, although the implementer is not obligated to prove its laws on a language level. As an example, the implementation of the typeclass \texttt{Eq} gives to the type all comparable operations ($==$ and $!=$). Figure \ref{fig:adHocPoly} shows the implementation of \texttt{Ord} typeclass for the presented \texttt{ClockTime}, giving it capabilities for sorting instances of such type.
 
 \begin{figure}[ht!]
 \centering
@@ -150,25 +150,25 @@ In some situations, changing the type of the structure is not the desired proper
 \label{fig:adHocPoly}
 \end{figure}
 
-Algebraic data types, when combined with polymorphism, are a powerful tool in programming, being a useful way to model the domain of interest. However, both sum and product types cannot portray by themselves the intuition of a \textbf{procedure}. A data transformation process, as showed in Figure \ref{fig:functions}, can be utilized in a variety of different ways. Imagine, for instance, a system where validation can vary according to the current situation. Any validation algorithm would be using the same data, such as a record called \texttt{SystemData}, and returning a boolean as the result of the validation, but the internals of these functions would be totally different. This is represented in Figure \ref{fig:pipeline}. In Haskell, this motivates the use of functions as \textbf{first class citizens}, meaning that they are values and can be treated equally in comparison with data types that carries information, such as being used as arguments to another functions, so-called high order functions.
+Algebraic data types, when combined with polymorphism, are a powerful tool in programming, being a useful way to model the domain of interest. However, both sum and product types cannot portray by themselves the intuition of a \textit{procedure}. A data transformation process, as showed in Figure \ref{fig:functions}, can be utilized in a variety of different ways. Imagine, for instance, a system where validation can vary according to the current situation. Any validation algorithm would be using the same data, such as a record called \texttt{SystemData}, and returning a boolean as the result of the validation, but the internals of these functions would be totally different. This is represented in Figure \ref{fig:pipeline}. In Haskell, this motivates the use of functions as \textit{first class citizens}, meaning that they are values and can be treated equally in comparison with data types that carries information, such as being used as arguments to another functions, so-called high order functions.
 
-\figuraBib{Pipeline}{Replacements for the validation function within a pipeline like the above is common}{}{fig:pipeline}{width=.75\textwidth}%
+\figuraBib{Pipeline}{Replacements for the validation function within a pipeline like the above are common}{}{fig:pipeline}{width=.75\textwidth}%
 
 \section{Modeling Reality}
 \label{sec:diff}
 
-The continuous time problem explained in the introduction was initially addressed by mathematics, which represents physical quantities by \textbf{differential equations}. This set of equations establishes a relationship between functions and their repurespective derivatives; the function express the variable of interest and its derivative describe how it changes over time. It is common in the engineering and in the physics domain to know the rate of change of a given variable, but the function itself is still unknown. These variables describe the state of the system, e.g, velocity, water flow, electrical current, etc. When those variables are allowed to vary continuously --- in arbitrarily small increments --- differential equations arise as the standard tool to describe them.
+The continuous time problem explained in the introduction was initially addressed by mathematics, which represents physical quantities by \textit{differential equations}. This set of equations establishes a relationship between functions and their respective derivatives; the function express the variable of interest and its derivative describe how it changes over time. It is common in the engineering and in the physics domain to know the rate of change of a given variable, but the function itself is still unknown. These variables describe the state of the system, e.g, velocity, water flow, electrical current, etc. When those variables are allowed to vary continuously --- in arbitrarily small increments --- differential equations arise as the standard tool to describe them.
 
-While some differential equations have more than one independent variable per function, being classified as a \textbf{partial differential equation}, some phenomena can be modeled with only one independent variable per function in a given set, being described as a set of \textbf{ordinary differential equations}. However, because the majority of such equations does not have an analytical solution, i.e., cannot be described as a combination of other analytical formulas, numerical procedures are used to solve the system. These mechanisms \textbf{quantize} the physical time duration into an interval of numbers, each spaced by a \textbf{time step} from the other, and the sequence starts from an \textbf{initial value}. Afterward, the derivative is used to calculate the slope or the direction in which the tangent of the function is moving in time in order to predict the value of the next step, i.e., determine which point better represents the function in the next time step. The order of the method varies its precision during the prediction of the steps, e.g, the Runge-Kutta method of 4th order is more precise than the Euler method or the Runge-Kutta of 2nd order.
+While some differential equations have more than one independent variable per function, being classified as a \textit{partial differential equation}, some phenomena can be modeled with only one independent variable per function in a given set, being described as a set of \textit{ordinary differential equations}. However, because the majority of such equations does not have an analytical solution, i.e., cannot be described as a combination of other analytical formulas, numerical procedures are used to solve the system. These mechanisms \textit{quantize} the physical time duration into an interval of numbers, each spaced by a \textit{time step} from the other, and the sequence starts from an \textit{initial value}. Afterward, the derivative is used to calculate the slope or the direction in which the tangent of the function is moving in time in order to predict the value of the next step, i.e., determine which point better represents the function in the next time step. The order of the method varies its precision during the prediction of the steps, e.g, the Runge-Kutta method of 4th order is more precise than the Euler method or the Runge-Kutta of 2nd order.
 
-These numerical methods are used to solve problems purespecified by the following mathematical relations:
+These numerical methods are used to solve problems specified by the following mathematical relations:
 
 \begin{equation}
 \dot{y}(t) = f(t, y(t)) \quad y(t_0) = y_0
 \label{eq:diffEq}
 \end{equation}
 
-As showed, both the derivative and the function --- the mathematical formulation of the system --- varies according to \textbf{time}. Both acts as functions in which for a given time value, it produces a numerical outcome. Moreover, this equality assumes that the next step following the derivative's direction will not be that different from the actual value of the function $y$ if the time step is small enough. Further, it is assumed that in case of a small enough time step, the difference between time samples is $h$, i.e., the time step. In order to model this mathematical relationship between the functions and its repurespective derivative, these methods use iteration-based approximations. For instance, the following equation represents one step of the first-order Euler method, the simplest numerical method: 
+As showed, both the derivative and the function --- the mathematical formulation of the system --- varies according to \textit{time}. Both acts as functions in which for a given time value, it produces a numerical outcome. Moreover, this equality assumes that the next step following the derivative's direction will not be that different from the actual value of the function $y$ if the time step is small enough. Further, it is assumed that in case of a small enough time step, the difference between time samples is $h$, i.e., the time step. In order to model this mathematical relationship between the functions and its respective derivative, these methods use iteration-based approximations. For instance, the following equation represents one step of the first-order Euler method, the simplest numerical method: 
 
 \begin{equation}
 y_{n + 1} = y_n + hf(t_n, y_n)
@@ -192,7 +192,7 @@ $$ y_{5} = y_4 + 1 * f(4, y_4) \rightarrow y_{5} = 27 + 1 * (27 + 4) \rightarrow
 
 \section{Making Mathematics Cyber}
 
-Our primary goal is to combine the knowledge levered in section \ref{sec:types} --- modeling capabilities of Haskell's algebraic type system --- with the core notion of differential equations presented in section \ref{sec:diff}. The type system will model equation \ref{eq:nextStep}, detailed in the previous section.
+Our primary goal is to combine the knowledge levered in Section \ref{sec:types} --- modeling capabilities of Haskell's algebraic type system --- with the core notion of differential equations presented in Section \ref{sec:diff}. The type system will model equation \ref{eq:nextStep}, detailed in the previous Section.
 
 Any representation of a physical system that can be modeled by a set of differential equations has an outcome value at any given moment in time. The type \texttt{CT} (stands for \textit{continuous machine}) in Figure \ref{fig:firstDynamics} is a first draft of representing the continuous physical dynamics~\cite{LeeModeling} --- the evolution of a system state in time:
 
@@ -211,11 +211,11 @@ Any representation of a physical system that can be modeled by a set of differen
   \centering
   \includegraphics[width=0.95\linewidth]{MastersThesis/img/SimpleDynamics}
 \end{minipage}
-\caption{In Haskell, the \texttt{type} keyword works for alias. The first draft of the \texttt{CT} type is a \textbf{function}, in which providing a floating point value as time returns another value as outcome.}
+\caption{In Haskell, the \texttt{type} keyword works for alias. The first draft of the \texttt{CT} type is a \textit{function}, in which providing a floating point value as time returns another value as outcome.}
 \label{fig:firstDynamics}
 \end{figure}
 
-This type seems to capture the concept, whilst being compatible with the definition of a tagged system presented by Lee and Sangiovanni~\cite{LeeSangiovanni}. However, because numerical methods assume that the time variable is \textbf{discrete}, i.e., it is in the form of \textbf{iterations} that they solve differential equations. Thus, some tweaks to this type are needed, such as the number of the current iteration, which method is being used, in which stage the method is and when the final time of the simulation will be reached. With this in mind, new types are introduced. Figure \ref{fig:dynamicsAux} shows the auxiliary types to build a new version of the \texttt{CT} type.
+This type seems to capture the concept, whilst being compatible with the definition of a tagged system presented by Lee and Sangiovanni~\cite{LeeSangiovanni}. However, because numerical methods assume that the time variable is \textit{discrete}, i.e., it is in the form of \textit{iterations} that they solve differential equations. Thus, some tweaks to this type are needed, such as the number of the current iteration, which method is being used, in which stage the method is and when the final time of the simulation will be reached. With this in mind, new types are introduced. Figure \ref{fig:dynamicsAux} shows the auxiliary types to build a new version of the \texttt{CT} type.
 
 \ignore{
 \begin{code}
@@ -281,9 +281,9 @@ data Parameters = Parameters { interval  :: Interval,
 \label{fig:dynamicsAux}
 \end{figure}
 
-The above auxiliary types serve a common purpose: to provide at any given moment in time, all the information to execute a solver method until the end of the simulation. The type \texttt{Interval} determines when the simulation should start and when it should end. The \texttt{Method} sum type is used inside the \texttt{Solver} type to set solver sensible information, such as the size of the time step, which method will be used and in which stage the method is in at the current moment (more about the stage field on a later chapter). Finally, the \texttt{Parameters} type combines everything together, alongside with the current time value as well as its discrete counterpart, iteration.
+The above auxiliary types serve a common purpose: to provide at any given moment in time, all the information to execute a solver method until the end of the simulation. The type \texttt{Interval} determines when the simulation should start and when it should end. The \texttt{Method} sum type is used inside the \texttt{Solver} type to set solver sensible information, such as the size of the time step, which method will be used and in which stage the method is in at the current moment (more about the stage field on a later Chapter). Finally, the \texttt{Parameters} type combines everything together, alongside with the current time value as well as its discrete counterpart, iteration.
 
-Further, the new \texttt{CT} type can also be parametrically polymorphic, removing the limitation of only using \texttt{Double} values as the outcome. Figure \ref{fig:dynamics} depicts the final type for the physical dynamics. The \texttt{IO} wrapper is needed to cope with memory management and side effects, all of which will be explained in the next chapter. Below,
+Further, the new \texttt{CT} type can also be parametrically polymorphic, removing the limitation of only using \texttt{Double} values as the outcome. Figure \ref{fig:dynamics} depicts the final type for the physical dynamics. The \texttt{IO} wrapper is needed to cope with memory management and side effects, all of which will be explained in the next Chapter. Below,
 we have the definition for the \texttt{CT} type used in previous work~\cite{Lemos2022}:
 
 \begin{figure}[H]
@@ -371,4 +371,4 @@ instance (Floating a) => Floating (CT a) where
 \end{code}
 }
 
-This summarizes the main pilars in the design: FF-GPAC, the mathematical definition of the problem and how we are modeling this domain in Haskell. The next chapter, \textit{Effectful Integrals}, will start from this foundation, by adding typeclasses to the \texttt{CT} type, and will later describe the last core type before explaining the solver execution: the \texttt{Integrator} type. These improvements for the \texttt{CT} type and the new \texttt{Integrator} type will later be mapped to their FF-GPAC counterparts, explaining that they resemble the basic units mentioned in section \ref{sec:gpac}.
+This summarizes the main pilars in the design: FF-GPAC, the mathematical definition of the problem and how we are modeling this domain in Haskell. The next Chapter, \textit{Effectful Integrals}, will start from this foundation, by adding typeclasses to the \texttt{CT} type, and will later describe the last core type before explaining the solver execution: the \texttt{Integrator} type. These improvements for the \texttt{CT} type and the new \texttt{Integrator} type will later be mapped to their FF-GPAC counterparts, explaining that they resemble the basic units mentioned in Section \ref{sec:gpac}.
diff --git a/doc/MastersThesis/Lhs/Enlightenment.lhs b/doc/MastersThesis/Lhs/Enlightenment.lhs
index 1def305..5993fac 100644
--- a/doc/MastersThesis/Lhs/Enlightenment.lhs
+++ b/doc/MastersThesis/Lhs/Enlightenment.lhs
@@ -34,14 +34,14 @@ oldLorenzSystem = runCTFinal oldLorenzModel 100 lorenzSolver
 \end{code}
 }
 
-Previously, we presented in detail the latter core type of the implementation, the \texttt{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: describe how to map a set of differential equations to an executable model, reveal which functions execute a given example and 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.
 
 \section{From Models to Models}
 
-Systems of differential equations reside in the mathematical domain. In order to \textbf{execute} using the \texttt{FACT} DSL, this model needs to be converted into an executable model following the DSL's guidelines. Further, we saw that these requirements resemble FF-GPAC's description of its basic units and rules of composition. Thus, the mappings between these worlds need to be established. Chapters 2 and 3 explained the mapping between \texttt{FACT} and FF-GPAC. It remains to map the \textit{semantics} of the mathematical world to the \textit{operational} world of \texttt{FACT}. This mapping goes as the following:
+Systems of differential equations reside in the mathematical domain. In order to \textit{execute} using the \texttt{FACT} DSL, this model needs to be converted into an executable model following the DSL's guidelines. Further, we saw that these requirements resemble FF-GPAC's description of its basic units and rules of composition. Thus, the mappings between these worlds need to be established. Chapters 2 and 3 explained the mapping between \texttt{FACT} and FF-GPAC. It remains to map the \textit{semantics} of the mathematical world to the \textit{operational} world of \texttt{FACT}. This mapping goes as the following:
 
 \begin{itemize}
-  \item The relationship between the derivatives and their respective functions will be modeled by \textbf{feedback} loops with \texttt{Integrator} type.
+  \item The relationship between the derivatives and their respective functions will be modeled by \textit{feedback} loops with \texttt{Integrator} type.
   \item The initial condition will be modeled by the \texttt{initial} pointer within an integrator.
   \item Combinational aspects, such as addition and multiplication of constants and the time $t$, will be represented by typeclasses and the \texttt{CT} type.
 \end{itemize}
@@ -73,15 +73,15 @@ $\dot{y} = y + t \quad \quad y(0) = 1$
 
 \figuraBib{Rivika2GPAC}{The developed DSL translates a system described by differential equations to an executable model that resembles FF-GPAC's description}{}{fig:rivika2gpac}{width=.8\textwidth}%
 
-In line 5, a record with type \texttt{Integrator} is created, with $1$ being the initial condition of the system. Line 6 creates a \textbf{state variable}, a label that gives us access to the output of an integrator, \texttt{integ} in this case. Afterward, in line 7, the \textit{updateInteg} function connects the inputs to a given integrator by creating a combinational circuit, \texttt{(y + t)}. Polynomial circuits and integrators' outputs can be used as available inputs, as well as the \textit{time} of the simulation. Finally, line 8 returns the state variable as the output for the \textbf{driver}, the main topic of the next section.
+In line 5, a record with type \texttt{Integrator} is created, with $1$ being the initial condition of the system. Line 6 creates a \textit{state variable}, a label that gives us access to the output of an integrator, \texttt{integ} in this case. Afterward, in line 7, the \textit{updateInteg} function connects the inputs to a given integrator by creating a combinational circuit, \texttt{(y + t)}. Polynomial circuits and integrators' outputs can be used as available inputs, as well as the \textit{time} of the simulation. Finally, line 8 returns the state variable as the output for the \textit{driver}, the main topic of the next Section.
 
-There is, however, an useful improvement to be made into the definition of a model within the DSL. The presented example used only a single state variable, although it is common to have \textbf{multiple} state variables, i.e., multiple integrators interacting with each other, modeling different aspects of a given scenario. Moreover, when dealing with multiple state variables, it is important to maintain \textbf{synchronization} between them, i.e., the same \texttt{Parameters} is being applied to \textbf{all} state variables at the same time.
+There is, however, an useful improvement to be made into the definition of a model within the DSL. The presented example used only a single state variable, although it is common to have \textit{multiple} state variables, i.e., multiple integrators interacting with each other, modeling different aspects of a given scenario. Moreover, when dealing with multiple state variables, it is important to maintain \textit{synchronization} between them, i.e., the same \texttt{Parameters} is being applied to \textit{all} state variables at the same time.
 
-To address both of these requirements, we will use the \textit{sequence} function, available in Haskell's standard library. This function manipulates \textbf{nested} structures and change their internal structure. The only requirement is that the outer type have to implement the \texttt{Traversable} typeclass. For instance, applying this function to a list of values of type \texttt{Maybe} would generate a single \texttt{Maybe} value in which its content is a list of the previous content individually wrapped by the \texttt{Maybe} type. This is only possible because the external or "bundler" type, list in this case, has implemented the \texttt{Traversable} typeclass. Figure \ref{fig:sequence} depicts the example before and after applying the function.
+To address both of these requirements, we will use the \textit{sequence} function, available in Haskell's standard library. This function manipulates \textit{nested} structures and change their internal structure. The only requirement is that the outer type have to implement the \texttt{Traversable} typeclass. For instance, applying this function to a list of values of type \texttt{Maybe} would generate a single \texttt{Maybe} value in which its content is a list of the previous content individually wrapped by the \texttt{Maybe} type. This is only possible because the external or "bundler" type, list in this case, has implemented the \texttt{Traversable} typeclass. Figure \ref{fig:sequence} depicts the example before and after applying the function.
 
 \figuraBib{Sequence}{Because the list implements the \texttt{Traversable} typeclass, it allows this type to use the \textit{traverse} and \textit{sequence} functions, in which both are related to changing the internal behaviour of the nested structures}{}{fig:sequence}{width=.95\textwidth}%
 
-Similarly to the preceding example, the list structure will be used to involve all the state variables with type \texttt{CT Double}. This tweak is effectively creating a \textbf{vector} of state variables whilst sharing the same notion of time across all of them. So, the final type signature of a model is \texttt{CT [Double]} or, by using a type aliases for \texttt{[Double]} as \texttt{Vector}, \texttt{CT Vector}. A second alias can be created to make it more descriptive, as exemplified in Figure \ref{fig:exampleMultiple}:
+Similarly to the preceding example, the list structure will be used to involve all the state variables with type \texttt{CT Double}. This tweak is effectively creating a \textit{vector} of state variables whilst sharing the same notion of time across all of them. So, the final type signature of a model is \texttt{CT [Double]} or, by using a type aliases for \texttt{[Double]} as \texttt{Vector}, \texttt{CT Vector}. A second alias can be created to make it more descriptive, as exemplified in Figure \ref{fig:exampleMultiple}:
 
 \begin{figure}[ht!]
 \begin{minipage}{.5\textwidth}
@@ -107,7 +107,7 @@ $\dot{x} = y * x \quad \quad x(0) = 1$
 $\dot{y} = y + t \quad \quad y(0) = 1$
 \end{center}
 \end{minipage}
-\caption{A \textbf{state vector} comprises multiple state variables and requires the use of the \textit{sequence} function to sync time across all variables.}
+\caption{A \textit{state vector} comprises multiple state variables and requires the use of the \textit{sequence} function to sync time across all variables.}
 \label{fig:exampleMultiple}
 \end{figure}
 
@@ -117,7 +117,7 @@ Finally, when creating a model, the same steps have to be done in the same order
 \begin{center}
 \includegraphics[width=0.97\linewidth]{MastersThesis/img/ModelPipeline}
 \end{center}
-\caption{When building a model for simulation, the above pipeline is always used, from both points of view. The operations with meaning, i.e., the ones in the \texttt{Semantics} pipeline, are mapped to executable operations in the \texttt{Operational} pipeline, and vice-versa.}
+\caption[Execution pipeline of a model.]{When building a model for simulation, the above pipeline is always used, from both points of view. The operations with meaning, i.e., the ones in the \texttt{Semantics} pipeline, are mapped to executable operations in the \texttt{Operational} pipeline, and vice-versa.}
 \label{fig:modelPipe}
 \end{figure}
 
@@ -141,15 +141,15 @@ runCT m t sl =
 \end{spec}
 
 On line 3, we convert the final \textit{time value} for the simulation into an interval value for the simulation (\texttt{iv}) --- the simulation always starts at 0 and goes all the
-way up to the requested time. Next up, on line 4, we convert the interval to an \textit{iteration} interval in the format of a tuple, i.e., the continuous interval becomes the tuple $(0, \frac{stopTime - startTime}{timeStep})$, in which the second value of the tuple is \textbf{rounded}. From line 5 to line 11, we are defining an auxiliary function \textit{parameterise}. This function picks a natural number, which represents the iteration
+way up to the requested time. Next up, on line 4, we convert the interval to an \textit{iteration} interval in the format of a tuple, i.e., the continuous interval becomes the tuple $(0, \frac{stopTime - startTime}{timeStep})$, in which the second value of the tuple is \textit{rounded}. From line 5 to line 11, we are defining an auxiliary function \textit{parameterize}. This function picks a natural number, which represents the iteration
 index, and creates a new record with the type \texttt{Parameters}. Additionally, it uses the auxiliary function \textit{iterToTime} (line 7), which converts the iteration number from
-the domain of discrete \textbf{steps} to the domain of \textbf{discrete time}, i.e., the time the solver methods can operate with (chapter 5 will explore more of this concept). This conversion is based on the time step being used, as well as which method and in which stage it is for that specific iteration. Finally, line 13 produces the outcome of the \textit{runCT} function. The final result is the output from a function called \textit{map} piped it as an argument for the \textit{sequence} function.
+the domain of discrete \textit{steps} to the domain of \textit{discrete time}, i.e., the time the solver methods can operate with (Chapter 5 will explore more of this concept). This conversion is based on the time step being used, as well as which method and in which stage it is for that specific iteration. Finally, line 13 produces the outcome of the \textit{runCT} function. The final result is the output from a function called \textit{map} piped it as an argument for the \textit{sequence} function.
 
-The \textit{map} operation is provided by the \texttt{Functor} of the list monad, and it applies an arbitrary function to the internal members of a list in a \textbf{sequential} manner. In this case, the \textit{parameterise} function, composed with the continuous machine \texttt{m}, is the one being mapped. Thus, a custom value of the type \texttt{Parameters} is taking place of each natural natural number in the list, and this is being applied to the received \texttt{CT} value. It produces a list of answers in order, each one wrapped in the \texttt{IO} monad. To abstract out the \texttt{IO}, thus getting \texttt{IO [a]} rather than \texttt{[IO a]}, the \textit{sequence} function finishes the implementation. Additionally, there is an analogous implementation of this function, so-called \textit{runCTFinal}, that return only the final result of the simulation instead of the outputs at the time step samples.
+The \textit{map} operation is provided by the \texttt{Functor} of the list monad, and it applies an arbitrary function to the internal members of a list in a \textit{sequential} manner. In this case, the \textit{parameterise} function, composed with the continuous machine \texttt{m}, is the one being mapped. Thus, a custom value of the type \texttt{Parameters} is taking place of each natural natural number in the list, and this is being applied to the received \texttt{CT} value. It produces a list of answers in order, each one wrapped in the \texttt{IO} monad. To abstract out the \texttt{IO}, thus getting \texttt{IO [a]} rather than \texttt{[IO a]}, the \textit{sequence} function finishes the implementation. Additionally, there is an analogous implementation of this function, so-called \textit{runCTFinal}, that return only the final result of the simulation instead of the outputs at the time step samples. The next section will provide an example of this in a step-by-step manner.
 
 \section{An attractive example}
 
-For the example walkthrough, the same example introduced in the chapter \textit{Introduction} will be used in this section. So, we will be solving a system, composed by a set of chaotic solutions, called \textbf{the Lorenz Attractor}. In these types of systems, the ordinary differential equations are used to model chaotic systems, providing solutions based on parameter values and initial conditions. The original differential equations are presented bellow:
+For the example walkthrough, the same example introduced in the Chapter \textit{Introduction} will be used in this Section. So, we will be solving a simpler system for demonstration purposes, composed by a set of chaotic solutions, called \textit{the Lorenz Attractor}. In these types of systems, the ordinary differential equations are used to model chaotic systems, providing solutions based on parameter values and initial conditions. The original differential equations are presented bellow:
 
 $$ \sigma = 10.0 $$
 $$ \rho = 28.0 $$
@@ -195,25 +195,25 @@ lorenzSystem = runCT lorenzModel 100 lorenzSolver
 
 The first records, \texttt{Solver}, sets the environment (lines 1 to 4). It configures the solver with $0.01$ seconds as the time step, whilst executing the second-order Runge-Kutta method from the initial stage (lines 3 to 6). The \textit{lorenzModel}, presented after setting the constants (lines 6 to 8), executes the aforementioned pipeline to create the model: allocate memory (lines 12 to 14), create read-only pointers (lines 15 to 17), change the computation (lines 18 to 20) and dispatch it (line 21). Finally, the function \textit{lorenzSystem} groups everything together calling the \textit{runCT} driver (line 22).
 
-After this overview, let's follow the execution path used by the compiler. Haskell's compiler works in a lazily manner, meaning that it calls for execution only the necessary parts. So, the first step calling \textit{lorenzSystem} is to call the \textit{runCT} function with a model, final time for the simulation and solver configurations. Following its path of execution, the \textit{map} function (inside the driver) forces the application of a parametric record generated by the \textit{parameterise} function to the provided model, \textit{lorenzModel} in this case. Thus, it needs to be executed in order to return from the \textit{runCT} function.
+After this overview, let's follow the execution path used by the compiler. Haskell's compiler works in a lazily manner, meaning that it calls for execution only the necessary parts. So, the first step calling \textit{lorenzSystem} is to call the \textit{runCT} function with a model, final time for the simulation and solver configurations. Following its path of execution, the \textit{map} function (inside the driver) forces the application of a parametric record generated by the \textit{parameterize} function to the provided model, \textit{lorenzModel} in this case. Thus, it needs to be executed in order to return from the \textit{runCT} function.
 
-To understand the model, we need to follow the execution sequence of the output: \texttt{sequence [x, y, z]}, which requires executing all the lines before this line to obtain the all the state variables. For the sake of simplicity, we will follow the execution of the operations related to the $x$ variable, given that the remaining variables have an analogous execution walkthrough. First and foremost, memory is allocated for the integrator to work with (line 12). Figure \ref{fig:allocateExample} depicts this idea, as well as being a reminder of what the \textit{createInteg} and \textit{initialize} functions do, described in the chapter \textit{Effectful Integrals}. In this image, the integrator \texttt{integX} comprises two fields, \texttt{initial} and \texttt{computation}. The former is a simple value of the type \texttt{CT Double} that, regardless of the parameters record it receives, it returns the initial condition of the system. The latter is a pointer or address that references a specific \texttt{CT Double} computation in memory: in the case of receiving a parametric record \texttt{ps}, it fixes potential problems with it via the \texttt{initialize} block, and it applies this fixed value in order to get \texttt{i}, i.e., the initial value $1$, the same being saved in the other field of the record, \texttt{initial}.
+To understand the model, we need to follow the execution sequence of the output: \texttt{sequence [x, y, z]}, which requires executing all the lines before this line to obtain all the state variables. For the sake of simplicity, we will follow the execution of the operations related to the $x$ variable, given that the remaining variables have an analogous execution walkthrough. First and foremost, memory is allocated for the integrator to work with (line 12). Figure \ref{fig:allocateExample} depicts this idea, as well as being a reminder of what the \textit{createInteg} and \textit{initialize} functions do, described in the Chapter \textit{Effectful Integrals}. In this image, the integrator \texttt{integX} comprises two fields, \texttt{initial} and \texttt{computation}. The former is a simple value of the type \texttt{CT Double} that, regardless of the parameters record it receives, returns the initial condition of the system. The latter is a pointer or address that references a specific \texttt{CT Double} computation in memory: in the case of receiving a parametric record \texttt{ps}, it fixes potential problems with it via the \texttt{initialize} block, and it applies this fixed value in order to get \texttt{i}, i.e., the initial value $1$, the same being saved in the other field of the record, \texttt{initial}.
 
 \figuraBib{ExampleAllocate}{After \textit{createInteg}, this record is the final image of the integrator. The function \textit{initialize} gives us protecting against wrong records of the type \texttt{Parameters}, assuring it begins from the first iteration, i.e., $t_0$}{}{fig:allocateExample}{width=.90\textwidth}%
 
-The next step is the creation of the independent state variable $x$ via \textit{readInteg} function (line 15). This variable will read the computations that are executing under the hood by the integrator. The core idea is to read from the computation pointer inside the integrator and create a new \texttt{CT Double} value. Figure \ref{fig:readExample} portrays this mental image. When reading a value from an integrator, the computation pointer is being used to access the memory region previously allocated. Also, what's being stored in memory is a \texttt{CT Double} value. The state variable, $x$ in this case, combines its received \texttt{Parameters} value, so-called \texttt{ps}, and \textbf{applies} it to the stored continuous machine. The result \texttt{v} is then returned.
+The next step is the creation of the independent state variable $x$ via \textit{readInteg} function (line 15). This variable will read the computations that are executing under the hood by the integrator. The core idea is to read from the computation pointer inside the integrator and create a new \texttt{CT Double} value. Figure \ref{fig:readExample} portrays this mental image. When reading a value from an integrator, the computation pointer is being used to access the memory region previously allocated. Also, what's being stored in memory is a \texttt{CT Double} value. The state variable, $x$ in this case, combines its received \texttt{Parameters} value, so-called \texttt{ps}, and \textit{applies} it to the stored continuous machine. The result \texttt{v} is then returned.
 
 \figuraBib{ExampleRead}{After \textit{readInteg}, the final floating point values is obtained by reading from memory a computation and passing to it the received parameters record. The result of this application, $v$, is the returned value}{}{fig:readExample}{width=.90\textwidth}%
 
-The final step is to \textbf{change} the computation \textbf{inside} the memory region (line 18). Until this moment, the stored computation is always returning the value of the system at $t_0$, whilst changing the obtained parameters record to be correct via the \textit{initialize} function. Our goal is to modify this behaviour to the actual solution of the differential equations via using numerical methods, i.e., using the solver of the simulation. The function \textit{updateInteg} fulfills this role and its functionality is illustrated in Figure \ref{fig:changeExample}. With the integrator \texttt{integX} and the differential equation $\sigma (y - x)$ on hand, this function picks the provided parametric record \texttt{ps} and it returns the result of a step of the solver \texttt{RK2}, second-order Runge-Kutta method in this case. Additionally, the solver method receives as a dependency what is being pointed by the \texttt{computation} pointer, represented by \texttt{c} in the image, alongside the differential equation and initial value, pictured by \texttt{d} and \texttt{i} respectively.
+The final step is to \textit{change} the computation \textit{inside} the memory region (line 18). Until this moment, the stored computation is always returning the value of the system at $t_0$, whilst changing the obtained parameters record to be correct via the \textit{initialize} function. Our goal is to modify this behaviour to the actual solution of the differential equations via using numerical methods, i.e., using the solver of the simulation. The function \textit{updateInteg} fulfills this role and its functionality is illustrated in Figure \ref{fig:changeExample}. With the integrator \texttt{integX} and the differential equation $\sigma (y - x)$ on hand, this function picks the provided parametric record \texttt{ps} and it returns the result of a step of the solver \texttt{RK2}, second-order Runge-Kutta method in this case. Additionally, the solver method receives as a dependency what is being pointed by the \texttt{computation} pointer, represented by \texttt{c} in the image, alongside the differential equation and initial value, pictured by \texttt{d} and \texttt{i} respectively.
 
 \figuraBib{ExampleChange}{The \textit{updateInteg} function only does side effects, meaning that only affects memory. The internal variable \texttt{c} is a pointer to the computation \textit{itself}, i.e., the computation being created references this exact procedure}{}{fig:changeExample}{width=.90\textwidth}%
 
 \figuraBib{ExampleFinalModel}{After setting up the environment, this is the final depiction of an independent variable. The reader $x$ reads the values computed by the procedure stored in memory, a second-order Runge-Kutta method in this case}{}{fig:finalModelExample}{width=.90\textwidth}%
 
-Figure \ref{fig:finalModelExample} shows the final image for state variable $x$ after until this point in the execution. Lastly, the state variable is wrapped inside a list and it is applied to the \textit{sequence} function, as explained in the previous section. This means that the list of variable(s) in the model, with the signature \texttt{[CT Double]}, is transformed into a value with the type \texttt{CT [Double]}. The transformation can be visually understood when looking at Figure \ref{fig:finalModelExample}. Instead of picking one \texttt{ps} of type \texttt{Parameters} and returning a value \textit{v}, the same parametric record returns a \textbf{list} of values, with the \textbf{same} parametric dependency being applied to all state variables inside $[x, y, z]$.
+Figure \ref{fig:finalModelExample} shows the final image for state variable $x$ after until this point in the execution. Lastly, the state variable is wrapped inside a list and it is applied to the \textit{sequence} function, as explained in the previous Section. This means that the list of variable(s) in the model, with the signature \texttt{[CT Double]}, is transformed into a value with the type \texttt{CT [Double]}. The transformation can be visually understood when looking at Figure \ref{fig:finalModelExample}. Instead of picking one \texttt{ps} of type \texttt{Parameters} and returning a value \textit{v}, the same parametric record returns a \textit{list} of values, with the \textit{same} parametric dependency being applied to all state variables inside $[x, y, z]$.
 
-However, this only addresses \textbf{how} the driver triggers the entire execution, but does \textbf{not} explain how the differential equations are actually being calculated with the \texttt{RK2} numerical method. This is done by the solver functions (\textit{integEuler}, \textit{integRK2} and \textit{integRK4}) and those are all based on equation \ref{eq:solverEquation} regardless of the chosen method. The equation goes as the following:
+However, this only addresses \textit{how} the driver triggers the entire execution, but does \textit{not} explain how the differential equations are actually being calculated with the \texttt{RK2} numerical method. This is done by the solver functions (\textit{integEuler}, \textit{integRK2} and \textit{integRK4}) and those are all based on equation \ref{eq:solverEquation} regardless of the chosen method. The equation goes as the following:
 
 $$y_{n+1} = y_n + hf(t_n,y_n) \rightarrow y_n = y_{n-1} + hf(t_{n-1}, y_{n-1})$$
 
@@ -225,11 +225,11 @@ The equation above makes the dependencies in the \texttt{RK2} example in Figure
  \item \texttt{i} and \texttt{c} $\Rightarrow$ The initial value of the system, as well as a solver step function, will be used to calculate the previous iteration result ($y_{n-1}$).
 \end{itemize}
 
-It is worth mentioning that the dependency \texttt{c} is a call of a \textbf{solver step}, meaning that it is capable of calculating the previous step $y_{n-1}$. This is accomplished in a \textbf{recursive} manner, since for every iteration the previous one is necessary. When the base case is achieved, by calculating the value at the first iteration using the \texttt{i} dependency, the recursion stops and the process folds, getting the final result for the iteration that has started the chain. This is the same pattern across all the implemented solvers (\texttt{Euler}, \texttt{RungeKutta2} and \texttt{RungeKutta4}).
+It is worth mentioning that the dependency \texttt{c} is a call of a \textit{solver step}, meaning that it is capable of calculating the previous step $y_{n-1}$. This is accomplished in a \textit{recursive} manner, since for every iteration the previous one is necessary. When the base case is achieved, by calculating the value at the first iteration using the \texttt{i} dependency, the recursion stops and the process folds, getting the final result for the iteration that has started the chain. This is the same pattern across all the implemented solvers (\texttt{Euler}, \texttt{RungeKutta2} and \texttt{RungeKutta4}).
 
 \section{Lorenz's Butterfly}
 
-After all the explained theory behind the project, it remains to be seen if this can be converted into practical results. With certain constant values, the generated graph of the Lorenz's Attractor example used in the last chapter is known for oscillation and getting the shape of two fixed point attractors, meaning that the system evolves to an oscillating state even if slightly disturbed. As showed in Figure \ref{fig:lorenzPlots}, the obtained graph from the Lorenz's Attractor model matches what was expected for a Lorenz's system. It is worth noting that changing the values of $\sigma$, $\rho$ and $\beta$ can produce completely different answers, destroying the resembled "butterfly" shape of the graph. Although correct, the presented solution has a few drawbacks. The next three chapters will explain and address the identified problems with the current implementation.
+After all the explained theory behind the project, it remains to be seen if this can be converted into practical results. As depicted in Figure \ref{fig:lorenzPlots}, the obtained graph from the Lorenz's Attractor model matches what was expected for a Lorenz's system. It is worth noting that changing the values of $\sigma$, $\rho$ and $\beta$ can produce completely different answers, destroying the resembled "butterfly" shape of the graph. Although correct, the presented solution has a few drawbacks. The next three chapters will explain and address the identified problems with the current implementation.
 
 \figuraBib{LorenzPlot1}{The Lorenz's Attractor example has a very famous butterfly shape from certain angles and constant values in the graph generated by the solution of the differential equations.}{}{fig:lorenzPlots}{width=.90\textwidth}%
 
diff --git a/doc/MastersThesis/Lhs/Fixing.lhs b/doc/MastersThesis/Lhs/Fixing.lhs
index 61f1e85..d866ef8 100644
--- a/doc/MastersThesis/Lhs/Fixing.lhs
+++ b/doc/MastersThesis/Lhs/Fixing.lhs
@@ -18,14 +18,14 @@ The last improvement for FACT is in terms of \textit{familiarity}. When someone
 the main goal should be that the least amount of friction when using the simulation software, the better.
 Hence, the requirement of knowing implementation details or programming language details is something we would like to avoid, given that
 it leaks noise into the designer's mind. The designer's concern should be to pay attention to the system's description and FACT having an extra
-step of translation or noisy setups just adds an extra burden with no real gains on the engineering of simulating continuous time. This chapter
+step of translation or noisy setups just adds an extra burden with no real gains on the engineering of simulating continuous time. This Chapter
 will present \textit{FFACT}, an evolution of FACT which aims to reduce the noise even further.
 
 \section{Integrator's Noise}
 
 Chapter 4, \textit{Execution Walkthrough}, described the semantics and usability on an example of a system in mathematical specification
 and its mapping to a simulation-ready description provided by FACT.
-Below we have this example modeled using FACT (same code as provided in section~\ref{sec:intro}):
+We have this example modeled using FACT (same code as provided in Section~\ref{sec:intro}):
 %
 \vspace{0.1cm}
 \begin{spec}
@@ -51,7 +51,7 @@ lorenzModel =
 
 It is noticeable, however, that FACT imposes a significant amount of overhead from the user's perspective due to the \textbf{explicit use of integrators} for most memory-required simulations.
 When creating stateful circuits, an user of FACT is obligated to use the integrator's API, i.e., use the functions \texttt{createInteg} (lines 6 to 8), \texttt{readInteg} (lines 9 to 11), and \texttt{updateInteg} (lines 12 to 14). Although these functions remove the
-management of the aforementioned implicit mutual recursion mentioned in chapter 3, \textit{Effectful Integrals}, from the user, it is still required to follow
+management of the aforementioned implicit mutual recursion mentioned in Chapter 3, \textit{Effectful Integrals}, from the user, it is still required to follow
 a specific sequence of steps to complete a model for any simulation:
 %
 \begin{enumerate}
@@ -60,7 +60,15 @@ a specific sequence of steps to complete a model for any simulation:
 \item Update integrators with the actual ODEs of interest (via the use of \textit{updateInteg}).
 \end{enumerate}
 
-Visually, this step-by-step list for FACT's models follow the pattern detailed in Figure~\ref{fig:modelPipe} in chapter 4, \textit{Execution Walkthrough}.
+Visually, this step-by-step list for FACT's models follow the pattern detailed in Figure~\ref{fig:modelPipe} in Chapter 4, \textit{Execution Walkthrough}:
+
+\begin{figure}[H]
+\begin{center}
+\includegraphics[width=0.97\linewidth]{MastersThesis/img/ModelPipeline}
+\end{center}
+\caption[Execution pipeline of a model.]{Pipeline of execution when creating a model in \texttt{FACT}.}
+\end{figure}
+
 More importantly, \emph{all} those steps are visible and transparent from an usability's point of view.
 Hence, a system's designer \emph{must} be aware of this \emph{entire} sequence of mandatory steps, even if his interest probably only relates to lines 12 to 14.
 Although one's goal is being able to specify a system and start a simulation, there is no escape -- one has to bear the noise created due to
@@ -75,10 +83,14 @@ required piece to get rid of the \texttt{Integrator} type, thus also removing it
 \section{The Fixed-Point Combinator}
 \label{subsec:fix}
 
+It is worth noting that the term \textit{fixed-point} has different meanings in the domains of engineering and mathematics. When referencing the
+fractional representations within a computer, one may use the \textit{fixed-point method}. Thus, to avoid confusion, the following is the definition
+of such concept in this dissertation, alongside a set of examples of its use case as a mathematical combinator that can be used to implement recursion.
+
 On the surface, the fixed-point combinator is a simple mapping that fulfills the following property:
 a point \emph{p} is a fixed-point of a function \emph{f} if \emph{f(p)} lies on the identity function, i.e., \emph{f(p) = p}.
 Not all functions have fixed-points, and some functions may have more than one~\cite{tennent1991}.
-Further, we seek to establish theorems and algorithms in which one can guarantees fixed-points and their uniqueness, such as the Banach fixed-point theorem~\cite{bryant1985}.
+Further, we seek to establish theorems and algorithms in which one can guarantee fixed-points and their uniqueness, such as the Banach fixed-point theorem~\cite{bryant1985}.
 In programming terms, by following specific requirements one could find the fixed-point of a function via an iterative process
 that involves going back and forth between it and the identity function until the difference in outcomes is less than or equal to an arbitrary~$\epsilon$.
 
@@ -137,7 +149,7 @@ For readers unfamiliar with the use of this combinator, equational reasoning~\ci
 ...
 \end{lstlisting}
 
-We left as exercise for the reader to check that the result of this process will yield the factorial of 5, i.e., 120.
+The result of this process will yield the factorial of 5, i.e., 120.
 When using \texttt{fix} to define recursive processes, the function being \emph{applied} to it must be the one defining the convergence criteria for the iterative process of looking for the fixed-point.
 In our factorial case, this is done via the conditional check at the beginning of body of the lambda.
 The fixed point combinator's responsibility is to keep the \emph{repetition} process going -- something that may diverge and run out of computer resources.
@@ -154,8 +166,7 @@ Furthermore, this process can be used in conjunction with monadic operations as
 \end{purespec}
 \vspace{-0.1cm}
 %
-This combination, however, cannot address \emph{all} cases when using side-effects.
-In the above, executing the side-effect in \texttt{countDown} do not contribute to its own \emph{definition}.
+This combination, however, cannot address \emph{all} cases when using side-effects. Executing the side-effect in \texttt{countDown} do not contribute to its own \emph{definition}.
 There is no construct or variable that requires the side-effect to be executed in order to determine its meaning.
 This ability -- being able to set values based on the result of running side-effects whilst keep the fixed-point running -- is something of interest because, as we are about to see, this allows the use of \emph{cyclic} definitions.
 
@@ -185,13 +196,13 @@ By allowing this behavior, mutually recursive bindings are made possible and thu
 Haskell's vanilla \texttt{let} already acts like a \texttt{letrec}, and it would be useful to replicate this property to monadic bindings as well.
 
 In the case of the \texttt{counter} example, the execution of a side-effect is mandatory to evaluate the values of the bindings, such as \texttt{next}, \texttt{inc}, \texttt{out}, and \texttt{zero} (lines 2 to 5).
-In contrast, the example \texttt{countDown} in section~\ref{subsec:fix} has none of its bindings locked by side-effects, e.g, the bindings \texttt{f} and \texttt{n} have nothing to do with the effect of printing a message on \texttt{stdout}.
+In contrast, the example \texttt{countDown} in Section~\ref{subsec:fix} has none of its bindings locked by side-effects, e.g, the bindings \texttt{f} and \texttt{n} have nothing to do with the effect of printing a message on \texttt{stdout}.
 When dealing with the latter of these cases, the usual fixed-point combinator is enough to model its recursion.
 The former case, however, needs a special kind of recursion, so-called \emph{value recursion}~\cite{leventThesis}.
 
 As we are about to understand on Section~\ref{sec:ffact}, the use of value recursion to have monadic's bindings with the same convenience of \texttt{letrec} will be the key to our improvement on FFACT over FACT.
 Fundamentally, it will \emph{tie the recursion knot} done in FACT via the complicated implicit recursion mentioned in Section~\ref{sec:integrator}.
-In terms of implementation, this is being achieved by the use of the \texttt{mfix} construct~\cite{levent2000}, which is accompained by a \emph{recursive do} syntax sugar~\cite{levent2002}, with the caveat of not being able to do shadowing -- much like the \texttt{let} and \texttt{where} constructs in Haskell.
+In terms of implementation, this is being achieved by the use of the \texttt{mfix} construct~\cite{levent2000}, which is accompanied by a \emph{recursive do} syntax sugar~\cite{levent2002}, with the caveat of not being able to do shadowing -- much like the \texttt{let} and \texttt{where} clauses in Haskell.
 In order for a type to be able to use this construct, it should follow specific algebraic laws~\cite{leventThesis} to then implement the \texttt{MonadFix} type class found in \texttt{Control.Monad.Fix}~\footnote{\texttt{Control.Monad.Fix} \href{https://hackage.haskell.org/package/base-4.21.0.0/docs/Control-Monad-Fix.html}{\textcolor{blue}{hackage documentation}}.} package:
 %
 %% \vspace{-0.8cm}
@@ -235,7 +246,7 @@ updateInteg integ diff = do
   liftIO $ writeIORef (computation integ) z
 \end{purespec}
 
-\figuraBib{createInteg}{Diagram of \texttt{createInteg} primitive for intuition.}{}{fig:createIntegDiagram}{width=.97\textwidth}%
+\figuraBib{createInteg}{Diagram of \texttt{createInteg} primitive for intuition}{}{fig:createIntegDiagram}{width=.97\textwidth}%
 
 \section{Tweak IV: Fixing FACT}
 \label{sec:ffact}
@@ -303,7 +314,7 @@ integ diff i =
 \end{code}
 \vspace{-0.2cm}
 %
-This new functin received the differential equation of interest, named \texttt{diff}, and the initial condition of the simulation, identified
+This new function received the differential equation of interest, named \texttt{diff}, and the initial condition of the simulation, identified
 as \texttt{i}, on line 2. Interpolation and memoization requirements from FACT are being maintained, as shown on line 3. Lines 3 to 6 demonstrate the use case for FFACT's \texttt{mdo}.
 A continuous machine created by the memoization function (line 3), \texttt{y}, uses another continuous machine, \texttt{z}, yet to be defined.
 This continuous machine, defined on line 4, retrieves the numerical method chosen by a value of type \texttt{Parameters}, via the function \texttt{f}.
@@ -324,10 +335,155 @@ lorenzSystem = runCT lorenzModel 100 lorenzSolver
 \end{code}
 
 Not surprisingly, the results of this new approach using the monadic fixed-point combinator are very similar to the
-performance metrics depicted in chapter 6, \textit{Caching the Speed Pill}. Figure~\ref{fig:fixed-graph} shows the new results:
+performance metrics depicted in Chapter 6, \textit{Caching the Speed Pill} --- indicating that we are \textit{not} trading performance
+for a gain in conciseness. Figure~\ref{fig:fixed-graph} shows the new results.
 
 \figuraBib{Graph3}{Results of FFACT are similar to the final version of FACT.}{}{fig:fixed-graph}{width=.97\textwidth}%
 
+\newpage
+
+\section{Examples and Comparisons}
+\label{sec:examples}
+
+In order to assess how \textit{concise} model can be in FFACT, in comparison with the mathematical descriptions of the models,
+we present comparisons between this dissertation's proposed implementation and the same example in SimulinkSimulink~\footnote{Simulink \href{http://www.mathworks.com/products/simulink/}{\textcolor{blue}{documentation}}.}, Matlab~\footnote{Matlab \href{https://www.mathworks.com/products/matlab.html}{\textcolor{blue}{documentation}}.}, Mathematica~\footnote{Mathematica \href{https://www.wolfram.com/mathematica/}{\textcolor{blue}{documentation}}.}, and \texttt{Yampa}~\footnote{Yampa \href{https://hackage.haskell.org/package/Yampa}{\textcolor{blue}{hackage documentation}}.}. It is worth noting that the last one, \texttt{Yampa}, is also implemented in Haskell as a HEDSL. In each pair of comparisons both conciseness and differences will be considered when implementing the Lorenz Attractor model. Ideally, a system's description should contain the \textit{least} amount of notation noise and artifacts to his mathematical counterpart. It is worth noting that these examples only show \textit{the system's description}, i.e., the \textit{drivers} of the simulations
+are being omitted when not necessary to describe the system.
+
+Figure~\ref{fig:lorenz-simulink} depicts a side-by-side comparison between FFACT and Simulink. The Haskell HEDSL specifies a model in text format, whilst Simulink
+is a visual tool --- you draw a diagram that represents the system, including the feedback loop of integrators, something exposed in Simulink.
+A visual tool can be useful for educational purposes, and a pictorial version of FFACT could be made by an external tool that from a diagram
+it compiles down to the correspondent Haskell code of the HEDSL.
+
+\begin{figure}[ht!]
+  \begin{minipage}{0.45\linewidth}
+     \begin{purespec}
+        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}
+  \end{minipage}
+  \begin{minipage}{0.5\linewidth}
+      \centering
+      \includegraphics[width=0.95\linewidth]{MastersThesis/img/lorenzSimulink}
+  \end{minipage}
+\caption{Comparison of the Lorenz Attractor Model between FFACT and a Simulink implementation~\cite{Simulink}.}
+\label{fig:lorenz-simulink}
+\end{figure}
+
+Figure ~\ref{fig:lorenz-matlab} shows a comparison between FFACT and Matlab. The main differetiating factor between the two
+implementations is in Matlab the system, constructed via a separate lambda function (named \texttt{f} in the example), has the initial
+conditions of the system at \(t_0\) only added when calling the \textit{driver} of the simulation --- the call of the \texttt{ode45}
+function. In FFACT, the interval for the simulation and which numerical method will be used are completely separate of the system's
+description; a \textit{model}. Furthermore, Matlab's description of the system introduces some notation noise via the use of \texttt{vars}, exposing
+implementation details to the system's designer.
+
+\begin{figure}[ht!]
+  \begin{minipage}{0.45\linewidth}
+     \begin{purespec}
+        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}
+  \end{minipage} \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;
+  \begin{minipage}{0.54\linewidth}
+    \begin{matlab}
+       sigma = 10;
+       beta = 8/3;
+       rho = 28;
+       f = @(t,vars) 
+           [sigma*(vars(2) - vars(1)); 
+            vars(1)*(rho - vars(3)) - vars(2); 
+            vars(1)*vars(2) - beta*vars(3)];
+       [t,vars] = ode45(f,[0 50],[1 1 1]);
+    \end{matlab}
+  \end{minipage}
+\caption{Comparison of the Lorenz Attractor Model between FFACT and a Matlab implementation.}
+\label{fig:lorenz-matlab}
+\end{figure}
+
+
+The next comparison is between Mathematica and FFACT, as depicted in Figure~\ref{fig:lorenz-mathematica}.
+Differently than Matlab, Mathematica uses the state variables' names when describing the system. However, just like
+with Matlab, the initial conditions of the system are only provided when calling the driver of the simulation. Moreover,
+there's significant noise in Mathematica's version in comparison to FFACT's version.
+
+\begin{figure}[ht!]
+  \begin{minipage}{0.45\linewidth}
+     \begin{purespec}
+        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}
+  \end{minipage} \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;
+  \begin{minipage}{0.54\linewidth}
+    \begin{mathematica}
+       lorenzModel = NonlinearStateSpaceModel[
+          {{sigma (y - x),
+            x (rho - z) - y,
+            x y - beta z}, {}},
+          {x, y, z},
+          {sigma, rho, beta}];
+       soln[t_] = StateResponse[
+          {lorenzModel, {1, 1, 1}},
+          {10, 28, 8/3},
+          {t, 0, 50}];
+    \end{mathematica}
+  \end{minipage}
+\caption{Comparison of the Lorenz Attractor Model between FFACT and a Mathematica implementation.}
+\label{fig:lorenz-mathematica}
+\end{figure}
+
+Finally, Figure~\ref{fig:lorenz-yampa} contrasts FFACT with \texttt{Yampa}, another HEDSL for time modeling and simulation.
+Although \texttt{Yampa} is more powerful and expressive than FFACT --- \texttt{Yampa} can accomodate hybrid simulations with
+both \textit{discrete} and \textit{continuous} time modeling --- its approach introduces some noise in the Lorenz Attractor model.
+The introduction of \texttt{proc}, \texttt{pre}, \texttt{>>>}, \texttt{imIntegral}, and \texttt{-<} all introduce extra burden on the
+system's designer to describe the system. After learning about \texttt{proc-notation}~\cite{Yampa} and Arrows~\footnote{Arrows \href{https://hackage.haskell.org/package/base-4.18.1.0/docs/Control-Arrow.html}{\textcolor{blue}{hackage documentation}}.}, one can describe more complex systems in Yampa.
+
+\begin{figure}[ht!]
+  \begin{minipage}{0.45\linewidth}
+     \begin{purespec}
+        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}
+  \end{minipage} \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;
+  \hspace{-2.4cm}
+  \begin{minipage}{0.64\linewidth}
+     \begin{purespec}
+        lorenzModel = proc () -> do
+          rec x <- pre >>> imIntegral 1.0 -< sigma*(y - x)
+              y <- pre >>> imIntegral 1.0 -< x*(rho - z) - y
+              z <- pre >>> imIntegral 1.0 -< (x*y) - (beta*z)
+              let sigma = 10.0
+                  rho = 28.0
+                  beta = 8.0 / 3.0
+          returnA -< (x, y, z)
+    \end{purespec}
+  \end{minipage}
+\caption{Comparison of the Lorenz Attractor Model between FFACT and a Yampa implementation.}
+\label{fig:lorenz-yampa}
+\end{figure}
+
 The function \texttt{integ} alone in FFACT ties the recursion knot previously done via the \texttt{computation} and \texttt{cache} fields from the original integrator data type in FACT.
-Hence, a lot of implementation noise of the DSL is kept away from the user --- the designer of the system --- when using FFACT. With this chapter, we addressed
-the third and final concerned explained in chapter 1, \textit{Introduction}. The final chapter, \textit{Conclusion}, will conclude this work, pointing out limitations of the project, as well as future improvements and final thoughts about the project.
+Hence, a lot of implementation noise of the DSL is kept away from the user --- the designer of the system --- when using FFACT. With this Chapter, we addressed
+the third and final concerned explained in Chapter 1, \textit{Introduction}. The final Chapter, \textit{Conclusion}, will conclude this work, pointing out limitations of the project, as well as future improvements and final thoughts about the project.
diff --git a/doc/MastersThesis/Lhs/Implementation.lhs b/doc/MastersThesis/Lhs/Implementation.lhs
index 87df9b2..b966633 100644
--- a/doc/MastersThesis/Lhs/Implementation.lhs
+++ b/doc/MastersThesis/Lhs/Implementation.lhs
@@ -9,21 +9,21 @@ import Control.Monad.Trans.Reader
 \end{code}
 }
 
-This chapter details the next steps to simulate continuous-time behaviours. It starts by enhancing the previously defined \texttt{CT} type by implementing some specific typeclasses. Next, the second core type of the simulation, the \texttt{Integrator} type, will be introduced alongside its functions. These improvements will then be compared to FF-GPAC's basic units, our source of formalism within the project. At the end of the chapter, an implicit recursion will be blended with a lot of effectful operations, making the \texttt{Integrator} type hard to digest. This will be addressed by a guided Lorenz Attractor example in the next chapter, \textit{Execution Walkthrough}.
+This Chapter details the next steps to simulate continuous-time behaviours using more advanced Haskell concepts, like typeclasses~\footnote{\texttt{Classes in Haskell:} \href{https://www.haskell.org/tutorial/classes.html}{\textcolor{blue}{reference}}.}. It starts by enhancing the previously defined \texttt{CT} type by implementing some specific typeclasses. Next, the second core type of the simulation, the \texttt{Integrator} type, will be introduced alongside its functions. These improvements will then be compared to FF-GPAC's basic units, our source of formalism within the project. At the end of the Chapter, an implicit recursion will be blended with a lot of effectful operations, making the \texttt{Integrator} type hard to digest. This will be addressed by a guided Lorenz Attractor example in the next Chapter, \textit{Execution Walkthrough}.
 
 \section{Uplifting the CT Type}
 \label{sec:typeclasses}
 
-The \texttt{CT} type needs \textbf{algebraic operations} to be better manipulated, i.e., useful operations that can be applied to the type preserving its external structure. These procedures are algebraic laws or properties that enhance the capabilities of the proposed function type wrapped by a \texttt{CT} shell. Towards this goal, a few typeclasses need to be implemented.
+The \texttt{CT} type needs \textit{algebraic operations} to be better manipulated, i.e., useful operations that can be applied to the type preserving its external structure. These procedures are algebraic laws or properties that enhance the capabilities of the proposed function type wrapped by a \texttt{CT} shell. Towards this goal, a few typeclasses need to be implemented.
 
 Across the spectrum of available typeclasses in Haskell, we are interested in the ones that allow data manipulation with a single or multiple \texttt{CT} and provide mathematical operations.
 To address the former group of operations, the typeclasses \texttt{Functor}, \texttt{Applicative}, \texttt{Monad} and \texttt{MonadIO} will be implemented. The later group of properties is dedicated to provide mathematical operations, such as $+$ and $\times$, and it can be acquired by implementing the typeclasses \texttt{Num}, \texttt{Fractional}, and \texttt{Floating}.
 
-The typeclasses \texttt{Functor}, \texttt{Applicative} and \texttt{Monad} are all \textbf{lifting} operations, meaning that they allow functions to be lifted or involved by the chosen type. While they differ \textbf{which} functions will be lifted, i.e., each one of them lift a function with a different type signature, they share the intuition that these functions will be interacting with the \texttt{CT} type. This perspective is crucial for a practical understanding of these patterns. A function with a certain \textbf{shape} and details will be lifted using one of those typeclasses and their respective operators.
+The typeclasses \texttt{Functor}, \texttt{Applicative} and \texttt{Monad} are all \textit{lifting} operations, meaning that they allow functions to be lifted or involved by the chosen type. While they differ \textit{which} functions will be lifted, i.e., each one of them lift a function with a different type signature, they share the intuition that these functions will be interacting with the \texttt{CT} type. This perspective is crucial for a practical understanding of these patterns. A function with a certain \textit{shape} and details will be lifted using one of those typeclasses and their respective operators.
 
 Given that the \texttt{CT} type is just a type alias with \texttt{ReaderT} as the under the hood type, all of these lift operations are already provided in Haskell's libraries.
 However, it is still valuable to present their implementation to completely understand how the final look for the DSL will look like. Hence, the following implementations will
-assume we \textbf{aren't} use CT as the type alias and instead we will be showing the implementations as if we are using the definition used previously~\cite{Lemos2022} for the
+assume we \textit{aren't} using CT as the type alias and instead we will be showing the implementations as if we are using the definition used previously~\cite{Lemos2022} for the
 \texttt{CT} type:
 
 \begin{purespec}
@@ -46,7 +46,7 @@ instance Functor CT where
 \label{fig:functor}
 \end{figure}
 
-The next typeclass, \texttt{Applicative}, deals with functions that are inside the \texttt{CT} type. When implemented (again, referring to the non-type-alias version), this algebraic operation lifts this internal function, wrapped by the type of choice, applying the \textbf{external} type to its \textbf{internal} members, thus generating again a function with the signature \texttt{CT a -> CT b}. The minimum requirements for this typeclass is the function \textit{pure}, a function responsible for wrapping any value with the \texttt{CT} wrapper, and the \texttt{<*>} operator, which does the aforementioned interaction between the internal values with the outer shell. The implementation of this typeclass is presented in the code bellow, in which the dependency \texttt{df} has the signature \texttt{CT (a -> b)} and its internal function \texttt{a -> b} is being lifted to the \texttt{CT} type. Figure \ref{fig:applicative} illustrates the described lifting with \texttt{Applicative}.
+The next typeclass, \texttt{Applicative}, deals with functions that are inside the \texttt{CT} type. When implemented (again, referring to the non-type-alias version), this algebraic operation lifts this internal function, wrapped by the type of choice, applying the \textit{external} type to its \textit{internal} members, thus generating again a function with the signature \texttt{CT a -> CT b}. The minimum requirements for this typeclass is the function \textit{pure}, a function responsible for wrapping any value with the \texttt{CT} wrapper, and the \texttt{<*>} operator, which does the aforementioned interaction between the internal values with the outer shell. The implementation of this typeclass has the dependency \texttt{df} has the signature \texttt{CT (a -> b)} and its internal function \texttt{a -> b} is being lifted to the \texttt{CT} type. Figure \ref{fig:applicative} illustrates the described lifting with \texttt{Applicative}.
 
 \begin{figure}[ht!]
 \begin{minipage}{.55\textwidth}
@@ -72,7 +72,7 @@ appComposition (CT df) (CT da)
 \label{fig:applicative}
 \end{figure}
 
-The third and final lifting is the \texttt{Monad} typeclass. In this case, the function being lifted \textbf{generates} structure as the outcome, although its dependency is a pure value. As Figure \ref{fig:monad} portrays, a function with the signature \texttt{a -> CT b} can be lifted to the signature \texttt{CT a -> CT b} by using the \texttt{Monad} typeclass. This new operation for lifting, so-called \textit{bind}, is written below, alongside the \textit{return} function, which is the same \textit{pure} function from the \texttt{Applicative} typeclass. Together, these two functions represent the minimum requirements of the \texttt{Monad} typeclass. Figure \ref{fig:monad} illustrates the aforementioned scenario.
+The third and final lifting is the \texttt{Monad} typeclass. In this case, the function being lifted \textit{generates} structure as the outcome, although its dependency is a pure value. As Figure \ref{fig:monad} portrays, a function with the signature \texttt{a -> CT b} can be lifted to the signature \texttt{CT a -> CT b} by using the \texttt{Monad} typeclass. This new operation for lifting, so-called \textit{bind}, is written below, alongside the \textit{return} function, which is the same \textit{pure} function from the \texttt{Applicative} typeclass. Together, these two functions represent the minimum requirements of the \texttt{Monad} typeclass. Figure \ref{fig:monad} illustrates the aforementioned scenario.
 
 \begin{figure}[ht!]
 \begin{minipage}{.55\textwidth}
@@ -98,7 +98,7 @@ bind k (CT m)
 \label{fig:monad}
 \end{figure}
 
-Aside from lifting operations, the final typeclass related to data manipulation is the \texttt{MonadIO} typeclass. It comprises only one function, \textit{liftIO}, and its purpose is to change the structure that is wrapping the value, going from an \texttt{IO} outer shell to the monad of interest, \texttt{CT} in this case. The usefulness of this typeclass will be more clear in the next topic, section \ref{sec:integrator}. The implementation is bellow, alongside its visual representation in Figure \ref{fig:monadIO}. Once again, consider the explicit
+Aside from lifting operations, the final typeclass related to data manipulation is the \texttt{MonadIO} typeclass. It comprises only one function, \textit{liftIO}, and its purpose is to change the structure that is wrapping the value, going from an \texttt{IO} outer shell to the monad of interest, \texttt{CT} in this case. The usefulness of this typeclass will be more clear in the next topic, Section \ref{sec:integrator}. The implementation follows, alongside its visual representation in Figure \ref{fig:monadIO}. Once again, consider the explicit
 definition for the \texttt{CT} type instead of the type alias.
 
 \begin{figure}[ht!]
@@ -117,8 +117,8 @@ instance MonadIO CT where
 \label{fig:monadIO}
 \end{figure}
 
-Finally, there are the typeclasses related to mathematical operations. The typeclasses \texttt{Num}, \texttt{Fractional} and \texttt{Floating} provide unary and binary numerical operations, such as arithmetic operations and trigonometric functions. However, because we want to use them with the \texttt{CT} type, their implementation involve lifting. Further, the \texttt{Functor} and \texttt{Applicative} typeclasses allow us to execute this lifting, since they are designed for this purpose. The code bellow depicts the implementation for unary and binary operations, which are used in the requirements for those typeclasses. As a side note, to make these implementations possible for the type-aliased version of the \texttt{CT} type, it is
-required to use a compiler extension \texttt{FlexibleInstances}. Further, the same operations below can be used as internal helpers for both versions of the type:
+Finally, there are the typeclasses related to mathematical operations. The typeclasses \texttt{Num}, \texttt{Fractional} and \texttt{Floating} provide unary and binary numerical operations, such as arithmetic operations and trigonometric functions. However, because we want to use them with the \texttt{CT} type, their implementation involve lifting. Further, the \texttt{Functor} and \texttt{Applicative} typeclasses allow us to execute this lifting, since they are designed for this purpose. The following code depicts the implementation for unary and binary operations, which are used in the requirements for those typeclasses. As a side note, to make these implementations possible for the type-aliased version of the \texttt{CT} type, it is
+required to use a compiler extension \texttt{FlexibleInstances}. Further, the same operations can be used as internal helpers for both versions of the type:
 
 \begin{purespec}
 unaryOP :: (a -> b) -> CT a -> CT b
@@ -130,36 +130,36 @@ binaryOP func da db = (fmap func da) <*> db
 
 \section{GPAC Bind I: CT}
 
-After these improvements in the \texttt{CT} type, it is possible to map some of them to FF-GPAC's concepts. As we will see shortly, the implemented numerical typeclasses, when combined with the lifting typeclasses (\texttt{Functor}, \texttt{Applicative}, \texttt{Monad}), express 3 out of 4 FF-GPAC's basic circuits presented in Figure \ref{fig:gpacBasic} in the previous chapter.
+After these improvements in the \texttt{CT} type, it is possible to map some of them to FF-GPAC's concepts. As we will see shortly, the implemented numerical typeclasses, when combined with the lifting typeclasses (\texttt{Functor}, \texttt{Applicative}, \texttt{Monad}), express 3 out of 4 FF-GPAC's basic circuits presented in Figure \ref{fig:gpacBasic} in the previous Chapter.
 
 First and foremost, all FF-GPAC units receive \textit{time} as an available input to compute. The \texttt{CT} type represents continuous physical dynamics~\cite{LeeModeling}, which means that it portrays a function from time to physical output. Hence, it already has time embedded into its definition; a record with type \texttt{Parameters} is received as a dependency to obtain the final result at that moment. Furthermore, it remains to model the FF-GPAC's black boxes and the composition rules that bind them together.
 
-The simplest unit of all, \texttt{Constant Unit}, can be achieved via the implementation of the \texttt{Applicative} and \texttt{Num} typeclasses. First, this unit needs to receive the time of simulation at that point, which is an granted by the \texttt{CT} type. Next, it needs to return a constant value $k$ for all moments in time. The \texttt{Num} given the \texttt{CT} type the option of using number representations, such as the types \texttt{Int}, \texttt{Integer}, \texttt{Float} and \texttt{Double}. Further, the \texttt{Applicative} typeclass can lift those number-related functions to the desired type by using the \textit{pure} function.
+The simplest unit of all, \texttt{Constant Unit}, can be achieved via the implementation of the \texttt{Applicative} and \texttt{Num} typeclasses. First, this unit needs to receive the time of simulation at that point, which is granted by the \texttt{CT} type. Next, it needs to return a constant value $k$ for all moments in time. The \texttt{Num} given the \texttt{CT} type the option of using number representations, such as the types \texttt{Int}, \texttt{Integer}, \texttt{Float} and \texttt{Double}. Further, the \texttt{Applicative} typeclass can lift those number-related functions to the desired type by using the \textit{pure} function.
 
-Arithmetic basic units, such as the \texttt{Adder Unit} and the \texttt{Multiplier Unit}, are being modeled by the \texttt{Functor}, \texttt{Applicative} and \texttt{Num} typeclasses. Those two units use binary operations with physical signals. As demonstrated in the previous section, the combination of numerical and lifting typeclasses let us to model such operations. Figure \ref{fig:gpacBind1} shows FF-GPAC's analog circuits alongside their \texttt{FACT} counterparts. The forth unit and the composition rules will be mapped after describing the second main type of \texttt{FACT}: the \texttt{Integrator} type.
+Arithmetic basic units, such as the \texttt{Adder Unit} and the \texttt{Multiplier Unit}, are being modeled by the \texttt{Functor}, \texttt{Applicative} and \texttt{Num} typeclasses. Those two units use binary operations with physical signals. As demonstrated in the previous Section, the combination of numerical and lifting typeclasses let us to model such operations. Figure \ref{fig:gpacBind1} shows FF-GPAC's analog circuits alongside their \texttt{FACT} counterparts. The forth unit and the composition rules will be mapped after describing the second main type of \texttt{FACT}: the \texttt{Integrator} type.
 
 \figuraBib{GPACBind1}{The ability of lifting numerical values to the \texttt{CT} type resembles three FF-GPAC analog circuits: \texttt{Constant}, \texttt{Adder} and \texttt{Multiplier}}{}{fig:gpacBind1}{width=.9\textwidth}%
 
 \section{Exploiting Impurity}
 \label{sec:integrator}
 
-The \texttt{CT} type directly interacts with a second type that intensively explores \textbf{side effects}. The notion of a side effect correlates to changing a \textbf{state}, i.e., if you see a computer program as a state machine, an operation that goes beyond returning a value --- it has an observable interference somewhere else --- is called a side effect operation or an \textbf{impure} functionality. Examples of common use cases goes from modifying memory regions to performing input-output procedures via system-calls. The nature of purity comes from the mathematical domain, in which a function is a procedure that is deterministic, meaning that the output value is always the same if the same input is provided --- a false assumption when programming with side effects. An example of an imaginary state machine can be viewed in Figure \ref{fig:stateMachine}.
+The \texttt{CT} type directly interacts with a second type that intensively explores \textit{side effects}. The notion of a side effect correlates to changing a \textit{state}, i.e., if you see a computer program as a state machine, an operation that goes beyond returning a value --- it has an observable interference somewhere else --- is called a side effect operation or an \textit{impure} functionality. Examples of common use cases goes from modifying memory regions to performing input-output procedures via system-calls. The nature of purity comes from the mathematical domain, in which a function is a procedure that is deterministic, meaning that the output value is always the same if the same input is provided --- a false assumption when programming with side effects. An example of an imaginary state machine can be viewed in Figure \ref{fig:stateMachine}.
 
 \begin{figure}[ht!]
   \begin{minipage}[c]{0.67\textwidth}
     \includegraphics[width=0.95\linewidth]{MastersThesis/img/StateMachine}
   \end{minipage}\hfill
   \begin{minipage}[c]{0.32\textwidth}
-    \caption{State Machines are a common abstraction in computer science due to its easy mapping between function calls and states. Memory regions and peripherals are embedded with the idea of a state, not only pure functions. Further, side effects can even act as the trigger to move from one state to another, meaning that executing a simple function can do more than return a value. Its internal guts can significantly modify the state machine.}
+    \caption[Example of a State Machine]{State Machines are a common abstraction in computer science due to its easy mapping between function calls and states. Memory regions and peripherals are embedded with the idea of a state, not only pure functions. Further, side effects can even act as the trigger to move from one state to another, meaning that executing a simple function can do more than return a value. Its internal guts can significantly modify the state machine.}
 \label{fig:stateMachine}
   \end{minipage}
 \end{figure}
 
-In low-level and imperative languages, such as C, Fortran, Zig, Rust, impurity is present across the program and can be easily and naturally added via \textbf{pointers} --- addresses to memory regions where values, or even other pointers, can be stored. In contrast, functional programming languages advocate to a more explicit use of such aspect, given that it prioritizes pure and mathematical functions instead of allowing the developer to mix these two facets. So, the feature is still available but the developer has to take extra effort to add an effectful function into the program, clearly separating these two different styles of programming.
+In low-level and imperative languages, such as C, Fortran, Zig, Rust, impurity is present across the program and can be easily and naturally added via \textit{pointers} --- addresses to memory regions where values, or even other pointers, can be stored. In contrast, functional programming languages advocate to a more explicit use of such aspect, given that it prioritizes pure and mathematical functions instead of allowing the developer to mix these two facets. So, the feature is still available but the developer has to take extra effort to add an effectful function into the program, clearly separating these two different styles of programming.
 
-The second core type of the present work, the \texttt{Integrator}, is based on this idea of side effect operations, manipulating data directly in memory, always consulting and modifying data in the impure world. Foremost, it represents a differential equation, as explained in chapter 2, \textit{Design Philosophy} section \ref{sec:diff}, meaning that the \texttt{Integrator} type models the calculation of an \textbf{integral}. It accomplishes this task by driving the numerical algorithms of a given solver method, implying that this is where the \textit{operational} semantics of our DSL reside.
+The second core type of the present work, the \texttt{Integrator}, is based on this idea of side effect operations, manipulating data directly in memory, always consulting and modifying data in the impure world. Foremost, it represents a differential equation, as explained in Chapter 2, \textit{Design Philosophy} Section \ref{sec:diff}, meaning that the \texttt{Integrator} type models the calculation of an \textit{integral}. It accomplishes this task by driving the numerical algorithms of a given solver method, implying that this is where the \textit{operational} semantics of our DSL reside.
 
-With this in mind, the \texttt{Integrator} type is responsible for executing a given solver method to calculate a given integral. This type comprises the initial value of the system, i.e., the value of a given function at time $t_0$, and a pointer to a memory region for future use, called \texttt{computation}. In Haskell, something similar to a pointer and memory allocation can be made by using the \texttt{IORef} type. This memory region is being allocated to be used with the type \texttt{CT Double}. Also, the initial value is also represented by \texttt{CT Double}, and the initial condition can be lifted to this type because the typeclass \texttt{Num} is implemented (section \ref{sec:typeclasses}). It is worth noticing that these pointers are pointing to functions or \textbf{computations} and not to double precision values.
+With this in mind, the \texttt{Integrator} type is responsible for executing a given solver method to calculate a given integral. This type comprises the initial value of the system, i.e., the value of a given function at time $t_0$, and a pointer to a memory region for future use, called \texttt{computation}. In Haskell, something similar to a pointer and memory allocation can be made by using the \texttt{IORef} type. This memory region is being allocated to be used with the type \texttt{CT Double}. Also, the initial value is also represented by \texttt{CT Double}, and the initial condition can be lifted to this type because the typeclass \texttt{Num} is implemented (Section \ref{sec:typeclasses}). It is worth noticing that these pointers are pointing to functions or \textit{computations} and not to double precision values.
 
 \begin{purespec}
 data Integrator = Integrator { initial     :: CT Double,
@@ -167,7 +167,7 @@ data Integrator = Integrator { initial     :: CT Double,
                              }
 \end{purespec}
 
-There are three functions that involve the \texttt{Integrator} and the \texttt{CT} types together: the function \textit{createInteg}, responsible for allocating the memory that the pointer will pointer to, \textit{readInteg}, letting us to read from the pointer, and \textit{updateInteg}, a function that alters the content of the region being pointed. In summary, these functions allow us to create, read and update data from that region, if we have the pointer on-hand. All functions related to the integrator use what's known as \texttt{do-notation}, a syntax sugar of the \texttt{Monad} typeclass for the bind operator. The code bellow is the implementation of the \textit{createInteg} function, which creates an integrator:
+There are three functions that involve the \texttt{Integrator} and the \texttt{CT} types together: the function \textit{createInteg}, responsible for allocating the memory that the pointer will point to, \textit{readInteg}, letting us to read from the pointer, and \textit{updateInteg}, a function that alters the content of the region being pointed. In summary, these functions allow us to create, read and update data from that region, if we have the pointer on-hand. All functions related to the integrator use what's known as \texttt{do-notation}, a syntax sugar of the \texttt{Monad} typeclass for the bind operator. The following code is the implementation of the \textit{createInteg} function, which creates an integrator:
 
 \begin{spec}
 createInteg :: CT Double -> CT Integrator
@@ -178,9 +178,9 @@ createInteg i = do
   return integ
 \end{spec}
 
-The first step to create an integrator is to manage the initial value, which is a function with the type \texttt{Parameters -> IO Double} wrapped in \texttt{CT} via the \texttt{ReaderT}. After acquiring a given initial value \texttt{i}, the integrator needs to assure that any given parameter record is the beginning of the computation process, i.e., it starts from $t_0$. The \texttt{initialize} function (line 3) fulfills this role, doing a reset in \texttt{time}, \texttt{iteration} and \texttt{stage} in a given parameter record. This is necessary because all the implemented solvers presumes \textbf{sequential steps}, starting from the initial condition. So, in order to not allow this error-prone behaviour, the integrator makes sure that the initial state of the system is configured correctly. The next step is to allocate memory to this computation --- a procedure that will get you the initial value, while modifying the parameter record dependency of the function accordingly.
+The first step to create an integrator is to manage the initial value, which is a function with the type \texttt{Parameters -> IO Double} wrapped in \texttt{CT} via the \texttt{ReaderT}. After acquiring a given initial value \texttt{i}, the integrator needs to assure that any given parameter record is the beginning of the computation process, i.e., it starts from $t_0$. The \texttt{initialize} function (line 3) fulfills this role, doing a reset in \texttt{time}, \texttt{iteration} and \texttt{stage} in a given parameter record. This is necessary because all the implemented solvers presumes \textit{sequential steps}, starting from the initial condition. So, in order to not allow this error-prone behaviour, the integrator makes sure that the initial state of the system is configured correctly. The next step is to allocate memory to this computation --- a procedure that will get you the initial value, while modifying the parameter record dependency of the function accordingly.
 
-The following stage is to do a type conversion, given that in order to create the \texttt{Integrator} record, it is necessary to have the type \texttt{IORef (CT Double)}. At first glance, this can seem to be an issue because the result of the \textit{newIORef} function is wrapped with the \texttt{IO} monad~\footnote{\label{foot:IORef} \texttt{IORef} \href{https://hackage.haskell.org/package/base-4.16.1.0/docs/Data-IORef.html}{\textcolor{blue}{hackage documentation}}.}. This conversion is the reason why the \texttt{IO} monad is being used in the implementation, and hence forced us to implement the typeclass \texttt{MonadIO}. The function \texttt{liftIO} (liine 3) is capable of removing the \texttt{IO} wrapper and adding an arbitrary monad in its place, \texttt{CT} in this case. So, after line 3 the \texttt{comp} value has the desired \texttt{CT} type. The remaining step of this creation process is to construct the integrator itself by building up the record with the correct fields, e.g., the CT version of the initial value and the pointer to the constructed computation written in memory (lines 4 and 5).
+The following stage is to do a type conversion, given that in order to create the \texttt{Integrator} record, it is necessary to have the type \texttt{IORef (CT Double)}. At first glance, this seems to be an issue because the result of the \textit{newIORef} function is wrapped with the \texttt{IO} monad~\footnote{\label{foot:IORef} \texttt{IORef} \href{https://hackage.haskell.org/package/base-4.16.1.0/docs/Data-IORef.html}{\textcolor{blue}{hackage documentation}}.}. This conversion is the reason why the \texttt{IO} monad is being used in the implementation, and hence forced us to implement the typeclass \texttt{MonadIO}. The function \texttt{liftIO} (liine 3) is capable of removing the \texttt{IO} wrapper and adding an arbitrary monad in its place, \texttt{CT} in this case. So, after line 3 the \texttt{comp} value has the desired \texttt{CT} type. The remaining step of this creation process is to construct the integrator itself by building up the record with the correct fields, e.g., the CT version of the initial value and the pointer to the constructed computation written in memory (lines 4 and 5).
 
 \begin{purespec}
 readInteg :: Integrator -> CT Double
@@ -189,7 +189,7 @@ readInteg = join . liftIO . readIORef . computation
 
 To read the content of this region, it is necessary to provide the integrator to the $readInteg$ function. Its implementation is straightforward: build a new \texttt{CT} that applies the given record of \texttt{Parameters} to what's being stored in the region. This is accomplished by using the function \texttt{join} with the $readIORef$ function~\footref{foot:IORef}.
 
-Finally, the function \textit{updateInteg} is a side-effect-only function that changes \textbf{which computation} will be used by the integrator. It is worth noticing that after the creation of the integrator, the \texttt{computation} pointer is addressing a simple and, initially, useless computation: given an arbitrary record of \texttt{Parameters}, it will fix it to assure it is starting at $t_0$, and it will return the initial value in form of a \texttt{CT Double}. To update this behaviour, the \textit{updateInteg} change the content being pointed by the integrator's pointer:
+Finally, the function \textit{updateInteg} is a side-effect-only function that changes \textit{which computation} will be used by the integrator. It is worth noticing that after the creation of the integrator, the \texttt{computation} pointer is addressing a simple and, initially, useless computation: given an arbitrary record of \texttt{Parameters}, it will fix it to assure it is starting at $t_0$, and it will return the initial value in form of a \texttt{CT Double}. To update this behaviour, the \textit{updateInteg} change the content being pointed by the integrator's pointer:
 
 \begin{spec}
 updateInteg :: Integrator -> CT Double -> CT ()
@@ -206,18 +206,18 @@ updateInteg integ diff = do
 \end{spec}
 
 In the beginning of the function (line 3), we extract the initial value from the integrator, so-called \texttt{i}. Next (line 4 onward),
-create a new computation, so-called \texttt{z} --- a function wrapped in the \texttt{CT} type that receives a \texttt{Parameters} record and computes the result based on the solving method.
-Because this computation needs to do lookups on some configuration values, we use the function \texttt{ask} (line 5) from \texttt{ReaderT} to get our environment values; this case
-a value of type \texttt{Parameters}. Later on, the follow-up step is to build a copy of the \textbf{same process} being pointed by the \texttt{computation} pointer (line 6).
-Finally, after checking the chosen solver (line 7), it is executed one iteration of the process by calling \textit{integEuler}, or \textit{integRK2} or \textit{integRK4}. After line 10, this entire process \texttt{z} is being pointed by the \texttt{computation} pointer, being done by the $writeIORef$ function~\footref{foot:IORef}. It may seem confusing that inside \texttt{z} we are \textbf{reading} what is being pointed and later, on the last line of \textit{updateInteg}, this is being used on the final line to update that same pointer. This is necessary, as it will be explained in the next chapter \textit{Execution Walkthrough}, to allow the use of an \textbf{implicit recursion} to assure the sequential aspect needed by the solvers. For now, the core idea is this: the \textit{updateInteg} function alters the \textbf{future} computations; it rewrites which procedure will be pointed by the \texttt{computation} pointer. This new procedure, which we called \texttt{z}, creates an intermediate computation, \texttt{whatToDo} (line 6), that \textbf{reads} what this pointer is addressing, which is \texttt{z} itself.
+we create a new computation, so-called \texttt{z} --- a function wrapped in the \texttt{CT} type that receives a \texttt{Parameters} record and computes the result based on the solving method.
+Because this computation needs to do lookups on some configuration values, we use the function \texttt{ask} (line 5) from \texttt{ReaderT} to get our environment values; in this case
+a value of type \texttt{Parameters}. Later on, the follow-up step is to build a copy of the \textit{same process} being pointed by the \texttt{computation} pointer (line 6).
+Finally, after checking the chosen solver (line 7), it is executed one iteration of the process by calling \textit{integEuler}, or \textit{integRK2} or \textit{integRK4}. After line 10, this entire process \texttt{z} is being pointed by the \texttt{computation} pointer, being done by the $writeIORef$ function~\footref{foot:IORef}. It may seem confusing that inside \texttt{z} we are \textit{reading} what is being pointed and later, on the last line of \textit{updateInteg}, this is being used on the final line to update that same pointer. This is necessary, as it will be explained in the next Chapter \textit{Execution Walkthrough}, to allow the use of an \textit{implicit recursion} to assure the sequential aspect needed by the solvers. For now, the core idea is this: the \textit{updateInteg} function alters the \textit{future} computations; it rewrites which procedure will be pointed by the \texttt{computation} pointer. This new procedure, which we called \texttt{z}, creates an intermediate computation, \texttt{whatToDo} (line 6), that \textit{reads} what this pointer is addressing, which is \texttt{z} itself.
 
-Initially, this strange behaviour may cause the idea that this computation will never halt. However, Haskell's \textit{laziness} assures that a given computation will not be computed unless it is necessary to continue execution and this is \textbf{not} the case in the current stage, given that we are just setting the environment in the memory to further calculate the solution of the system.
+Initially, this strange behaviour may cause the idea that this computation will never halt. However, Haskell's \textit{laziness} assures that a given computation will not be computed unless it is necessary to continue execution and this is \textit{not} the case in the current stage, given that we are just setting the environment in the memory to further calculate the solution of the system.
 
 \section{GPAC Bind II: Integrator}
 
-The \texttt{Integrator} type introduced in the previous section corresponds to FF-GPAC's forth and final basic unit, the integrator. The analog version of the integrator used in FF-GPAC had the goal of using physical systems (shafts and gears) that obeys the same mathematical relations that control other physical or technical phenomenon under investigation~\cite{Graca2004}. In contrast, the integrator modeled in {FACT} uses pointers in a digital computer that point to iteration-based algorithms that can approximate the solution of the problem at a requested moment $t$ in time.
+The \texttt{Integrator} type introduced in the previous Section corresponds to FF-GPAC's forth and final basic unit, the integrator. The analog version of the integrator used in FF-GPAC had the goal of using physical systems (shafts and gears) that obeys the same mathematical relations that control other physical or technical phenomenon under investigation~\cite{Graca2004}. In contrast, the integrator modeled in {FACT} uses pointers in a digital computer that point to iteration-based algorithms that can approximate the solution of the problem at a requested moment $t$ in time.
 
-Lastly, there are the composition rules in FF-GPAC --- constraints that describe how the units can be interconnected. The following are the same composition rules presented in chapter 2, \textit{Design Philosophy}, section \ref{sec:gpac}:
+Lastly, there are the composition rules in FF-GPAC --- constraints that describe how the units can be interconnected. The following are the same composition rules presented in Chapter 2, \textit{Design Philosophy}, Section \ref{sec:gpac}:
 
 \begin{enumerate}
   \item An input of a polynomial circuit should be the input $t$ or the output of an integrator. Feedback can only be done from the output of integrators to inputs of polynomial circuits.
@@ -226,11 +226,11 @@ Lastly, there are the composition rules in FF-GPAC --- constraints that describe
   \item Each variable of integration of an integrator is the input \textit{t}.
 \end{enumerate}
 
-The preceding rules include defining connections with polynomial circuits --- an acyclic circuit composed only by constant functions, adders and multipliers. These special circuits are already being modeled in \texttt{FACT} by the \texttt{CT} type with a set of typeclasses, as explained in the previous section about GPAC. The \textbf{integrator functions}, e.g., \textit{readInteg} and \textit{updateInteg}, represent the composition rules.
+The preceding rules include defining connections with polynomial circuits --- an acyclic circuit composed only by constant functions, adders and multipliers. These special circuits are already being modeled in \texttt{FACT} by the \texttt{CT} type with a set of typeclasses, as explained in the previous Section about GPAC. The \textit{integrator functions}, e.g., \textit{readInteg} and \textit{updateInteg}, represent the composition rules.
 
-Going back to the type signature of the \textit{updateInteg}, \texttt{Integrator -> CT Double -> CT ()}, we can interpret this function as a \textbf{wiring} operation. This function connects as an input of the integrator, represented by the \textbf{Integrator} type, the output of a polynomial circuit, represented by the value with \texttt{CT Double} type. Because the operation is just setting up the connections between the two, the functions ends with the type \texttt{CT ()}.
+Going back to the type signature of the \textit{updateInteg}, \texttt{Integrator -> CT Double -> CT ()}, we can interpret this function as a \textit{wiring} operation. This function connects as an input of the integrator, represented by the \textit{Integrator} type, the output of a polynomial circuit, represented by the value with \texttt{CT Double} type. Because the operation is just setting up the connections between the two, the functions ends with the type \texttt{CT ()}.
 
-A polynomial circuit can have the time $t$ or an output of another integrator as inputs, with restricted feedback (rule 1). This rule is being matched by the following: the \texttt{CT} type makes time available to the circuits, and the \textit{readInteg} function allows us to read the output of another integrators. The second rule, related to multiple inputs in the combinational circuit, is being followed because we can link inputs using arithmetic operations, feature provided by the \texttt{Num} typeclass. Moreover, because the sole purpose of \texttt{FACT} is to solve differential equations, we are \textbf{only} interested in circuits that calculates integrals, meaning that it is guaranteed that the integrand of the integrator will always be the output of a polynomial unit (rule 3), as we saw with the type signature of the \textit{updateInteg} function. The forth rule is also being attended it, given that the solver methods inside the \textit{updateInteg} function always calculate the integral in respect to the time variable. Figure \ref{fig:gpacBind2} summarizes these last mappings between the implementation, and FF-GPAC's integrator and rules of composition.
+A polynomial circuit can have the time $t$ or an output of another integrator as inputs, with restricted feedback (rule 1). This rule is being matched by the following: the \texttt{CT} type makes time available to the circuits, and the \textit{readInteg} function allows us to read the output of another integrators. The second rule, related to multiple inputs in the combinational circuit, is being followed because we can link inputs using arithmetic operations, feature provided by the \texttt{Num} typeclass. Moreover, because the sole purpose of \texttt{FACT} is to solve differential equations, we are \textit{only} interested in circuits that calculates integrals, meaning that it is guaranteed that the integrand of the integrator will always be the output of a polynomial unit (rule 3), as we saw with the type signature of the \textit{updateInteg} function. The fourth rule is also being attended it, given that the solver methods inside the \textit{updateInteg} function always calculate the integral in respect to the time variable. Figure \ref{fig:gpacBind2} summarizes these last mappings between the implementation, and FF-GPAC's integrator and rules of composition.
 
 \figuraBib{GPACBind2}{The integrator functions attend the rules of composition of FF-GPAC, whilst the \texttt{CT} and \texttt{Integrator} types match the four basic units}{}{fig:gpacBind2}{width=.9\textwidth}%
 
@@ -239,15 +239,15 @@ A polynomial circuit can have the time $t$ or an output of another integrator as
 
 \section{Using Recursion to solve Math}
 
-The remaining topic of this chapter is to describe in detail how the solver methods are being implemented. There are three solvers currently implemented:
+The remaining topic of this Chapter is to describe in detail how the solver methods are being implemented. There are three solvers currently implemented:
 
 \begin{itemize}
 \item Euler Method or First-order Runge-Kutta Method
 \item Second-order Runge-Kutta Method
-\item Forth-order Runge-Kutta Method
+\item Fourth-order Runge-Kutta Method
 \end{itemize}
 
-To explain how the solvers work and their nuances, it is useful to go into the implementation of the simplest one --- the Euler method. However, the implementation of the solvers use a slightly different function for the next step or iteration in comparison to the one explained in chapter 2. Hence, it is worthwhile to remember how this method originally iterates in terms of its mathematical description and compare it to the new function. From equation \ref{eq:nextStep}, we can obtain a different function to next step, by subtracting the index from both sides of the equation:
+To explain how the solvers work and their nuances, it is useful to go into the implementation of the simplest one --- the Euler method. However, the implementation of the solvers use a slightly different function for the next step or iteration in comparison to the one explained in Chapter 2. Hence, it is worthwhile to remember how this method originally iterates in terms of its mathematical description and compare it to the new function. From equation \ref{eq:nextStep}, we can obtain a different function to next step, by subtracting the index from both sides of the equation:
 
 \begin{equation}
 y_{n+1} = y_n + hf(t_n,y_n) \rightarrow y_n = y_{n-1} + hf(t_{n-1}, y_{n-1})
@@ -300,7 +300,7 @@ integEuler diff init compute = do
 \end{code}
 }
 
-On line 5, it is possible to see which functions are available in order to execute a step in the solver. The dependency \texttt{diff} is the representation of the differential equation itself. The initial value, $y(t_0)$, can be obtained by applying any \texttt{Parameters} record to the \texttt{init} dependency function. The next dependency, \texttt{compute}, execute everything previously defined in \textit{updateInteg}; thus effectively executing a new step using the \textbf{same} solver. The result of \texttt{compute} depends on which parametric record will be applied, meaning that we call a new and different solver step in the current one, potentially building a chain of solver step calls. This mechanism --- of executing again a solver step, inside the solver itself --- is the aforementioned implicit recursion, described in the earlier section. By changing the \texttt{ps} record, originally obtained via the \texttt{ReaderT} with the \texttt{ask} function, to the \textbf{previous} moment and iteration with the solver starting from initial stage, it is guaranteed that for any step the previous one can be computed, a requirement when using numerical methods.
+On line 5, it is possible to see which functions are available in order to execute a step in the solver. The dependency \texttt{diff} is the representation of the differential equation itself. The initial value, $y(t_0)$, can be obtained by applying any \texttt{Parameters} record to the \texttt{init} dependency function. The next dependency, \texttt{compute}, execute everything previously defined in \textit{updateInteg}; thus effectively executing a new step using the \textit{same} solver. The result of \texttt{compute} depends on which parametric record will be applied, meaning that we call a new and different solver step in the current one, potentially building a chain of solver step calls. This mechanism --- of executing again a solver step, inside the solver itself --- is the aforementioned implicit recursion, described in the earlier Section. By changing the \texttt{ps} record, originally obtained via the \texttt{ReaderT} with the \texttt{ask} function, to the \textit{previous} moment and iteration with the solver starting from initial stage, it is guaranteed that for any step the previous one can be computed, a requirement when using numerical methods.
 
 With this in mind, the solver function treats the initial value case as the base case of the recursion, whilst it treats normally the remaining ones (line 9). In the base case (lines 7 and 8), the outcome is obtained by just returning the continuous machine with the initial value. Otherwise, it is necessary to know the result from the previous iteration in order to generate the current one. To address this requirement, the solver builds another parametric record (lines 10 to 13) and call another solver step (line 14). Also, it calculates the value from applying this record to \texttt{diff} (line 15), the differential equation. These machines, based on \texttt{compute} and \texttt{diff}, need to be modified with a value of type \texttt{Parameters}
 containing the previous iteration (so-called \texttt{psy} in the code). Hence, the function \texttt{local} is used to alterate the existing parameters value in those readers. 
@@ -416,4 +416,4 @@ integRK4 f i y = do
 \end{code}
 }
 
-This finishes this chapter, where we incremented the capabilities of the \texttt{CT} type and used it in combination with a brand-new type, the \texttt{Integrator}. Together these types represent the mathematical integral operation. The solver methods are involved within this implementation, and they use an implicit recursion to maintain their sequential behaviour. Also, those abstractions were mapped to FF-GPAC's ideas in order to bring some formalism to the project. However, the used mechanisms, such as implicit recursion and memory manipulation, make it hard to visualize how to execute the project given a description of a physical system. The next chapter, \textit{Execution Walkthrough}, will introduce the \textbf{driver} of the simulation and present a step-by-step concrete example. Later on, we will improve the DSL to completely remove all the noise introduced in its use because of such implicit recursion.
+This finishes this Chapter, where we incremented the capabilities of the \texttt{CT} type and used it in combination with a brand-new type, the \texttt{Integrator}. Together these types represent the mathematical integral operation. The solver methods are involved within this implementation, and they use an implicit recursion to maintain their sequential behaviour. Also, those abstractions were mapped to FF-GPAC's ideas in order to bring some formalism to the project. However, the used mechanisms, such as implicit recursion and memory manipulation, make it hard to visualize how to execute the project given a description of a physical system. The next Chapter, \textit{Execution Walkthrough}, will introduce the \textit{driver} of the simulation and present a step-by-step concrete example. Later on, we will improve the DSL to completely remove all the noise introduced in its use because of such implicit recursion.
diff --git a/doc/MastersThesis/Lhs/Interpolation.lhs b/doc/MastersThesis/Lhs/Interpolation.lhs
index ea139f5..b621638 100644
--- a/doc/MastersThesis/Lhs/Interpolation.lhs
+++ b/doc/MastersThesis/Lhs/Interpolation.lhs
@@ -25,22 +25,22 @@ iterToTime interv solver n (SolverStage st) =
 \end{code}
 }
 
-The previous chapter ended anouncing that drawbacks are present in the current implementation. This chapter will introduce the first concern: numerical methods do not reside in the continuous domain, the one we are actually interested in. After this chapter, this domain issue will be addressed via \textbf{interpolation}, with a few tweaks in the integrator and driver.
+The previous Chapter ended anouncing that drawbacks are present in the current implementation. This Chapter will introduce the first concern: numerical methods do not reside in the continuous domain, the one we are actually interested in. After this Chapter, this domain issue will be addressed via \textit{interpolation}, with a few tweaks in the integrator and driver.
 
 \section{Time Domains}
 
-When dealing with continuous time, \texttt{FACT} changes the domain in which \textbf{time} is being modeled. Figure \ref{fig:timeDomains} shows the domains that the implementation interact with during execution:
+When dealing with continuous time, \texttt{FACT} changes the domain in which \textit{time} is being modeled. Figure \ref{fig:timeDomains} shows the domains that the implementation interact with during execution:
 
 \figuraBib{TimeDomains}{During simulation, functions change the time domain to the one that better fits certain entities, such as the \texttt{Solver} and the driver. The image is heavily inspired by a figure in~\cite{Edil2017}}{}{fig:timeDomains}{width=.85\textwidth}%
 
-The problems starts in the physical domain. The goal is to obtain a value of an unknown function $y(t)$ at time $t_x$. However, because the solution is based on \textbf{numerical methods} a sampling process occurs and the continuous time domain is transformed into a \textbf{discrete} time domain, where the solver methods reside --- those are represented by the functions \textit{integEuler}, \textit{integRK2} and \textit{integRK4}. A solver depends on the chosen time step to execute a numerical algorithm. Thus, time is modeled by the sum of $t_0$ with $n\Delta$, where $n$ is a natural number. Hence, from the solver perspective, time is always dependent on the time step, i.e., only values that can be described as $t_0 + n\Delta$ can be properly visualized by the solver. Finally, there's the \textbf{iteration} domain, used by the driver functions, \textit{runCT} and \textit{runCTFinal}. When executing the driver, one of its first steps is to call the function \textit{iterationsBnds}, which converts the simulation time interval to a tuple of numbers that represent the amount of iterations based on the time step of the solver. This function is presented bellow:
+The problems starts in the physical domain. The goal is to obtain a value of an unknown function $y(t)$ at time $t_x$. However, because the solution is based on \textit{numerical methods} a sampling process occurs and the continuous time domain is transformed into a \textit{discrete} time domain, where the solver methods reside --- those are represented by the functions \textit{integEuler}, \textit{integRK2} and \textit{integRK4}. A solver depends on the chosen time step to execute a numerical algorithm. Thus, time is modeled by the sum of $t_0$ with $n\Delta$, where $n$ is a natural number. Hence, from the solver perspective, time is always dependent on the time step, i.e., only values that can be described as $t_0 + n\Delta$ can be properly visualized by the solver. Finally, there's the \textit{iteration} domain, used by the driver functions, \textit{runCT} and \textit{runCTFinal}. When executing the driver, one of its first steps is to call the function \textit{iterationsBnds}, which converts the simulation time interval to a tuple of numbers that represent the amount of iterations based on the time step of the solver. This function is presented bellow:
 
 \begin{spec}
 iterationBnds :: Interval -> Double -> (Int, Int)
 iterationBnds interv dt = (0, ceiling ((stopTime interv - startTime interv) / dt))
 \end{spec}
 
-To achieve the total number of iterations, the function \textit{iterationBnds} does a \textbf{ceiling} operation on the sampled result of iterations, based on the time interval (\textit{startTime} and \textit{stopTime}) and the time step (\texttt{dt}). The second member of the tuple is always the answer, given that it is assumed that the first member of the tuple is always zero.
+To achieve the total number of iterations, the function \textit{iterationBnds} does a \textit{ceiling} operation on the sampled result of iterations, based on the time interval (\textit{startTime} and \textit{stopTime}) and the time step (\texttt{dt}). The second member of the tuple is always the answer, given that it is assumed that the first member of the tuple is always zero.
 
 The function that allows us to go back to the discrete time domain being in the iteration axis is the \textit{iterToTime} function. It uses the solver information, the current iteration and the interval to transition back to time, as depicted by the following code:
 
@@ -61,10 +61,10 @@ iterToTime interv solver n st =
             delta RungeKutta4 3 = dt solver
 \end{spec}
 
-A transformation from iteration to time depends on and on the chosen solver method due to their next step functions.
-For instance, the second and forth order Runge-Kutta methods have more stages, and it uses fractions of the time step for more granular use of the derivative function. This is why lines 11 and 12 are using half of the time step. Moreover, all discrete time calculations assume that the value starts from the beginning of the simulation (\textit{startTime}). The result is obtained by the sum of the initial value, the solver-dependent \textit{delta} function and the iteration times the solver time step (line 6).
+A transformation from iteration to time depends on the chosen solver method due to their next step functions.
+For instance, the second and fourth order Runge-Kutta methods have more stages, and it uses fractions of the time step for more granular use of the derivative function. This is why lines 11 and 12 are using half of the time step. Moreover, all discrete time calculations assume that the value starts from the beginning of the simulation (\textit{startTime}). The result is obtained by the sum of the initial value, the solver-dependent \textit{delta} function and the iteration times the solver time step (line 6).
 
-There is, however, a missing transition: from the discrete time domain to the domain of interest in CPS --- the continuous time axis. This means that if the time value $t_x$ is not present from the solver point of view, it is not possible to obtain $y(t_x)$. The proposed solution is to add an \textbf{interpolation} function into the pipeline, which addresses this transition. Thus, values in between solver steps will be transfered back to the continuous domain.
+There is, however, a missing transition: from the discrete time domain to the domain of interest in CPS --- the continuous time axis. This means that if the time value $t_x$ is not present from the solver point of view, it is not possible to obtain $y(t_x)$. The proposed solution is to add an \textit{interpolation} function into the pipeline, which addresses this transition. Thus, values in between solver steps will be transfered back to the continuous domain.
 
 \section{Tweak I: Interpolation}
 
@@ -93,13 +93,13 @@ data Stage = SolverStage Int
 The type \texttt{Stage} allows values to be either the normal flow of execution, marked by the use of \texttt{SolverStage}, or the
 indication that an extra step for interpolation needs to be done, marked by the \texttt{Interpolate} tag. Moreover, previous types and functions
 described in previous chapters, such as \textit{Design Philosophy}, and \textit{Effectful Integrals} need to be adapted to use this new
-type instead of the original \texttt{Int} previously proposed (in chapter 2, \textit{Design Philosophy}). Types like \texttt{Parameters} and
+type instead of the original \texttt{Int} previously proposed (in Chapter 2, \textit{Design Philosophy}). Types like \texttt{Parameters} and
 functions like \textit{integEuler}, \textit{iterToTime}, and \textit{runCT} need to be updated accordingly. In all of those instances, processing will just continue
 normally; \texttt{SolverStage} will be used.
 
-Next, the driver needs to be updated. So, the proposed mechanism is the following: the driver will identify these corner cases and communicate to the integrator --- via the new \texttt{Stage} field in the \texttt{Solver} data type --- that the interpolation needs to be added into the pipeline of execution. When this flag is not on, i.e., the \texttt{Stage} informs to continue execution normally, the implementation goes as the previous chapters detailed. This behaviour is altered \textbf{only} in particular scenarios, which the driver will be responsible for identifying.
+Next, the driver needs to be updated. So, the proposed mechanism is the following: the driver will identify these corner cases and communicate to the integrator --- via the new \texttt{Stage} field in the \texttt{Solver} data type --- that the interpolation needs to be added into the pipeline of execution. When this flag is not on, i.e., the \texttt{Stage} informs to continue execution normally, the implementation goes as the previous chapters detailed. This behaviour is altered \textit{only} in particular scenarios, which the driver will be responsible for identifying.
 
-It remains to re-implement the driver functions. The driver will notify the integrator that an interpolation needs to take place. The code below shows these changes:
+It remains to re-implement the driver functions. The driver will notify the integrator that an interpolation needs to take place. The following code shows these changes:
 
 \ignore{
 \begin{code}
@@ -147,12 +147,12 @@ runCT m t sl =
          in init values ++ [runReaderT m ps]
 \end{spec}
 
-The implementation of \textit{iterationBnds} uses \textit{ceiling} function because this rounding is used to go to the iteration domain. However, given that the interpolation \textbf{requires} both solver steps --- the one that came before $t_x$ and the one immediately
+The implementation of \textit{iterationBnds} uses \textit{ceiling} function because this rounding is used to go to the iteration domain. However, given that the interpolation \textit{requires} both solver steps --- the one that came before $t_x$ and the one immediately
 afterwards --- the number of iterations needs always to surpass the requested time. For instance, the time 5.3 seconds will demand the fifth and sixth iterations with a time step of 1 second. When using \textit{ceiling}, it is assured that the value of interest will be in the interval of computed values. So, when dealing with 5.3, the integrator will calculate all values up to 6 seconds.
 
-Lines 5 to 15 are equal to the previous implementation of the \textit{runCT} function. On line 16, the discrete version of \texttt{t}, \texttt{disct}, will be used for detecting if an
+Lines 5 to 15 (from the previous code snippet) are equal to the previous implementation of the \textit{runCT} function. On line 16, the discrete version of \texttt{t}, \texttt{disct}, will be used for detecting if an
 interpolation will be needed. All the simulation values are being prepared on line 17 --- Haskell being a lazy language the label \texttt{values} will not necessarily
-be evaluated strictly. Line 19 establishes a condition, checkiing if the difference between the time of interest \texttt{t} and \texttt{disct} is greater or not
+be evaluated strictly. Line 19 establishes a condition, checking if the difference between the time of interest \texttt{t} and \texttt{disct} is greater or not
 than a value \texttt{epslon}, to identify if
 the normal flow of execution can proceed. If it can't, on line 22 a new record of type \texttt{Parameters} is created (\texttt{ps}), especifically to these special cases of mismatch between discrete and continuous time. The main difference within this special record is relevant: the stage field of the solver is being set to \texttt{Interpolate}.
 Finally, on line 25 the last element from the list of outputs \texttt{values} is removed and it is appended the simulation using the created \texttt{ps} with
@@ -185,7 +185,7 @@ interpolate m = do
       in z1 + (z2 - z1) * pure ((t - t1) / (t2 - t1))
 \end{code}
 
-Lines 1 to 5 continues the simulation with the normal workflow. If a corner case comes in, the reminaing code applies \textbf{linear interpolation} to it. It accomplishes this by first comparing the next and previous discrete times (lines 16 and 19) relative to \texttt{x} (line 11) --- the discrete counterpart of the time of interest \texttt{t} (line 9). These time points are calculated by their correspondent iterations (lines 12 and 13). Then, the integrator calculates the outcomes at these two points, i.e., do applications of the previous and next modeled times points with their respective parametric records (lines 22 and 23). Finally, line 24 executes the linear interpolation with the obtained values that surround the non-discrete time point. This particular interpolation was chosen for the sake of simplicity, but it can be replaced by higher order methods. Figure \ref{fig:interpolate} illustrates the effect of the \textit{interpolate} function when converting domains.
+Lines 1 to 5 (from the previuos code snippet) continues the simulation with the normal workflow. If a corner case comes in, the reminaing code applies \textit{linear interpolation} to it. It accomplishes this by first comparing the next and previous discrete times (lines 16 and 19) relative to \texttt{x} (line 11) --- the discrete counterpart of the time of interest \texttt{t} (line 9). These time points are calculated by their correspondent iterations (lines 12 and 13). Then, the integrator calculates the outcomes at these two points, i.e., do applications of the previous and next modeled times points with their respective parametric records (lines 22 and 23). Finally, line 24 executes the linear interpolation with the obtained values that surround the non-discrete time point. This particular interpolation was chosen for the sake of simplicity, but it can be replaced by higher order methods. Figure \ref{fig:interpolate} illustrates the effect of the \textit{interpolate} function when converting domains.
 
 \begin{spec}
 updateInteg :: Integrator -> CT Double -> CT ()
@@ -203,8 +203,8 @@ updateInteg integ diff = do
 
 \figuraBib{Interpolate}{Linear interpolation is being used to transition us back to the continuous domain.}{}{fig:interpolate}{width=.7\textwidth}%
 
-The last step in this tweak is to add this function into the integrator function \textit{updateInteg}. The code is almost identical to the one presented in chapter 3, \textit{Effectful Integrals}. The main difference is in line 11, where the interpolation function is being applied to \texttt{z}. Figure \ref{fig:diffInterpolate} shows the same visual representation for the \textit{updateInteg} function used in chapter 4, but with the aforementioned modifications.
+The last step in this tweak is to add this function into the integrator function \textit{updateInteg}. The code is almost identical to the one presented in Chapter 3, \textit{Effectful Integrals}. The main difference is in line 11, where the interpolation function is being applied to \texttt{z}. Figure \ref{fig:diffInterpolate} shows the same visual representation for the \textit{updateInteg} function used in Chapter 4, but with the aforementioned modifications.
 
 \figuraBib{DiffIntegInterpolate}{The new \textit{updateInteg} function add linear interpolation to the pipeline when receiving a parametric record}{}{fig:diffInterpolate}{width=.9\textwidth}%
 
-This concludes the first tweak in \texttt{FACT}. Now, the mismatches between the stop time of the simulation and the time step are being treated differently, going back to the continuous domain thanks to the added interpolation. The next chapter, \textit{Caching the Speed Pill}, goes deep into the program's performance and how this can be fixed with a caching strategy.
+This concludes the first tweak in \texttt{FACT}. Now, the mismatches between the stop time of the simulation and the time step are being treated differently, going back to the continuous domain thanks to the added interpolation. The next Chapter, \textit{Caching the Speed Pill}, goes deep into the program's performance and how this can be fixed with a caching strategy.
diff --git a/doc/MastersThesis/Lhs/Introduction.lhs b/doc/MastersThesis/Lhs/Introduction.lhs
index 276ef8f..5dd7055 100644
--- a/doc/MastersThesis/Lhs/Introduction.lhs
+++ b/doc/MastersThesis/Lhs/Introduction.lhs
@@ -9,84 +9,101 @@ import MastersThesis.Lhs.Enlightenment
 
 Continuous behaviours are deeply embedded into the real world. However, even our most advanced computers are not capable of completely modeling such phenomena due to its discrete nature; thus becoming a still-unsolved challenge. Cyber-physical systems (CPS) --- the integration of computers and physical processes~\cite{LeeModeling, LeeChallenges} --- tackles this problem by attempting to include into the \textit{semantics} of computing the physical notion of \textit{time}~\cite{LeeChallenges, Lee2016, Lee2014, Ungureanu2018, Seyed2020, Edil2021}, i.e., treating time as a measurement of \textit{correctness}, not \textit{performance}~\cite{LeeModeling} nor just an accident of implementation~\cite{LeeChallenges}. Additionally, many systems perform in parallel, which requires precise and sensitive management of time; a non-achievable goal by using traditional computing abstractions, e.g., \textit{threads}~\cite{LeeChallenges}.
 
-Examples of these concepts are older than the digital computers; analog computers were used to model battleships' fire systems and core functionalities of fly-by-wire aircraft~\cite{Graca2003}. The mechanical metrics involved in these problems change continuously, such as space, speed and area, e.g., the firing's range and velocity are crucial in fire systems, and surfaces of control are indispensable to model aircraft's flaps. The main goal of such models was, and still is, to abstract away the continuous facet of the scenario to the computer. In this manner, the human in the loop aspect only matters when interfacing with the computer, with all the heavy-lifting being done by formalized use of shafts and gears in analog machines~\cite{Shannon, Bush1931, Graca2003}, and by \textbf{software} after the digital era.
+Examples of these concepts are older than the digital computers; analog computers were used to model battleships' fire systems and core functionalities of fly-by-wire aircraft~\cite{Graca2003}. The mechanical metrics involved in these problems change continuously, such as space, speed and area, e.g., the firing's range and velocity are crucial in fire systems, and surfaces of control are indispensable to model aircraft's flaps. The main goal of such models was, and still is, to abstract away the continuous facet of the scenario to the computer. In this manner, the human in the loop aspect only matters when interfacing with the computer, with all the heavy-lifting being done by formalized use of shafts and gears in analog machines~\cite{Shannon, Bush1931, Graca2003}, and by \textit{software} after the digital era.
 
 Within software, the aforementioned issues --- the lack of time semantics and the wrong tools for implementing concurrency --- are only a glimpse of serious concerns orbiting around CPS. The main villain is that today's computer science and engineering primarily focus on matching software demands, not expressing essential aspects of physical systems~\cite{LeeChallenges, LeeComponent}. Further, its sidekick is the weak formalism surrounding the semantics of model-based design tools; modeling languages whose semantics are defined by the tools rather than by the language itself~\cite{LeeComponent}, encouraging ad-hoc design practices, thus adding inertia into a dangerous legacy we want to avoid~\cite{Churchill1943}. With this in mind, Lee advocated that leveraging better formal abstractions is the paramount goal to advance continuous time modeling~\cite{LeeChallenges, LeeComponent}. More importantly, these new ideas need to embrace the physical world, taking into account predictability, reliability and interoperability.
 
 The development of a \textit{model of computation} (MoC) to define and express models is the major hero towards this better set of abstractions, given that it provides clear, formal and well-defined semantics~\cite{LeeModeling} on how engineering artifacts should behave~\cite{Lee2016}. These MoCs determine how concurrency works in the model, choose which communication protocols will be used, define whether different components share the notion of time, as well as whether and how they share state~\cite{LeeModeling, LeeComponent}. Also, Sangiovanni and Lee~\cite{LeeSangiovanni} proposed a formalized denotational framework to allow understanding and comparison between mixtures of MoCs, thus solving the heterogeneity issue that raises naturally in many situations during design~\cite{LeeModeling, LeeComponent}. Moreover, their framework also describes how to compose different MoCs, along with addressing the absence of time in models, via what is defined as \textit{tagged systems}~\cite{Chupin2019, Perez2023, Rovers2011} --- a relationship between a \textit{tag}, generally used to order events, and an output value.
 
-Ingo et al. went even further~\cite{Sander2017} by presenting a framework based on the idea of tagged systems, known as \textit{ForSyDe}. The tool's main goal is to push system design to a higher level of abstraction, by combining MoCs with the functional programming paradigm. The technique separates the design into two phases, specification and synthesis. The former stage, specification, focus on creating a high-level abstraction model, in which mathematical formalism is taken into account. The latter part, synthesis, is responsible for applying design transformations --- the model is adapted to ForSyDe's semantics --- and mapping this result onto a chosen architecture for later be implemented in a target programming language or hardware platform~\cite{Sander2017}. Afterward, Seyed-Hosein and Ingo~\cite{Seyed2020} created a co-simulation architecture for multiple models based on ForSyDe's methodology, addressing heterogeneity across languages and tools with different semantics. One example of such tools treated in the reference is Simulink~\footnote{Simulink \href{http://www.mathworks.com/products/simulink/}{\textcolor{blue}{documentation}}.}, the de facto model-based design tool that lacks a formal semantics basis~\cite{Seyed2020}. Simulink being the standard tool for modeling means that, despite all the effort into utilizing a formal approach to model-based design, this is still an open problem.
+Ingo et al. went even further~\cite{Sander2017} by presenting a framework based on the idea of tagged systems, known as \textit{ForSyDe}. The tool's main goal is to push system design to a higher level of abstraction, by combining MoCs with the functional programming paradigm. The technique separates the design into two phases, specification and synthesis. The former stage, specification, focus on creating a high-level abstraction model, in which mathematical formalism is taken into account. The latter part, synthesis, is responsible for applying design transformations --- the model is adapted to ForSyDe's semantics --- and mapping this result onto a chosen architecture to be implemented later in a target programming language or hardware platform~\cite{Sander2017}. Afterward, Seyed-Hosein and Ingo~\cite{Seyed2020} created a co-simulation architecture for multiple models based on ForSyDe's methodology, addressing heterogeneity across languages and tools with different semantics. One example of such tools treated in the reference is Simulink~\footnote{Simulink \href{http://www.mathworks.com/products/simulink/}{\textcolor{blue}{documentation}}.}, the de facto model-based design tool that lacks a formal semantics basis~\cite{Seyed2020}. Simulink being the standard tool for modeling means that, despite all the effort into utilizing a formal approach to model-based design, this is still an open problem.
 
-\section{Proposal}
-
-The aforementioned works --- the formal notion of MoCs, the ForSyDe framework and its interaction with modeling-related tools like Simulink --- comprise the domain of model-based design or \textbf{model-based engineering}. Furthermore, the main goal of the present work contribute to this area of CPS by creating a domain-specific language tool (DSL) for simulating continuous-time systems that addresses the absence of a formal basis. Thus, this tool will help to cope with the incompatibility of the mentioned sets of abstractions~\cite{LeeChallenges} --- the discreteness of digital computers with the continuous nature of physical phenomena.
+\section{Contribution}
+\label{sec:intro}
 
-The proposed DSL has three special properties of interest: it needs to be a set of well-defined \textit{operational} semantics, thus being \textbf{executable}; it needs to be related to a \textit{formalized} reasoning process; and it should bring familiarity in its use to the \textit{system's designer} -- the pilot of the DSL which strives to execute a given specification or golden model. The first aspect provides \textbf{verification via simulation}, a type of verification that is useful when dealing with \textbf{non-preserving} semantic transformations, i.e., modifications and tweaks in the model that do not assure that properties are being preserved. Such phenomena are common within the engineering domain, given that a lot of refinement goes into the modeling process in which previous proof-proved properties are not guaranteed to be maintained after iterations with the model. A work-around solution for this problem would be to prove again that the features are in fact present in the new model; an impractical activity when models start to scale in size and complexity. Thus, by using an executable tool as a virtual workbench, models that suffered from those transformations could be extensively tested and verified.
+The aforementioned works --- the formal notion of MoCs, the ForSyDe framework and its interaction with modeling-related tools like Simulink --- comprise the domain of model-based design or \textit{model-based engineering}. Furthermore, the main goal of this work is to contribute to this area of CPS by creating a domain-specific language tool (DSL) for simulating continuous-time systems that addresses the absence of a formal basis. Thus, this tool will help to deal with the incompatibility of the mentioned sets of abstractions~\cite{LeeChallenges} --- the discreteness of digital computers with the continuous nature of physical phenomena.
 
-In order to address the second property, a solid and formal foundation, the tool is inspired by the general-purpose analog computer (GPAC) formal guidelines, proposed by Shannon~\cite{Shannon} in 1941. This concept was developed to model a Differential Analyzer --- an analog computer composed by a set of interconnected gears and shafts intended to solve numerical problems~\cite{Graca2004}. The mechanical parts represents \textit{physical quantities} and their interaction results in solving differential equations, a common activity in engineering, physics and other branches of science~\cite{Shannon}. The model was based on a set of black boxes, so-called \textit{circuits} or \textit{analog units}, and a set of proved theorems that guarantees that the composition of these units are the minimum necessary to model the system, given some conditions. For instance, if a system is composed by a set of \textit{differentially algebraic} equations with prescribed initial conditions~\cite{Graca2003}, then a GPAC circuit can be built to model it. Later on, some extensions of the original GPAC were developed, going from solving unaddressed problems contained in the original scope of the model~\cite{Graca2003} all the way to make GPAC capable of expressing generable functions, Turing universality and hypertranscendental functions~\cite{Graca2004, Graca2016}. Furthermore, although the analog computer has been forgotten in favor of its digital counterpart~\cite{Graca2003}, recent studies in the development of hybrid systems~\cite{Edil2018} brought GPAC back to the spotlight in the CPS domain.
+The proposed DSL has three special properties of interest:
 
-Finally, the third property of interest, the designer's familiarity between the mathematical specification and
-the DSL's usability, will be assured by the use of the \textit{fixed-point combinator}; a mathematical construct used in the DSL's machineary to hide implementation details noise from the user's perspective, keeping on the surface only the constructs that matter from the designer's point of view. Hence, it is expected that one with less programming experience but familiar with the system's mathematical description will be able to leverage the DSL either when improving the system's description, using the DSL as a refinment tool, or as a way to execute an already specified system. The present work being a direct continuation~\cite{Lemos2022}, it is important to highlight that this final property is the differentiating factor between the two pieces.
+\begin{enumerate}
+\item it needs to have well-defined \textit{operational} semantics, as well as being a piece of \textit{executable} software;
+\item it needs to be related or inspired by a \textit{formal} foundation, moving past \textit{ad-hoc} implementations;
+\item it should be \textit{concise}; its lack of noise will bring familiarity to the \textit{system's designer} --- the pilot of the DSL which strives to execute a given specification or golden model.
+\end{enumerate}
 
-With these three core properties in mind, the proposed DSL will translate GPAC's original set of black boxes to some executable software leveraging mathematical constructs to simplify its usability.
+\subsection{Executable Simulation}
 
-\section{Goal}
-\label{sec:intro}
+By making an executable software capable of running continuous time simulations, \textit{verification via simulation} will be available --- a type of verification that is useful when dealing with \textit{non-preserving} semantic transformations, i.e., modifications and tweaks in the model that do not assure that properties are being preserved. Such phenomena are common within the engineering domain, given that a lot of refinement goes into the modeling process in which previous proof-proved properties are not guaranteed to be maintained after iterations with the model. A work-around solution for this problem would be to prove again that the features are in fact present in the new model; an impractical activity when models start to scale in size and complexity. Thus, by using an executable tool as a virtual workbench, models that suffered from those transformations could be extensively tested and verified.
 
-The main goal of the present work is to build a library that can solve differential equations and resembles the core idea of the GPAC model. The programming language of choice was \textbf{Haskell}, due to a variety of different reasons. First, the approach of making specialized programming languages, or \textit{vocabularies}, within consistent and well-defined host programming languages has already proven to be valuable, as noted by Landin~\cite{Landin1966}. Second, this strategy is already being used in the CPS domain in some degree, as showed by the ForSyDe framework~\cite{Sander2017, Seyed2020}. Third, Lee describes a lot of properties~\cite{LeeModeling} that matches the functional programming paradigm almost perfectly:
-
-\begin{itemize}
- \item Prevent misconnected MoCs by using great interfaces in between $\Rightarrow$ Such interfaces can be built using Haskell's \textbf{strong type system}
- \item Enable composition of MoCs $\Rightarrow$ Composition is a first-class feature in functional programming languages
- \item It should be possible to conjoin a functional model with an implementation model $\Rightarrow$ Functions programming languages makes a clear the separation between the \textit{denotational} aspect of the program, i.e., its meaning, from the \textit{operational} functionality
- \item All too often the semantics emerge accidentally from the software implementation rather than being built-in from the start $\Rightarrow$ A denotative approach with no regard for implementation details is common in the functional paradigm
- \item The challenge is to define MoCs that are sufficiently expressive and have strong formal properties that enable systematic validation of designs and correct-by-construction synthesis of implementations $\Rightarrow$ Functional languages are commonly used for formal mathematical applications, such as proof of theorems and properties, as well as also being known for "correct-by-construction" approaches 
-\end{itemize}
-
-The recognition that the functional paradigm (FP) provides better well-defined, mathematical and rigourous abstractions has been by Backus~\cite{Backus1978} in his Turing Award lecture; where he argued that FP is the path to liberate computing from the limitations of the \textit{von Neumann style} when thinking about systems.
-Thus, continuous time being specified in mathematical terms,  we believe that the use of functional programming for modeling continuous time is not a coincidence; properties that are established as fundamental to leverage better abstractions for CPS simulation seem to be within or better described in the functional programming paradigm. Furthermore, this implementation is based on \texttt{Aivika}~\footnote{\texttt{Aivika} \href{https://github.com/dsorokin/aivika}{\textcolor{blue}{source code}}.} --- an open source multi-method library for simulating a variety of paradigms, including partial support for physical dynamics, written in Haskell. Our version is modified for our needs, such as demonstrating similarities between the implementation and GPAC, shrinking some functionality in favor of focusing on continuous time modeling, and re-thinking the overall organization of the project for better understanding, alongside code refactoring using other Haskell's abstractions. So, this reduced and refactored version of \texttt{Aivika}, so-called \texttt{FACT}~\footnote{\texttt{FACT} \href{https://github.com/FP-Modeling/fact/releases/tag/3.0}{\textcolor{blue}{source code}}.}, will be a Haskell Embedded Domain-Specific Language (HEDSL) within the model-based engineering domain. The built DSL will explore Haskell's specific features and details, such as the type system and typeclasses, to solve differential equations. Figure \ref{fig:introExample} shows a side-by-side comparison between the original implementation of Lorenz Attractor in FACT, presented in~\cite{Lemos2022}, and its final form for the same physical system.
+Furthermore, this implementation is based on \texttt{Aivika}~\footnote{\texttt{Aivika} \href{https://github.com/dsorokin/aivika}{\textcolor{blue}{source code}}.} --- an open source multi-method library for simulating a variety of paradigms, including partial support for physical dynamics, written in Haskell. Our version is modified for our needs, such as demonstrating similarities between the implementation and GPAC, shrinking some functionality in favor of focusing on continuous time modeling, and re-thinking the overall organization of the project for better understanding, alongside code refactoring using other Haskell's abstractions. So, this reduced and refactored version of \texttt{Aivika}, so-called \texttt{FACT}~\footnote{\texttt{FACT} \href{https://github.com/FP-Modeling/fact/releases/tag/3.0}{\textcolor{blue}{source code}}.}, will be a Haskell Embedded Domain-Specific Language (HEDSL) within the model-based engineering domain. The built DSL will explore Haskell's specific features and details, such as the type system and typeclasses, to solve differential equations. Figure \ref{fig:introExample} shows a side-by-side comparison between the original implementation of Lorenz Attractor in FACT, presented in~\cite{Lemos2022}, and its final form, so-called FFACT, for the same physical system.
 
 \begin{figure}[ht!]
-  \begin{minipage}{0.45\linewidth}
-% \vspace{-0.8cm}
+  \begin{minipage}{0.5\linewidth}
     \begin{purespec}
-        -- Original version of FACT
+        -- FACT
         lorenzModel = do
-        integX <- createInteg 1.0
-        integY <- createInteg 1.0
-        integZ <- createInteg 1.0
-        let x = readInteg integX
-            y = readInteg integY
-            z = readInteg integZ
-            sigma = 10.0
-            rho = 28.0
-            beta = 8.0 / 3.0
-        updateInteg integX (sigma * (y - x))
-        updateInteg integY (x * (rho - z) - y)
-        updateInteg integZ (x * y - beta * z)
-        return $ sequence [x, y, z]
+          integX <- createInteg 1.0
+          integY <- createInteg 1.0
+          integZ <- createInteg 1.0
+          let x = readInteg integX
+              y = readInteg integY
+              z = readInteg integZ
+              sigma = 10.0
+              rho = 28.0
+              beta = 8.0 / 3.0
+          updateInteg integX (sigma * (y - x))
+          updateInteg integY (x * (rho - z) - y)
+          updateInteg integZ (x * y - beta * z)
+          return $ sequence [x, y, z]
     \end{purespec}
   \end{minipage} \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;
-  \begin{minipage}{0.45\linewidth}
+  \begin{minipage}{0.49\linewidth}
     \begin{purespec}
-        -- Final version of FACT
-        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]          
+        -- FFACT
+        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}
   \end{minipage}
-\caption{The translation between the world of software and the mathematical description of differential equations are explicit in the final version of \texttt{FACT}.}
+\caption{The translation between the world of software and the mathematical description of differential equations are more concise and explicit in \texttt{FFACT}.}
 \label{fig:introExample}
 \end{figure}
 
+\subsection{Formal Foundation}
+
+The tool is inspired by the general-purpose analog computer (GPAC) formal guidelines, proposed by Shannon~\cite{Shannon} in 1941, as an inspiration for a solid and formal foundation. This concept was developed to model a Differential Analyzer --- an analog computer composed by a set of interconnected gears and shafts intended to solve numerical problems~\cite{Graca2004}. The mechanical parts represents \textit{physical quantities} and their interaction results in solving differential equations, a common activity in engineering, physics and other branches of science~\cite{Shannon}. The model was based on a set of black boxes, so-called \textit{circuits} or \textit{analog units}, and a set of proved theorems that guarantees that the composition of these units are the minimum necessary to model the system, given some conditions. For instance, if a system is composed by a set of \textit{differentially algebraic} equations with prescribed initial conditions~\cite{Graca2003}, then a GPAC circuit can be built to model it. Later on, some extensions of the original GPAC were developed, going from solving unaddressed problems contained in the original scope of the model~\cite{Graca2003} all the way to make GPAC capable of expressing generable functions, Turing universality and hypertranscendental functions~\cite{Graca2004, Graca2016}. Furthermore, although the analog computer has been forgotten in favor of its digital counterpart~\cite{Graca2003}, recent studies in the development of hybrid systems~\cite{Edil2018} brought GPAC back to the spotlight in the CPS domain.
+
+The HEDSL will translate GPAC's original set of black boxes to some executable software leveraging mathematical constructs to simplify its usability. The programming language of choice was \textit{Haskell} --- a well known language in the functional paradigm (FP). The recognition that such paradigm provides better well-defined, mathematical and rigourous abstractions has been proposed by Backus~\cite{Backus1978} in his Turing Award lecture; where he argued that FP is the path to liberate computing from the limitations of the \textit{von Neumann style} when thinking about systems. Thus, continuous time being specified in mathematical terms,  we believe that the use of functional programming for modeling continuous time is not a coincidence; properties that are established as fundamental to leverage better abstractions for CPS simulation seem to be within or better described in FP.
+Lee describes a lot of properties~\cite{LeeModeling} that matches this programming
+paradigm almost perfectly:
+
+\begin{enumerate}
+ \item Prevent misconnected MoCs by using great interfaces in between $\Rightarrow$ Such interfaces can be built using Haskell's \textit{strong type system}
+ \item Enable composition of MoCs $\Rightarrow$ Composition is a first-class feature in functional programming languages
+ \item It should be possible to conjoin a functional model with an implementation model $\Rightarrow$ Functions programming languages makes a clear the separation between the \textit{denotational} aspect of the program, i.e., its meaning, from the \textit{operational} functionality
+ \item All too often the semantics emerge accidentally from the software implementation rather than being built-in from the start $\Rightarrow$ A denotative approach with no regard for implementation details is common in the functional paradigm
+ \item The challenge is to define MoCs that are sufficiently expressive and have strong formal properties that enable systematic validation of designs and correct-by-construction synthesis of implementations $\Rightarrow$ Functional languages are commonly used for formal mathematical applications, such as proof of theorems and properties, as well as also being known for "correct-by-construction" approaches 
+\end{enumerate}
+
+In terms of the DSL being \textit{embedded} in Haskell, this approach of making specialized programming languages, or \textit{vocabularies}, within consistent and well-defined host programming languages, has already proven to be valuable, as noted by Landin~\cite{Landin1966}. Further, this strategy is already being used in the CPS domain in some degree, as showed by the ForSyDe framework~\cite{Sander2017, Seyed2020}.
+
+\subsection{Conciseness}
+
+Finally, conciseness to improve the DSL's usability will be assured by the use of the \textit{fixed-point combinator}; a mathematical construct used in the DSL's machinery to hide implementation details noise from the user's perspective, keeping on the surface only the constructs that matter from the designer's point of view. As the dissertation will explain, this happens due to an \textit{abstraction leak} in the original DSL~\cite{Lemos2022}, identified via
+an overloaded syntax. Once the leak is solved, it is expected that the \textit{target audience} --- system's designers with less programming experience but familiar with the system's mathematical description --- will be able to leverage the DSL either when improving the system's description, using the DSL as a refinement tool, or as a way to execute an already specified system. Given that the present work, FFACT, being a direct continuation of FACT~\cite{Lemos2022}, it is important to highlight that this final property is the main differentiating factor between the two pieces.
+
+When comparing models in FFACT to other implementations in other ecosystems and programming languages, FFACT's conciseness brings more familiarity, i.e.,
+one using the HEDSL needs less knowledge about the host programming language, Haskell in our case, \textit{and} one can more easily bridge the gap between a mathematical
+description of the problem and its analogous written in FFACT, due to less syntatical burden and noise from a user's perpective. Examples and comparisons will be
+depicted in Chapter 7, \textit{Fixing Recursion}, Section~\ref{sec:examples}.
+
 \section{Outline}
 
-This thesis is a step in a broader story, started in 2018 by Edil Medeiros et al.~\cite{Edil2018}. Medeiros' work had some limitations, such as having difficulty
+This dissertation is a step in a broader story, started in 2018 by Edil Medeiros et al.~\cite{Edil2018}. Medeiros' work had some limitations, such as having difficulty
 modeling systems via explicit signal manipulation, and later publications addressed this issue~\cite{Lemos2022, EdilLemos2023}. The chapters
 in this work encompass the previous milestones from this story, giving the reader a complete overview from the ground up in this research thread.
 
@@ -94,7 +111,10 @@ Chapter 2, \textit{Design Philosophy}, presents the foundation of this work, sta
 original work and this work are far apart, the mathematical base is the same. Chapters 3 to 6 describe future improvements made in 2022~\cite{Lemos2022} and
 2023~\cite{EdilLemos2023}. These chapters go in detail about the DSL's implementation details, such as the used abstractions, going through executable examples,
 pointing out and addressing problems in its usability and design. Issues like performance, and continuous time implementation are explained
-and then addressed. The latest of this work is concentrated in Chapter 7, \textit{Fixing Recursion}, which dedicates itself to improving an abstraction
+and then addressed. Whilst the implementation of Chapters 2 to 6 were vastly improved during the making of this dissertation, alongside improvements
+on the writing of their respective chapters,
+the latest inclusion to this research is
+concentrated in Chapter 7, \textit{Fixing Recursion}, which dedicates itself to improving an abstraction
 leak in the most recent published version of the DSL~\cite{EdilLemos2023}. Those improvements leverage the \textit{fixed point combinator} to eliminate
-abstraction leaks, thus making the DSL more familiar to a system's designer.
-These enhacements were submitted and are waiting approval in a related journal~\footnote{\href{https://www.cambridge.org/core/journals/journal-of-functional-programming}{\textcolor{blue}{Journal of Functional Programming}}.}. Finally, limitations, future improvements and final thoughts are drawn in chapter 8, \textit{Conclusion}.
+abstraction leaks, thus making the DSL more concise and familiar to a system's designer.
+These enhacements were submitted and are waiting approval in a related journal~\footnote{\href{https://www.cambridge.org/core/journals/journal-of-functional-programming}{\textcolor{blue}{Journal of Functional Programming}}.}. Finally, limitations, future improvements and final thoughts are drawn in Chapter 8, \textit{Conclusion}.
diff --git a/doc/MastersThesis/bibliography.bib b/doc/MastersThesis/bibliography.bib
index 9181212..148ed59 100644
--- a/doc/MastersThesis/bibliography.bib
+++ b/doc/MastersThesis/bibliography.bib
@@ -438,4 +438,31 @@ @book{knuth1992
 isbn = {0937073806},
 publisher = {Center for the Study of Language and Information},
 address = {USA}
+}
+
+@article{Simulink,
+author = {Ekhande, Rahul},
+year = {2014},
+month = {01},
+title = {Chaotic Signal for Signal Masking in Digital Communications},
+volume = {4},
+journal = {IOSR Journal of Engineering},
+doi = {10.9790/3021-04252933}
+}
+
+@inproceedings{Yampa,
+author = {Perez, Ivan},
+title = {The Beauty and Elegance of Functional Reactive Animation},
+year = {2023},
+isbn = {9798400702952},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+url = {https://doi.org/10.1145/3609023.3609806},
+doi = {10.1145/3609023.3609806},
+booktitle = {Proceedings of the 11th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling, and Design},
+pages = {8–20},
+numpages = {13},
+keywords = {Functional Reactive Programming, animation, dataflow, domain-specific languages},
+location = {Seattle, WA, USA},
+series = {FARM 2023}
 }
\ No newline at end of file
diff --git a/doc/MastersThesis/img/TimeDomains.pdf b/doc/MastersThesis/img/TimeDomains.pdf
index 9519529..d8aba9c 100644
Binary files a/doc/MastersThesis/img/TimeDomains.pdf and b/doc/MastersThesis/img/TimeDomains.pdf differ
diff --git a/doc/MastersThesis/img/lorenzSimulink.pdf b/doc/MastersThesis/img/lorenzSimulink.pdf
new file mode 100644
index 0000000..92d3ec0
Binary files /dev/null and b/doc/MastersThesis/img/lorenzSimulink.pdf differ
diff --git a/doc/MastersThesis/tex/abstract.tex b/doc/MastersThesis/tex/abstract.tex
index 8e6b588..d9d9f97 100644
--- a/doc/MastersThesis/tex/abstract.tex
+++ b/doc/MastersThesis/tex/abstract.tex
@@ -1,2 +1,2 @@
 
-Physical phenomena is difficult to properly model due to its continuous nature. Its paralellism and nuances were a challenge before the transistor, and even after the digital computer still is an unsolved issue. In the past, some formalism were brought with the General Purpose Analog Computer proposed by Shannon in the 1940s. Unfortunately, this formal foundation was lost in time, with \textit{ad-hoc} practices becoming mainstream to simulate continuous time. In this work, we propose a domain-specific language (DSL) -- FACT and its evolution FFACT -- written in Haskell that resembles GPAC's concepts. The main goal is to take advantage of high level abtractions, both from the areas of programming and mathematics, to execute systems of differential equations, which describe physical problems mathematically. We evaluate performance and domain problems and address them accordingly. Future improvements for the DSL are also explored and detailed.
+Physical phenomena are difficult to properly model due to their continuous nature. Its paralellism and nuances were a challenge before the transistor, and even after the digital computer it still is an unsolved issue. In the past, some formalism were brought with the General Purpose Analog Computer proposed by Shannon in the 1940s. Unfortunately, this formal foundation was lost in time, with \textit{ad-hoc} practices becoming mainstream to simulate continuous time. In this work, we propose a domain-specific language (DSL) -- FACT and its evolution FFACT -- written in Haskell that resembles GPAC's concepts. The main goal is to take advantage of high level abtractions, both from the areas of programming and mathematics, to execute systems of differential equations, which describe physical problems mathematically. We evaluate performance and domain problems and address them accordingly. Future improvements for the DSL are also explored and detailed.
diff --git a/doc/MastersThesis/tex/acknowledgments.tex b/doc/MastersThesis/tex/acknowledgments.tex
index 24083e4..077c4ae 100644
--- a/doc/MastersThesis/tex/acknowledgments.tex
+++ b/doc/MastersThesis/tex/acknowledgments.tex
@@ -1,14 +1,13 @@
-First and foremost, I thank my main advisor Edil Medeiros.
+First, I must acknowledge my main advisor, Edil Medeiros.
 Since graduation, and now in my masters, he trusted that my effort could go on and beyond, surpassing my own expectations
 and limits, getting out of my comfort zone. All the endless meetings, including on the weekends, filled with thoughtful advice and helpful comments,
-will be the most remarkable memory of the best teacher I have encountered to this day -- title that Edil got back when I was doing graduation and he
+will be the most remarkable memory of the best mentor I have encountered to this day -- a title that Edil got back when I was doing graduation, and he
 continues to be worthy.
 
-I'm thankful to my Computer Science study group, Dr.Nekoma, for the continue joyful programminig practices leveraging functional programming principles, something that is
-still the core foundation of the present work, even though this paradigm remains as uncommon both in the industry of software development and in the academia.
+I'm thankful to my Computer Science study group, Dr.Nekoma, for the continued joyful programming practices leveraging functional programming principles, something that is
+still the core foundation of the present work, even though this paradigm remains uncommon both in the industry of software development industry and in academia.
 
-I'm grateful for the company I'm currently working in, Tontine Trust, where I'm surrounded by real problems being solved in the Haskell; a programming language
-that I ended up being a fond of since my final graduation project written in it.
+I'm grateful for the company I'm currently working in, Tontine Trust, where I'm a member of a great team delivering a challenging product to the market. Some of these challenges are being solved in Haskell; a programming language
+I grew fond of it since my final graduation project was written in it. This work is a continuation of that.
 
-Finally, a special thanks for everybody that took any amount of time to read any draft I had of this thesis, providing honest feedback to enhance my thesis
-before the end of my masters. 
+Finally, a special thanks to everybody who took any amount of time to read any draft I had of this dissertation, providing honest feedback. 
diff --git a/doc/MastersThesis/tex/dedication.tex b/doc/MastersThesis/tex/dedication.tex
index 4ffe879..44930e0 100644
--- a/doc/MastersThesis/tex/dedication.tex
+++ b/doc/MastersThesis/tex/dedication.tex
@@ -3,7 +3,7 @@
 
 To my father Rodolfo Rocha, for sharing with me his wise and insightful perceptions about life.
 Your distinct perspectives bring me awareness about any subject that we end up
-discussing. Not everyone can have the luxuary of having
+discussing. Not everyone can have the luxury of having
 civil and calm conversations with whom they may fundamentally disagree. My dad gave me my first
 opportunities of this kind and I'm truly grateful to him for that.
 
diff --git a/doc/MastersThesis/thesis.lhs b/doc/MastersThesis/thesis.lhs
index 80a74cb..c0db057 100644
--- a/doc/MastersThesis/thesis.lhs
+++ b/doc/MastersThesis/thesis.lhs
@@ -1,4 +1,4 @@
-\documentclass[qualificacao,mestrado,ppgi]{UnB-CIC}
+\documentclass[mestrado,ppgi]{UnB-CIC}
 
 %include polycode.fmt
 %include MastersThesis/lineno.fmt
@@ -32,6 +32,9 @@
 \newminted[code]{haskell}{breaklines,autogobble,linenos=true, numberblanklines=false, fontsize=\footnotesize}
 \newminted[spec]{haskell}{breaklines,autogobble,linenos=true, numberblanklines=false, fontsize=\footnotesize}
 \newminted[purespec]{haskell}{breaklines,autogobble,linenos=false, numberblanklines=false, fontsize=\footnotesize}
+\newminted[matlab]{matlab}{breaklines,autogobble,linenos=false, numberblanklines=false, fontsize=\footnotesize}
+\newminted[python]{python}{breaklines,autogobble,linenos=false, numberblanklines=false, fontsize=\footnotesize}
+\newminted[mathematica]{mathematica}{breaklines,autogobble,linenos=false, numberblanklines=false, fontsize=\footnotesize}
 
 \orientador{\prof Eduardo Peixoto}{CIC/UnB}%
 \coorientador{\prof José Edil Guimarães}{ENE/UnB}%
@@ -43,7 +46,7 @@
 
 \autor{Eduardo L.}{Rocha}%
 
-\titulo{Continuous Time Modeling Made Functional: Fixing Differential Equations with Haskell}%
+\titulo{FFACT: A Fix-based Domain-Specific Language based on a Functional Algebra for Continuous Time Modeling}%
 
 \palavraschave{equações diferenciais, sistemas contínuos, GPAC, integrador, ponto fixo, recursão monádica}
 \keywords{differential equations, continuous systems, GPAC, integrator, fixed-point, fixed-point combinator, monadic recursion}%
diff --git a/doc/MastersThesis/thesis.lof b/doc/MastersThesis/thesis.lof
index fa57bb1..9d455e6 100644
--- a/doc/MastersThesis/thesis.lof
+++ b/doc/MastersThesis/thesis.lof
@@ -2,58 +2,63 @@
 \babel@toc {american}{}\relax 
 \babel@toc {american}{}\relax 
 \addvspace {10\p@ }
-\contentsline {figure}{\numberline {1.1}{\ignorespaces The translation between the world of software and the mathematical description of differential equations are explicit in the final version of \texttt {FACT}.}}{5}{figure.caption.6}%
-\addvspace {10\p@ }
-\contentsline {figure}{\numberline {2.1}{\ignorespaces The combination of these four basic units compose any GPAC circuit (taken from~\cite {Edil2018} with permission).}}{8}{figure.caption.7}%
-\contentsline {figure}{\numberline {2.2}{\ignorespaces Polynomial circuits resembles combinational circuits, in which the circuit respond instantly to changes on its inputs (taken from~\cite {Edil2018} with permission).}}{9}{figure.caption.8}%
-\contentsline {figure}{\numberline {2.3}{\ignorespaces Types are not just labels; they enhance the manipulated data with new information. Their difference in shape can work as the interface for the data.}}{10}{figure.caption.9}%
-\contentsline {figure}{\numberline {2.4}{\ignorespaces Functions' signatures are contracts; they purespecify which shape the input information has as well as which shape the output information will have.}}{10}{figure.caption.9}%
-\contentsline {figure}{\numberline {2.5}{\ignorespaces Sum types can be understood in terms of sets, in which the members of the set are available candidates for the outer shell type. Parity and possible values in digital states are examples.}}{11}{figure.caption.10}%
-\contentsline {figure}{\numberline {2.6}{\ignorespaces Product types are a combination of different sets, where you pick a representative from each one. Digital clocks' time and objects' coordinates in space are common use cases. In Haskell, a product type can be defined using a \textbf {record} alongside with the constructor, where the labels for each member inside it are explicit.}}{11}{figure.caption.11}%
-\contentsline {figure}{\numberline {2.7}{\ignorespaces Depending on the application, different representations of the same structure need to used due to the domain of interest and/or memory constraints.}}{12}{figure.caption.12}%
-\contentsline {figure}{\numberline {2.8}{\ignorespaces The minimum requirement for the \texttt {Ord} typeclass is the $<=$ operator, meaning that the functions $<$, $<=$, $>$, $>=$, \texttt {max} and \texttt {min} are now unlocked for the type \texttt {ClockTime} after the implementation. Typeclasses can be viewed as a third dimension in a type.}}{12}{figure.caption.13}%
-\contentsline {figure}{\numberline {2.9}{\ignorespaces Replacements for the validation function within a pipeline like the above is common.}}{13}{figure.caption.14}%
-\contentsline {figure}{\numberline {2.10}{\ignorespaces The initial value is used as a starting point for the procedure. The algorithm continues until the time of interest is reached in the unknown function. Due to its large time step, the final answer is really far-off from the expected result.}}{15}{figure.caption.15}%
-\contentsline {figure}{\numberline {2.11}{\ignorespaces In Haskell, the \texttt {type} keyword works for alias. The first draft of the \texttt {CT} type is a \textbf {function}, in which providing a floating point value as time returns another value as outcome.}}{15}{figure.caption.16}%
-\contentsline {figure}{\numberline {2.12}{\ignorespaces The \texttt {Parameters} type represents a given moment in time, carrying over all the necessary information to execute a solver step until the time limit is reached. Some useful typeclasses are being derived to these types, given that Haskell is capable of inferring the implementation of typeclasses in simple cases.}}{16}{figure.caption.17}%
-\contentsline {figure}{\numberline {2.13}{\ignorespaces The \texttt {CT} type is a function of from time related information to an arbitrary potentially effectful outcome value.}}{17}{figure.caption.18}%
-\contentsline {figure}{\numberline {2.14}{\ignorespaces The \texttt {CT} type can leverage monad transformers in Haskell via \texttt {Reader} in combination with \texttt {IO}.}}{17}{figure.caption.19}%
-\addvspace {10\p@ }
-\contentsline {figure}{\numberline {3.1}{\ignorespaces Given a parametric record \texttt {ps} and a dynamic value \texttt {da}, the \textit {fmap} functor of the \texttt {CT} type applies the former to the latter. Because the final result is wrapped inside the \texttt {IO} shell, a second \textit {fmap} is necessary.}}{19}{figure.caption.20}%
-\contentsline {figure}{\numberline {3.2}{\ignorespaces With the \texttt {Applicative} typeclass, it is possible to cope with functions inside the \texttt {CT} type. Again, the \textit {fmap} from \texttt {IO} is being used in the implementation.}}{20}{figure.caption.21}%
-\contentsline {figure}{\numberline {3.3}{\ignorespaces The $>>=$ operator used in the implementation is the \textit {bind} from the \texttt {IO} shell. This indicates that when dealing with monads within monads, it is frequent to use the implementation of the internal members.}}{21}{figure.caption.22}%
-\contentsline {figure}{\numberline {3.4}{\ignorespaces The typeclass \texttt {MonadIO} transforms a given value wrapped in \texttt {IO} into a different monad. In this case, the parameter \texttt {m} of the function is the output of the \texttt {CT} type.}}{21}{figure.caption.23}%
-\contentsline {figure}{\numberline {3.5}{\ignorespaces The ability of lifting numerical values to the \texttt {CT} type resembles three FF-GPAC analog circuits: \texttt {Constant}, \texttt {Adder} and \texttt {Multiplier}.}}{22}{figure.caption.24}%
-\contentsline {figure}{\numberline {3.6}{\ignorespaces State Machines are a common abstraction in computer science due to its easy mapping between function calls and states. Memory regions and peripherals are embedded with the idea of a state, not only pure functions. Further, side effects can even act as the trigger to move from one state to another, meaning that executing a simple function can do more than return a value. Its internal guts can significantly modify the state machine.}}{23}{figure.caption.25}%
-\contentsline {figure}{\numberline {3.7}{\ignorespaces The integrator functions attend the rules of composition of FF-GPAC, whilst the \texttt {CT} and \texttt {Integrator} types match the four basic units.}}{28}{figure.caption.26}%
-\addvspace {10\p@ }
-\contentsline {figure}{\numberline {4.1}{\ignorespaces The integrator functions are essential to create and interconnect combinational and feedback-dependent circuits.}}{32}{figure.caption.27}%
-\contentsline {figure}{\numberline {4.2}{\ignorespaces The developed DSL translates a system described by differential equations to an executable model that resembles FF-GPAC's description.}}{32}{figure.caption.28}%
-\contentsline {figure}{\numberline {4.3}{\ignorespaces Because the list implements the \texttt {Traversable} typeclass, it allows this type to use the \textit {traverse} and \textit {sequence} functions, in which both are related to changing the internal behaviour of the nested structures.}}{33}{figure.caption.29}%
-\contentsline {figure}{\numberline {4.4}{\ignorespaces A \textbf {state vector} comprises multiple state variables and requires the use of the \textit {sequence} function to sync time across all variables.}}{33}{figure.caption.30}%
-\contentsline {figure}{\numberline {4.5}{\ignorespaces When building a model for simulation, the above pipeline is always used, from both points of view. The operations with meaning, i.e., the ones in the \texttt {Semantics} pipeline, are mapped to executable operations in the \texttt {Operational} pipeline, and vice-versa.}}{34}{figure.caption.31}%
-\contentsline {figure}{\numberline {4.6}{\ignorespaces Using only FF-GPAC's basic units and their composition rules, it's possible to model the Lorenz Attractor example.}}{37}{figure.caption.32}%
-\contentsline {figure}{\numberline {4.7}{\ignorespaces After \textit {createInteg}, this record is the final image of the integrator. The function \textit {initialize} gives us protecting against wrong records of the type \texttt {Parameters}, assuring it begins from the first iteration, i.e., $t_0$.}}{38}{figure.caption.33}%
-\contentsline {figure}{\numberline {4.8}{\ignorespaces After \textit {readInteg}, the final floating point values is obtained by reading from memory a computation and passing to it the received parameters record. The result of this application, $v$, is the returned value.}}{39}{figure.caption.34}%
-\contentsline {figure}{\numberline {4.9}{\ignorespaces The \textit {updateInteg} function only does side effects, meaning that only affects memory. The internal variable \texttt {c} is a pointer to the computation \textit {itself}, i.e., the computation being created references this exact procedure.}}{39}{figure.caption.35}%
-\contentsline {figure}{\numberline {4.10}{\ignorespaces After setting up the environment, this is the final depiction of an independent variable. The reader $x$ reads the values computed by the procedure stored in memory, a second-order Runge-Kutta method in this case.}}{40}{figure.caption.36}%
-\contentsline {figure}{\numberline {4.11}{\ignorespaces The Lorenz's Attractor example has a very famous butterfly shape from certain angles and constant values in the graph generated by the solution of the differential equations..}}{41}{figure.caption.37}%
-\addvspace {10\p@ }
-\contentsline {figure}{\numberline {5.1}{\ignorespaces During simulation, functions change the time domain to the one that better fits certain entities, such as the \texttt {Solver} and the driver. The image is heavily inspired by a figure in~\cite {Edil2017}.}}{42}{figure.caption.38}%
-\contentsline {figure}{\numberline {5.2}{\ignorespaces Updated auxiliary types for the \texttt {Parameters} type.}}{44}{figure.caption.39}%
-\contentsline {figure}{\numberline {5.3}{\ignorespaces Linear interpolation is being used to transition us back to the continuous domain..}}{47}{figure.caption.40}%
-\contentsline {figure}{\numberline {5.4}{\ignorespaces The new \textit {updateInteg} function add linear interpolation to the pipeline when receiving a parametric record.}}{48}{figure.caption.41}%
-\addvspace {10\p@ }
-\contentsline {figure}{\numberline {6.1}{\ignorespaces With just a few iterations, the exponential behaviour of the implementation is already noticeable.}}{50}{figure.caption.43}%
-\contentsline {figure}{\numberline {6.2}{\ignorespaces The new \textit {createInteg} function relies on interpolation composed with memoization. Also, this combination \textbf {produces} results from the computation located in a different memory region, the one pointed by the \texttt {computation} pointer in the integrator.}}{56}{figure.caption.45}%
-\contentsline {figure}{\numberline {6.3}{\ignorespaces The function \textbf {reads} information from the caching pointer, rather than the pointer where the solvers compute the results.}}{57}{figure.caption.46}%
-\contentsline {figure}{\numberline {6.4}{\ignorespaces The new \textit {updateInteg} function gives to the solver functions access to the region with the cached data.}}{58}{figure.caption.47}%
-\contentsline {figure}{\numberline {6.5}{\ignorespaces Caching changes the direction of walking through the iteration axis. It also removes an entire pass through the previous iterations.}}{59}{figure.caption.48}%
-\contentsline {figure}{\numberline {6.6}{\ignorespaces By using a logarithmic scale, we can see that the final implementation is performant with more than 100 million iterations in the simulation.}}{63}{figure.caption.51}%
-\addvspace {10\p@ }
-\contentsline {figure}{\numberline {7.1}{\ignorespaces Resettable counter in hardware, inspired by Levent's works~\cite {levent2000, levent2002}.}}{68}{figure.caption.52}%
-\contentsline {figure}{\numberline {7.2}{\ignorespaces Diagram of \texttt {createInteg} primitive for intuition..}}{70}{figure.caption.53}%
-\contentsline {figure}{\numberline {7.3}{\ignorespaces Results of FFACT are similar to the final version of FACT..}}{73}{figure.caption.54}%
+\contentsline {figure}{\numberline {1.1}{\ignorespaces The translation between the world of software and the mathematical description of differential equations are more concise and explicit in \texttt {FFACT}.}}{4}{figure.caption.8}%
+\addvspace {10\p@ }
+\contentsline {figure}{\numberline {2.1}{\ignorespaces The combination of these four basic units compose any GPAC circuit (taken from~\cite {Edil2018} with permission).}}{9}{figure.caption.9}%
+\contentsline {figure}{\numberline {2.2}{\ignorespaces Polynomial circuits resembles combinational circuits, in which the circuit respond instantly to changes on its inputs (taken from~\cite {Edil2018} with permission).}}{10}{figure.caption.10}%
+\contentsline {figure}{\numberline {2.3}{\ignorespaces Types are not just labels; they enhance the manipulated data with new information. Their difference in shape can work as the interface for the data.}}{11}{figure.caption.11}%
+\contentsline {figure}{\numberline {2.4}{\ignorespaces Functions' signatures are contracts; they purespecify which shape the input information has as well as which shape the output information will have.}}{11}{figure.caption.11}%
+\contentsline {figure}{\numberline {2.5}{\ignorespaces Sum types can be understood in terms of sets, in which the members of the set are available candidates for the outer shell type. Parity and possible values in digital states are examples.}}{12}{figure.caption.12}%
+\contentsline {figure}{\numberline {2.6}{\ignorespaces Product types are a combination of different sets, where you pick a representative from each one. Digital clocks' time and objects' coordinates in space are common use cases. In Haskell, a product type can be defined using a \textit {record} alongside with the constructor, where the labels for each member inside it are explicit.}}{12}{figure.caption.13}%
+\contentsline {figure}{\numberline {2.7}{\ignorespaces Depending on the application, different representations of the same structure need to used due to the domain of interest and/or memory constraints.}}{13}{figure.caption.14}%
+\contentsline {figure}{\numberline {2.8}{\ignorespaces The minimum requirement for the \texttt {Ord} typeclass is the $<=$ operator, meaning that the functions $<$, $<=$, $>$, $>=$, \texttt {max} and \texttt {min} are now unlocked for the type \texttt {ClockTime} after the implementation. Typeclasses can be viewed as a third dimension in a type.}}{13}{figure.caption.15}%
+\contentsline {figure}{\numberline {2.9}{\ignorespaces Replacements for the validation function within a pipeline like the above are common.}}{14}{figure.caption.16}%
+\contentsline {figure}{\numberline {2.10}{\ignorespaces The initial value is used as a starting point for the procedure. The algorithm continues until the time of interest is reached in the unknown function. Due to its large time step, the final answer is really far-off from the expected result.}}{16}{figure.caption.17}%
+\contentsline {figure}{\numberline {2.11}{\ignorespaces In Haskell, the \texttt {type} keyword works for alias. The first draft of the \texttt {CT} type is a \textit {function}, in which providing a floating point value as time returns another value as outcome.}}{16}{figure.caption.18}%
+\contentsline {figure}{\numberline {2.12}{\ignorespaces The \texttt {Parameters} type represents a given moment in time, carrying over all the necessary information to execute a solver step until the time limit is reached. Some useful typeclasses are being derived to these types, given that Haskell is capable of inferring the implementation of typeclasses in simple cases.}}{17}{figure.caption.19}%
+\contentsline {figure}{\numberline {2.13}{\ignorespaces The \texttt {CT} type is a function of from time related information to an arbitrary potentially effectful outcome value.}}{18}{figure.caption.20}%
+\contentsline {figure}{\numberline {2.14}{\ignorespaces The \texttt {CT} type can leverage monad transformers in Haskell via \texttt {Reader} in combination with \texttt {IO}.}}{18}{figure.caption.21}%
+\addvspace {10\p@ }
+\contentsline {figure}{\numberline {3.1}{\ignorespaces Given a parametric record \texttt {ps} and a dynamic value \texttt {da}, the \textit {fmap} functor of the \texttt {CT} type applies the former to the latter. Because the final result is wrapped inside the \texttt {IO} shell, a second \textit {fmap} is necessary.}}{20}{figure.caption.22}%
+\contentsline {figure}{\numberline {3.2}{\ignorespaces With the \texttt {Applicative} typeclass, it is possible to cope with functions inside the \texttt {CT} type. Again, the \textit {fmap} from \texttt {IO} is being used in the implementation.}}{21}{figure.caption.23}%
+\contentsline {figure}{\numberline {3.3}{\ignorespaces The $>>=$ operator used in the implementation is the \textit {bind} from the \texttt {IO} shell. This indicates that when dealing with monads within monads, it is frequent to use the implementation of the internal members.}}{22}{figure.caption.24}%
+\contentsline {figure}{\numberline {3.4}{\ignorespaces The typeclass \texttt {MonadIO} transforms a given value wrapped in \texttt {IO} into a different monad. In this case, the parameter \texttt {m} of the function is the output of the \texttt {CT} type.}}{22}{figure.caption.25}%
+\contentsline {figure}{\numberline {3.5}{\ignorespaces The ability of lifting numerical values to the \texttt {CT} type resembles three FF-GPAC analog circuits: \texttt {Constant}, \texttt {Adder} and \texttt {Multiplier}.}}{23}{figure.caption.26}%
+\contentsline {figure}{\numberline {3.6}{\ignorespaces Example of a State Machine}}{24}{figure.caption.27}%
+\contentsline {figure}{\numberline {3.7}{\ignorespaces The integrator functions attend the rules of composition of FF-GPAC, whilst the \texttt {CT} and \texttt {Integrator} types match the four basic units.}}{29}{figure.caption.28}%
+\addvspace {10\p@ }
+\contentsline {figure}{\numberline {4.1}{\ignorespaces The integrator functions are essential to create and interconnect combinational and feedback-dependent circuits.}}{33}{figure.caption.29}%
+\contentsline {figure}{\numberline {4.2}{\ignorespaces The developed DSL translates a system described by differential equations to an executable model that resembles FF-GPAC's description.}}{33}{figure.caption.30}%
+\contentsline {figure}{\numberline {4.3}{\ignorespaces Because the list implements the \texttt {Traversable} typeclass, it allows this type to use the \textit {traverse} and \textit {sequence} functions, in which both are related to changing the internal behaviour of the nested structures.}}{34}{figure.caption.31}%
+\contentsline {figure}{\numberline {4.4}{\ignorespaces A \textit {state vector} comprises multiple state variables and requires the use of the \textit {sequence} function to sync time across all variables.}}{34}{figure.caption.32}%
+\contentsline {figure}{\numberline {4.5}{\ignorespaces Execution pipeline of a model.}}{35}{figure.caption.33}%
+\contentsline {figure}{\numberline {4.6}{\ignorespaces Using only FF-GPAC's basic units and their composition rules, it's possible to model the Lorenz Attractor example.}}{38}{figure.caption.34}%
+\contentsline {figure}{\numberline {4.7}{\ignorespaces After \textit {createInteg}, this record is the final image of the integrator. The function \textit {initialize} gives us protecting against wrong records of the type \texttt {Parameters}, assuring it begins from the first iteration, i.e., $t_0$.}}{39}{figure.caption.35}%
+\contentsline {figure}{\numberline {4.8}{\ignorespaces After \textit {readInteg}, the final floating point values is obtained by reading from memory a computation and passing to it the received parameters record. The result of this application, $v$, is the returned value.}}{40}{figure.caption.36}%
+\contentsline {figure}{\numberline {4.9}{\ignorespaces The \textit {updateInteg} function only does side effects, meaning that only affects memory. The internal variable \texttt {c} is a pointer to the computation \textit {itself}, i.e., the computation being created references this exact procedure.}}{40}{figure.caption.37}%
+\contentsline {figure}{\numberline {4.10}{\ignorespaces After setting up the environment, this is the final depiction of an independent variable. The reader $x$ reads the values computed by the procedure stored in memory, a second-order Runge-Kutta method in this case.}}{41}{figure.caption.38}%
+\contentsline {figure}{\numberline {4.11}{\ignorespaces The Lorenz's Attractor example has a very famous butterfly shape from certain angles and constant values in the graph generated by the solution of the differential equations..}}{42}{figure.caption.39}%
+\addvspace {10\p@ }
+\contentsline {figure}{\numberline {5.1}{\ignorespaces During simulation, functions change the time domain to the one that better fits certain entities, such as the \texttt {Solver} and the driver. The image is heavily inspired by a figure in~\cite {Edil2017}.}}{43}{figure.caption.40}%
+\contentsline {figure}{\numberline {5.2}{\ignorespaces Updated auxiliary types for the \texttt {Parameters} type.}}{45}{figure.caption.41}%
+\contentsline {figure}{\numberline {5.3}{\ignorespaces Linear interpolation is being used to transition us back to the continuous domain..}}{48}{figure.caption.42}%
+\contentsline {figure}{\numberline {5.4}{\ignorespaces The new \textit {updateInteg} function add linear interpolation to the pipeline when receiving a parametric record.}}{49}{figure.caption.43}%
+\addvspace {10\p@ }
+\contentsline {figure}{\numberline {6.1}{\ignorespaces With just a few iterations, the exponential behaviour of the implementation is already noticeable.}}{51}{figure.caption.45}%
+\contentsline {figure}{\numberline {6.2}{\ignorespaces The new \textit {createInteg} function relies on interpolation composed with memoization. Also, this combination \textit {produces} results from the computation located in a different memory region, the one pointed by the \texttt {computation} pointer in the integrator.}}{57}{figure.caption.47}%
+\contentsline {figure}{\numberline {6.3}{\ignorespaces The function \textit {reads} information from the caching pointer, rather than the pointer where the solvers compute the results.}}{58}{figure.caption.48}%
+\contentsline {figure}{\numberline {6.4}{\ignorespaces The new \textit {updateInteg} function gives to the solver functions access to the region with the cached data.}}{59}{figure.caption.49}%
+\contentsline {figure}{\numberline {6.5}{\ignorespaces Caching changes the direction of walking through the iteration axis. It also removes an entire pass through the previous iterations.}}{60}{figure.caption.50}%
+\contentsline {figure}{\numberline {6.6}{\ignorespaces By using a logarithmic scale, we can see that the final implementation is performant with more than 100 million iterations in the simulation.}}{64}{figure.caption.53}%
+\addvspace {10\p@ }
+\contentsline {figure}{\numberline {7.1}{\ignorespaces Execution pipeline of a model.}}{66}{figure.caption.54}%
+\contentsline {figure}{\numberline {7.2}{\ignorespaces Resettable counter in hardware, inspired by Levent's works~\cite {levent2000, levent2002}.}}{69}{figure.caption.55}%
+\contentsline {figure}{\numberline {7.3}{\ignorespaces Diagram of \texttt {createInteg} primitive for intuition.}}{72}{figure.caption.56}%
+\contentsline {figure}{\numberline {7.4}{\ignorespaces Results of FFACT are similar to the final version of FACT..}}{75}{figure.caption.57}%
+\contentsline {figure}{\numberline {7.5}{\ignorespaces Comparison of the Lorenz Attractor Model between FFACT and a Simulink implementation~\cite {Simulink}.}}{76}{figure.caption.58}%
+\contentsline {figure}{\numberline {7.6}{\ignorespaces Comparison of the Lorenz Attractor Model between FFACT and a Matlab implementation.}}{76}{figure.caption.59}%
+\contentsline {figure}{\numberline {7.7}{\ignorespaces Comparison of the Lorenz Attractor Model between FFACT and a Mathematica implementation.}}{77}{figure.caption.60}%
+\contentsline {figure}{\numberline {7.8}{\ignorespaces Comparison of the Lorenz Attractor Model between FFACT and a Yampa implementation.}}{77}{figure.caption.61}%
 \addvspace {10\p@ }
 \addvspace {10\p@ }
 \babel@toc {american}{}\relax 
diff --git a/doc/MastersThesis/thesis.toc b/doc/MastersThesis/thesis.toc
index ee6b495..beb0bee 100644
--- a/doc/MastersThesis/thesis.toc
+++ b/doc/MastersThesis/thesis.toc
@@ -2,47 +2,52 @@
 \babel@toc {american}{}\relax 
 \babel@toc {american}{}\relax 
 \contentsline {chapter}{\numberline {1}Introduction}{1}{chapter.1}%
-\contentsline {section}{\numberline {1.1}Proposal}{2}{section.1.1}%
-\contentsline {section}{\numberline {1.2}Goal}{4}{section.1.2}%
-\contentsline {section}{\numberline {1.3}Outline}{6}{section.1.3}%
-\contentsline {chapter}{\numberline {2}Design Philosophy}{7}{chapter.2}%
-\contentsline {section}{\numberline {2.1}Shannon's Foundation: GPAC}{7}{section.2.1}%
-\contentsline {section}{\numberline {2.2}The Shape of Information}{9}{section.2.2}%
-\contentsline {section}{\numberline {2.3}Modeling Reality}{13}{section.2.3}%
-\contentsline {section}{\numberline {2.4}Making Mathematics Cyber}{15}{section.2.4}%
-\contentsline {chapter}{\numberline {3}Effectful Integrals}{18}{chapter.3}%
-\contentsline {section}{\numberline {3.1}Uplifting the CT Type}{18}{section.3.1}%
-\contentsline {section}{\numberline {3.2}GPAC Bind I: CT}{21}{section.3.2}%
-\contentsline {section}{\numberline {3.3}Exploiting Impurity}{23}{section.3.3}%
-\contentsline {section}{\numberline {3.4}GPAC Bind II: Integrator}{26}{section.3.4}%
-\contentsline {section}{\numberline {3.5}Using Recursion to solve Math}{28}{section.3.5}%
-\contentsline {chapter}{\numberline {4}Execution Walkthrough}{31}{chapter.4}%
-\contentsline {section}{\numberline {4.1}From Models to Models}{31}{section.4.1}%
-\contentsline {section}{\numberline {4.2}Driving the Model}{34}{section.4.2}%
-\contentsline {section}{\numberline {4.3}An attractive example}{35}{section.4.3}%
-\contentsline {section}{\numberline {4.4}Lorenz's Butterfly}{41}{section.4.4}%
-\contentsline {chapter}{\numberline {5}Travelling across Domains}{42}{chapter.5}%
-\contentsline {section}{\numberline {5.1}Time Domains}{42}{section.5.1}%
-\contentsline {section}{\numberline {5.2}Tweak I: Interpolation}{44}{section.5.2}%
-\contentsline {chapter}{\numberline {6}Caching the Speed Pill}{49}{chapter.6}%
-\contentsline {section}{\numberline {6.1}Performance}{49}{section.6.1}%
-\contentsline {section}{\numberline {6.2}The Saving Strategy}{51}{section.6.2}%
-\contentsline {section}{\numberline {6.3}Tweak II: Memoization}{52}{section.6.3}%
-\contentsline {section}{\numberline {6.4}A change in Perspective}{58}{section.6.4}%
-\contentsline {section}{\numberline {6.5}Tweak III: Model and Driver}{59}{section.6.5}%
-\contentsline {section}{\numberline {6.6}Results with Caching}{61}{section.6.6}%
-\contentsline {chapter}{\numberline {7}Fixing Recursion}{64}{chapter.7}%
-\contentsline {section}{\numberline {7.1}Integrator's Noise}{64}{section.7.1}%
-\contentsline {section}{\numberline {7.2}The Fixed-Point Combinator}{65}{section.7.2}%
-\contentsline {section}{\numberline {7.3}Value Recursion with Fixed-Points}{67}{section.7.3}%
-\contentsline {section}{\numberline {7.4}Tweak IV: Fixing FACT}{70}{section.7.4}%
-\contentsline {chapter}{\numberline {8}Conclusion}{74}{chapter.8}%
-\contentsline {section}{\numberline {8.1}Limitations}{74}{section.8.1}%
-\contentsline {section}{\numberline {8.2}Future Improvements}{75}{section.8.2}%
-\contentsline {section}{\numberline {8.3}Final Thoughts}{77}{section.8.3}%
-\contentsline {chapter}{\numberline {9}Appendix}{78}{chapter.9}%
-\contentsline {section}{\numberline {9.1}Literate Programming}{78}{section.9.1}%
-\contentsline {chapter}{References}{80}{section*.55}%
+\contentsline {section}{\numberline {1.1}Contribution}{2}{section.1.1}%
+\contentsline {subsection}{\numberline {1.1.1}Executable Simulation}{3}{subsection.1.1.1}%
+\contentsline {subsection}{\numberline {1.1.2}Formal Foundation}{4}{subsection.1.1.2}%
+\contentsline {subsection}{\numberline {1.1.3}Conciseness}{5}{subsection.1.1.3}%
+\contentsline {section}{\numberline {1.2}Outline}{6}{section.1.2}%
+\contentsline {chapter}{\numberline {2}Design Philosophy}{8}{chapter.2}%
+\contentsline {section}{\numberline {2.1}Shannon's Foundation: GPAC}{8}{section.2.1}%
+\contentsline {section}{\numberline {2.2}The Shape of Information}{10}{section.2.2}%
+\contentsline {section}{\numberline {2.3}Modeling Reality}{14}{section.2.3}%
+\contentsline {section}{\numberline {2.4}Making Mathematics Cyber}{16}{section.2.4}%
+\contentsline {chapter}{\numberline {3}Effectful Integrals}{19}{chapter.3}%
+\contentsline {section}{\numberline {3.1}Uplifting the CT Type}{19}{section.3.1}%
+\contentsline {section}{\numberline {3.2}GPAC Bind I: CT}{22}{section.3.2}%
+\contentsline {section}{\numberline {3.3}Exploiting Impurity}{24}{section.3.3}%
+\contentsline {section}{\numberline {3.4}GPAC Bind II: Integrator}{27}{section.3.4}%
+\contentsline {section}{\numberline {3.5}Using Recursion to solve Math}{29}{section.3.5}%
+\contentsline {chapter}{\numberline {4}Execution Walkthrough}{32}{chapter.4}%
+\contentsline {section}{\numberline {4.1}From Models to Models}{32}{section.4.1}%
+\contentsline {section}{\numberline {4.2}Driving the Model}{35}{section.4.2}%
+\contentsline {section}{\numberline {4.3}An attractive example}{36}{section.4.3}%
+\contentsline {section}{\numberline {4.4}Lorenz's Butterfly}{42}{section.4.4}%
+\contentsline {chapter}{\numberline {5}Travelling across Domains}{43}{chapter.5}%
+\contentsline {section}{\numberline {5.1}Time Domains}{43}{section.5.1}%
+\contentsline {section}{\numberline {5.2}Tweak I: Interpolation}{45}{section.5.2}%
+\contentsline {chapter}{\numberline {6}Caching the Speed Pill}{50}{chapter.6}%
+\contentsline {section}{\numberline {6.1}Performance}{50}{section.6.1}%
+\contentsline {section}{\numberline {6.2}The Saving Strategy}{52}{section.6.2}%
+\contentsline {section}{\numberline {6.3}Tweak II: Memoization}{53}{section.6.3}%
+\contentsline {section}{\numberline {6.4}A change in Perspective}{59}{section.6.4}%
+\contentsline {section}{\numberline {6.5}Tweak III: Model and Driver}{60}{section.6.5}%
+\contentsline {section}{\numberline {6.6}Results with Caching}{62}{section.6.6}%
+\contentsline {chapter}{\numberline {7}Fixing Recursion}{65}{chapter.7}%
+\contentsline {section}{\numberline {7.1}Integrator's Noise}{65}{section.7.1}%
+\contentsline {section}{\numberline {7.2}The Fixed-Point Combinator}{67}{section.7.2}%
+\contentsline {section}{\numberline {7.3}Value Recursion with Fixed-Points}{69}{section.7.3}%
+\contentsline {section}{\numberline {7.4}Tweak IV: Fixing FACT}{71}{section.7.4}%
+\contentsline {section}{\numberline {7.5}Examples and Comparisons}{75}{section.7.5}%
+\contentsline {chapter}{\numberline {8}Conclusion}{78}{chapter.8}%
+\contentsline {section}{\numberline {8.1}Final Thoughts}{78}{section.8.1}%
+\contentsline {section}{\numberline {8.2}Future Work}{79}{section.8.2}%
+\contentsline {subsection}{\numberline {8.2.1}Formalism}{79}{subsection.8.2.1}%
+\contentsline {subsection}{\numberline {8.2.2}Extensions}{80}{subsection.8.2.2}%
+\contentsline {subsection}{\numberline {8.2.3}Refactoring}{80}{subsection.8.2.3}%
+\contentsline {chapter}{\numberline {9}Appendix}{82}{chapter.9}%
+\contentsline {section}{\numberline {9.1}Literate Programming}{82}{section.9.1}%
+\contentsline {chapter}{References}{84}{section*.62}%
 \babel@toc {american}{}\relax 
 \babel@toc {american}{}\relax 
 \babel@toc {american}{}\relax 
diff --git a/src/Examples/Lorenz.hs b/src/Examples/Lorenz.hs
index 3fe3455..225e026 100644
--- a/src/Examples/Lorenz.hs
+++ b/src/Examples/Lorenz.hs
@@ -47,7 +47,7 @@ lorenzSolver100M = Solver { dt = 0.000001,
                             method = RungeKutta2,
                             stage = SolverStage 0
                           }
-
+  
 
 lorenzSolver1B = Solver { dt = 0.0000001,
                             method = RungeKutta2,
@@ -76,6 +76,13 @@ lorenzModel = mdo
        beta = 8.0 / 3.0
    return $ sequence [x, y, z]
 
+lorenzSolverYampa = Solver { dt = 0.01,
+                           method = Euler,
+                           stage = SolverStage 0
+                         }
+
+lorenzYampa = runCTFinal lorenzModel 1000 lorenzSolverYampa
+
 lorenz100 = runCTFinal lorenzModel 100 lorenzSolver100
 
 lorenz1k = runCTFinal lorenzModel 100 lorenzSolver1k