-\begin{lstClean}[numbers=left,caption={The \gls{UI} and code for entering a person in \gls{ITASK}.},label={lst:enter_person}]
-:: Person = { name :: String, gender :: Gender, dateOfBirth :: Date }[+\label{lst:dt_fro}+]
-:: Gender = Male | Female | Other String[+\label{lst:dt_to}+]
-
-derive class iTask Person, Gender[+\label{lst:dt_derive}+]
-
-enterPerson :: Task Person
-enterPerson
- = Hint "Enter a person:" @>> enterInformation [][+\label{lst:task_ui}+]
- >>! \result->Hint "You Entered:" @>> viewInformation [] result[+\label{lst:task_comb}+]
-\end{lstClean}
-
-\subsection{\texorpdfstring{\Gls{MTASK}}{MTask}}
-This thesis uses \gls{ITASK} in conjunction with \gls{MTASK}, an innovative \gls{TOP} language designed for defining interactive systems for \gls{IOT} edge devices \citep{koopman_task-based_2018}.
-It is written in \gls{CLEAN} as a multi-view \gls{EDSL} and hence there are multiple interpretations of the language of which the byte code compiler is the most relevant for this thesis.
-From the terms in the \gls{TOP} language, a very compact binary representation of the work that needs to be done is compiled.
-This specification is then sent to a device that runs the \gls{MTASK} \gls{RTS}, a domain-specific \gls{TOP} engine implemented as a feather-light domain-specific \gls{OS}.
-\Gls{MTASK} is seamlessly integrated with \gls{ITASK}, it allows the programmer to define all layers of an \gls{IOT} system from a single declarative specification.
-
-\todo[inline]{Is this example useful? I think it's too technical}
-\Cref{lst:intro_blink} shows an interactive \gls{MTASK}\slash{}\gls{ITASK} application for blinking \pgls{LED} on the microcontroller every user-specified interval.
-\Crefrange{lst:intro:itask_fro}{lst:intro:itask_to} show the \gls{ITASK} part.
-First a \gls{SDS} is defined to communicate the blinking interval, then the \gls{MTASK} is connected using \cleaninline{withDevice}.
-Once connected, the \cleaninline{intBlink} task is sent to the device (\cref{lst:intro_liftmtask}) and in parallel, the value of the interval \gls{SDS} can be updated using an editor (\cref{lst:intro_editor}).
-The \cleaninline{intBlink} task (\crefrange{lst:intro:mtask_fro}{lst:intro:mtask_to}) is the \gls{MTASK} part of the application that has its own tasks, \glspl{SDS}, and \gls{UOD}.
-This task first defines \gls{GPIO} pin 13 to be of the output type (\cref{lst:intro:declarePin}) followed by lifting the \gls{ITASK} \gls{SDS} to an \gls{MTASK} \gls{SDS} (\cref{lst:intro:liftsds}).
-The main expression of the program calls the \cleaninline{blink} function with the initial state.
-This function on \crefrange{lst:intro:blink_fro}{lst:intro:blink_to} first reads the interval \gls{SDS}, waits the specified delay, writes the state to the \gls{GPIO} pin and calls itself recursively using the inverse of the state.
-
-\begin{lstClean}[numbers=left,caption={\Gls{MTASK}\slash{}\gls{ITASK} interactive blinking.},label={lst:intro_blink}]
-interactiveBlink :: Task Int[+\label{lst:intro:itask_fro}+]
-interactiveBlink =
- withShared 500 \iInterval->[+\label{lst:intro_withshared}+]
- withDevice {TCPSettings | host = ..., port = ...} \dev->
- liftmTask (intBlink iInterval) dev[+\label{lst:intro_liftmtask}+]
- -|| Hint "Interval (ms)" @>> updateSharedInformation [] iInterval[+\label{lst:intro_editor}+][+\label{lst:intro:itask_to}+]
-
-intBlink :: Shared sds Int -> MTask v Int | mtask, liftsds v & RWShared sds[+\label{lst:intro:mtask_fro}+]
-intBlink iInterval =
- declarePin D13 PMOutput \d13->[+\label{lst:intro:declarePin}+]
- liftsds \mInterval=iInterval[+\label{lst:intro:liftsds}+]
- In fun \blink=(\st->[+\label{lst:intro:blink_fro}+]
- getSds mInterval >>=. \i->delay i
- >>|. writeD d13 st >>|. blink (Not st))[+\label{lst:intro:blink_to}+]
- In {main = blink true}[+\label{lst:intro:mtask_to}+]
-\end{lstClean}
-
-\subsection{Other \texorpdfstring{\glsxtrshort{TOP}}{TOP} languages}
-While \gls{ITASK} conceived \gls{TOP}, it is not the only \gls{TOP} language and engine.
-Some \gls{TOP} languages and systems arose from Master's and Bachelor's thesis projects (e.g.\ \textmu{}Task \citep{piers_task-oriented_2016} and LTasks \citep{van_gemert_task_2022}) or were created to solve a practical problem (e.g.\ Toppyt \citep{lijnse_toppyt_2022} and hTask \citep{lubbers_htask_2022}).
-Furthermore, \gls{TOPHAT} is a fully formally specified \gls{TOP} language designed to capture the essence of \gls{TOP} formally \citep{steenvoorden_tophat_2019}.
-It is also possible to translate \gls{TOPHAT} code to \gls{ITASK} to piggyback on the \gls{TOP} engine it offers \citep[\citesection{G.3}]{steenvoorden_tophat_2022}.
-
-\section{Contributions}\label{sec:contributions}
-This section provides a thorough overview of the relation to publications and the scientific contributions of the episodes and chapters.
+As an example, \cref{lst:todo,fig:todo} show the code and \gls{UI} for an interactive to-do list application.
+The user modifies a shared to-do list through an editor directly or using some predefined actions.
+Furthermore, in parallel, the length of the list is shown to demonstrate \glspl{SDS}.
+Using \gls{ITASK}, complex collaborations of users and tasks can be described on a high level.
+
+From the data type definitions (\cref{lst:todo_dt}), using generic programming (\cref{lst:todo_derive}), the \glspl{UI} for the data types are automatically generated.
+Then, using the parallel task combinator (\cleaninline{-\|\|}) the task for updating the to-dos (\cref{lst:todo_update}) and the task for viewing the length are combined (\cref{lst:todo_length}).
+This particular parallel combinator uses the result of the left-hand side task.
+Both tasks operate on the to-do \gls{SDS} (\cref{lst:todo_sds}).
+The task for updating the to-do list is an editor (\cref{lst:todo_editor}) combined using a step combinator (\crefrange{lst:todo_contfro}{lst:todo_contto}).
+The actions either change the value, sorting or clearing it, or terminate the task by returning the current value of the \gls{SDS}.
+Special combinators (e.g.\ \cleaninline{@>>} at \cref{lst:todo_ui}) are used to tweak the \gls{UI} to display informative labels.
+
+\cleaninputlisting[float=,firstline=6,lastline=22,tabsize=3,numbers=left,caption={The code for a shared to-do list in \gls{ITASK}.},label={lst:todo}]{lst/sharedlist.icl}
+
+\begin{figure}
+ \centering
+ \includegraphics[width=\linewidth]{todo0g}
+ \caption{The \gls{UI} for the shared to-do list in \gls{ITASK}.}%
+ \label{fig:todo}
+\end{figure}
+
+\subsection{The mTask system}
+The work for \gls{IOT} edge devices can often be succinctly described by \gls{TOP} programs.
+Software on microcontrollers is usually composed of smaller basic tasks, are interactive, and share data with other components or the server.
+The \gls{ITASK} system seems an obvious candidate for bringing \gls{TOP} to \gls{IOT} edge devices.
+However, an \gls{ITASK} application contains many features that are not needed on \emph{edge devices} such as higher-order tasks, support for a distributed architecture, or a multi-user web server.
+Furthermore, \gls{IOT} edge devices are in general not powerful enough to run or interpret \gls{CLEAN}\slash\gls{ABC} code, they just lack the processor speed and memory.
+To bridge this gap, \gls{MTASK} is developed, a domain-specific \gls{TOP} system for \gls{IOT} edge devices that is integrated in \gls{ITASK} \citep{koopman_task-based_2018}.
+The \gls{ITASK} language abstracts away from details such as user interfaces, data storage, client-side platforms, and persistent workflows.
+On the other hand, \gls{MTASK} offers abstractions for edge layer-specific details such as the heterogeneity of architectures, platforms, and frameworks; peripheral access; (multi) task scheduling; and lowering energy consumption.
+
+The \gls{MTASK} system is seamlessly integrated with \gls{ITASK}.
+Tasks in \gls{MTASK} are integrated in such a way that they function as regular \gls{ITASK} tasks.
+Furthermore, \glspl{SDS} on the device can proxy \gls{ITASK} \glspl{SDS}.
+Using \gls{MTASK}, the programmer can define all layers of an \gls{IOT} system as a single declarative specification.
+The \gls{MTASK} language is written in \gls{CLEAN} as a multi-view \gls{EDSL} and hence there are multiple interpretations possible.
+The byte code compiler is the most relevant for this thesis.
+From an \gls{MTASK} task constructed at run time, a compact binary representation of the work that needs to be done is compiled.
+This byte code is then sent to a device that running the \gls{MTASK} \gls{RTS}.
+This feather-light domain-specific \gls{OS} is written in portable \gls{C} with a minimal device specific interface and it executes the tasks using interpretation and rewriting.
+
+To illustrate \imtask{}, an example application is shown.
+The application is an interactive application for blinking \pgls{LED} on the microcontroller at a certain frequency that can be set and updated at run time.
+\Cref{lst:intro_blink,fig:intro_blink} show the \gls{ITASK} part of the code and a screenshot.
+Using \cleaninline{enterInformation}, the connection specification of the \gls{TCP} device is queried through a web editor (\cref{lst:intro_enterDevice,fig:intro_blink_dev}).
+\Cref{lst:intro_withshared} defines \pgls{SDS} to communicate the blinking interval between the server and the edge device.
+The \gls{MTASK} device is connected using \cleaninline{withDevice} at \cref{lst:intro_withdevice}.
+Once connected, the \cleaninline{intBlink} task is sent to the device (\cref{lst:intro_liftmtask}) and, in parallel, a web editor is shown that updates the value of the interval \gls{SDS} (\cref{lst:intro_editor,fig:intro_blink_int}).
+To allow terminating of the task, the \gls{ITASK} task ends with a sequential operation that returns a constant value when the button is pressed, making the task stable.
+
+\cleaninputlisting[firstline=10,lastline=18,numbers=left,caption={The \gls{ITASK} code for the interactive blinking application.},label={lst:intro_blink}]{lst/blink.icl}
+
+\begin{figure}
+ \centering
+ \begin{subfigure}{.5\textwidth}
+ \centering
+ \includegraphics[width=.9\linewidth]{blink1g}
+ \caption{Device selection.}\label{fig:intro_blink_dev}
+ \end{subfigure}%
+ \begin{subfigure}{.5\textwidth}
+ \centering
+ \includegraphics[width=.9\linewidth]{blink2g}
+ \caption{Changing the interval.}\label{fig:intro_blink_int}
+ \end{subfigure}
+ \caption{The \gls{UI} for the interactive blink application in \gls{MTASK}.}%
+ \label{fig:intro_blink}
+\end{figure}
+
+The \cleaninline{intBlink} task (\cref{lst:intro_blink_mtask}) is the \gls{MTASK} part of the application.
+It has its own tasks, \glspl{SDS}, and \gls{UOD}.
+This task first defines \gls{GPIO} pin 13 to be of the output type (\cref{lst:intro:declarePin}), followed by lifting the \gls{ITASK} \gls{SDS} to an \gls{MTASK} \gls{SDS} (\cref{lst:intro:liftsds}).
+The main expression of the program calls the \cleaninline{blink} function with an initial state.
+This function on \crefrange{lst:intro:blink_fro}{lst:intro:blink_to} first reads the interval \gls{SDS}, waits the specified delay, writes the state to the \gls{GPIO} pin, and calls itself recursively using the inverse of the state in order to run continuously.
+
+\begin{lstClean}[numbers=left,belowskip=0pt]
+intBlink :: (Shared sds Int) -> Main (MTask v Int) | mtask v & ...\end{lstClean}
+\cleaninputlisting[aboveskip=0pt,firstnumber=4,firstline=23,numbers=left,caption={The \gls{MTASK} code for the interactive blinking application.},label={lst:intro_blink_mtask}]{lst/blink.icl}
+
+\subsection{Other TOP languages}
+While \gls{ITASK} conceived \gls{TOP}, it is no longer the only \gls{TOP} system.
+Some \gls{TOP} languages were created to fill a gap encountered in practise.
+Toppyt \citep{lijnse_toppyt_2022} is a general purpose \gls{TOP} language written in \gls{PYTHON} used to host frameworks for modelling command \& control systems, and hTask \citep{lubbers_htask_2022}, a vessel for experimenting with asynchronous \glspl{SDS}.
+Furthermore, some \gls{TOP} systems arose from Master's and Bachelor's thesis projects.
+For example, \textmu{}Task \citep{piers_task-oriented_2016}, a \gls{TOP} language for modelling non-interruptible embedded systems in \gls{HASKELL}, and LTasks \citep{van_gemert_task_2022}, a \gls{TOP} language written in the dynamically typed programming language Lua.
+Finally, there are \gls{TOP} languages with strong academic foundations.
+\Gls{TOPHAT} is a fully formally specified \gls{TOP} language designed to capture the essence of \gls{TOP} \citep{steenvoorden_tophat_2019}.
+Such a formal specification allows for symbolic execution, hint generation, but also the translation to \gls{ITASK} for actually performing the work \citep{steenvoorden_tophat_2022}.
+\Citeauthor{steenvoorden_tophat_2022} distinguishes two instruments for \gls{TOP}: \gls{TOP} languages and \gls{TOP} engines.
+The language is the \emph{formal} language for specifying interactive systems.
+The engine is the software or hardware that executes these specifications as a ready-for-work application.
+
+\section{Contributions}%
+\label{sec:contributions}
+This section provides a thorough overview of the relation between the scientific publications and the contents of this thesis.