diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp
index a54233d..0ae965b 100644
--- a/util/PrismFormulaPrinter.cpp
+++ b/util/PrismFormulaPrinter.cpp
@@ -2,28 +2,84 @@
 
 #include <map>
 #include <string>
+#include <algorithm>
 
+std::string capitalize(std::string string) {
+  string[0] = std::toupper(string[0]);
+  return string;
+}
 
 std::string cellToConjunction(const AgentName &agentName, const cell &c) {
   return "x" + agentName + "=" + std::to_string(c.column) + "&y" + agentName + "=" + std::to_string(c.row);
 }
 
+std::string coordinatesToConjunction(const AgentName &agentName, const coordinates &c, const ViewDirection viewDirection) {
+  return "x" + agentName + "=" + std::to_string(c.first) + "&y" + agentName + "=" + std::to_string(c.second) + "&view" + agentName + "=" + std::to_string(viewDirection);
+}
+
+std::map<ViewDirection, coordinates> getSurroundingCells(const cell &c) {
+  return {{1, c.getNorth()}, {2, c.getEast()}, {3, c.getSouth()}, {0, c.getWest()}};
+}
+
 namespace prism {
-  PrismFormulaPrinter::PrismFormulaPrinter() {}
+  PrismFormulaPrinter::PrismFormulaPrinter(std::ostream &os, const AgentName &agentName, const std::map<std::string, cells> &restrictions, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys)
+    : os(os), agentName(agentName), restrictions(restrictions), boxes(boxes), balls(balls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys)
+  { }
+
+  void PrismFormulaPrinter::printFormulas() {
+    for(const auto& [direction, cells] : restrictions) {
+      printRestrictionFormula(direction, cells);
+    }
+
+    for(const auto& ball : balls) {
+      std::string color = capitalize(ball.getColor());
+      printRestrictionFormulaWithCondition(color + "Ball", getSurroundingCells(ball), "!" + color + "BallPickedUp");
+    }
+
+    for(const auto& box : boxes) {
+      std::string color = capitalize(box.getColor());
+      printRestrictionFormulaWithCondition(color + "Box", getSurroundingCells(box), "!" + color + "BoxPickedUp");
+    }
+
+    for(const auto& key : keys) {
+      std::string color = capitalize(key.getColor());
+      printRestrictionFormulaWithCondition(color + "Key", getSurroundingCells(key), "!" + color + "KeyPickedUp");
+    }
 
-  std::ostream& PrismFormulaPrinter::printRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &grid_cells) {
-    os << buildFormula(agentName + "CannotMove" + direction, buildDisjunction(agentName, grid_cells));
-    return os;
+    for(const auto& door : unlockedDoors) {
+      std::string color = capitalize(door.getColor());
+      printRestrictionFormulaWithCondition(color + "Door", getSurroundingCells(door), "!" + color + "DoorOpened");
+    }
+
+    for(const auto& door : lockedDoors) {
+      std::string color = capitalize(door.getColor());
+      printRestrictionFormulaWithCondition(color + "Door", getSurroundingCells(door), "!" + color + "DoorOpened");
+    }
   }
-  std::ostream& PrismFormulaPrinter::printRestrictionFormulaWithCondition(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &grid_cells, const std::vector<std::string> conditions) {
-    os << buildFormula(agentName + "Something", buildDisjunction(agentName, grid_cells, conditions));
-    return os;
+
+  void PrismFormulaPrinter::printRestrictionFormula(const std::string &direction, const cells &grid_cells) {
+    os << buildFormula(agentName + "CannotMove" + direction + "Wall", buildDisjunction(agentName, grid_cells));
+  }
+
+  void PrismFormulaPrinter::printRestrictionFormulaWithCondition(const std::string &reason, const std::map<ViewDirection, coordinates> &coordinates, const std::string &condition) {
+    os << buildFormula(agentName + "CannotMove" + reason, "(" + buildDisjunction(agentName, coordinates) + ") & " + condition);
   }
 
   std::string PrismFormulaPrinter::buildFormula(const std::string &formulaName, const std::string &formula) {
     return "formula " + formulaName + " = " + formula + ";\n";
   }
 
+  std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const std::map<ViewDirection, coordinates> &cells) {
+    bool first = true;
+    std::string disjunction = "";
+    for(const auto [viewDirection, coordinates] : cells) {
+      if(first) first = false;
+      else disjunction += " | ";
+      disjunction += "(" + coordinatesToConjunction(agentName, coordinates, viewDirection) + ")";
+    }
+    return disjunction;
+  }
+
   std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const cells &cells, const std::vector<std::string> &conditions) {
     bool first = true;
     std::string disjunction = "";
diff --git a/util/PrismFormulaPrinter.h b/util/PrismFormulaPrinter.h
index a9b5df4..73ecc19 100644
--- a/util/PrismFormulaPrinter.h
+++ b/util/PrismFormulaPrinter.h
@@ -6,16 +6,34 @@
 #include "PrismPrinter.h"
 #include "ConfigYaml.h"
 
+
+std::string cellToConjunction(const AgentName &agentName, const cell &c);
+std::string coordinatesToConjunction(const AgentName &agentName, const coordinates &c, const ViewDirection viewDirection);
+std::map<ViewDirection, coordinates> getSurroundingCells(const cell &c);
+
 namespace prism {
   class PrismFormulaPrinter {
     public:
-      PrismFormulaPrinter();
+      PrismFormulaPrinter(std::ostream &os, const AgentName &agentName, const std::map<std::string, cells> &restrictions, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys);
+
+      void printFormulas();
 
-      std::ostream& printRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &grid_cells);
-      std::ostream& printRestrictionFormulaWithCondition(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &grid_cells, const std::vector<std::string> conditions);
+      void printRestrictionFormula(const std::string &direction, const cells &grid_cells);
+      void printRestrictionFormulaWithCondition(const std::string &reason, const std::map<ViewDirection, coordinates> &coordinates, const std::string &condition);
     private:
       std::string buildFormula(const std::string &formulaName, const std::string &formula);
       std::string buildLabel(const std::string &labelName, const std::string &label);
+      std::string buildDisjunction(const AgentName &agentName, const std::map<ViewDirection, coordinates> &cells);
       std::string buildDisjunction(const AgentName &agentName, const cells &cells, const std::vector<std::string> &conditions = {});
+
+      std::ostream &os;
+      AgentName agentName;
+      std::map<std::string, cells> restrictions;
+      cells boxes;
+      cells balls;
+      cells lockedDoors;
+      cells unlockedDoors;
+      cells keys;
+
   };
 }
diff --git a/util/PrismPrinter.h b/util/PrismPrinter.h
index 55f4ada..a120803 100644
--- a/util/PrismPrinter.h
+++ b/util/PrismPrinter.h
@@ -5,10 +5,12 @@
 #include "cell.h"
 
 typedef std::string AgentName;
+typedef size_t ViewDirection;
 typedef std::pair<std::string, coordinates> AgentNameAndPosition;
 typedef AgentNameAndPosition KeyNameAndPosition;
 typedef std::map<AgentNameAndPosition::first_type, AgentNameAndPosition::second_type> AgentNameAndPositionMap;
 typedef std::map<KeyNameAndPosition::first_type, KeyNameAndPosition::second_type> KeyNameAndPositionMap;
+typedef std::pair<cell, std::string> CellAndCondition;
 
 namespace prism {
   enum class ModelType {