From 9fd7969c5c531b48524de182ecb5919e68d51257 Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Sun, 13 Mar 2016 15:21:11 +0100
Subject: [PATCH] formal description done'

---
 report1/mart.tex    | 2 +-
 report1/pre.tex     | 4 ++--
 report1/report1.tex | 6 ++++++
 3 files changed, 9 insertions(+), 3 deletions(-)

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}
-- 
2.20.1