+\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}
\maketitle
\tableofcontents
-\setcounter{section}{-1}
-\section{General approach}
-Implementing all the problems by hand in SMT-Lib format would be too much work
-and therefore all problems have an accompanying bash script contains a function
-\lstinline{generate} that generates the SMT-Lib format. The script feeds the
-SMT-Lib format to yices after which the output is feeded to a Python script
-that visualizes the solution. This means that for all problems $p$ for $p\in
-\{1,\ldots, 4\}$ there exist $2$ files. \texttt{ap.bash} that generates the
-solution and \texttt{ap.py} that visualizes the solution. All solving is done
-on the benchmark system listed in Listing~\ref{listing:benchmark}.
-
-\begin{lstlisting}[caption={Benchmark system},label={listing:benchmark}]
-CPU: 3600MHz AMD FX(tm)-4100 Quad-Core Processor
-RAM: 8GB
-
-Yices: 2.4.1
-SMT-Lib: 1.2
-Bash: 4.3.30(1)
-\end{lstlisting}
+%\setcounter{section}{-1}
+%\section{General approach}
+%Implementing all the problems by hand in SMT-Lib format would be too much work
+%and therefore all problems have an accompanying bash script contains a function
+%\lstinline{generate} that generates the SMT-Lib format. The script feeds the
+%SMT-Lib format to yices after which the output is feeded to a Python script
+%that visualizes the solution. This means that for all problems $p$ for $p\in
+%\{1,\ldots, 4\}$ there exist $2$ files. \texttt{ap.bash} that generates the
+%solution and \texttt{ap.py} that visualizes the solution. All solving is done
+%on the benchmark system listed in Listing~\ref{listing:benchmark}.
+%
+%\begin{lstlisting}[caption={Benchmark system},label={listing:benchmark}]
+%CPU: 3600MHz AMD FX(tm)-4100 Quad-Core Processor
+%RAM: 8GB
+%
+%Yices: 2.4.1
+%SMT-Lib: 1.2
+%Bash: 4.3.30(1)
+%\end{lstlisting}
\newpage
\input{1.tex}
\documentclass{article}
-\usepackage{hyperref} % For clickable links
-\usepackage{a4wide} % For better page usage
-\usepackage{float} % For better placement of tables/figures
-\usepackage{amsmath} % For align
-\usepackage{listings} % For code snippets
-\usepackage{booktabs} % For nice tables
+\usepackage{hyperref} % For clickable links
+\usepackage{a4wide} % For better page usage
+\usepackage{booktabs} % For nice tables
+\usepackage{enumerate} % For nice tables
+\usepackage{amsmath} % For nice tables
-\everymath{\displaystyle\allowdisplaybreaks}
-
-\lstset{%
- basicstyle=\scriptsize,
- breakatwhitespace=true,
- breaklines=true,
- keepspaces=true,
- numbers=left,
- numberstyle=\tiny,
- frame=L,
- showspaces=false,
- showstringspaces=false,
- showtabs=false,
- tabsize=2
-}
+\everymath{\displaystyle}
\author{Mart Lubbers (s4109503)}
\title{Automated reasoning Assignment 2}
--- /dev/null
+MODULE main
+DEFINE
+max1:=144; max2:=72; max3:=16;
+VAR
+b1: 0..max1; b2: 0..max2; b3: 0..max3;
+INIT
+b1=3 & b2=0 & b3=0
+TRANS
+-- Empty bottle 1
+(next(b1)=0 & next(b2)=b2 & next(b3)=b3) |
+-- Empty bottle 2
+(next(b1)=b1 & next(b2)=0 & next(b3)=b3) |
+-- Empty bottle 3
+(next(b1)=b1 & next(b2)=b2 & next(b3)=0) |
+-- Fill bottle 1
+(next(b1)=max1 & next(b2)=b2 & next(b3)=b3) |
+-- Fill bottle 2
+(next(b1)=b1 & next(b2)=max2 & next(b3)=b3) |
+-- Fill bottle 3
+(next(b1)=b1 & next(b2)=b2 & next(b3)=max3) |
+-- Empty bottle 1 in 2
+( next(b1)=b1 - min(max2 - b2, b1) &
+ next(b2)=b2 + min(max2 - b2, b1) &
+ next(b3)=b3) |
+-- Empty bottle 1 in 3
+( next(b1)=b1 - min(max3 - b3, b1) &
+ next(b2)=b2 &
+ next(b3)=b3 + min(max3 - b3, b1)) |
+-- Empty bottle 2 in 1
+( next(b1)=b1 + min(max1 - b1, b2) &
+ next(b2)=b2 - min(max1 - b1, b2) &
+ next(b3)=b3) |
+-- Empty bottle 2 in 3
+( next(b1)=b1 &
+ next(b2)=b2 - min(max3 - b3, b2) &
+ next(b3)=b3 + min(max3 - b3, b2)) |
+-- Empty bottle 3 in 1
+( next(b1)=b1 + min(max1 - b1, b3) &
+ next(b2)=b2 &
+ next(b3)=b3 - min(max1 - b1, b3))
+LTLSPEC G !(b1=8 & b2=11)
--- /dev/null
+MODULE main
+DEFINE
+max1:=144; max2:=80; max3:=16;
+VAR
+b1: 0..max1; b2: 0..max2; b3: 0..max3;
+INIT
+b1=3 & b2=0 & b3=0
+TRANS
+-- Empty bottle 1
+(next(b1)=0 & next(b2)=b2 & next(b3)=b3) |
+-- Empty bottle 2
+(next(b1)=b1 & next(b2)=0 & next(b3)=b3) |
+-- Empty bottle 3
+(next(b1)=b1 & next(b2)=b2 & next(b3)=0) |
+-- Fill bottle 1
+(next(b1)=max1 & next(b2)=b2 & next(b3)=b3) |
+-- Fill bottle 2
+(next(b1)=b1 & next(b2)=max2 & next(b3)=b3) |
+-- Fill bottle 3
+(next(b1)=b1 & next(b2)=b2 & next(b3)=max3) |
+-- Empty bottle 1 in 2
+( next(b1)=b1 - min(max2 - b2, b1) &
+ next(b2)=b2 + min(max2 - b2, b1) &
+ next(b3)=b3) |
+-- Empty bottle 1 in 3
+( next(b1)=b1 - min(max3 - b3, b1) &
+ next(b2)=b2 &
+ next(b3)=b3 + min(max3 - b3, b1)) |
+-- Empty bottle 2 in 1
+( next(b1)=b1 + min(max1 - b1, b2) &
+ next(b2)=b2 - min(max1 - b1, b2) &
+ next(b3)=b3) |
+-- Empty bottle 2 in 3
+( next(b1)=b1 &
+ next(b2)=b2 - min(max3 - b3, b2) &
+ next(b3)=b3 + min(max3 - b3, b2)) |
+-- Empty bottle 3 in 1
+( next(b1)=b1 + min(max1 - b1, b3) &
+ next(b2)=b2 &
+ next(b3)=b3 - min(max1 - b1, b3))
+LTLSPEC G !(b1=8 & b2=11)
--- /dev/null
+MODULE main
+DEFINE
+max1:=144; max2:=72; max3:=28;
+VAR
+b1: 0..max1; b2: 0..max2; b3: 0..max3;
+INIT
+b1=3 & b2=0 & b3=0
+TRANS
+-- Empty bottle 1
+(next(b1)=0 & next(b2)=b2 & next(b3)=b3) |
+-- Empty bottle 2
+(next(b1)=b1 & next(b2)=0 & next(b3)=b3) |
+-- Empty bottle 3
+(next(b1)=b1 & next(b2)=b2 & next(b3)=0) |
+-- Fill bottle 1
+(next(b1)=max1 & next(b2)=b2 & next(b3)=b3) |
+-- Fill bottle 2
+(next(b1)=b1 & next(b2)=max2 & next(b3)=b3) |
+-- Fill bottle 3
+(next(b1)=b1 & next(b2)=b2 & next(b3)=max3) |
+-- Empty bottle 1 in 2
+( next(b1)=b1 - min(max2 - b2, b1) &
+ next(b2)=b2 + min(max2 - b2, b1) &
+ next(b3)=b3) |
+-- Empty bottle 1 in 3
+( next(b1)=b1 - min(max3 - b3, b1) &
+ next(b2)=b2 &
+ next(b3)=b3 + min(max3 - b3, b1)) |
+-- Empty bottle 2 in 1
+( next(b1)=b1 + min(max1 - b1, b2) &
+ next(b2)=b2 - min(max1 - b1, b2) &
+ next(b3)=b3) |
+-- Empty bottle 2 in 3
+( next(b1)=b1 &
+ next(b2)=b2 - min(max3 - b3, b2) &
+ next(b3)=b3 + min(max3 - b3, b2)) |
+-- Empty bottle 3 in 1
+( next(b1)=b1 + min(max1 - b1, b3) &
+ next(b2)=b2 &
+ next(b3)=b3 - min(max1 - b1, b3))
+LTLSPEC G !(b1=8 & b2=11)
export PATH=$PATH:/home/mart/downloads/NuSMV-2.5.4/nusmv
+export PATH=$PATH:/home/mart/projects/NuSMV-2.6.0-Linux/bin
repositories / ar1516.git / commitdiff