\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
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$
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
$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}