process many comments

[phd-thesis.git] / top / int.tex

diff --git a/top/int.tex b/top/int.tex
index 1051188..1a4eb01 100644 (file)
--- a/top/int.tex
+++ b/top/int.tex
@@ -1,12 +1,13 @@
+%chktex-file 17

 \documentclass[../thesis.tex]{subfiles}
 
 \input{subfilepreamble}
 
 \documentclass[../thesis.tex]{subfiles}
 
 \input{subfilepreamble}
 

-\setcounter{chapter}{5}
+\setcounter{chapter}{6}

 
 \begin{document}
 \input{subfileprefix}
 
 \begin{document}
 \input{subfileprefix}

-\chapter{Integration of \texorpdfstring{\gls{MTASK}}{mTask} and \texorpdfstring{\gls{ITASK}}{iTask}}%
+\chapter{Integration of mTask and iTask}%

 \label{chp:integration_with_itask}
 \begin{chapterabstract}
        This chapter shows the integration of \gls{MTASK} and \gls{ITASK} by showing:
 \label{chp:integration_with_itask}
 \begin{chapterabstract}
        This chapter shows the integration of \gls{MTASK} and \gls{ITASK} by showing:


@@ -14,13 +15,15 @@
                \item an architectural overview of \gls{MTASK} applications;
                \item the interface for connecting devices;
                \item the interface for lifting \gls{MTASK} tasks to \gls{ITASK} tasks;
                \item an architectural overview of \gls{MTASK} applications;
                \item the interface for connecting devices;
                \item the interface for lifting \gls{MTASK} tasks to \gls{ITASK} tasks;

-               \item a interface for lowering \gls{ITASK} \glspl{SDS} to \gls{MTASK} \glspl{SDS};
+               \item the interface for lowering \gls{ITASK} \glspl{SDS} to \gls{MTASK} \glspl{SDS};

                \item and a non-trivial home automation example application using all integration mechanisms;
        \end{itemize}
 \end{chapterabstract}
 
                \item and a non-trivial home automation example application using all integration mechanisms;
        \end{itemize}
 \end{chapterabstract}
 

-The \gls{MTASK} language is a multi-view \gls{DSL}, there are multiple interpretations possible for a single \gls{MTASK} term.
-When using the byte code compiler (\cleaninline{BCInterpret}) \gls{DSL} interpretation, \gls{MTASK} tasks are fully integrated in \gls{ITASK}.
+The \gls{MTASK} system is a \gls{TOP} \gls{DSL} for edge devices.
+It is a multi-view \gls{DSL}, there are multiple interpretations possible for a single \gls{MTASK} term.
+The main interpretation of \gls{MTASK} terms is the byte code compiler, \cleaninline{:: BCInterpret a}.
+When using this interpretation and a few integration functions, \gls{MTASK} tasks are fully integrated in \gls{ITASK}.

 They execute as regular \gls{ITASK} tasks and they can access \glspl{SDS} from \gls{ITASK}.
 Devices in the \gls{MTASK} system are set up with a domain-specific \gls{OS} and become little \gls{TOP} engines in their own respect, being able to execute tasks.
 
 They execute as regular \gls{ITASK} tasks and they can access \glspl{SDS} from \gls{ITASK}.
 Devices in the \gls{MTASK} system are set up with a domain-specific \gls{OS} and become little \gls{TOP} engines in their own respect, being able to execute tasks.
 


@@ -31,6 +34,8 @@ The diagram contains three labelled arrows that denote the integration functions
 Devices are connected to the system using the \cleaninline{withDevice} function (see \cref{sec:withdevice}).
 Using \cleaninline{liftmTask}, \gls{MTASK} tasks are lifted to a device (see \cref{sec:liftmtask}).
 \glspl{SDS} from \gls{ITASK} are lowered to the \gls{MTASK} device using \cleaninline{lowerSds} (see \cref{sec:liftsds}).
 Devices are connected to the system using the \cleaninline{withDevice} function (see \cref{sec:withdevice}).
 Using \cleaninline{liftmTask}, \gls{MTASK} tasks are lifted to a device (see \cref{sec:liftmtask}).
 \glspl{SDS} from \gls{ITASK} are lowered to the \gls{MTASK} device using \cleaninline{lowerSds} (see \cref{sec:liftsds}).

+\todo[inline]{mTask device\textsubscript{n} naar hfstk 5? Uitleg over taken en sensoren en \ldots? evt.\ zelfs naar intro hmmm?}
+\todo[inline]{Benoem dat er meerdere devices kunnen zijn en meerdere tasks op één device, en verwijs naar 6.5}

 
 \begin{figure}
        \centering
 
 \begin{figure}
        \centering


@@ -70,7 +75,7 @@ The \cleaninline{MTDevice} abstract type is internally represented as three \gls
 The first \gls{SDS} is the information about the \gls{RTS} of the device, i.e.\ metadata on the tasks that are executing, the hardware specification and capabilities, and a list of fresh task identifiers.
 The second \gls{SDS} is a map storing downstream \gls{SDS} updates.
 When a lowered \gls{SDS} is updated on the device, a message is sent to the server.
 The first \gls{SDS} is the information about the \gls{RTS} of the device, i.e.\ metadata on the tasks that are executing, the hardware specification and capabilities, and a list of fresh task identifiers.
 The second \gls{SDS} is a map storing downstream \gls{SDS} updates.
 When a lowered \gls{SDS} is updated on the device, a message is sent to the server.

-This message is initially queued in the map in order to properly handly multiple updates asychronously.
+This message is initially queued in the map in order to properly handle multiple updates asynchronously.

 Finally, the \cleaninline{MTDevices} type contains the communication channels.
 
 The \cleaninline{withDevice} task itself first constructs the \glspl{SDS} using the \gls{ITASK} function \cleaninline{withShared}.
 Finally, the \cleaninline{MTDevices} type contains the communication channels.
 
 The \cleaninline{withDevice} task itself first constructs the \glspl{SDS} using the \gls{ITASK} function \cleaninline{withShared}.


@@ -88,17 +93,19 @@ Then, it performs the following four tasks in parallel to monitor the edge devic
 \end{enumerate}
 
 \begin{lstClean}[caption={Pseudocode for the \texttt{withDevice} function in \gls{MTASK}.},label={lst:pseudo_withdevice}]
 \end{enumerate}
 
 \begin{lstClean}[caption={Pseudocode for the \texttt{withDevice} function in \gls{MTASK}.},label={lst:pseudo_withdevice}]

+withDevice :: a (MTDevice -> Task b) -> Task b | ...

 withDevice spec deviceTask =
 withDevice spec deviceTask =

-       withShared default \dev->parallel
+       withShared default \dev->

        withShared newMap \sdsupdates->
        withShared ([], [MTTSpecRequest], False) \channels->
        withShared newMap \sdsupdates->
        withShared ([], [MTTSpecRequest], False) \channels->

-               [ channelSync spec channels
-               , watchForShutdown channels
-               , watchChannelMessages dev channels
-               , waitForSpecification
-                       >>| deviceTask (MTDevice dev sdsupdates channels)
-                       >>* [ifStable: issueShutdown]
-               ]
+               parallel
+                       [ channelSync spec channels
+                       , watchForShutdown channels
+                       , watchChannelMessages dev channels
+                       , waitForSpecification
+                               >>| deviceTask (MTDevice dev sdsupdates channels)
+                               >>* [OnValue $ ifStable $ \_->issueShutdown]
+                       ]

 \end{lstClean}
 
 If at any stage an unrecoverable device error occurs, an \gls{ITASK} exception is thrown in the \cleaninline{withDevice} task.
 \end{lstClean}
 
 If at any stage an unrecoverable device error occurs, an \gls{ITASK} exception is thrown in the \cleaninline{withDevice} task.


@@ -106,17 +113,17 @@ This exception can be caught in order to devise fail-safe mechanisms.
 For example, if a device fails, the task can be sent to another device as can be seen in \cref{lst:failover}.
 This function executes an \gls{MTASK} task on a pool of devices connected through \gls{TCP}.
 If a device error occurs during execution, the next device in the pool is tried until the pool is exhausted.
 For example, if a device fails, the task can be sent to another device as can be seen in \cref{lst:failover}.
 This function executes an \gls{MTASK} task on a pool of devices connected through \gls{TCP}.
 If a device error occurs during execution, the next device in the pool is tried until the pool is exhausted.

-If another type of error occurs, it is rethrown for a parent task to catch.
+If another type of error occurs, it is re-thrown for a parent task to catch.

 
 \begin{lstClean}[caption={An \gls{MTASK} failover combinator.},label={lst:failover}]
        failover :: [TCPSettings] (Main (MTask BCInterpret a)) -> Task a
        failover []     _     = throw "Exhausted device pool"
        failover [d:ds] mtask = try (withDevice d (liftmTask mtask)) except
        where except MTEUnexpectedDisconnect = failover ds mtask
 
 \begin{lstClean}[caption={An \gls{MTASK} failover combinator.},label={lst:failover}]
        failover :: [TCPSettings] (Main (MTask BCInterpret a)) -> Task a
        failover []     _     = throw "Exhausted device pool"
        failover [d:ds] mtask = try (withDevice d (liftmTask mtask)) except
        where except MTEUnexpectedDisconnect = failover ds mtask

-       except _                       = throw e
+             except e                       = throw e

 \end{lstClean}
 
 \end{lstClean}
 

-\section{Lifting \texorpdfstring{\gls{MTASK}}{mTask} tasks}\label{sec:liftmtask}
+\section{Lifting mTask tasks}\label{sec:liftmtask}

 Once the connection with the device is established, \gls{MTASK} tasks are lifted to \gls{ITASK} tasks using the \cleaninline{liftmTask} function (see \cref{lst:liftmtask}).
 Given an \gls{MTASK} task in the \cleaninline{BCInterpret} view and a device handle obtained from \cleaninline{withDevice}, an \gls{ITASK} task is returned.
 This \gls{ITASK} task proxies the \gls{MTASK} task that is executed on the microcontroller.
 Once the connection with the device is established, \gls{MTASK} tasks are lifted to \gls{ITASK} tasks using the \cleaninline{liftmTask} function (see \cref{lst:liftmtask}).
 Given an \gls{MTASK} task in the \cleaninline{BCInterpret} view and a device handle obtained from \cleaninline{withDevice}, an \gls{ITASK} task is returned.
 This \gls{ITASK} task proxies the \gls{MTASK} task that is executed on the microcontroller.


@@ -144,11 +151,12 @@ Then, in parallel:
 \end{enumerate}
 
 \begin{lstClean}[label={lst:liftmTask_pseudo},caption={Pseudocode implementation for \texttt{liftmTask}.}]
 \end{enumerate}
 
 \begin{lstClean}[label={lst:liftmTask_pseudo},caption={Pseudocode implementation for \texttt{liftmTask}.}]

+liftmTask :: (Main (MTask BCInterpret a)) MTDevice -> Task a | iTask a

 liftmTask task (MTDevice dev sdsupdates channels)
        = freshTaskId dev
        >>= \tid->withCleanupHook (sendmessage [MTTTaskDel tid] channels) (
                compile task \mrefs msgs->
 liftmTask task (MTDevice dev sdsupdates channels)
        = freshTaskId dev
        >>= \tid->withCleanupHook (sendmessage [MTTTaskDel tid] channels) (
                compile task \mrefs msgs->

-                       sendMessage msgs channels
+                           sendMessage msgs channels

                        >>| waitForReturnAndValue tid dev
                        -|| watchSharesDownstream mrefs tid sdsupdates
                        -|| watchSharesUpstream mrefs channels tid)
                        >>| waitForReturnAndValue tid dev
                        -|| watchSharesDownstream mrefs tid sdsupdates
                        -|| watchSharesUpstream mrefs channels tid)


@@ -160,7 +168,7 @@ To mitigate this problem, \gls{MTASK} tasks can be preloaded on a device.
 Preloading means that the task is compiled and integrated into the device firmware.
 On receiving a \cleaninline{TaskPrep}, a hashed value of the task to be sent is included.
 The device then checks the preloaded task registry and uses the local preloaded version if the hash matches.
 Preloading means that the task is compiled and integrated into the device firmware.
 On receiving a \cleaninline{TaskPrep}, a hashed value of the task to be sent is included.
 The device then checks the preloaded task registry and uses the local preloaded version if the hash matches.

-Of course this only works for tasks that are not tailor made for the current work specification and not depend on run time information.
+Of course this only works for tasks that are not tailor-made for the current work specification and not depend on run time information.

 The interface for task preloading can be found in \cref{lst:preload}.
 Given an \gls{MTASK} task, a header file is created that should be placed in the source code directory of the \gls{RTS} before building to include it in the firmware.
 
 The interface for task preloading can be found in \cref{lst:preload}.
 Given an \gls{MTASK} task, a header file is created that should be placed in the source code directory of the \gls{RTS} before building to include it in the firmware.
 


@@ -168,7 +176,7 @@ Given an \gls{MTASK} task, a header file is created that should be placed in the
 preloadTask :: (Main (MTask BCInterpret a)) -> Task String
 \end{lstClean}
 
 preloadTask :: (Main (MTask BCInterpret a)) -> Task String
 \end{lstClean}
 

-\section{Lowering \texorpdfstring{\gls{ITASK}}{iTask} \texorpdfstring{\glsxtrlongpl{SDS}}{shared data sources}}\label{sec:liftsds}
+\section{Lowering iTask shared data sources}\label{sec:liftsds}

 Lowering \gls{ITASK} \glspl{SDS} to \gls{MTASK} \glspl{SDS} is something that mostly happens at the \gls{DSL} level using the \cleaninline{lowerSds} function (see \cref{lst:mtask_itasksds}).
 Lowering \pgls{SDS} proxies the \gls{ITASK} \gls{SDS} for use in \gls{MTASK}.
 \Glspl{SDS} in \gls{MTASK} always have an initial value.
 Lowering \gls{ITASK} \glspl{SDS} to \gls{MTASK} \glspl{SDS} is something that mostly happens at the \gls{DSL} level using the \cleaninline{lowerSds} function (see \cref{lst:mtask_itasksds}).
 Lowering \pgls{SDS} proxies the \gls{ITASK} \gls{SDS} for use in \gls{MTASK}.
 \Glspl{SDS} in \gls{MTASK} always have an initial value.


@@ -176,6 +184,7 @@ For regular \gls{SDS} this value is given in the source code, for lowered \gls{I
 On the device, there is just one difference between lowered \glspl{SDS} and regular \glspl{SDS}: after changing a lowered \gls{SDS}, a message is sent to the server containing this new value.
 The \cleaninline{withDevice} task (see \cref{sec:withdevice}) receives and processes this message by writing to the \gls{ITASK} \gls{SDS}.
 Tasks watching this \gls{SDS} get notified then through the normal notification mechanism of \gls{ITASK}.
 On the device, there is just one difference between lowered \glspl{SDS} and regular \glspl{SDS}: after changing a lowered \gls{SDS}, a message is sent to the server containing this new value.
 The \cleaninline{withDevice} task (see \cref{sec:withdevice}) receives and processes this message by writing to the \gls{ITASK} \gls{SDS}.
 Tasks watching this \gls{SDS} get notified then through the normal notification mechanism of \gls{ITASK}.

+\Cref{lst:imp_sds} shows the implementation of this type class for the byte code compiler.

 
 \begin{lstClean}[label={lst:mtask_itasksds},caption={Lowered \gls{ITASK} \glspl{SDS} in \gls{MTASK}.}]
 class lowerSds v where
 
 \begin{lstClean}[label={lst:mtask_itasksds},caption={Lowered \gls{ITASK} \glspl{SDS} in \gls{MTASK}.}]
 class lowerSds v where


@@ -199,55 +208,17 @@ where
        mtask :: (Shared sds Bool) -> Main (MTask v Bool)
                | mtask, lowerSds v & RWShared sds
        mtask sh =
        mtask :: (Shared sds Bool) -> Main (MTask v Bool)
                | mtask, lowerSds v & RWShared sds
        mtask sh =

-               declarePin D13 PMOutput \d13->
+               declarePin D13 PMOutput \ledPin->

                lowerSds \ls=sh
                In fun \f=(\st->
                             getSds ls
                lowerSds \ls=sh
                In fun \f=(\st->
                             getSds ls

-                       >>*. [IfValue (\v->v !=. st) (\v->writeD d13 v)]
-                       >>|. f (Not st))
-               In {main=f true}
-\end{lstClean}
-
-\subsection{Implementation}
-The compilation of the code and the serialisation of the data throws away all typing information.
-\Glspl{SDS} are stored in the compiler state as a map from identifiers to either an initial value or an \cleaninline{MTLens}.
-The \cleaninline{MTLens} is a type synonym for \pgls{SDS} that represents the typeless serialised value of the underlying \gls{SDS}.
-This is done so that the \cleaninline{withDevice} task can write the received \gls{SDS} updates to the according \gls{SDS} while the \gls{SDS} is not in scope.
-The \gls{ITASK} notification mechanism then takes care of the rest.
-Such \pgls{SDS} is created by using the \cleaninline{mapReadWriteError} which, given a pair of read and write functions with error handling, produces \pgls{SDS} with the lens embedded.
-The read function transforms converts the typed value to a typeless serialised value.
-The write function will, given a new serialised value and the old typed value, produce a new typed value.
-It tries to decode the serialised value, if that succeeds, it is written to the underlying \gls{SDS}, an error is thrown otherwise.
-\Cref{lst:mtask_itasksds_lens} shows the implementation for this.
-
-% VimTeX: SynIgnore on
-\begin{lstClean}[label={lst:mtask_itasksds_lens},caption={Lens applied to lowered \gls{ITASK} \glspl{SDS} in \gls{MTASK}.}]
-lens :: (Shared sds a) -> MTLens | type a & RWShared sds
-lens sds = mapReadWriteError
-       ( \r->   Ok (fromString (toByteCode{|*|} r)
-       , \w r-> ?Just <$> iTasksDecode (toString w)
-       ) ?None sds
+                       >>*. [IfValue (\v->v !=. st) (writeD ledPin)]
+                       >>=. f)
+               In {main=getSds ls >>~. f}

 \end{lstClean}
 \end{lstClean}

-% VimTeX: SynIgnore off
-
-\Cref{lst:mtask_itasksds_lift} shows the code for the implementation of \cleaninline{lowerSds} that uses the \cleaninline{lens} function shown earlier.
-First, the \gls{SDS} to be lowered is extracted from the expression by bootstrapping the fixed point with a dummy value.
-This is safe because the expression on the right-hand side of the \cleaninline{In} is never evaluated.
-Then, using \cleaninline{addSdsIfNotExist}, the identifier for this particular \gls{SDS} is either retrieved from the compiler state or generated freshly.
-This identifier is then used to provide a reference to the \cleaninline{def} definition to evaluate the main expression.
-
-% VimTeX: SynIgnore on
-\begin{lstClean}[label={lst:mtask_itasksds_lift},caption={The implementation for lowering \glspl{SDS} in \gls{MTASK}.}]
-instance lowerSds BCInterpret where
-       lowerSds def = {main =
-                       let (t In _) = def (abort "lowerSds: expression too strict")
-                       in addSdsIfNotExist (Right $ lens t)
-                               >>= \sdsi->let (_ In e) = def (pure (Sds sdsi)) in e.main
-               }\end{lstClean}
-% VimTeX: SynIgnore off

 
 \section{Conclusion}
 
 \section{Conclusion}

-When \gls{IOT} edge devices run the \gls{MTASK} \gls{RTS}, they become little \gls{TOP} engines of their own.
+This chapter explained the integration of \gls{MTASK} programs with \gls{ITASK}.

 Using just three \gls{ITASK} functions, \gls{MTASK} devices are integrated in \gls{ITASK} seamlessly.
 Devices, using any supported type of connection, are integrated in \gls{ITASK} using the \cleaninline{withDevice} function.
 Once connected, \gls{MTASK} tasks are sent to the device for execution using \cleaninline{liftmTask}, lifting them to full-fledged \gls{ITASK} tasks.
 Using just three \gls{ITASK} functions, \gls{MTASK} devices are integrated in \gls{ITASK} seamlessly.
 Devices, using any supported type of connection, are integrated in \gls{ITASK} using the \cleaninline{withDevice} function.
 Once connected, \gls{MTASK} tasks are sent to the device for execution using \cleaninline{liftmTask}, lifting them to full-fledged \gls{ITASK} tasks.


@@ -255,23 +226,29 @@ To lower the bandwidth, tasks can also be preloaded.
 Furthermore, the \gls{MTASK} tasks interact with \gls{ITASK} \glspl{SDS} using the \cleaninline{lowerSds} construct.
 All of this together allows programming all layers of an \gls{IOT} system from a single source and in a single paradigm.
 All details regarding interoperation are automatically taken care of.
 Furthermore, the \gls{MTASK} tasks interact with \gls{ITASK} \glspl{SDS} using the \cleaninline{lowerSds} construct.
 All of this together allows programming all layers of an \gls{IOT} system from a single source and in a single paradigm.
 All details regarding interoperation are automatically taken care of.

-The following section contains an elaborate example using all integration functions that has deliberately been placed after the conclusion so that the code listing and description are on facing pages.
+The following section contains an elaborate example using all integration functions that has deliberately been placed after the conclusion.
+
+\newpage
+\vspace*{\fill}
+\hfill
+\begin{center}
+       \cleaninline[basewidth=0pt,columns=flexible,basicstyle=\tt\footnotesize]{let p = [['This page would be intentionally blank if I were not telling you that ']:p] in p} % chktex 10
+\end{center}
+\vspace{\fill}
+\newpage

 
 

-\begin{figure}[p]
-       \begin{leftfullpage}
-               \vspace{\headsep}

 \section{Home automation}
 \section{Home automation}

+\todo[inline]{Meer uitleg over de applicatie? ADT ipv strings voor keuze?}

 This section presents an interactive home automation program (\cref{lst:example_home_automation}) to illustrate the integration of the \gls{MTASK} language and the \gls{ITASK} system.
 This section presents an interactive home automation program (\cref{lst:example_home_automation}) to illustrate the integration of the \gls{MTASK} language and the \gls{ITASK} system.

-It consists of a web interface for the user to control which tasks are executed on either one of two connected devices: an \gls{ARDUINO} UNO, connected via a serial port; and an ESP8266 based prototyping board called NodeMCU, connected via \gls{TCP} over \gls{WIFI}.
-
+It consists of a web interface for the user to control which tasks are executed on either one of two connected devices: an \gls{ARDUINO} UNO, connected via a serial port; and an ESP8266 based prototyping board called NodeMCU, connected via \gls{TCP}\slash{}\gls{WIFI}.

 \Crefrange{lst:example:spec1}{lst:example:spec2} show the specification for the devices.
 \Crefrange{lst:example:spec1}{lst:example:spec2} show the specification for the devices.

-The UNO is connected via serial using the unix filepath \path{/dev/ttyACM0} and the default serial port settings.
+The UNO is connected via serial using the UNIX filepath \path{/dev/ttyACM0} and the default serial port settings.

 The NodeMCU is connected via \gls{WIFI} and hence the \cleaninline{TCPSettings} record is used.
 The NodeMCU is connected via \gls{WIFI} and hence the \cleaninline{TCPSettings} record is used.

-Both types have \cleaninline{channelSync} instances.
+%Both types have \cleaninline{channelSync} instances.

 
 The code consists of an \gls{ITASK} part and several \gls{MTASK} parts.
 \Crefrange{lst:example:task1}{lst:example:task2} contains the \gls{ITASK} task that coordinates the \gls{IOT} application.
 
 The code consists of an \gls{ITASK} part and several \gls{MTASK} parts.
 \Crefrange{lst:example:task1}{lst:example:task2} contains the \gls{ITASK} task that coordinates the \gls{IOT} application.

-First the devices are connected (\crefrange{lst:example:conn1}{lst:example:conn2}) followed by launching a \cleaninline{parallel} task, visualized as a tabbed window, and a shutdown button to terminate the program (\crefrange{lst:example:par1}{lst:example:par2}).
+First the devices are connected (\crefrange{lst:example:conn1}{lst:example:conn2}) followed by launching a \cleaninline{parallel} task, visualised as a tabbed window, and a shutdown button to terminate the program (\crefrange{lst:example:par1}{lst:example:par2}).

 This parallel task is the controller of the tasks that run on the edge devices.
 It contains one task that allows adding new tasks (using \cleaninline{appendTask}) and all other tasks in the process list will be \gls{MTASK} tasks once they are added by the user.
 The controller task, \cleaninline{chooseTask} as shown in \crefrange{lst:example:ct1}{lst:example:ct2}, allows the user to pick a task, and sending it to the specified device.
 This parallel task is the controller of the tasks that run on the edge devices.
 It contains one task that allows adding new tasks (using \cleaninline{appendTask}) and all other tasks in the process list will be \gls{MTASK} tasks once they are added by the user.
 The controller task, \cleaninline{chooseTask} as shown in \crefrange{lst:example:ct1}{lst:example:ct2}, allows the user to pick a task, and sending it to the specified device.


@@ -284,30 +261,28 @@ For example, when selecting the \cleaninline{temperature} task, the current temp
 This task just sends a simple temperature monitoring task to the device using \cleaninline{liftmTask} and provides a view on its task value using the \cleaninline{>\&>} \gls{ITASK} combinator.
 This combinator allows the observation of the left-hand side task's value through \pgls{SDS}.
 The light switch task at \crefrange{lst:example:ls1}{lst:example:ls2} is a task that has bidirectional interaction using the definition of \cleaninline{lightswitch} shown in \cref{lst:mtask_liftsds_ex}.
 This task just sends a simple temperature monitoring task to the device using \cleaninline{liftmTask} and provides a view on its task value using the \cleaninline{>\&>} \gls{ITASK} combinator.
 This combinator allows the observation of the left-hand side task's value through \pgls{SDS}.
 The light switch task at \crefrange{lst:example:ls1}{lst:example:ls2} is a task that has bidirectional interaction using the definition of \cleaninline{lightswitch} shown in \cref{lst:mtask_liftsds_ex}.

-Using \cleaninline{liftsds}, the status of the light switch is synchronised with the user.
+Using \cleaninline{lowerSds}, the status of the light switch is synchronised with the user.

 Finally, a task that calculates the factorial of a user-provided number is shown in the list.
 
 Finally, a task that calculates the factorial of a user-provided number is shown in the list.
 

-               \vspace{4ex}
-               \begin{center}
-                       \begin{subfigure}[b]{.3\linewidth}
-                               \includegraphics[width=\linewidth]{home_auto1}
-                               \caption{Select task.}%
-                               \label{fig:example_screenshots1}
-                       \end{subfigure}
-                       \begin{subfigure}[b]{.3\linewidth}
-                               \includegraphics[width=\linewidth]{home_auto2}
-                               \caption{Select device.}%
-                               \label{fig:example_screenshots2}
-                       \end{subfigure}
-                       \begin{subfigure}[b]{.3\linewidth}
-                               \includegraphics[width=\linewidth]{home_auto3}
-                               \caption{View result.}%
-                               \label{fig:example_screenshots3}
-                       \end{subfigure}
-                       \caption{Screenshots of the home automation example program in action.}%
-                       \label{fig:example_screenshots}
-               \end{center}
-       \end{leftfullpage}
+\begin{figure}[!ht]
+       \centering
+       \begin{subfigure}[b]{.3\linewidth}
+               \includegraphics[width=\linewidth]{home_auto1}
+               \caption{Select task.}%
+               \label{fig:example_screenshots1}
+       \end{subfigure}
+       \begin{subfigure}[b]{.3\linewidth}
+               \includegraphics[width=\linewidth]{home_auto2}
+               \caption{Select device.}%
+               \label{fig:example_screenshots2}
+       \end{subfigure}
+       \begin{subfigure}[b]{.3\linewidth}
+               \includegraphics[width=\linewidth]{home_auto3}
+               \caption{View result.}%
+               \label{fig:example_screenshots3}
+       \end{subfigure}
+       \caption{Screenshots of the home automation example program in action.}%
+       \label{fig:example_screenshots}

 \end{figure}
 
 \begin{figure}[p]
 \end{figure}
 
 \begin{figure}[p]