Merge branch 'master' of github.com:dopefishh/mc1516pa
[mc1516pa.git] / report1 / mart.tex
index ee1d9b5..b0eae6a 100644 (file)
@@ -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$$