containing an unbounded supply. The villages only have a limited capacity to
store food packages: for $A$ and $B$ this capacity is $120$, for $C$ it is
$200$. Initially, the truck is in $S$ and is fully loaded, and in $A$, $B$ and
-$C$ there are $40$, $30$ and $145$ food packages, respectively.}
+$C$ there are $40$, $30$ and $145$ food packages, respectively.}\\
-The problem can be described as a SAT problem that we can solve in SAT-solver.
-Every movement from the truck from a city to a city is called an iteration $i$
-for $i\in I$ where $I=\{0\ldots\}$. For every iteration $i$ we make variables
-$a_i, b_i, c_i, t_i, l_i, d_i$ respectively for the capacity of city $A$,
-city $B$, city $C$, the truck, the trucks location and a help variable to
-record how much food is dumped in the city. The distance between two cities is
-described with the function $dist(x, y)$. For all cities except $S$ and the
-truck a variable is defined that states the maximum capacity. We express all
-the constant values in the formula called $const$.
+The problem can be solved by transforming it to a SAT problem. Every movement
+from the truck from a city to a city is called an iteration $i\in I$ where
+$I=\{0\ldots\}$. For every iteration $i$ variables $a_i, b_i, c_i, t_i, l_i,
+d_i$ are createde respectively for the stock of city $A$, city $B$, city $C$,
+the truck, the trucks location and the amount of food dumped. We introduce a
+function $dist(x,y)$ that returns the distance between two cities. For $A,B,C$
+and the truck a variable is declared which states the maximum capacity. All the
+constants together is called $\mathcal{CON}$.
$$a_{\max}=120\wedge b_{\max}=120\wedge c_{\max}=200\wedge t_{\max}=300$$
Iteration $0$ depicts the initial state and can be described with a simple
-conjunction called $initial$.
+conjunction called $\mathcal{INI}$.
$$a_0=40\wedge b_0=30\wedge c_0=145\wedge t_0=300\wedge l_0=S\wedge d_0=0$$
In every iteration there are certain constraints that always have to hold. We
-call them $constraints$ and they are expressed as:
+call them $\mathcal{CST}(i)$ and they are expressed as:
$$d_i>0\wedge
d_i\leq t_{\max}\wedge
t_i\geq\wedge
t_i\leq t_{\max}\wedge
\bigwedge_{k\in\{A,B,C\}}k_i>0$$
-We reason about the new iteration $i$ from the things we know about iteration
-$i-1$. The crucial part is the location we were in iteration $i-1$ and we make
-a disjunction over all possible cities and describe the result in the following
-formula called $trans$. We introduce a function $conn(s)$ that returns the set
-of all cities connected to city $s$. To begin with $(1)$ sets the location of
-the previous iteration correct and checks whether the city will not run out of
-food while travelled too. $(2)$ deals with the fact that the truck can not dump
-any food in city $S$ and constraints the amount of food dumped in the city.
-$(3)$ deals with the fact that the dumped food is added to the current stock of
-the city. Sub formula $(4)$ deals with the fact that if the truck is in $S$ it
-is replenished and otherwise the dumped load is subtracted from the trucks
-load. Finally $(5)$ deals with the other cities which will have their stock
-decremented with the distance traveled.
-
+Besides the constraints the movement of the truck should be modeled. Depending
+on $l_{i-1}$ we want to reason about the consequences of the truck moving to
+$l_{i}$. The formula is called $\mathcal{TRA}$. We introduce a function
+$conn(s)$ that returns the set of all cities connected to city $s$. $(1)$ sets
+the location of the previous iteration correct and checks whether the city is
+reachable without running out of food. $(2)$ limits the amount of food dumped
+according to distance traveled, the old stock and the truck stock. When the
+truck is in $S$ the truck will just be filled. $(3)$ adds the dumped food to
+the stock of the city. $(4)$ subtracts the dumped food stock from the truck.
+Finally $(5)$ subtracts the distance traveled from the food stock.
\begin{align}
\bigvee_{k\in\{S\}\cup V}
l_{i-1}=k\wedge
k''_i=k''_{i-1}-dist(k,k')
\end{align}
-We tie all this together in one big formula that is as follows:
-$$const\wedge initial\wedge
-\bigwedge_{i\in I}\left(constraints\wedge trans\right)$$
+All the formulas tied together leads to the final formula that is satisfiable
+if and only if there is never a depleted city in any iteration.
+$$\mathcal{CON}\wedge\mathcal{INI}\wedge
+\bigwedge_{i\in I}\left(\mathcal{CST}(i)\wedge\mathcal{TRA}(i)\right)$$
+\newpage
\begin{enumerate}[(a)]
\item \emph{Show that it is impossible to deliver food packages in such a
way that each of the villages consumes one food package per time unit
forever.}
Incrementally increasing the number of iterations does result in
finding an unsatisfiable formula with $I=21$. Thus there is no infinite
- path that keeps the cities saturated forever.
+ path that keeps the cities saturated.
\item \emph{Show that this is possible if the capacity of the truck is
increased to 320 food packages. (Note that a finite graph contains an
infinite path starting in a node $v$ if and only if there is a path
$$\bigvee_{i\in I}\bigvee_{j\in \{0\ldots i-1\}}\left(
t_i=t_j\wedge l_i=l_j\wedge\bigwedge_{k\in V}k_i=k_j\right)
$$
-
- When we incrementally increase the number of iterations we see that
- when we have more then $10$ iterations we encounter a cycle. This is
- shown in Table~\ref{tbl:s3b} where iteration $4$ and iteration $11$ are
- equal.
- \begin{table}[H]
- \centering
- \begin{tabular}{lrrrrcr}
- \toprule
- $I$ & $A$ & $B$ & $C$ & Truck & Location & Dump\\
- \midrule
- $0$ & $40$ & $30$ & $145$ & $320$ & $S$ & $0$\\
- $1$ & $19$ & $35$ & $124$ & $294$ & $B$ & $26$\\
- $2$ & $120$ & $18$ & $107$ & $176$ & $A$ & $118$\\
- $3$ & $103$ & $120$ & $90$ & $57$ & $B$ & $119$\\
- \textbf{4} & \textbf{82} & \textbf{99} & \textbf{69} &
- \textbf{320} & \textbf{S} & \textbf{0}\\
- $5$ & $119$ & $70$ & $40$ & $254$ & $A$ & $66$\\
- $6$ & $87$ & $38$ & $194$ & $68$ & $C$ & $186$\\
- $7$ & $50$ & $67$ & $157$ & $2$ & $B$ & $66$\\
- $8$ & $29$ & $46$ & $136$ & $320$ & $S$ & $0$\\
- $9$ & $120$ & $17$ & $107$ & $200$ & $A$ & $120$\\
- $10$ & $103$ & $120$ & $90$ & $80$ & $B$ & $120$\\
- \textbf{11} & \textbf{82} & \textbf{99} & \textbf{69} &
- \textbf{320} & \textbf{S} & \textbf{0}\\
- \bottomrule
- \end{tabular}
- \caption{Solution for problem $3b$}\label{tbl:s3b}
- \end{table}
+ Since $(c)$ is also true the solution in Table~\ref{tbl:s3c} is also
+ correct for a truck with size $320$.
\item \emph{Figure out whether it is possible if the capacity of the truck
is set to $318$.}
-
+ When we incrementally increase the number of iterations we see that
+ when we have more then $10$ iterations we encounter a cycle. Changing
+ $t_{\max}=318$ and keeping the rest the same as in $b$ we find also
+ cycle after $11$ iterations as shown in Table~\ref{tbl:s3c}
\end{enumerate}
+\begin{table}[h]
+ \centering
+ \begin{tabular}{lrrrrcr}
+ \toprule
+ $I$ & $A$ & $B$ & $C$ & Truck & Location & Dump\\
+ \midrule
+ $0$ & $40$ & $30$ & $145$ & $318$ & $0$ & $0$\\
+ $1$ & $19$ & $35$ & $124$ & $292$ & $2$ & $26$\\
+ $2$ & $120$ & $18$ & $107$ & $174$ & $1$ & $118$\\
+ $3$ & $103$ & $120$ & $90$ & $55$ & $2$ & $119$\\
+ \textbf{4} & \textbf{82} & \textbf{99} &
+ \textbf{69} & \textbf{318} & \textbf{0} & \textbf{0}\\
+ $5$ & $119$ & $70$ & $40$ & $252$ & $1$ & $66$\\
+ $6$ & $87$ & $38$ & $194$ & $66$ & $3$ & $186$\\
+ $7$ & $50$ & $67$ & $157$ & $0$ & $2$ & $66$\\
+ $8$ & $29$ & $46$ & $136$ & $318$ & $0$ & $0$\\
+ $9$ & $120$ & $17$ & $107$ & $198$ & $1$ & $120$\\
+ $10$ & $103$ & $120$ & $90$ & $78$ & $2$ & $120$\\
+ \textbf{11} & \textbf{82} & \textbf{99} &
+ \textbf{69} & \textbf{318} & \textbf{0} & \textbf{0}\\
+ \bottomrule
+ \end{tabular}
+ \caption{Solution for problem $3b$ and $3c$}\label{tbl:s3c}
+\end{table}
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}
As found by \textsc{prover9} a proof for $inv(inv(x))=x$.
\begin{lstlisting}
-1 inv(inv(x)) = x. [goal].
-2 x * (y * z) = (x * y) * z.[assumption].
-3 (x * y) * z = x * (y * z).[copy(2),flip(a)].
-4 x * I = x. [assumption]
-5 x * inv(x) = I. [assumption].
-6 inv(inv(c1)) != c1. [deny(1)].
-7 x * (I * y) = x * y. [para(4(a,1),3(a,1,1)),flip(a)].
-8 x * (inv(x) * y) = I * y. [para(5(a,1),3(a,1,1)),flip(a)].
-13 I * inv(inv(x)) = x. [para(5(a,1),8(a,1,2)),rewrite([4(2)]),flip(a)].
-15 x * inv(inv(y)) = x * y. [para(13(a,1),3(a,2,2)),rewrite([4(2)])].
-16 I * x = x. [para(13(a,1),7(a,2)),rewrite([15(5),7(4)])].
19 x * (inv(x) * y) = y. [back_rewrite(8),rewrite([16(5)])].
22 inv(inv(x)) = x. [para(5(a,1),19(a,1,2)),rewrite([4(2)]),flip(a)].
23 \$F. [resolve(22,a,6,a)].
As found by \textsc{prover9} a proof for $x*inv(x)=I$.
\begin{lstlisting}
-1 inv(x) * x = I. [goal].
-2 x * (y * z) = (x * y) * z.[assumption].
-3 (x * y) * z = x * (y * z).[copy(2),flip(a)].
-4 x * I = x. [assumption].
-5 x * inv(x) = I. [assumption].
-6 inv(c1) * c1 != I. [deny(1)].
-7 x * (I * y) = x * y. [para(4(a,1),3(a,1,1)),flip(a)].
-8 x * (inv(x) * y) = I * y. [para(5(a,1),3(a,1,1)),flip(a)].
-13 I * inv(inv(x)) = x. [para(5(a,1),8(a,1,2)),rewrite([4(2)]),flip(a)].
-15 x * inv(inv(y)) = x * y. [para(13(a,1),3(a,2,2)),rewrite([4(2)])].
-16 I * x = x. [para(13(a,1),7(a,2)),rewrite([15(5),7(4)])].
-19 x * (inv(x) * y) = y. [back_rewrite(8),rewrite([16(5)])].
-22 inv(inv(x)) = x. [para(5(a,1),19(a,1,2)),rewrite([4(2)]),flip(a)].
24 inv(x) * x = I. [para(22(a,1),5(a,1,2))].
25 \$F. [resolve(24,a,6,a)].
\end{lstlisting}
\textsc{prover9} fails to find a proof for $x*y=y*x$.
- Running the same file with \textsc{mace4} gives the following
+ Running the same file with \textsc{mace4} gives the smallest
counterexample listed in Table~\ref{tab:s3a}.
\begin{table}[H]
& 5 & 5 & 3 & 4 & 1 & 2 & 0
\end{array}\right.$
\end{tabular}
- \caption{Solution for problem 3a}\label{tab:s3a}
+ \caption{Smallest counterexample for problem 3a}\label{tab:s3a}
\end{table}
+ \newpage
\item\emph{A term rewrite system consists of the single rule
$$a(x,a(y,a(z,u)))\rightarrow a(y,a(z,a(x,u))),$$
in which $a$ is a binary symbol and $x,y,z,u$ are variables.
When inspecting the rewrite rule more closely we see that the
entire structure of the formula stays the same and that only
- the variables $x,y,z$ are changed in order. Because of this we
- can simplify the rule to
- $$x,y,z\rightarrow y,z,x$$
- and we can simplify the question to asking whether
- $b,c,d,e,f,b$ rewrites to $b,d,c,e,f,b$.\\
+ the variables $x,y,z$ are changed in order. Thus we can simplify the
+ rule and question to
+ $$x,y,z\rightarrow y,z,x\text{ and }
+ b,c,d,e,f,b\overset{*?}{\rightarrow}b,d,c,e,f,b$$
- Because of this the nature of the rewritten problem becomes
- solvable by a symbolic model checker. We define for every
- position $i\in\{0\ldots5\}$ a variable $p_i$ of the enumeration
- type $\{b,c,d,e,f\}$. To keep track of the moves we define a
- move $m\in\{0\ldots4\}$ variable that indicates the location of
- the first variable or $0$ for the initial value. The initial
- values of the position variables is
- $$p_0=b,p_1=c,p_2=d,p_3=e,p_4=f,p_5=b$$
- There are four possible transitions and they are put in a
- disjunction and shown below:
- $$\begin{array}{rl}
- next(m)=1 \wedge & next(p_0)=p_1 \wedge next(p_1)=p_2
+ Applying these changes changes the problem into a model checking
+ problem. For every position $i\in\{0\ldots5\}$ a variable $p_i$ of the
+ enumeration type $\{b,c,d,e,f\}$ is defined. To keep track of the moves
+ a move $m\in\{0\ldots4\}$ variable that indicates the location of the
+ first variable or $0$ for the initial value is defined. The initial
+ values of the position variables are
+ $$p_0=b\wedge p_1=c\wedge p_2=d\wedge p_3=e\wedge p_4=f\wedge p_5=b
+ \wedge m=0$$
+ There are four possible transitions as shown below.
+ $$\begin{array}{rrl}
+ & (next(m)=1 \wedge & next(p_0)=p_1 \wedge next(p_1)=p_2
\wedge next(p_2)=p_0 \wedge\\
- & next(p_3)=p_3 \wedge next(p_4)=p_4 \wedge next(p_5)=p_5\\
-
- next(m)=2 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_2
+ & & next(p_3)=p_3 \wedge next(p_4)=p_4 \wedge next(p_5)=p_5)\\
+ \vee & (next(m)=2 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_2
\wedge next(p_2)=p_3 \wedge\\
- & next(p_3)=p_1 \wedge next(p_4)=p_4 \wedge next(p_5)=p_5\\
-
- next(m)=3 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_1
+ & & next(p_3)=p_1 \wedge next(p_4)=p_4 \wedge next(p_5)=p_5)\\
+ \vee & (next(m)=3 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_1
\wedge next(p_2)=p_3 \wedge\\
- & next(p_3)=p_4 \wedge next(p_4)=p_2 \wedge next(p_5)=p_5\\
- next(m)=4 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_1
+ & & next(p_3)=p_4 \wedge next(p_4)=p_2 \wedge next(p_5)=p_5)\\
+ \vee & (next(m)=4 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_1
\wedge next(p_2)=p_2 \wedge\\
- & next(p_3)=p_4 \wedge next(p_4)=p_5 \wedge next(p_5)=p_3
+ & & next(p_3)=p_4 \wedge next(p_4)=p_5 \wedge next(p_5)=p_3)
\end{array}$$
- The LTL logic goal state would then be
+ With the following goal the solution below is
+ found by \textsc{NuSMV} within $0.01$ seconds.
$$\mathcal{G} \neg(p_0=b\wedge p_1=d\wedge p_2=c\wedge
p_3=e\wedge p_4=f\wedge p_5=b)$$
-
- The solution described below is found by
- \textsc{NuSMV} within $0.01$ seconds. Lined over triples are the
- ones changed in the next.
$$\begin{array}{rl}
\overline{b,c,d},e,f,b
& \rightarrow c,d,\overline{b,e,f},b\\
\usepackage{a4wide}
\usepackage{amsmath}
+\usepackage{array}
\usepackage{booktabs}
\usepackage{enumerate}
\usepackage{float}
)
GEN
done
-# echo "(or"
-# for i in $(seq 0 $ITERATIONS); do
-# for j in $(seq $((i+1)) $ITERATIONS); do
-# echo "(and (= t$i t$j) (= l$i l$j) (= a$i a$j) (= b$i b$j) (= c$i c$j))"
-# done
-# done
-# echo ")"
+ echo "(or"
+ for i in $(seq 0 $ITERATIONS); do
+ for j in $(seq $((i+1)) $ITERATIONS); do
+ echo "(and (= t$i t$j) (= l$i l$j) (= a$i a$j) (= b$i b$j) (= c$i c$j))"
+ done
+ done
+ echo ")"
echo "))"
}
it=1
-while generate $it 318 | $YICES | pee sort "grep -q \"^sat\""
+while generate $it 318 | $YICES -m | pee sort "grep -q \"^unsat\""
do
echo $((it++))
done
repositories / ar1516.git / commitdiff