From: Mart Lubbers Date: Sun, 3 Jan 2016 17:55:05 +0000 (+0100) Subject: update spellcheck X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=b0382cc788bf958e7482ee188f78d172b624ffed;p=ar1516.git update spellcheck --- diff --git a/.gitignore b/.gitignore index 52dfa5e..1237fdb 100644 --- a/.gitignore +++ b/.gitignore @@ -6,4 +6,4 @@ *.toc *.pdf *.png -a[1234].tex +*.xyc diff --git a/a2/1.tex b/a2/1.tex index 8aeb788..324e7d8 100644 --- a/a2/1.tex +++ b/a2/1.tex @@ -41,7 +41,7 @@ formula called $trans$. We introduce a function $conn(s)$ that returns the set of all cities connected to city $s$. $(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. Subformula $(4)$ deals with the fact that if 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. @@ -61,7 +61,7 @@ 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)$$ -\begin{enumerate}[a.] +\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.} @@ -69,7 +69,7 @@ $$const\wedge initial\wedge state where a city is without food. Therefore we try to find proof that the truck is actually capable of keeping all cities saturated. - To show this we need to prove that there is a state in the statespace + To show this we need to prove that there is a state in the state space that is exactly the same as some previous state. To do this we add the following formula to the conjunction. $$\bigvee_{i\in I}\bigvee_{j\in \{0\ldots i-1\}}\left( @@ -107,10 +107,10 @@ $$const\wedge initial\wedge 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.)} - Solution idem to $a.$. Just imagine the truck operator glueing $20$ + Solution idem to $(a)$. Just imagine the truck operator glueing $20$ food packages to the truck which he can not deliver. \item \emph{Figure out whether it is possible if the capacity of the truck is set to $318$.} - Solution idem to $a.$. Just imagine the truck operator glueing $18$ + Solution idem to $(a)$. Just imagine the truck operator glueing $18$ food packages to the truck which he can not deliver. \end{enumerate} diff --git a/a2/2.tex b/a2/2.tex index 174dfd6..0c51035 100644 --- a/a2/2.tex +++ b/a2/2.tex @@ -12,7 +12,7 @@ times: \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 +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 @@ -20,10 +20,10 @@ 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:\\ + If we fill a bottle $b_i$ the contents 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:\\ + If we empty a bottle $b_i$ the contents 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$ @@ -38,7 +38,7 @@ 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.] +\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 @@ -123,6 +123,6 @@ joining them with logical or operators. $29$ & $8$ & $11$ & $28$ & Poured $2$ in $3$\\ \bottomrule \end{tabular} - \caption{Solution for problem 3}\label{tab:sol2c} + \caption{Solution for problem 2}\label{tab:sol2c} \end{table} \end{enumerate} diff --git a/a2/3.tex b/a2/3.tex index a7b1b60..20d8feb 100644 --- a/a2/3.tex +++ b/a2/3.tex @@ -1,10 +1,10 @@ \section{Problem 3} \emph{The goal of this problem is to exploit the power of the recommended tools rather than elaborating the questions by hand.} -\begin{enumerate}[a.] +\begin{enumerate}[(a)] \item\emph{In mathematics, a \emph{group} is defined to be a set $G$ with an element $I\in G$, a binary operator $∗$ and a unary - operator inv satisfying. + operator $inv$ satisfying. $$x*(y*z)=(x*y)*z, x*I=x\text{ and }x*inv(x)=I,$$ for all $x,y,z\in G$. Determine whether in every group each of the four properties @@ -142,7 +142,7 @@ tools rather than elaborating the questions by hand.} p_3=e\wedge p_4=f\wedge p_5=b)$$ The solution described below is found by - \textsc{NuSMV} within $0.01$ seconds. Overlined triples are the + \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 diff --git a/a2/4.model b/a2/4.model deleted file mode 100644 index e69de29..0000000 diff --git a/a2/pre.tex b/a2/pre.tex index cd9af74..db9947a 100644 --- a/a2/pre.tex +++ b/a2/pre.tex @@ -1,12 +1,12 @@ \documentclass{article} -\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 -\usepackage{listings} % For nice tables -\usepackage{float} % For nice tables +\usepackage{hyperref} +\usepackage{a4wide} +\usepackage{booktabs} +\usepackage{enumerate} +\usepackage{amsmath} +\usepackage{listings} +\usepackage{float} \usepackage{graphicx} \usepackage{xypic} \usepackage{multirow} @@ -15,9 +15,8 @@ \lstset{keepspaces=true,captionpos=b,basicstyle=\scriptsize\ttfamily} -\CompileMatrices% - +\CompileMatrices \author{Mart Lubbers (s4109503)} -\title{Automated reasoning Assignment 2} +\title{Automated reasoning Assignment $2$} \date{\today}