From 8c38856fafa8c5ab078cd7fec05ff8c9dd3e0f6b Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Sun, 16 Feb 2025 14:40:50 +0100
Subject: [PATCH] started to add non-directional slippery tiles

---
 util/Grid.cpp                | 8 +++++---
 util/Grid.h                  | 1 +
 util/MinigridGrammar.h       | 1 +
 util/PrismFormulaPrinter.cpp | 3 +--
 util/cell.cpp                | 9 +++++----
 util/cell.h                  | 1 +
 6 files changed, 14 insertions(+), 9 deletions(-)

diff --git a/util/Grid.cpp b/util/Grid.cpp
index 2e44298..c80570c 100644
--- a/util/Grid.cpp
+++ b/util/Grid.cpp
@@ -11,6 +11,7 @@ Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float>
   std::copy_if(gridCells.begin(),  gridCells.end(),  std::back_inserter(walls),         [](cell c) { return c.type == Type::Wall; });
   std::copy_if(gridCells.begin(),  gridCells.end(),  std::back_inserter(lava),          [](cell c) { return c.type == Type::Lava; });
   std::copy_if(gridCells.begin(),  gridCells.end(),  std::back_inserter(floor),         [](cell c) { return c.type == Type::Floor; }); // TODO CHECK IF ALL AGENTS ARE ADDED TO FLOOR
+  std::copy_if(gridCells.begin(),  gridCells.end(),  std::back_inserter(slippery),      [](cell c) { return c.type == Type::Slippery; });
   std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyNorth), [](cell c) { return c.type == Type::SlipperyNorth; });
   std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyEast),  [](cell c) { return c.type == Type::SlipperyEast; });
   std::copy_if(background.begin(), background.end(), std::back_inserter(slipperySouth), [](cell c) { return c.type == Type::SlipperySouth; });
@@ -26,6 +27,7 @@ Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float>
   std::copy_if(gridCells.begin(),  gridCells.end(),  std::back_inserter(boxes),         [](cell c) { return c.type == Type::Box; });
   std::copy_if(gridCells.begin(),  gridCells.end(),  std::back_inserter(balls),         [](cell c) { return c.type == Type::Ball; });
   std::copy_if(gridCells.begin(),  gridCells.end(),  std::back_inserter(adversaries),   [](cell c) { return c.type == Type::Adversary; });
+
   agent = *std::find_if(gridCells.begin(), gridCells.end(), [](cell c) { return c.type == Type::Agent; });
   floor.push_back(agent);
 
@@ -65,7 +67,7 @@ Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float>
       backgroundTiles.emplace(color, cellsOfColor);
     }
   }
-  
+
   if (adversaries.empty()) {
     modelType = prism::ModelType::MDP;
   } else {
@@ -161,7 +163,7 @@ void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configurat
 
 
   std::map<std::string, cells> wallRestrictions = {{"North", northRestriction}, {"East", eastRestriction}, {"South", southRestriction}, {"West", westRestriction}};
-  std::map<std::string, cells> slipperyTiles    = {{"North", slipperyNorth}, {"East", slipperyEast}, {"South", slipperySouth}, {"West", slipperyWest}, {"NorthWest", slipperyNorthWest}, {"NorthEast", slipperyNorthEast},{"SouthWest", slipperySouthWest},{"SouthEast", slipperySouthEast}};
+  std::map<std::string, cells> slipperyTiles    = {{"Slippery", slippery}, {"North", slipperyNorth}, {"East", slipperyEast}, {"South", slipperySouth}, {"West", slipperyWest}, {"NorthWest", slipperyNorthWest}, {"NorthEast", slipperyNorthEast},{"SouthWest", slipperySouthWest},{"SouthEast", slipperySouthEast}};
 
   std::vector<AgentName> agentNames;
   std::transform(agentNameAndPositionMap.begin(),
@@ -197,4 +199,4 @@ void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configurat
 void Grid::setModelType(prism::ModelType type)
 {
   modelType = type;
-}
\ No newline at end of file
+}
diff --git a/util/Grid.h b/util/Grid.h
index f741473..74e4e9f 100644
--- a/util/Grid.h
+++ b/util/Grid.h
@@ -42,6 +42,7 @@ class Grid {
 
     cells walls;
     cells floor;
+    cells slippery;
     cells slipperyNorth;
     cells slipperyEast;
     cells slipperySouth;
diff --git a/util/MinigridGrammar.h b/util/MinigridGrammar.h
index ea6c1cf..629f040 100644
--- a/util/MinigridGrammar.h
+++ b/util/MinigridGrammar.h
@@ -62,6 +62,7 @@ template <typename It>
       ("B", Type::Box)
       ("G", Type::Goal)
       ("V", Type::Lava)
+      ("S", Type::Slippery)
       ("n", Type::SlipperyNorth)
       ("e", Type::SlipperyEast)
       ("s", Type::SlipperySouth)
diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp
index 4115da2..ba214be 100644
--- a/util/PrismFormulaPrinter.cpp
+++ b/util/PrismFormulaPrinter.cpp
@@ -67,7 +67,6 @@ namespace prism {
     for(const auto& [direction, cells] : restrictions) {
       printRestrictionFormula(agentName, direction, cells);
     }
-
     if(slipperyBehaviour()) {
       for(const auto& [direction, cells] : slipperyTiles) {
         printIsOnFormula(agentName, "Slippery", cells, direction);
@@ -235,7 +234,7 @@ namespace prism {
   }
 
   bool PrismFormulaPrinter::slipperyBehaviour() const {
-    return !slipperyTiles.at("North").empty() || !slipperyTiles.at("East").empty() || !slipperyTiles.at("South").empty() || !slipperyTiles.at("West").empty();
+    return !slipperyTiles.at("Slippery").empty() || !slipperyTiles.at("North").empty() || !slipperyTiles.at("East").empty() || !slipperyTiles.at("South").empty() || !slipperyTiles.at("West").empty();
   }
   bool PrismFormulaPrinter::anyPortableObject() const {
     return !keys.empty();
diff --git a/util/cell.cpp b/util/cell.cpp
index c4812f9..40302c6 100644
--- a/util/cell.cpp
+++ b/util/cell.cpp
@@ -72,17 +72,18 @@ std::string cell::getColor() const {
 
 std::string cell::getType() const {
   switch(type) {
-    case Type::Wall:         return "Wall";
-    case Type::Floor:        return "Floor";
-    case Type::Door:         return "Door";
+    case Type::Wall:          return "Wall";
+    case Type::Floor:         return "Floor";
+    case Type::Door:          return "Door";
     case Type::LockedDoor:    return "LockedDoor";
-    case Type::Key:          return "Key";
+    case Type::Key:           return "Key";
     case Type::Ball:          return "Ball";
     case Type::Box:           return "Box";
     case Type::Goal:          return "Goal";
     case Type::Lava:          return "Lava";
     case Type::Agent:         return "Agent";
     case Type::Adversary:     return "Adversary";
+    case Type::Slippery:      return "Slippery";
     case Type::SlipperyNorth: return "SlipperyNorth";
     case Type::SlipperySouth: return "SlipperySouth";
     case Type::SlipperyEast:  return "SlipperyEast";
diff --git a/util/cell.h b/util/cell.h
index 5e69e3b..329844e 100644
--- a/util/cell.h
+++ b/util/cell.h
@@ -20,6 +20,7 @@ enum class Type : char {
   Lava       = 'V',
   Agent      = 'X',
   Adversary  = 'Z',
+  Slippery   = 'S',
   SlipperyNorth = 'n',
   SlipperySouth = 's',
   SlipperyEast  = 'e',