From: pimjager Date: Wed, 16 Dec 2015 15:07:45 +0000 (+0100) Subject: improved modeling section based on feedback Ramon X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=0ab264df5e1ec5a7dcd0c38918f7b1f54a08d46d;p=tt2015.git improved modeling section based on feedback Ramon --- diff --git a/a3/1modelingTCP.tex b/a3/1modelingTCP.tex index 6449dcc..23aeb21 100644 --- a/a3/1modelingTCP.tex +++ b/a3/1modelingTCP.tex @@ -15,20 +15,16 @@ 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 -and output. For our SUT this means that is is not just possible to model the -behaviour of the SUT regarding its internal state, but also its behaviour -regarding its output. +Mealy Machines are a variant of LTS in which each label is a tuple of input +and output. This forces each state transition to consume both input and +produce output. The model for the SUT (see Section~\ref{subsec:sut_model}) +however contains state transitions with sequences of output which do not +require new input. -For simplicity however we have chosen to model the SUT with the assumption that -it is only handed correct input and will then generate correct output (assuming -that the internal state transition function is correct). Therefore the extra -functionality provided by modeling our SUT as a Mealy Machine is not necessary. \ No newline at end of file +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