a2/2.tex

   1 \section{Problem 2}
   2 \emph{Three bottles can hold 144, 72 and 16 units (say, centiliters),
   3 respectively. Initially the first one contains 3 units of water, the
   4 others are empty. The following actions may be performed any number of
   5 times:
   6 \begin{itemize}
   7         \item One of the bottles is fully filled, at some water tap.
   8         \item One of the bottles is emptied.
   9         \item The content of one bottle is poured into another one. If it fits,
  10                 then the full content is poured, otherwise the pouring stops when the
  11                 other bottle is full.
  12 \end{itemize}}
  13
  14 The problem is easily solvable using a symbolic model checker since it is
  15 cleary a problem that progresses with state transfers up to a goal. For all
  16 bottles $b_i$ for $i\in\{1\ldots3\}$ we create a variable stating the contents
  17 in the current state $b_i$ and a constant that describes the maximum content
  18 $b_{i\max}$. State transitions come in three classes. With the next
  19 function we describe the transition to the next state. If the next state is not
  20 defined for a bottle $b_i$ we assume $\text{next}(b_i)=b_i$.
  21 \begin{itemize}
  22         \item Filling a bottle $b_i$\\
  23                 If we fill a bottle $b_i$ the contens will be the maximum thus:\\
  24                 $\text{next}(b_i)=b_{i\max}$.
  25         \item Emptying a bottle $b_i$\\
  26                 If we empty a bottle $b_i$ the contens will become zero thus:\\
  27                 $\text{next}(b_i)=0$.
  28         \item Pouring a bottle $b_i$ in bottle $b_j$ for $i\neq j$\\
  29                 If we pour a bottle $b_i$ into $b_j$, the contents that fits in $b_j$
  30                 will be subtracted from $b_i$ and added to $b_j$. What exactly fits in
  31                 $b_j$ can be described as $\min(b_{j\max}-b_j, b_i)$ thus the following
  32                 state changes can be defined:\\
  33                 $\text{next}(b_i)=b_i-\min(b_{j\max}-b_j, b_i)$\\
  34                 $\text{next}(b_j)=b_j+\min(b_{j\max}-b_j, b_i)$
  35 \end{itemize}
  36
  37 All transitions are unconstrained and therefore we can convert this very easily
  38 to \textsc{NuSMV} by enclosing all the transition classes in brackets and
  39 joining them with logical or operators.
  40
  41 \begin{enumerate}[a.]
  42         \item
  43                 \emph{Determine whether it is possible to arrive at a situation in
  44                 which the first bottle contains 8 units and the second one contains 11
  45                 units. If so, give a scenario reaching this situation.}
  46
  47                 The solution described in \autoref{tab:sol2a} is found by
  48                 \textsc{NuSMV} within $0.29$ seconds.
  49                 \begin{table}[H]
  50                         \centering\small
  51                         \begin{tabular}{rrrrl}
  52                                 \toprule
  53                                 State & Bottle 1 & Bottle 2 & Bottle 3 & Action\\
  54                                 \midrule
  55                                 $0$ & $3$ & $0$ & $0$ &\\
  56                                 $1$ & $0$ & $0$ & $3$ & Poured $1$ in $3$\\
  57                                 $2$ & $144$ & $0$ & $3$ & Filled $1$\\
  58                                 $3$ & $72$ & $72$ & $3$ & Poured $1$ in $2$\\
  59                                 $4$ & $72$ & $59$ & $16$ & Poured $2$ in $3$\\
  60                                 $5$ & $88$ & $59$ & $0$ & Poured $3$ in $1$\\
  61                                 $6$ & $88$ & $43$ & $16$ & Poured $2$ in $3$\\
  62                                 $7$ & $104$ & $43$ & $0$ & Poured $3$ in $1$\\
  63                                 $8$ & $104$ & $27$ & $16$ & Poured $2$ in $3$\\
  64                                 $9$ & $120$ & $27$ & $0$ & Poured $3$ in $1$\\
  65                                 $10$ & $120$ & $11$ & $16$ & Poured $2$ in $3$\\
  66                                 $11$ & $136$ & $11$ & $0$ & Poured $3$ in $1$\\
  67                                 $12$ & $136$ & $11$ & $16$ & Filled $3$\\
  68                                 $13$ & $144$ & $11$ & $8$ & Poured $3$ in $1$\\
  69                                 $14$ & $0$ & $11$ & $8$ & Emptied $1$\\
  70                                 $15$ & $8$ & $11$ & $8$ & Poured $3$ in $1$\\
  71                                 \bottomrule
  72                         \end{tabular}
  73                         \caption{Solution for problem 1}\label{tab:sol2a}
  74                 \end{table}
  75         \item
  76                 \emph{Do the same for the variant in which the second bottle is
  77                 replaced by a bottle that can hold 80 units, and all the rest remains
  78                 the same.}
  79
  80                 There is no solution for this configuration.
  81         \item
  82                 \emph{Do the same for the variant in which the third bottle is replaced
  83                 by a bottle that can hold 28 units, and all the rest (including the
  84                 capacity of 72 of the second bottle) remains the same.}
  85
  86                 The solution described in \autoref{tab:sol2c} is found by
  87                 \textsc{NuSMV} within $1.8$ seconds.
  88                 \begin{table}[H]
  89                         \centering\small
  90                         \begin{tabular}{rrrrl}
  91                                 \toprule
  92                                 State & Bottle 1 & Bottle 2 & Bottle 3 & Action\\
  93                                 \midrule
  94                                 $0$ & $3$ & $0$ & $0$ &\\
  95                                 $1$ & $3$ & $72$ & $0$ & Filled $2$\\
  96                                 $2$ & $3$ & $44$ & $28$ & Poured $2$ in $3$\\
  97                                 $3$ & $0$ & $47$ & $28$ & Poured $1$ in $2$\\
  98                                 $4$ & $28$ & $47$ & $0$ & Poured $3$ in $1$\\
  99                                 $5$ & $28$ & $47$ & $28$ & Filled $3$\\
 100                                 $6$ & $56$ & $47$ & $0$ & Poured $3$ in $1$\\
 101                                 $7$ & $56$ & $19$ & $28$ & Poured $2$ in $3$\\
 102                                 $8$ & $84$ & $19$ & $0$ & Poured $3$ in $1$\\
 103                                 $9$ & $84$ & $0$ & $19$ & Poured $2$ in $3$\\
 104                                 $10$ & $12$ & $72$ & $19$ & Poured $2$ in $1$\\
 105                                 $11$ & $12$ & $63$ & $28$ & Poured $2$ in $3$\\
 106                                 $12$ & $40$ & $63$ & $0$ & Poured $3$ in $1$\\
 107                                 $13$ & $40$ & $35$ & $28$ & Poured $2$ in $3$\\
 108                                 $14$ & $68$ & $35$ & $0$ & Poured $3$ in $1$\\
 109                                 $15$ & $68$ & $7$ & $28$ & Poured $2$ in $3$\\
 110                                 $16$ & $96$ & $7$ & $0$ & Poured $3$ in $1$\\
 111                                 $17$ & $96$ & $0$ & $7$ & Poured $2$ in $3$\\
 112                                 $18$ & $24$ & $72$ & $7$ & Poured $1$ in $2$\\
 113                                 $19$ & $24$ & $51$ & $28$ & Poured $2$ in $3$\\
 114                                 $20$ & $52$ & $51$ & $0$ & Poured $3$ in $1$\\
 115                                 $21$ & $52$ & $23$ & $28$ & Poured $2$ in $1$\\
 116                                 $22$ & $80$ & $23$ & $0$ & Poured $3$ in $1$\\
 117                                 $23$ & $80$ & $0$ & $23$ & Poured $2$ in $3$\\
 118                                 $24$ & $8$ & $72$ & $23$ & Poured $1$ in $2$\\
 119                                 $25$ & $8$ & $67$ & $28$ & Poured $2$ in $3$\\
 120                                 $26$ & $8$ & $67$ & $0$ & Emptied $3$\\
 121                                 $27$ & $8$ & $39$ & $28$ & Poured $2$ in $3$\\
 122                                 $28$ & $8$ & $39$ & $0$ & Emptied $3$\\
 123                                 $29$ & $8$ & $11$ & $28$ & Poured $2$ in $3$\\
 124                                 \bottomrule
 125                         \end{tabular}
 126                         \caption{Solution for problem 3}\label{tab:sol2c}
 127                 \end{table}
 128 \end{enumerate}