# HG changeset patch
# User Eugen Sawin <sawine@me73.com>
# Date 1310507527 -7200
# Node ID 83e17547d019c09b5dff7ad5ffbe90753aeb2500
# Parent  f016288bf0ad5347a348d24802bfa285758c639c
Tired.

diff -r f016288bf0ad -r 83e17547d019 paper/src/paper.tex
--- a/paper/src/paper.tex	Tue Jul 12 22:38:25 2011 +0200
+++ b/paper/src/paper.tex	Tue Jul 12 23:52:07 2011 +0200
@@ -13,6 +13,10 @@
 %\usepackage{arev}
 %\pagestyle{headings}
 
+\floatname{algorithm}{Function}
+\renewcommand{\algorithmicrequire}{\textbf{Input:}}
+\renewcommand{\algorithmicensure}{\textbf{Output:}}
+
 \renewcommand{\familydefault}{\sfdefault}
 \renewenvironment{proof}{{\bfseries Proof.}}{}
 \newcommand{\M}{\mathcal{M}}
@@ -497,33 +501,26 @@
 \noindent The soundness and completeness proofs are provided in \cite{ref:ltl&büchi}; the equivalance of the partial automata and the specification automata as defined in \ref{sec:specification automata} follows from the proofs.  
 
 \subsection{On-the-fly construction}
-So.
+
+
 \begin{algorithm}
-\caption{expand}
+\caption{expand: $\Phi^+ \times 2^Q \to 2^Q$}
 \label{alg:expand}
 \begin{algorithmic}
 \REQUIRE $Node, NodeSet$
-\IF {$New(Node) = \emptyset$} 
-  \IF {$\exists{N \in NodeSet}: Old(N) = Old(Node)$ and $Next(N) = Next(Node)$} 
-    \STATE $Incoming(N) = Incoming(N) \cup Incoming(Node)$
-  \ENDIF
-\ELSE
-  \STATE $n \in New$
-        \IF {$i+k\leq maxval$}
-                \STATE $i\gets i+k$
-        \ENDIF
-\ENDIF 
+\IF {$\dnf(\bigwedge snext(Node)) \notin NodeSet$}
+  \STATE $NodeSet = NodeSet \cup \dnf(\bigwedge snext(Node))$
+\ENDIF
+\RETURN $NodeSet$
 \end{algorithmic}
 \end{algorithm}
 
 \section*{Discussion}
-Linear-Time Temporal Logic and B\"uchi Automata \cite{ref:ltl&büchi} is an in-depth introduction to automated verification. It delivers the core concepts of model checking in a readable way. The formal proofs are clean and absorbable. The introduction section provides a good overview of the structure of the text and the basic theory behind all concepts. 
+Linear-Time Temporal Logic and B\"uchi Automata \cite{ref:ltl&büchi} is an in-depth introduction to automated verification. It delivers the core concepts of model checking in a readable way. The formal proofs are clean and absorbable. The introduction section provides a good overview of the text structure and the basic theory behind all concepts. 
 
 However, the author does not make an effort to deliver a motivation for the topic. From the beginning, the substance of the text resides within the world of model checking, without an external view on the practical applications and their significance to the industry.
 
-At some points, the definitions are either lacking formality or are inconsistent. It seems like several concepts are introduced ad-hoc and without rigor. In an introductory text, such inaccuracies may lead to confusion and diminish the confident in the reader's own understanding of the discussed topics.
-
-
+At some points, the definitions are either lacking formality or are inconsistent. It seems like several concepts are introduced ad-hoc and without rigor. In an introductory text, such inaccuracies may lead to confusion and distract the reader's attention from the essence of the content.
 
 \begin{thebibliography}{99}
 \bibitem{ref:ltl&büchi}