1.1 --- a/paper/src/paper.tex	Tue Jul 12 22:38:25 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Tue Jul 12 23:52:07 2011 +0200
     1.3 @@ -13,6 +13,10 @@
     1.4  %\usepackage{arev}
     1.5  %\pagestyle{headings}
     1.6  
     1.7 +\floatname{algorithm}{Function}
     1.8 +\renewcommand{\algorithmicrequire}{\textbf{Input:}}
     1.9 +\renewcommand{\algorithmicensure}{\textbf{Output:}}
    1.10 +
    1.11  \renewcommand{\familydefault}{\sfdefault}
    1.12  \renewenvironment{proof}{{\bfseries Proof.}}{}
    1.13  \newcommand{\M}{\mathcal{M}}
    1.14 @@ -497,33 +501,26 @@
    1.15  \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.  
    1.16  
    1.17  \subsection{On-the-fly construction}
    1.18 -So.
    1.19 +
    1.20 +
    1.21  \begin{algorithm}
    1.22 -\caption{expand}
    1.23 +\caption{expand: $\Phi^+ \times 2^Q \to 2^Q$}
    1.24  \label{alg:expand}
    1.25  \begin{algorithmic}
    1.26  \REQUIRE $Node, NodeSet$
    1.27 -\IF {$New(Node) = \emptyset$} 
    1.28 -  \IF {$\exists{N \in NodeSet}: Old(N) = Old(Node)$ and $Next(N) = Next(Node)$} 
    1.29 -    \STATE $Incoming(N) = Incoming(N) \cup Incoming(Node)$
    1.30 -  \ENDIF
    1.31 -\ELSE
    1.32 -  \STATE $n \in New$
    1.33 -        \IF {$i+k\leq maxval$}
    1.34 -                \STATE $i\gets i+k$
    1.35 -        \ENDIF
    1.36 -\ENDIF 
    1.37 +\IF {$\dnf(\bigwedge snext(Node)) \notin NodeSet$}
    1.38 +  \STATE $NodeSet = NodeSet \cup \dnf(\bigwedge snext(Node))$
    1.39 +\ENDIF
    1.40 +\RETURN $NodeSet$
    1.41  \end{algorithmic}
    1.42  \end{algorithm}
    1.43  
    1.44  \section*{Discussion}
    1.45 -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. 
    1.46 +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. 
    1.47  
    1.48  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.
    1.49  
    1.50 -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.
    1.51 -
    1.52 -
    1.53 +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.
    1.54  
    1.55  \begin{thebibliography}{99}
    1.56  \bibitem{ref:ltl&büchi}