*.toc
*.pdf
*.png
-a[1234].tex
+*.xyc
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.
$$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.}
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(
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}
\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
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$
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
$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}
\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
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
\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}
\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}
repositories / ar1516.git / commitdiff