From 5c3d877d8673d19dac7ecfa8051170381a4626b6 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Thu, 26 Nov 2015 18:05:45 +0100 Subject: [PATCH] 2 solved --- a2/2.tex | 128 +++++++++++++++++++++++++++++++++++++++++++++++++ a2/ar.tex | 38 +++++++-------- a2/pre.tex | 27 +++-------- a2/src/2a.smv | 41 ++++++++++++++++ a2/src/2b.smv | 41 ++++++++++++++++ a2/src/2c.smv | 41 ++++++++++++++++ a2/src/path.sh | 1 + 7 files changed, 277 insertions(+), 40 deletions(-) create mode 100644 a2/src/2a.smv create mode 100644 a2/src/2b.smv create mode 100644 a2/src/2c.smv diff --git a/a2/2.tex b/a2/2.tex index e69de29..da2bafd 100644 --- a/a2/2.tex +++ b/a2/2.tex @@ -0,0 +1,128 @@ +\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} diff --git a/a2/ar.tex b/a2/ar.tex index 7b5d21e..91fe795 100644 --- a/a2/ar.tex +++ b/a2/ar.tex @@ -3,25 +3,25 @@ \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} diff --git a/a2/pre.tex b/a2/pre.tex index 839423e..5f0513c 100644 --- a/a2/pre.tex +++ b/a2/pre.tex @@ -1,27 +1,12 @@ \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} diff --git a/a2/src/2a.smv b/a2/src/2a.smv new file mode 100644 index 0000000..300f580 --- /dev/null +++ b/a2/src/2a.smv @@ -0,0 +1,41 @@ +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) diff --git a/a2/src/2b.smv b/a2/src/2b.smv new file mode 100644 index 0000000..f0e169e --- /dev/null +++ b/a2/src/2b.smv @@ -0,0 +1,41 @@ +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) diff --git a/a2/src/2c.smv b/a2/src/2c.smv new file mode 100644 index 0000000..a735f05 --- /dev/null +++ b/a2/src/2c.smv @@ -0,0 +1,41 @@ +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) diff --git a/a2/src/path.sh b/a2/src/path.sh index 9d9e771..d7dfea0 100644 --- a/a2/src/path.sh +++ b/a2/src/path.sh @@ -1 +1,2 @@ export PATH=$PATH:/home/mart/downloads/NuSMV-2.5.4/nusmv +export PATH=$PATH:/home/mart/projects/NuSMV-2.6.0-Linux/bin -- 2.20.1