% Comparison between tools and how fit the tools we choose were

% Discuss and classify the MBT tools that you used, compare them, compare with 
% Manual testing, and reflect on the theory:
% • What is implementation relation?
% • Is there support for non-determinism, concurrency?
% • Are the generated tests sound, exhaustive? Why do you think so? 
% • Which method of test test selection is used?
% • What is the modeling notation, its expressiveness, and ease of use? 
% • Do the tools use on/off-line testing (on-the-fly/batch)?
% • Do they support both: test input generation and output checking?

The SUT has been tested using two tools, JTorX and \GAST. Both tools allowed
for extensive testing of the SUT compared to the model of 
Section~\ref{sec:modeling} using the architecture of Figure~\ref{fig:arch}.

However setting up both \GAST and JTorX required extensive effort. To be able 
to use \GAST extensive changes had to be made to the source code of \GAST. 
Without these changes \GAST could not be used effectively. This was due in 
part to problems with Cleans uniqueness typing when using \GAST over TCP. The
complete list of changes can be obtained by comparing \GAST s source code to the
source code found in the attached \texttt{code/Gast/} folder.

\GAST selects tests by trying all inputs from the alphabet in each possible 
state. When the SUT responds in a way which is not in the model the test case
fails. JTorX selects test cases by ???????????????
\GAST s selection ensures that all possible traces are covered, however, this
exhaustive search will also generate huge tests for big models. 

% hier iets over non-determinism?

Both JTorX and \GAST use on-line checking. They test the SUT on the fly by
syncing state transitions in the internal model of the SUT with observed output (after input) from the SUT.

For JTorX test generation was very simple since it accepts models in GraphViz
DOT language, which is also the language used for describing the models for this
report. For \GAST the model generation required a bit more work, as the model 
is written as a function in Clean. This translation is however easily done by 
hand. Because the model for \GAST is written as a function in Clean it is very
expressive, the modeling method chosen for  JTorX however is a lot less 
expressive, as it just allows for specification of states and transition labels
between them. However JTorX allows for many different modeling languages, which
can be more expressive than modeling using GraphViz models \cite{JTorXSite}.
However, for our tests GraphViz models were expressive enough. 