Added updated specs. Minor additions

macros.tex

@@ -21,6 +21,11 @@
 % automata learning theory
 \newcommand{\lstar}{\cal{L}*}
 
-\newcommand{\dlearner}{\term{learner}\xspace}
-\newcommand{\dmapper}{\term{mapper}\xspace}
-\newcommand{\dsut}{{\sc sul}\xspace}
\ No newline at end of file
+% learning components
+\newcommand{\dlearner}{\sc learner}
+\newcommand{\dmapper}{\sc mapper}
+\newcommand{\dsut}{\sc sul}
+\newcommand{\dsuts}{\sc suls}
+
+%alphabet related
+\newcommand{\dtimeout}{\sc noresp}
\ No newline at end of file

preliminaries.tex

@@ -44,16 +44,16 @@ a different output sequence for both Mealy machines, that is, $A_{\CH}(\sigma) \
 
 Model learning algorithms have been developed developed for learning deterministic Mealy machines using
 a finite number of queries. We point to \cite{Isberner2015} for a recent overview. These algorithms are leveraged
-in applications where one wants to learn a model of a black-box reactive system, or System Under Learning (\dsut). The teacher typically
-consists of the ~\dsut, which answers membership queries, and a conformance
+in applications where one wants to learn a model of a black-box reactive system, or System Under Learning ({\dsut}). The teacher typically
+consists of the {\dsut}, which answers membership queries, and a conformance
 testing tool \cite{LeeY96} that approximates the equivalence queries using a set
-of \emph{test queries}. A test query consists of asking to the \dsut for the response to an input sequence
+of \emph{test queries}. A test query consists of asking to the {\dsut} for the response to an input sequence
 $\sigma \in I^{\ast}$, similar to a membership query. 
 
 \subsection{Abstraction} \label{ssec:mappers}
 Most current learning algorithms are only applicable to Mealy machines with small alphabets comprising abstract messages. Practical systems typically 
 have parameterized input/output alphabets, whose application triggers updates on the system's state variables. To learn
-these systems we place a \emph{mapper} between the \dlearner and the \dsut. The mapper is a transducer which translates 
+these systems we place a \emph{mapper} between the {\dlearner} and the {\dsut}. The mapper is a transducer which translates 
 concrete inputs to abstract inputs and concrete outputs to abstract outputs. For a thorough definition of mappers, we refer to \cite{AJUV15}. 
 
 %Perhaps some explanation

specifications.txt

@@ -10,4 +10,43 @@ Upon receiving this message, a party MUST
    party when it has both sent and received SSH_MSG_CHANNEL_CLOSE, and
    the party may then reuse the channel number.  A party MAY send
    SSH_MSG_CHANNEL_CLOSE without having sent or received
-   SSH_MSG_CHANNEL_EOF.
\ No newline at end of file
+   SSH_MSG_CHANNEL_EOF.
+
+
+
+ Once a party has sent a SSH_MSG_KEXINIT message for key exchange or
+   re-exchange, until it has sent a SSH_MSG_NEWKEYS message (Section
+   7.3), it MUST NOT send any messages other than:
+
+   o  Transport layer generic messages (1 to 19) (but
+      SSH_MSG_SERVICE_REQUEST and SSH_MSG_SERVICE_ACCEPT MUST NOT be
+      sent);
+
+   o  Algorithm negotiation messages (20 to 29) (but further
+      SSH_MSG_KEXINIT messages MUST NOT be sent);
+
+   o  Specific key exchange method messages (30 to 49).
+
+
+
+
+
+If the server rejects the service request, it SHOULD send an
+appropriate SSH_MSG_DISCONNECT message and MUST disconnect.
+
+
+
+ After the SSH_MSG_KEXINIT message exchange, the key exchange
+   algorithm is run.  It may involve several packet exchanges, as
+   specified by the key exchange method.
+
+   Once a party has sent a SSH_MSG_KEXINIT message for key exchange or
+   re-exchange, until it has sent a SSH_MSG_NEWKEYS message (Section
+   7.3), it MUST NOT send any messages other than:
+
+   o  Transport layer generic messages (1 to 19) (but
+      SSH_MSG_SERVICE_REQUEST and SSH_MSG_SERVICE_ACCEPT MUST NOT be
+      sent);
+
+   o  Algorithm negotiation messages (20 to 29) (but further
+      SSH_MSG_KEXINIT messages MUST NOT be sent);(