+\section{Problem 2}
+\emph{Three bottles can hold 144, 72 and 16 units (say, centilite rs),
+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 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
+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
+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:\\
+ $\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:\\
+ $\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$
+ 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:\\
+ $\text{next}(b_i)=b_i-\min(b_{j\max}-b_j, b_i)$\\
+ $\text{next}(b_j)=b_j+\min(b_{j\max}-b_j, b_i)$
+\end{itemize}
+
+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.]
+ \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.}
+
+ The solution described in \autoref{tab:sol2a} is found by
+ \textsc{NuSMV} within $0.29$ seconds.
+ \begin{table}[h]
+ \centering\small
+ \begin{tabular}{rrrrl}
+ \toprule
+ State & Bottle 1 & Bottle 2 & Bottle 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
+ \end{tabular}
+ \caption{Solution for problem 1}\label{tab:sol2a}
+ \end{table}
+ \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.}
+
+ There is no solution for this configuration.
+ \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.}
+
+ The solution described in \autoref{tab:sol2c} is found by
+ \textsc{NuSMV} within $1.8$ seconds.
+ \begin{table}[h]
+ \centering\small
+ \begin{tabular}{rrrrl}
+ \toprule
+ State & Bottle 1 & Bottle 2 & Bottle 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
+ \end{tabular}
+ \caption{Solution for problem 3}\label{tab:sol2c}
+ \end{table}
+\end{enumerate}
repositories / ar1516.git / blobdiff