From: Mart Lubbers <mart@martlubbers.net>
Date: Sun, 13 Mar 2016 14:21:11 +0000 (+0100)
Subject: formal description done'
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=9fd7969c5c531b48524de182ecb5919e68d51257;hp=-c;p=mc1516pa.git

formal description done'
---

9fd7969c5c531b48524de182ecb5919e68d51257
diff --git a/report1/mart.tex b/report1/mart.tex
index ee1d9b5..b0eae6a 100644
--- a/report1/mart.tex
+++ b/report1/mart.tex
@@ -56,7 +56,7 @@ $$
 When the goal state is reached the $movement$ variable should be set to
 $finished$ to be able to specify the CTL specification more easily. Via the
 following invariant the goal state is tied to the $movement$ variable:
-$$\left(\bigvee_{B`\in perm(B)}
+$$\left(\bigvee_{B`\in perms(B)}
 	\bigwedge_{b\in B`, i\in 0\ldots k}\left(
 		b_x=t^i_x \wedge b_y=t^i_y
 \right)\right)\leftrightarrow movement=finished$$
diff --git a/report1/pre.tex b/report1/pre.tex
index 09bb5f2..81e71df 100644
--- a/report1/pre.tex
+++ b/report1/pre.tex
@@ -10,6 +10,6 @@
 	basicstyle=\scriptsize
 }
 
-\title{Solving Sokoban with NuSMV}
-\author{Alexander Fedotov(s4460952)\and Mart Lubbers(s4109503)}
+\title{Solving Sokoban with \textsc{NuSMV}}
+\author{Alexander Fedotov (s4460952)\and Mart Lubbers (s4109503)}
 \date{\today}
diff --git a/report1/report1.tex b/report1/report1.tex
index c212acd..0898bc2 100644
--- a/report1/report1.tex
+++ b/report1/report1.tex
@@ -1,5 +1,11 @@
 %&report1
 \begin{document}
+\maketitle
+\section{Introduction}
+
+%Object centered approach
 \input{mart.tex}
+
+%Coordinate centered approach
 \input{alex.tex}
 \end{document}