update spellcheck
[ar1516.git] / a2 / 2.tex
index 174dfd6..0c51035 100644 (file)
--- a/a2/2.tex
+++ b/a2/2.tex
@@ -12,7 +12,7 @@ times:
 \end{itemize}}
 
 The problem is easily solvable using a symbolic model checker since it is
-cleary a problem that progresses with state transfers up to a goal. For all
+clearly a problem that progresses with state transfers up to a goal. For all
 bottles $b_i$ for $i\in\{1\ldots3\}$ we create a variable stating the contents
 in the current state $b_i$ and a constant that describes the maximum content
 $b_{i\max}$. State transitions come in three classes. With the next
@@ -20,10 +20,10 @@ function we describe the transition to the next state. If the next state is not
 defined for a bottle $b_i$ we assume $\text{next}(b_i)=b_i$.
 \begin{itemize}
        \item Filling a bottle $b_i$\\
-               If we fill a bottle $b_i$ the contens will be the maximum thus:\\
+               If we fill a bottle $b_i$ the contents will be the maximum thus:\\
                $\text{next}(b_i)=b_{i\max}$.
        \item Emptying a bottle $b_i$\\
-               If we empty a bottle $b_i$ the contens will become zero thus:\\
+               If we empty a bottle $b_i$ the contents will become zero thus:\\
                $\text{next}(b_i)=0$.
        \item Pouring a bottle $b_i$ in bottle $b_j$ for $i\neq j$\\
                If we pour a bottle $b_i$ into $b_j$, the contents that fits in $b_j$
@@ -38,7 +38,7 @@ All transitions are unconstrained and therefore we can convert this very easily
 to \textsc{NuSMV} by enclosing all the transition classes in brackets and
 joining them with logical or operators.
 
-\begin{enumerate}[a.]
+\begin{enumerate}[(a)]
        \item
                \emph{Determine whether it is possible to arrive at a situation in
                which the first bottle contains 8 units and the second one contains 11
@@ -123,6 +123,6 @@ joining them with logical or operators.
                                $29$ & $8$ & $11$ & $28$ & Poured $2$ in $3$\\
                                \bottomrule
                        \end{tabular}
-                       \caption{Solution for problem 3}\label{tab:sol2c}
+                       \caption{Solution for problem 2}\label{tab:sol2c}
                \end{table}
 \end{enumerate}