formal description done'

diff --git a/report1/mart.tex b/report1/mart.tex
index ee1d9b5..b0eae6a 100644 (file)
--- 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 (file)
--- 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 (file)
--- 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}