spellcheck

diff --git a/a2/1.tex b/a2/1.tex
index 61dc95d..c9a7625 100644 (file)
--- a/a2/1.tex
+++ b/a2/1.tex
@@ -14,19 +14,19 @@ $C$ there are $40$, $30$ and $145$ food packages, respectively.}\\
 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,
 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}$.
+d_i$ are created respectively for the stock of city $A$, city $B$, city $C$,
+the truck, the trucks location and the amount of food dumped. A function
+$dist(x,y)$ that returns the distance between two cities is introduced. 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 $\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$$
 
 $$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 $\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 $\mathcal{CST}(i)$ and they are expressed as:
+In every iteration there are certain constraints that always have to hold and
+are called them $\mathcal{CST}(i)$ and expressed as:

 $$d_i>0\wedge 
 d_i\leq t_{\max}\wedge
 t_i\geq\wedge 
 $$d_i>0\wedge 
 d_i\leq t_{\max}\wedge
 t_i\geq\wedge 


@@ -35,8 +35,8 @@ t_i\leq t_{\max}\wedge
 
 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
 
 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
+$l_{i}$. The formula is called $\mathcal{TRA}$. A function $conn(s)$ is
+introduced 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
 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

diff --git a/a2/2.tex b/a2/2.tex
index f490d0d..aa88a8a 100644 (file)
--- a/a2/2.tex
+++ b/a2/2.tex
@@ -38,7 +38,7 @@ next state is not defined for a bottle $b_i$ we assume $next(b_i)=b_i$.
                $next(b_j)=b_j+\min(b_{j\max}-b_j, b_i)$
 \end{itemize}
 
                $next(b_j)=b_j+\min(b_{j\max}-b_j, b_i)$
 \end{itemize}
 

-All transitions together in a disjuction would specify all possible
+All transitions together in a disjunction would specify all possible

 transitions.
 
 \newpage
 transitions.
 
 \newpage