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
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
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$.
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:\\
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)$
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.
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.
}
47 The solution described in
\autoref{tab:sol2a
} is found by
48 \textsc{NuSMV
} within $
0.29$ seconds.
51 \begin{tabular
}{rrrrl
}
53 State & Bottle
1 & Bottle
2 & Bottle
3 & Action\\
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$\\
73 \caption{Solution for problem
1}\label{tab:sol2a
}
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
80 There is no solution for this configuration.
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.
}
86 The solution described in
\autoref{tab:sol2c
} is found by
87 \textsc{NuSMV
} within $
1.8$ seconds.
90 \begin{tabular
}{rrrrl
}
92 State & Bottle
1 & Bottle
2 & Bottle
3 & Action\\
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$\\
126 \caption{Solution for problem
3}\label{tab:sol2c
}