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,
-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$$
 
-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 
@@ -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
-$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

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}
 
-All transitions together in a disjuction would specify all possible
+All transitions together in a disjunction would specify all possible
 transitions.
 
 \newpage