From 5955bb97914f39e16ad55f695f7519304f4b4e2f Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Sat, 6 Jan 2024 18:35:41 +0100
Subject: [PATCH] isNextTo formulas for doors

---
 util/PrismFormulaPrinter.cpp | 18 ++++++++++++------
 util/PrismFormulaPrinter.h   |  5 +++--
 2 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp
index 0bcdd69..8f333f2 100644
--- a/util/PrismFormulaPrinter.cpp
+++ b/util/PrismFormulaPrinter.cpp
@@ -32,7 +32,7 @@ namespace prism {
     : os(os), agentName(agentName), restrictions(restrictions), boxes(boxes), balls(balls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), lava(lava)
   { }
 
-  void PrismFormulaPrinter::printFormulas() {
+  void PrismFormulaPrinter::print() {
     for(const auto& [direction, cells] : restrictions) {
       printRestrictionFormula(direction, cells);
     }
@@ -58,17 +58,19 @@ namespace prism {
     }
 
     for(const auto& door : unlockedDoors) {
-      std::string color = capitalize(door.getColor());
-      printRestrictionFormulaWithCondition(color + "Door", getSurroundingCells(door), "!" + color + "DoorOpened");
+      std::string identifier = capitalize(door.getColor()) + door.getType();
+      printRestrictionFormulaWithCondition(identifier, getSurroundingCells(door), "!" + identifier + "Open");
+      printIsNextToFormula(identifier, getSurroundingCells(door));
     }
 
     for(const auto& door : lockedDoors) {
-      std::string color = capitalize(door.getColor());
-      printRestrictionFormulaWithCondition(color + "Door", getSurroundingCells(door), "!" + color + "DoorOpened");
+      std::string identifier = capitalize(door.getColor()) + door.getType();
+      printRestrictionFormulaWithCondition(identifier, getSurroundingCells(door), "!" + identifier + "Open");
+      printIsNextToFormula(identifier, getSurroundingCells(door));
     }
 
     if(conditionalMovementRestrictions.size() > 0) {
-      os << buildFormula("CannotMoveConditionally", vectorToDisjunction(conditionalMovementRestrictions));
+      os << buildFormula(agentName + "CannotMoveConditionally", vectorToDisjunction(conditionalMovementRestrictions));
     }
   }
 
@@ -80,6 +82,10 @@ namespace prism {
     os << buildFormula(agentName + "IsOn" + type + direction, buildDisjunction(agentName, grid_cells));
   }
 
+  void PrismFormulaPrinter::printIsNextToFormula(const std::string &type, const std::map<ViewDirection, coordinates> &coordinates) {
+    os << buildFormula(agentName + "IsNextTo" + type, buildDisjunction(agentName, coordinates));
+  }
+
   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);
     conditionalMovementRestrictions.push_back(agentName + "CannotMove" + reason);
diff --git a/util/PrismFormulaPrinter.h b/util/PrismFormulaPrinter.h
index 97f77f8..4795f3e 100644
--- a/util/PrismFormulaPrinter.h
+++ b/util/PrismFormulaPrinter.h
@@ -17,10 +17,11 @@ namespace prism {
     public:
       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, const std::map<std::string, cells> &slipperyTiles, const cells &lava);
 
-      void printFormulas();
+      void print();
 
       void printRestrictionFormula(const std::string &direction, const cells &grid_cells);
       void printIsOnFormula(const std::string &type, const cells &grid_cells, const std::string &direction = "");
+      void printIsNextToFormula(const std::string &type, const std::map<ViewDirection, coordinates> &coordinates);
       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);
@@ -29,7 +30,7 @@ namespace prism {
       std::string buildDisjunction(const AgentName &agentName, const cells &cells, const std::vector<std::string> &conditions = {});
 
       std::ostream &os;
-      AgentName agentName;
+      AgentName agentName; // move this to functions
       std::map<std::string, cells> restrictions;
       cells boxes;
       cells balls;