From: Mart Lubbers <mart@martlubbers.net>
Date: Tue, 15 Dec 2015 11:23:03 +0000 (+0100)
Subject: some update'
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=374290fcbb281a1ef12f5d556bdadc74f50127be;p=ar1516.git

some update'
---

diff --git a/a2/1.tex b/a2/1.tex
index e69de29..b294ecc 100644
--- a/a2/1.tex
+++ b/a2/1.tex
@@ -0,0 +1,65 @@
+\section{Problem 1}
+{\em Three non-self-supporting villages $A$, $B$ and $C$ in the middle of
+nowhere consume one food package each per time unit. The required food packages
+are delivered by a truck, having a capacity of $300$ food packages. The
+locations of the villages are given in the following picture, in which the
+numbers indicate the distance, more precisely, the number of time units the
+truck needs to travel from one village to another, including loading or
+delivering. The truck has to pick up its food packages at location $S$
+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.}
+
+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$ a variable
+is defined that states the maximum capacity. 
+$$a_{max}=120\wedge b_{max}=120\wedge c_{max}=200$$
+Iteration $0$ depicts the initial state and can be described with a simple
+conjuction:
+$$a_0=40\wedge b_0=30\wedge c_0=145\wedge t_0=300\wedge l_0=S\wedge d_0=0$$.
+
+After that all iteration can be formalized as
+\begin{align}
+	\bigwedge_{i\in I} \Bigg(
+	% Bent in S
+		& \Bigg[l_i=S\wedge d_i=0\wedge t_i=300\wedge
+		\bigvee_{k\in\{A,B\}}\bigg(l_{i-1}=k\wedge
+		\bigwedge_{s\in\{A,B,C\}}s_i=s_{i-1}-dist(S, k)\bigg)\Bigg]\vee\\
+	% Bent in A,B,C
+		& \bigvee_{k\in\{a,b,c\}}
+			\Bigg[l_i=k\wedge d_i>0\wedge d_i<t_{i-1}\wedge d_i<k_{max}-k_{i-1}
+			t_i=t_i-d_i\wedge k_i=k_i+d_i\wedge\\
+		& \qquad\qquad\bigwedge_{k'\in\{k\}\setminus\{S,A,B,C\}}\bigg(
+		l_{i-1}=k'\wedge
+		\bigwedge_{s\in\{k\}\setminus\{A,B,C\}}
+			s_i=s_{i-1}-dist(k, s)\bigg)\Bigg]\\
+	\nonumber\Bigg)
+\end{align}
+
+\begin{enumerate}
+	\item This part of the formula describes what happens if the truck is in
+		$S$. This is a special case of the generalized case dsecribed in $2$
+		and $3$. The truck always gets a refill in $S$ and no food is dumped.
+		The truck could either have come from $A$ or $B$ and thus the food
+		stocks of $A,B$ and $C$ will drop accordingly.
+	\item
+\end{enumerate}
+
+\begin{enumerate}[a.]
+	\item {\em 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.}
+	\item {\em 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
+		from $v$ to a node $w$ for which there is a non-empty path from $w$ to
+		itself.)}
+	\item {\em Figure out whether it is possible if the capacity of the truck
+		is set to $318$.}
+\end{enumerate}
diff --git a/a2/2.tex b/a2/2.tex
index da2bafd..11b7eb8 100644
--- a/a2/2.tex
+++ b/a2/2.tex
@@ -91,7 +91,7 @@ joining them with logical or operators.
 				\toprule
 				State & Bottle 1 & Bottle 2 & Bottle 3 & Action\\
 				\midrule
-				$0$ & $3$ & $0$ & $0$ &\\
+				$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$\\
diff --git a/a2/src/1.bash b/a2/src/1.bash
index bcb1892..f9ed186 100755
--- a/a2/src/1.bash
+++ b/a2/src/1.bash
@@ -20,38 +20,63 @@ function generate {
 :extrafuns (
 GEN
 	for i in $(seq 0 $STATES); do
-		echo "(a$i Int) (b$i Int) (c$i Int) (t$i Int) (l$i Int)"
+		echo "(a$i Int) (b$i Int) (c$i Int) (t$i Int) (l$i Int) ) (d$i Int)"
 	done
 	cat <<GEN
 )
 :formula
 (and
-	(and (= a0 $AINIT) (= b0 $BINIT) (= c0 $CINIT) (= t0 $TINIT) (= l0 0))
+	(and 
+		(= a0 $AINIT)
+		(= b0 $BINIT)
+		(= c0 $CINIT)
+		(= t0 $TINIT)
+		(= l0 0) 
+		(= d0 0)
+	)
 GEN
 	for i in $(seq $STATES); do
 		j=$((i-1))
-		echo $i $j
+		echo "State: $i, prev: $j"
 		echo "(or"
-
+#
 		#Truck is in S
-		echo "(and"
-		echo "(= l$j 0)"
-		echo "(> dump
-		echo ")"
-		#Truck is in A
-		echo "(and"
-		echo "(= l$j 0)"
-		echo ")"
-		#Truck is in B
-		echo "(and"
-		echo "(= l$j 0)"
-		echo ")"
-		#Truck is in C
-		echo "(and"
-		echo "(= l$j 0)"
-		echo ")"
-
-		echo ")"
+		cat<<GEN
+	(or
+; Truck is in S
+		(and
+			(= l$j 0)
+			(or
+		; Truck can go to B
+				(and
+					(= l$i 2)
+					(and
+						(> d$i 0)
+						(<= d$i t$j)
+						(<= d$i (- $AMAX a$j))
+					)
+					(= a$j (
+					(= b$i (- b$j 29))
+					(= c$i (- b$j 29))
+				)
+		; Truck can go to A
+				(= l$i 1)
+				)
+			)
+; Truck is in A
+		(and
+			(= l$j 1)
+		)
+; Truck is in B
+		(and
+			(= l$j 2)
+		)
+; Truck is in C
+		(and
+			(= l$j 3)
+		)
+	)
+GEN
 	done	
 	echo "))"
 }
diff --git a/a2/src/path.sh b/a2/src/path.sh
index abe4d9a..0226b8c 100644
--- a/a2/src/path.sh
+++ b/a2/src/path.sh
@@ -1,3 +1 @@
-export PATH=$PATH:/home/mart/downloads/NuSMV-2.6.0-Linux/bin
-export PATH=$PATH:/home/mart/projects/NuSMV-2.6.0-Linux/bin
-export PATH=$PATH:/home/mart/projects/LADR-2009-11A/bin
+export PATH=$PATH:~/downloads/yices-2.4.2/bin
diff --git a/description b/description
deleted file mode 100644
index 24b4e26..0000000
--- a/description
+++ /dev/null
@@ -1 +0,0 @@
-2015-S1 - NWI-IMC009: Automated Reasoning