other bottle is full.
\end{itemize}}
-The problem is easily solvable using a symbolic model checker since it is
-clearly 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$.
+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:\\
- $\text{next}(b_i)=b_{i\max}$.
+ $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:\\
- $\text{next}(b_i)=0$.
+ $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)$
+ $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 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.
+All transitions together in a disjuction 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.}
-
- The solution described in \autoref{tab:sol2a} is found by
- \textsc{NuSMV} within $0.29$ seconds.
- \begin{table}[H]
- \centering\small
+ 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}{.5\linewidth}
\begin{tabular}{rrrrl}
\toprule
- State & Bottle 1 & Bottle 2 & Bottle 3 & Action\\
+ & Bottle 1 & Bottle 2 & Bottle 3 & Action\\
\midrule
$0$ & $3$ & $0$ & $0$ &\\
$1$ & $0$ & $0$ & $3$ & Poured $1$ in $3$\\
$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
+ \multicolumn{5}{c}{Solution for problem $2a$}
+ \end{tabular}\vspace{16.55em}
+ \end{minipage} & \quad &
+ \begin{minipage}{.5\linewidth}
\begin{tabular}{rrrrl}
\toprule
- State & Bottle 1 & Bottle 2 & Bottle 3 & Action\\
+ & Bottle 1 & Bottle 2 & Bottle 3 & Action\\
\midrule
$0$ & $3$ & $0$ & $0$ &\\
$1$ & $3$ & $72$ & $0$ & Filled $2$\\
$28$ & $8$ & $39$ & $0$ & Emptied $3$\\
$29$ & $8$ & $11$ & $28$ & Poured $2$ in $3$\\
\bottomrule
+ \multicolumn{5}{c}{Solution for problem $2c$}
\end{tabular}
- \caption{Solution for problem 2}\label{tab:sol2c}
- \end{table}
-\end{enumerate}
+ \end{minipage}
+ \end{tabular}
+ \caption{Solutions for problems $2a$ and $2c$}\label{tab:sol2}
+\end{table}
repositories / ar1516.git / blobdiff