diff --git a/util/Grid.cpp b/util/Grid.cpp
index a429c80..e47ea2f 100644
--- a/util/Grid.cpp
+++ b/util/Grid.cpp
@@ -37,13 +37,7 @@ Grid::Grid(cells gridCells, cells background, const GridOptions &gridOptions, co
   std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(goals), [](cell c) {
       return c.type == Type::Goal;
   });
-  std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(keys), [this](cell c) {
-      for (auto const& key : keys) {
-        if (key.color == c.color && key.type == c.type) {
-          throw std::logic_error("Multiple keys with same color not supported " + key.getColor() + "\n");
-        }
-      }
-
+  std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(keys), [this](cell c) {    
       return c.type == Type::Key;
   });
   std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(boxes), [](cell c) {
@@ -70,6 +64,18 @@ Grid::Grid(cells gridCells, cells background, const GridOptions &gridOptions, co
       throw;
     }
   }
+  for(auto const& key : keys) {
+    std::string color = key.getColor();
+    try {
+      auto success = keyNameAndPositionMap.insert({color, key.getCoordinates() });
+      if (!success.second) {
+        throw std::logic_error("Multiple keys with same color not supported " + color + "\n");
+      }
+    } catch(const std::logic_error& e) {
+      std::cerr << "Expected key colors to be different. Key with color : '" << color << "' already present." << std::endl;
+      throw;
+    }
+  }
   for(auto const& color : allColors) {
     cells cellsOfColor;
     std::copy_if(background.begin(), background.end(), std::back_inserter(cellsOfColor), [&color](cell c) {
@@ -233,13 +239,16 @@ void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configurat
     printer.printCrashLabel(os, agentNames);
   }
   size_t agentIndex  = 0;
+
+  printer.printInitStruct(os, agentNameAndPositionMap, keyNameAndPositionMap, lockedDoors, unlockedDoors);
+
+
   for(auto agentNameAndPosition = agentNameAndPositionMap.begin(); agentNameAndPosition != agentNameAndPositionMap.end(); ++agentNameAndPosition, agentIndex++) {
     AgentName agentName = agentNameAndPosition->first;
     //std::cout << "Agent Name: " << agentName << std::endl;
     bool agentWithView = std::find(gridOptions.agentsWithView.begin(), gridOptions.agentsWithView.end(), agentName) != gridOptions.agentsWithView.end();
     bool agentWithProbabilisticBehaviour = std::find(gridOptions.agentsWithProbabilisticBehaviour.begin(), gridOptions.agentsWithProbabilisticBehaviour.end(), agentName) != gridOptions.agentsWithProbabilisticBehaviour.end();
-    std::set<std::string> slipperyActions;
-  printer.printInitStruct(os, agentName, keys, lockedDoors, unlockedDoors);
+    std::set<std::string> slipperyActions; // TODO AGENT POSITION INITIALIZATIN
     if(agentWithProbabilisticBehaviour) printer.printModule(os, agentName, agentIndex, maxBoundaries, agentNameAndPosition->second, keys, backgroundTiles, agentWithView, gridOptions.probabilitiesForActions);
     else                                printer.printModule(os, agentName, agentIndex, maxBoundaries, agentNameAndPosition->second, keys, backgroundTiles, agentWithView);
     for(auto const& c : slipperyNorth) {
@@ -270,9 +279,10 @@ void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configurat
     printer.printRewards(os, agentName, stateRewards, lava, goals, backgroundTiles);
     //}
 
-    if (!configuration.empty()) {
-      printer.printConfiguration(os, configuration);
-    }
+  }
+
+  if (!configuration.empty()) {
+    printer.printConfiguration(os, configuration);
   }
   // TODO CHANGE HANDLING
   std::string agentName = agentNames.at(0);
diff --git a/util/Grid.h b/util/Grid.h
index a7c5667..c869945 100644
--- a/util/Grid.h
+++ b/util/Grid.h
@@ -46,6 +46,7 @@ class Grid {
     cell agent;
     cells adversaries;
     AgentNameAndPositionMap agentNameAndPositionMap;
+    KeyNameAndPositionMap keyNameAndPositionMap;
 
     cells walls;
     cells floor;
diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp
index ef510ff..4688b59 100644
--- a/util/PrismModulesPrinter.cpp
+++ b/util/PrismModulesPrinter.cpp
@@ -38,16 +38,22 @@ namespace prism {
     return os;
   }
 
-  std::ostream& PrismModulesPrinter::printRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction,  const cells &cells) {
+  std::ostream& PrismModulesPrinter::printRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction,  const cells &grid_cells, const cells &keys, const cells &doors) {
     bool first = true;
     os << "formula " << agentName << "CannotMove" << direction << " = " ;
-    for(auto const& cell : cells) {
+    for(auto const& cell : grid_cells) {
       if(first) first = false;
       else os << " | ";
       os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
     }
-    os << " | " << agentName << "CannotMove" << direction << "BecauseOfKey";
-    os << " | " << agentName << "CannotMove" << direction << "BecauseOfDoor";
+
+    if (!keys.empty()) {
+      os << " | " << agentName << "CannotMove" << direction << "BecauseOfKey";  
+    }
+    if (!doors.empty()) {
+      os << " | " << agentName << "CannotMove" << direction << "BecauseOfDoor";
+    }
+  
     os << ";\n";
     return os;
   }
@@ -205,7 +211,7 @@ namespace prism {
     os << "formula " << agentName << "SlipperyTurnLeftAllowed = true;\n";
     os << "formula " << agentName << "SlipperyTurnRightAllowed = true;\n";
     os << "formula " << agentName << "SlipperyMoveForwardAllowed = true;\n";
-    os << "label \"FixedStates\" = " << agentName << "IsFixed | !" << agentName << "SlipperyTurnRightAllowed | !" << agentName << "SlipperyTurnLeftAllowed | !" << agentName << "SlipperyMoveForwardAllowed | " << agentName << "IsInGoal | " << agentName << "IsInLava";
+    os << "label \"FixedStates" << agentName << "\" = " << agentName << "IsFixed | !" << agentName << "SlipperyTurnRightAllowed | !" << agentName << "SlipperyTurnLeftAllowed | !" << agentName << "SlipperyMoveForwardAllowed | " << agentName << "IsInGoal | " << agentName << "IsInLava";
     if(enforceOneWays) {
       os << " | " << agentName << "CannotTurn";
     }
@@ -243,10 +249,10 @@ namespace prism {
                               const cells &slipperyWest,
                               const cells &keys,
                               const cells &doors) {
-    printRestrictionFormula(os, agentName, "North", restrictionNorth);
-    printRestrictionFormula(os, agentName, "East", restrictionEast);
-    printRestrictionFormula(os, agentName, "South", restrictionSouth);
-    printRestrictionFormula(os, agentName, "West", restrictionWest);
+    printRestrictionFormula(os, agentName, "North", restrictionNorth, keys, doors);
+    printRestrictionFormula(os, agentName, "East", restrictionEast, keys, doors);
+    printRestrictionFormula(os, agentName, "South", restrictionSouth, keys, doors);
+    printRestrictionFormula(os, agentName, "West", restrictionWest, keys, doors);
     
     if (!keys.empty()) {
       printKeyRestrictionFormula(os, agentName, "North", keys);
@@ -373,7 +379,7 @@ namespace prism {
       os << "\n";
       std::string keyColor = key.getColor();
       os << "\t[pickup_" << keyColor << "_key]\t" << pickupGuard(agentName, keyColor) << "-> ";
-      os << "(" << agentName << "_has_" << keyColor << "_key'=true) & (" << agentName << "_is_carrying_object'=true) ;\n";
+      os << "(" << agentName << "_has_" << keyColor << "_key'=true) & (" << agentName << "_is_carrying_object'=true);\n";
       os << "\n";
      
       os << "\t[drop_" << keyColor << "_key_north]\t" << dropGuard(agentName, keyColor, 3) << "-> ";
@@ -412,19 +418,31 @@ namespace prism {
     return os;
   }
 
-  std::ostream& PrismModulesPrinter::printInitStruct(std::ostream &os, const AgentName &agentName, const cells &keys, const cells &lockedDoors, const cells &unlockedDoors) {
+  std::ostream& PrismModulesPrinter::printInitStruct(std::ostream &os, const AgentNameAndPositionMap &agents, const KeyNameAndPositionMap &keys, const cells &lockedDoors, const cells &unlockedDoors) {
     os << "init\n";
-    os << "\t(!AgentIsInGoal & !AgentIsInLava & !AgentDone & !AgentIsOnWall)";
-    if(enforceOneWays) {
-      os << " & ( !AgentCannotTurn ) ";
-    } else {
-      os << " & ( !AgentIsOnSlippery ) ";
-    }
+    os << "\t";
+    
+    bool first = true;
+    for (auto const& agent : agents) {
+      if (first) first = false;
+      else os << " & ";
+      os << "(!" << agent.first << "IsInGoal & !" << agent.first << "IsInLava & !" << agent.first << "Done & !" << agent.first << "IsOnWall & ";
+      os << "x" << agent.first << "=" << agent.second.second << " & y" << agent.first << "=" << agent.second.first << ")";
+      os << " & !" << agent.first << "_is_carrying_object";
+      if(enforceOneWays) {
+        os << " & ( !AgentCannotTurn ) ";
+      } else {
+        os << " & ( !AgentIsOnSlippery ) ";
+      }
 
+      for (auto const& key : keys) {
+         os << " & ( !" << agent.first << "_has_" << key.first << "_key )";
+      }
+    }
+    
     for (auto const& key : keys) {
-      os << " & ( !" << agentName << "_has_" << key.getColor() << "_key )";
-      os << " & ( xKey" << key.getColor() << "="<< key.column << ")";
-      os << " & ( yKey" << key.getColor() << "=" << key.row << ")";
+      os << " & ( xKey" << key.first << "="<< key.second.second<< ")";
+      os << " & ( yKey" << key.first << "=" << key.second.first << ")";
     }
 
     for (auto const& locked : lockedDoors) {
@@ -435,7 +453,7 @@ namespace prism {
       os << " & (!Door" << unlocked.getColor() << "locked & !Door" << unlocked.getColor() << "open)";
     }
 
-    os << " & ( !" << agentName << "_is_carrying_object" << ")";
+    // os << " & ( !" << agentName << "_is_carrying_object" << ")";
 
     os << "\nendinit\n\n";
 
@@ -487,8 +505,8 @@ namespace prism {
 
     os << "module " << keyIdentifier << "\n";
 
-    os << "\tx" << keyIdentifier << " : [1.." << boundaries.second  << "];\n";
-    os << "\ty" << keyIdentifier << " : [1.." << boundaries.first << "];\n";
+    os << "\tx" << keyIdentifier << " : [-1.." << boundaries.second  << "];\n";
+    os << "\ty" << keyIdentifier << " : [-1.." << boundaries.first << "];\n";
     os << "\n";
     printKeyActions(os, key ,keyIdentifier, agentName);
 
@@ -498,7 +516,10 @@ namespace prism {
   
   std::ostream& PrismModulesPrinter::printKeyActions(std::ostream &os, const cell &key ,const std::string &keyIdentifier, AgentName agentName) {
     std::string keyColor = key.getColor();
- 
+
+    os << "\t[pickup_" << keyColor << "key]\t" << pickupGuard(agentName, keyColor) << "-> ";
+    os <<  "(xKey" << keyColor << "'=-1) & (yKey" << keyColor << "'=-1)" << ";\n";
+
     os << "\t[drop_" << keyColor << "_key_north]\t" << dropGuard(agentName, keyColor, 3) << "-> ";
     os << "(xKey" << keyColor << "'=x" << agentName << ") & (yKey" << keyColor << "'=y" <<agentName << "-1) ;\n"; 
 
@@ -553,11 +574,11 @@ namespace prism {
   std::string PrismModulesPrinter::toggleGuard(const AgentName &agentName, const cell& door) {
     std::string doorColor = door.getColor();
     std::string ret;
-
+    ret += "!Door" + doorColor + "locked & (";
     ret +=  "(" + viewVariable(agentName, 0, true) + "x" + agentName + "+ 1 = " + std::to_string(door.column) + " & y" + agentName + "= " + std::to_string(door.row) + ")";
     ret +=  " | (" + viewVariable(agentName, 1, true) + "x" + agentName + " = " + std::to_string(door.column) + " & y" + agentName + " + 1 = " + std::to_string(door.row) + ")";
     ret +=  " | (" + viewVariable(agentName, 2, true) + "x" + agentName + "- 1 = " + std::to_string(door.column) + " & y" + agentName + "= " + std::to_string(door.row) + ")";
-    ret +=  " | (" + viewVariable(agentName, 3, true) + "x" + agentName + " = " + std::to_string(door.column) + " & y" + agentName + " - 1 = " + std::to_string(door.row) + ")";
+    ret +=  " | (" + viewVariable(agentName, 3, true) + "x" + agentName + " = " + std::to_string(door.column) + " & y" + agentName + " - 1 = " + std::to_string(door.row) + "))";
     
     
     
@@ -837,34 +858,34 @@ namespace prism {
 
   std::ostream& PrismModulesPrinter::printRewards(std::ostream &os, const AgentName &agentName, const std::map<coordinates, float> &stateRewards, const cells &lava, const cells &goals, const std::map<Color, cells> &backgroundTiles) {
     if(lava.size() != 0) {
-      os << "rewards \"SafetyNoBFS\"\n";
-      os << "\tAgentIsInLavaAndNotDone: -100;\n";
+      os << "rewards \"" << agentName << "SafetyNoBFS\"\n";
+      os << "\t" <<agentName << "IsInLavaAndNotDone: -100;\n";
       os << "endrewards\n";
     }
 
     if (!goals.empty() || !lava.empty())  {
-      os << "rewards \"SafetyNoBFSAndGoal\"\n";
-      if(goals.size() != 0) os << "\tAgentIsInGoalAndNotDone:  100;\n";
-      if(lava.size() != 0) os << "\tAgentIsInLavaAndNotDone: -100;\n";
+      os << "rewards \"" << agentName << "SafetyNoBFSAndGoal\"\n";
+      if(goals.size() != 0) os << "\t" << agentName << "IsInGoalAndNotDone:  100;\n";
+      if(lava.size() != 0) os << "\t" << agentName << "IsInLavaAndNotDone: -100;\n";
       os << "endrewards\n";
     }
 
-    os << "rewards \"Time\"\n";
-    os << "\t!AgentIsInGoal : -1;\n";
-    if(goals.size() != 0) os << "\tAgentIsInGoalAndNotDone:  100;\n";
-    if(lava.size() != 0) os << "\tAgentIsInLavaAndNotDone: -100;\n";
+    os << "rewards \"" << agentName << "Time\"\n";
+    os << "\t!" << agentName << "IsInGoal : -1;\n";
+    if(goals.size() != 0) os << "\t" << agentName << "IsInGoalAndNotDone:  100;\n";
+    if(lava.size() != 0) os << "\t" << agentName << "IsInLavaAndNotDone: -100;\n";
     os << "endrewards\n";
 
     if(stateRewards.size() > 0) {
-      os << "rewards \"SafetyWithBFS\"\n";
-      if(lava.size() != 0) os << "\tAgentIsInLavaAndNotDone: -100;\n";
+      os << "rewards \"" << agentName << "SafetyWithBFS\"\n";
+      if(lava.size() != 0) os << "\t" << agentName << "IsInLavaAndNotDone: -100;\n";
       for(auto const [coordinates, reward] : stateRewards) {
         os << "\txAgent=" << coordinates.first << "&yAgent=" << coordinates.second << " : " << reward << ";\n";
       }
       os << "endrewards\n";
     }
     if(stateRewards.size() > 0) {
-      os << "rewards \"SafetyWithBFSAndGoal\"\n";
+      os << "rewards \"" << agentName << "SafetyWithBFSAndGoal\"\n";
       if(goals.size() != 0) os << "\tAgentIsInGoalAndNotDone:  100;\n";
       if(lava.size() != 0) os << "\tAgentIsInLavaAndNotDone: -100;\n";
       for(auto const [coordinates, reward] : stateRewards) {
diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h
index 01cccd7..dd57a8c 100644
--- a/util/PrismModulesPrinter.h
+++ b/util/PrismModulesPrinter.h
@@ -11,7 +11,7 @@ namespace prism {
     public:
       PrismModulesPrinter(const ModelType &modelType, const size_t &numberOfPlayer, std::vector<Configuration> config ,const bool enforceOneWays = false);
 
-      std::ostream& printRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &cells);
+      std::ostream& printRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &grid_cells, const cells& keys, const cells& doors);
       std::ostream& printKeyRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &keys);
       std::ostream& printDoorRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &doors);
       std::ostream& printIsOnSlipperyFormula(std::ostream& os, const AgentName &agentName, const std::vector<std::reference_wrapper<cells>> &slipperyCollection, const cells &slipperyNorth, const cells &slipperyEast, const cells &slipperySouth, const cells &slipperyWest);
@@ -77,7 +77,7 @@ namespace prism {
       std::ostream& printActionsForKeys(std::ostream &os, const AgentName &agentName, const cells &keys);
       std::ostream& printBooleansForBackground(std::ostream &os, const AgentName &agentName, const std::map<Color, cells> &backgroundTiles);
       std::ostream& printActionsForBackground(std::ostream &os, const AgentName &agentName, const std::map<Color, cells> &backgroundTiles);
-      std::ostream& printInitStruct(std::ostream &os, const AgentName &agentName, const cells &keys, const cells &lockedDoors, const cells &unlockedDoors);
+      std::ostream& printInitStruct(std::ostream &os, const AgentNameAndPositionMap &agents, const KeyNameAndPositionMap &keys, const cells &lockedDoors, const cells &unlockedDoors);
       std::ostream& printModule(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const coordinates &boundaries, const coordinates& initialPosition, const cells &keys, const std::map<Color, cells> &backgroundTiles, const bool agentWithView, const std::vector<float> &probabilities = {});
       std::ostream& printMovementActions(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const bool agentWithView, const float &probability = 1.0);
       std::ostream& printDoneActions(std::ostream &os, const AgentName &agentName, const size_t &agentIndex);
diff --git a/util/PrismPrinter.h b/util/PrismPrinter.h
index ed12126..55f4ada 100644
--- a/util/PrismPrinter.h
+++ b/util/PrismPrinter.h
@@ -6,7 +6,9 @@
 
 typedef std::string AgentName;
 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;
 
 namespace prism {
   enum class ModelType {