diff --git a/util/Grid.cpp b/util/Grid.cpp
index d276c7b..0c9db49 100644
--- a/util/Grid.cpp
+++ b/util/Grid.cpp
@@ -181,12 +181,11 @@ void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configurat
   }
   if(agentNameAndPositionMap.size() > 1) formulas.printCollisionFormula(agentName);
   formulas.printInitStruct();
+  os << "const int WIDTH = " << maxBoundaries.first << ";\n";
+  os << "const int HEIGHT = " << maxBoundaries.second << ";\n";
 
   modules.print();
 
-
-
-
   //if(!stateRewards.empty()) {
   //  modules.printRewards(os, agentName, stateRewards, lava, goals, backgroundTiles);
   //}
diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp
index a2855da..ffe8a7b 100644
--- a/util/PrismModulesPrinter.cpp
+++ b/util/PrismModulesPrinter.cpp
@@ -5,10 +5,10 @@
 #include <stdexcept>
 
 
-std::string northUpdate(const AgentName &a) { return "(row"+a+"'=row"+a+"-1)"; }
-std::string southUpdate(const AgentName &a) { return "(row"+a+"'=row"+a+"+1)"; }
-std::string eastUpdate(const AgentName &a)  { return "(col"+a+"'=col"+a+"+1)"; }
-std::string westUpdate(const AgentName &a)  { return "(col"+a+"'=col"+a+"-1)"; }
+std::string northUpdate(const AgentName &a) { return "min(WIDTH, max(1, row"+a+"'=row"+a+"-1))"; }
+std::string southUpdate(const AgentName &a) { return "min(WIDTH, max(1, row"+a+"'=row"+a+"+1))"; }
+std::string eastUpdate(const AgentName &a)  { return "min(HEIGHT, max(1, col"+a+"'=col"+a+"+1))"; }
+std::string westUpdate(const AgentName &a)  { return "min(HEIGHT, max(1, col"+a+"'=col"+a+"-1))"; }
 
 namespace prism {
 
@@ -250,7 +250,7 @@ namespace prism {
     if(slipperyBehaviour())      guard += " & !" + a + "IsOnSlippery";
     if(anyLava)                  guard += " & !" + a + "IsOnLava";
     if(anyGoals && a == "Agent") guard += " & !" + a + "IsOnGoal";
-    guard += " & !" + a + "CannotMove" + direction + "Wall";
+    //guard += " & !" + a + "CannotMove" + direction + "Wall";
     if(anyPortableObject() || !lockedDoors.empty() || !unlockedDoors.empty()) guard += " & !" + a + "CannotMoveConditionally";
     guard += " -> ";
     return guard;