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 can be solved by transforming it into a symbolic model.  For all
  15 bottles $b_i$ for $i\in\{1\ldots3\}$ a variable is created that states the
  16 contents in that state. A constant variable is created per bottle that defines
  17 the maximum content $b_{i\max}$ the bottle can hold.  The initial state then
  18 becomes.
  19 $$b_0=3\wedge b_1=0\wedge b_2=0\wedge
  20 b_{1\max}=144\wedge b_{2\max}=72\wedge b_{3\max}=16$$
  21
  22 When we transition to the next state we can do three actions. With a $next$
  23 function we describe the transition to the next state for every bottle. If the
  24 next state is not defined for a bottle $b_i$ we assume $next(b_i)=b_i$.
  25 \begin{itemize}
  26         \item Filling a bottle $b_i$\\
  27                 If we fill a bottle $b_i$ the contents will be the maximum thus:\\
  28                 $next(b_i)=b_{i\max}$.
  29         \item Emptying a bottle $b_i$\\
  30                 If we empty a bottle $b_i$ the contents will become zero thus:\\
  31                 $next(b_i)=0$.
  32         \item Pouring a bottle $b_i$ in bottle $b_j$ for $i\neq j$\\
  33                 If we pour a bottle $b_i$ into $b_j$, the contents that fits in $b_j$
  34                 will be subtracted from $b_i$ and added to $b_j$. What exactly fits in
  35                 $b_j$ can be described as $\min(b_{j\max}-b_j, b_i)$ thus the following
  36                 state changes can be defined:\\
  37                 $next(b_i)=b_i-\min(b_{j\max}-b_j, b_i)$\\
  38                 $next(b_j)=b_j+\min(b_{j\max}-b_j, b_i)$
  39 \end{itemize}
  40
  41 All transitions together in a disjuction would specify all possible
  42 transitions.
  43
  44 \newpage
  45 \begin{enumerate}[(a)]
  46         \item
  47                 \emph{Determine whether it is possible to arrive at a situation in
  48                 which the first bottle contains 8 units and the second one contains 11
  49                 units. If so, give a scenario reaching this situation.}
  50                 With the following goal the solution in Table~\ref{tab:sol2} is
  51                 found by \textsc{NuSMV} within $0.29$ seconds.
  52                 $$\mathcal{G}\neg(b_1=8\wedge b_2=1)$$
  53         \item
  54                 \emph{Do the same for the variant in which the second bottle is
  55                 replaced by a bottle that can hold 80 units, and all the rest remains
  56                 the same.}
  57                 When updating variable $b_{2\max}=80$ and using the goal from $(a)$
  58                 \textsc{NuSMV} concludes that there is no there is no counterexample
  59                 within $0.1$ seconds.
  60         \item
  61                 \emph{Do the same for the variant in which the third bottle is replaced
  62                 by a bottle that can hold 28 units, and all the rest (including the
  63                 capacity of 72 of the second bottle) remains the same.}
  64                 When updating variable $b_{3\max}=28$ and using the goal from $(a)$
  65                 the solution in Table~\ref{tab:sol2} is found by \textsc{NuSMV} within
  66                 $1.8$ seconds.
  67 \end{enumerate}
  68 \begin{table}[h]
  69         \centering\small
  70         \begin{tabular}{ccc}
  71                 \begin{minipage}{.40\linewidth}
  72                         \begin{tabular}{rrrrl}
  73                                 \toprule
  74                                 & $b_1$ & $b_2$ & $b_3$ & Action\\
  75                                 \midrule
  76                                 $0$ & $3$ & $0$ & $0$ &\\
  77                                 $1$ & $0$ & $0$ & $3$ & Poured $1$ in $3$\\
  78                                 $2$ & $144$ & $0$ & $3$ & Filled $1$\\
  79                                 $3$ & $72$ & $72$ & $3$ & Poured $1$ in $2$\\
  80                                 $4$ & $72$ & $59$ & $16$ & Poured $2$ in $3$\\
  81                                 $5$ & $88$ & $59$ & $0$ & Poured $3$ in $1$\\
  82                                 $6$ & $88$ & $43$ & $16$ & Poured $2$ in $3$\\
  83                                 $7$ & $104$ & $43$ & $0$ & Poured $3$ in $1$\\
  84                                 $8$ & $104$ & $27$ & $16$ & Poured $2$ in $3$\\
  85                                 $9$ & $120$ & $27$ & $0$ & Poured $3$ in $1$\\
  86                                 $10$ & $120$ & $11$ & $16$ & Poured $2$ in $3$\\
  87                                 $11$ & $136$ & $11$ & $0$ & Poured $3$ in $1$\\
  88                                 $12$ & $136$ & $11$ & $16$ & Filled $3$\\
  89                                 $13$ & $144$ & $11$ & $8$ & Poured $3$ in $1$\\
  90                                 $14$ & $0$ & $11$ & $8$ & Emptied $1$\\
  91                                 $15$ & $8$ & $11$ & $8$ & Poured $3$ in $1$\\
  92                                 \bottomrule
  93                                 \multicolumn{5}{c}{Solution for problem $2a$}
  94                 \end{tabular}\vspace{16.55em}
  95         \end{minipage} & \quad &
  96                 \begin{minipage}{.40\linewidth}
  97                         \begin{tabular}{rrrrl}
  98                                 \toprule
  99                                  & $b_1$ & $b_2$ & $b_3$ & Action\\
 100                                 \midrule
 101                                 $0$ & $3$ & $0$ & $0$ &\\
 102                                 $1$ & $3$ & $72$ & $0$ & Filled $2$\\
 103                                 $2$ & $3$ & $44$ & $28$ & Poured $2$ in $3$\\
 104                                 $3$ & $0$ & $47$ & $28$ & Poured $1$ in $2$\\
 105                                 $4$ & $28$ & $47$ & $0$ & Poured $3$ in $1$\\
 106                                 $5$ & $28$ & $47$ & $28$ & Filled $3$\\
 107                                 $6$ & $56$ & $47$ & $0$ & Poured $3$ in $1$\\
 108                                 $7$ & $56$ & $19$ & $28$ & Poured $2$ in $3$\\
 109                                 $8$ & $84$ & $19$ & $0$ & Poured $3$ in $1$\\
 110                                 $9$ & $84$ & $0$ & $19$ & Poured $2$ in $3$\\
 111                                 $10$ & $12$ & $72$ & $19$ & Poured $2$ in $1$\\
 112                                 $11$ & $12$ & $63$ & $28$ & Poured $2$ in $3$\\
 113                                 $12$ & $40$ & $63$ & $0$ & Poured $3$ in $1$\\
 114                                 $13$ & $40$ & $35$ & $28$ & Poured $2$ in $3$\\
 115                                 $14$ & $68$ & $35$ & $0$ & Poured $3$ in $1$\\
 116                                 $15$ & $68$ & $7$ & $28$ & Poured $2$ in $3$\\
 117                                 $16$ & $96$ & $7$ & $0$ & Poured $3$ in $1$\\
 118                                 $17$ & $96$ & $0$ & $7$ & Poured $2$ in $3$\\
 119                                 $18$ & $24$ & $72$ & $7$ & Poured $1$ in $2$\\
 120                                 $19$ & $24$ & $51$ & $28$ & Poured $2$ in $3$\\
 121                                 $20$ & $52$ & $51$ & $0$ & Poured $3$ in $1$\\
 122                                 $21$ & $52$ & $23$ & $28$ & Poured $2$ in $1$\\
 123                                 $22$ & $80$ & $23$ & $0$ & Poured $3$ in $1$\\
 124                                 $23$ & $80$ & $0$ & $23$ & Poured $2$ in $3$\\
 125                                 $24$ & $8$ & $72$ & $23$ & Poured $1$ in $2$\\
 126                                 $25$ & $8$ & $67$ & $28$ & Poured $2$ in $3$\\
 127                                 $26$ & $8$ & $67$ & $0$ & Emptied $3$\\
 128                                 $27$ & $8$ & $39$ & $28$ & Poured $2$ in $3$\\
 129                                 $28$ & $8$ & $39$ & $0$ & Emptied $3$\\
 130                                 $29$ & $8$ & $11$ & $28$ & Poured $2$ in $3$\\
 131                                 \bottomrule
 132                                 \multicolumn{5}{c}{Solution for problem $2c$}
 133                         \end{tabular}
 134                 \end{minipage}
 135         \end{tabular}
 136         \caption{Solutions for problems $2a$ and $2c$}\label{tab:sol2}
 137 \end{table}