Merge branch 'master' of https://github.com/dopefishh/tt2015

[tt2015.git] / a3 / 1modelinvestigation.tex

diff --git a/a3/1modelinvestigation.tex b/a3/1modelinvestigation.tex
index e8d10c9..f0f6718 100644 (file)
--- a/a3/1modelinvestigation.tex
+++ b/a3/1modelinvestigation.tex
@@ -12,11 +12,16 @@ be a fitting model for our SUT as the
 behaviour of TCP is such that a TCP client is in a certain state (connection 
 closed, listening, connection established, etc.) and the TCP client transitions
 between those states based upon input coming from another connected client.
-In this case an LTS, in which the interactions would be initiated by the
-remote client, would be a fitting model for our SUT. 
+In this case an LTS, would be a fitting model for our SUT. 
 
 An LTS would not be a fitting model in case it would be desirable to model the
 behaviour when wrong input (such as wrong sequence numbers) is given to the SUT.
+An LTS could model this behaviour, but more expressive models exists (see below)
+which would limit the size of the model. 
+
+In this case we chose 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 as described in the TCP specification. 
 
 \paragraph{Mealy Machines} 
 Mealy Machines are an extension of LTS in which each label is a tuple of input