\section{Problem 2}
\emph{Three bottles can hold 144, 72 and 16 units (say, centiliters),
respectively. Initially the first one contains 3 units of water, the
others are empty. The following actions may be performed any number of
times:
\begin{itemize}
	\item One of the bottles is fully filled, at some water tap.
	\item One of the bottles is emptied.
	\item The content of one bottle is poured into another one. If it fits,
		then the full content is poured, otherwise the pouring stops when the
		other bottle is full.
\end{itemize}}

The problem can be solved by transforming it into a symbolic model.  For all
bottles $b_i$ for $i\in\{1\ldots3\}$ a variable is created that states the
contents in that state. A constant variable is created per bottle that defines
the maximum content $b_{i\max}$ the bottle can hold.  The initial state then
becomes.
$$b_0=3\wedge b_1=0\wedge b_2=0\wedge 
b_{1\max}=144\wedge b_{2\max}=72\wedge b_{3\max}=16$$

When we transition to the next state we can do three actions. With a $next$
function we describe the transition to the next state for every bottle. If the
next state is not defined for a bottle $b_i$ we assume $next(b_i)=b_i$.
\begin{itemize}
	\item Filling a bottle $b_i$\\
		If we fill a bottle $b_i$ the contents will be the maximum thus:\\
		$next(b_i)=b_{i\max}$.
	\item Emptying a bottle $b_i$\\
		If we empty a bottle $b_i$ the contents will become zero thus:\\
		$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$
		will be subtracted from $b_i$ and added to $b_j$. What exactly fits in
		$b_j$ can be described as $\min(b_{j\max}-b_j, b_i)$ thus the following
		state changes can be defined:\\
		$next(b_i)=b_i-\min(b_{j\max}-b_j, b_i)$\\
		$next(b_j)=b_j+\min(b_{j\max}-b_j, b_i)$
\end{itemize}

All transitions together in a disjunction would specify all possible
transitions.

\newpage
\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
		units. If so, give a scenario reaching this situation.}
		With the following goal the solution in Table~\ref{tab:sol2} is
		found by \textsc{NuSMV} within $0.29$ seconds.
		$$\mathcal{G}\neg(b_1=8\wedge b_2=1)$$
	\item
		\emph{Do the same for the variant in which the second bottle is
		replaced by a bottle that can hold 80 units, and all the rest remains
		the same.}
		When updating variable $b_{2\max}=80$ and using the goal from $(a)$
		\textsc{NuSMV} concludes that there is no there is no counterexample
		within $0.1$ seconds.
	\item
		\emph{Do the same for the variant in which the third bottle is replaced
		by a bottle that can hold 28 units, and all the rest (including the
		capacity of 72 of the second bottle) remains the same.}
		When updating variable $b_{3\max}=28$ and using the goal from $(a)$
		the solution in Table~\ref{tab:sol2} is found by \textsc{NuSMV} within
		$1.8$ seconds.
\end{enumerate}
\begin{table}[h]
	\centering\small
	\begin{tabular}{ccc}
		\begin{minipage}{.40\linewidth}
			\begin{tabular}{rrrrl}
				\toprule
				& $b_1$ & $b_2$ & $b_3$ & Action\\
				\midrule
				$0$ & $3$ & $0$ & $0$ &\\
				$1$ & $0$ & $0$ & $3$ & Poured $1$ in $3$\\
				$2$ & $144$ & $0$ & $3$ & Filled $1$\\
				$3$ & $72$ & $72$ & $3$ & Poured $1$ in $2$\\
				$4$ & $72$ & $59$ & $16$ & Poured $2$ in $3$\\
				$5$ & $88$ & $59$ & $0$ & Poured $3$ in $1$\\
				$6$ & $88$ & $43$ & $16$ & Poured $2$ in $3$\\
				$7$ & $104$ & $43$ & $0$ & Poured $3$ in $1$\\
				$8$ & $104$ & $27$ & $16$ & Poured $2$ in $3$\\
				$9$ & $120$ & $27$ & $0$ & Poured $3$ in $1$\\
				$10$ & $120$ & $11$ & $16$ & Poured $2$ in $3$\\
				$11$ & $136$ & $11$ & $0$ & Poured $3$ in $1$\\
				$12$ & $136$ & $11$ & $16$ & Filled $3$\\
				$13$ & $144$ & $11$ & $8$ & Poured $3$ in $1$\\
				$14$ & $0$ & $11$ & $8$ & Emptied $1$\\
				$15$ & $8$ & $11$ & $8$ & Poured $3$ in $1$\\
				\bottomrule
				\multicolumn{5}{c}{Solution for problem $2a$}
		\end{tabular}\vspace{16.55em}
	\end{minipage} & \quad & 
		\begin{minipage}{.40\linewidth}
			\begin{tabular}{rrrrl}
				\toprule
				 & $b_1$ & $b_2$ & $b_3$ & Action\\
				\midrule
				$0$ & $3$ & $0$ & $0$ &\\
				$1$ & $3$ & $72$ & $0$ & Filled $2$\\
				$2$ & $3$ & $44$ & $28$ & Poured $2$ in $3$\\
				$3$ & $0$ & $47$ & $28$ & Poured $1$ in $2$\\
				$4$ & $28$ & $47$ & $0$ & Poured $3$ in $1$\\
				$5$ & $28$ & $47$ & $28$ & Filled $3$\\
				$6$ & $56$ & $47$ & $0$ & Poured $3$ in $1$\\
				$7$ & $56$ & $19$ & $28$ & Poured $2$ in $3$\\
				$8$ & $84$ & $19$ & $0$ & Poured $3$ in $1$\\
				$9$ & $84$ & $0$ & $19$ & Poured $2$ in $3$\\
				$10$ & $12$ & $72$ & $19$ & Poured $2$ in $1$\\
				$11$ & $12$ & $63$ & $28$ & Poured $2$ in $3$\\
				$12$ & $40$ & $63$ & $0$ & Poured $3$ in $1$\\
				$13$ & $40$ & $35$ & $28$ & Poured $2$ in $3$\\
				$14$ & $68$ & $35$ & $0$ & Poured $3$ in $1$\\
				$15$ & $68$ & $7$ & $28$ & Poured $2$ in $3$\\
				$16$ & $96$ & $7$ & $0$ & Poured $3$ in $1$\\
				$17$ & $96$ & $0$ & $7$ & Poured $2$ in $3$\\
				$18$ & $24$ & $72$ & $7$ & Poured $1$ in $2$\\
				$19$ & $24$ & $51$ & $28$ & Poured $2$ in $3$\\
				$20$ & $52$ & $51$ & $0$ & Poured $3$ in $1$\\
				$21$ & $52$ & $23$ & $28$ & Poured $2$ in $1$\\
				$22$ & $80$ & $23$ & $0$ & Poured $3$ in $1$\\
				$23$ & $80$ & $0$ & $23$ & Poured $2$ in $3$\\
				$24$ & $8$ & $72$ & $23$ & Poured $1$ in $2$\\
				$25$ & $8$ & $67$ & $28$ & Poured $2$ in $3$\\
				$26$ & $8$ & $67$ & $0$ & Emptied $3$\\
				$27$ & $8$ & $39$ & $28$ & Poured $2$ in $3$\\
				$28$ & $8$ & $39$ & $0$ & Emptied $3$\\
				$29$ & $8$ & $11$ & $28$ & Poured $2$ in $3$\\
				\bottomrule
				\multicolumn{5}{c}{Solution for problem $2c$}
			\end{tabular}
		\end{minipage}
	\end{tabular}
	\caption{Solutions for problems $2a$ and $2c$}\label{tab:sol2}
\end{table}
