X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=top%2Fint.tex;h=1a4eb01b3ffd63f5a4abc16dc29fea4d9279a9ea;hb=7e45dc62707316dc88e19ea9ad6b779ad3c17833;hp=bddea2a8eeee618af8c57af6504108b19e1da6d3;hpb=529531e1028ae26ab889456d65958794154d5b25;p=phd-thesis.git

diff --git a/top/int.tex b/top/int.tex
index bddea2a..1a4eb01 100644
--- a/top/int.tex
+++ b/top/int.tex
@@ -34,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}).
+\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
@@ -91,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}]
+withDevice :: a (MTDevice -> Task b) -> Task b | ...
 withDevice spec deviceTask =
-	withShared default \dev->parallel
+	withShared default \dev->
 	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.
@@ -116,7 +120,7 @@ If another type of error occurs, it is re-thrown for a parent task to catch.
 	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}
 
 \section{Lifting mTask tasks}\label{sec:liftmtask}
@@ -147,11 +151,12 @@ Then, in parallel:
 \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->
-			sendMessage msgs channels
+			    sendMessage msgs channels
 			>>| waitForReturnAndValue tid dev
 			-|| watchSharesDownstream mrefs tid sdsupdates
 			-|| watchSharesUpstream mrefs channels tid)
@@ -203,13 +208,13 @@ where
 	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
-			>>*. [IfValue (\v->v !=. st) (\v->writeD d13 v)]
-			>>|. f (Not st))
-		In {main=f true}
+			>>*. [IfValue (\v->v !=. st) (writeD ledPin)]
+			>>=. f)
+		In {main=getSds ls >>~. f}
 \end{lstClean}
 
 \section{Conclusion}
@@ -233,6 +238,7 @@ The following section contains an elaborate example using all integration functi
 \newpage
 
 \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.
 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.