added something about the LTS model of TCP

diff --git a/a3/1modelingTCP.tex b/a3/1modelingTCP.tex
index 23aeb21..2c9125b 100644 (file)
--- a/a3/1modelingTCP.tex
+++ b/a3/1modelingTCP.tex
@@ -27,4 +27,21 @@ Due to this limitation Mealy Machines are not a very suitable model to model
 the SUT. Instead we choose to model the SUT as a LTS. Since LTSs provide the 
 functionality to express the desired properties of the SUT, that is, that the
 SUT transitions through states depending on input as described in the TCP
-specification and produces the output described by the TCP specification.
\ No newline at end of file
+specification and produces the output described by the TCP specification.
+
+\subsection{A LTS model of TCP} \label{subsec:sut_model}
+With these model based tests two major parts of the TCP specification will be 
+tested. These are (a) the establishment of connection (three-way handshake)
+between the SUT -which 
+will receive the connection- and an external host -which will initiate the 
+connection- and (b) the closing of a connection (tear down) initiated by the
+external host.
+
+Figure~\ref{fig:model_connection} shows a LTS model of the SUT for the 
+three-way handshake (a). Figure~\ref{fig:model_disconnect} shows a LTS model
+of the SUT for the tear down (b).
+
+Hier zou dus een plaatje van ``digraph Connection'' uit ``graphs.viz'' moeten komen. \label{fig:model_connection}.
+
+En hier een plaatje van ``digraph Close'' uit ``graphs.viz'' moeten komen.
+\label{fig:model_disconnect}
\ No newline at end of file