FitFramework/Minigrid2PRISM/0001-WIP-differentiate-betw...

From cbcb339cad57db456fb11dc844c99119cb8485e8 Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Wed, 5 Jul 2023 15:44:04 +0200
Subject: [PATCH] WIP: differentiate between slippery tilt direction

---
 Minigrid2PRISM/util/Grid.cpp                | 24 +++++++++++++++------
 Minigrid2PRISM/util/Grid.h                  |  5 ++++-
 Minigrid2PRISM/util/MinigridGrammar.h       |  5 ++++-
 Minigrid2PRISM/util/PrismModulesPrinter.cpp | 10 ++++-----
 4 files changed, 31 insertions(+), 13 deletions(-)

diff --git a/Minigrid2PRISM/util/Grid.cpp b/Minigrid2PRISM/util/Grid.cpp
index 9da5786..c6cf225 100644
--- a/Minigrid2PRISM/util/Grid.cpp
+++ b/Minigrid2PRISM/util/Grid.cpp
@@ -16,8 +16,17 @@ Grid::Grid(cells gridCells, cells background, const GridOptions &gridOptions, co
   std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(floor), [](cell c) {
       return c.type == Type::Floor;
   });
-  std::copy_if(background.begin(), background.end(), std::back_inserter(slippery), [](cell c) {
-      return c.type == Type::Slippery;
+  std::copy_if(background.begin(), background.end(), std::back_inserter(northSlippery), [](cell c) {
+      return c.type == Type::NorthSlippery;
+  });
+  std::copy_if(background.begin(), background.end(), std::back_inserter(southSlippery), [](cell c) {
+      return c.type == Type::SouthSlippery;
+  });
+  std::copy_if(background.begin(), background.end(), std::back_inserter(eastSlippery), [](cell c) {
+      return c.type == Type::EastSlippery;
+  });
+  std::copy_if(background.begin(), background.end(), std::back_inserter(westSlippery), [](cell c) {
+      return c.type == Type::WestSlippery;
   });
   std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(lockedDoors), [](cell c) {
       return c.type == Type::LockedDoor;
@@ -158,11 +167,14 @@ void Grid::printToPrism(std::ostream& os, const prism::ModelType& modelType) {
     std::set<std::string> slipperyActions;
     if(agentWithProbabilisticBehaviour) printer.printModule(os, agentName, agentIndex, maxBoundaries, agentNameAndPosition->second, keys, agentWithView, gridOptions.probabilitiesForActions);
     else                                printer.printModule(os, agentName, agentIndex, maxBoundaries, agentNameAndPosition->second, keys, agentWithView);
-    for(auto const& c : slippery) {
+    for(auto const& c : northSlippery) {
+      printer.printSlippery(os, agentName, agentIndex, c.getCoordinates(), slipperyActions, getWalkableDirOf8Neighborhood(c), 3);
+    for(auto const& c : southSlippery) {
+      printer.printSlippery(os, agentName, agentIndex, c.getCoordinates(), slipperyActions, getWalkableDirOf8Neighborhood(c), 3);
+    for(auto const& c : eastSlippery) {
+      printer.printSlippery(os, agentName, agentIndex, c.getCoordinates(), slipperyActions, getWalkableDirOf8Neighborhood(c), 3);
+    for(auto const& c : westSlippery) {
       printer.printSlippery(os, agentName, agentIndex, c.getCoordinates(), slipperyActions, getWalkableDirOf8Neighborhood(c), 3);
-      printer.printSlippery(os, agentName, agentIndex, c.getCoordinates(), slipperyActions, getWalkableDirOf8Neighborhood(c), 0);
-      printer.printSlippery(os, agentName, agentIndex, c.getCoordinates(), slipperyActions, getWalkableDirOf8Neighborhood(c), 1);
-      printer.printSlippery(os, agentName, agentIndex, c.getCoordinates(), slipperyActions, getWalkableDirOf8Neighborhood(c), 2);
       // printer.printSlipperyMoveNorth(os, agentName, agentIndex, c.getCoordinates(), isBlocked(c.getNorth()), isBlocked(c.getNorth(allGridCells).getEast()), isBlocked(c.getNorth(allGridCells).getWest()), slipperyActions, getWalkableDirOf8Neighborhood(c));
       // printer.printSlipperyMoveEast( os, agentName, agentIndex, c.getCoordinates(), isBlocked(c.getEast()),  isBlocked(c.getNorth(allGridCells).getEast()), isBlocked(c.getSouth(allGridCells).getEast()), slipperyActions);
       // printer.printSlipperyMoveSouth(os, agentName, agentIndex, c.getCoordinates(), isBlocked(c.getSouth()), isBlocked(c.getSouth(allGridCells).getEast()), isBlocked(c.getSouth(allGridCells).getWest()), slipperyActions);
diff --git a/Minigrid2PRISM/util/Grid.h b/Minigrid2PRISM/util/Grid.h
index f42b6e7..f908138 100644
--- a/Minigrid2PRISM/util/Grid.h
+++ b/Minigrid2PRISM/util/Grid.h
@@ -45,7 +45,10 @@ class Grid {
 
     cells walls;
     cells floor;
-    cells slippery;
+    cells northSlippery;
+    cells southSlippery;
+    cells eastSlippery;
+    cells westSlippery;
     cells lockedDoors;
     cells boxes;
     cells lava;
diff --git a/Minigrid2PRISM/util/MinigridGrammar.h b/Minigrid2PRISM/util/MinigridGrammar.h
index 5d73d87..e32db99 100644
--- a/Minigrid2PRISM/util/MinigridGrammar.h
+++ b/Minigrid2PRISM/util/MinigridGrammar.h
@@ -62,7 +62,10 @@ template <typename It>
       ("B", Type::Box)
       ("G", Type::Goal)
       ("V", Type::Lava)
-      ("S", Type::Slippery)
+      ("n", Type::NorthSlippery)
+      ("s", Type::SouthSlippery)
+      ("e", Type::EastSlippery)
+      ("w", Type::WestSlippery)
       ("X", Type::Agent)
       ("Z", Type::Adversary);
     color_.add
diff --git a/Minigrid2PRISM/util/PrismModulesPrinter.cpp b/Minigrid2PRISM/util/PrismModulesPrinter.cpp
index b6661ef..3a32932 100644
--- a/Minigrid2PRISM/util/PrismModulesPrinter.cpp
+++ b/Minigrid2PRISM/util/PrismModulesPrinter.cpp
@@ -184,9 +184,9 @@ namespace prism {
     if(agentWithView) {
       os << "\tview" << agentName << " : [0..3] init 0;\n";
     os << "\n";
-    os << "\t[" << agentName << "_turn_right] " << moveGuard(agentIndex) << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava -> (view" << agentName << "'=mod(view" << agentName << " + 1, 4)) " << moveUpdate(agentIndex) << ";\n";
-    os << "\t[" << agentName << "_turn_left]  " << moveGuard(agentIndex) << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & view" << agentName << ">0 -> (view" << agentName << "'=view" << agentName << " - 1) " << moveUpdate(agentIndex) << ";\n";
-    os << "\t[" << agentName << "_turn_left]  " << moveGuard(agentIndex) << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & view" << agentName << "=0 -> (view" << agentName << "'=3) " << moveUpdate(agentIndex) << ";\n";
+    os << "\t[" << agentName << "_turn_right] " << moveGuard(agentIndex) << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & !AgentIsOnSlippery-> (view" << agentName << "'=mod(view" << agentName << " + 1, 4)) " << moveUpdate(agentIndex) << ";\n";
+    os << "\t[" << agentName << "_turn_left]  " << moveGuard(agentIndex) << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & !AgentIsOnSlippery& view" << agentName << ">0 -> (view" << agentName << "'=view" << agentName << " - 1) " << moveUpdate(agentIndex) << ";\n";
+    os << "\t[" << agentName << "_turn_left]  " << moveGuard(agentIndex) << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & !AgentIsOnSlippery& view" << agentName << "=0 -> (view" << agentName << "'=3) " << moveUpdate(agentIndex) << ";\n";
     } else {
       os << "\t[" << agentName << "_turns]  " << moveGuard(agentIndex) << " true -> (x" << agentName << "'=x" << agentName << ")" << moveUpdate(agentIndex) << ";\n";
     }
@@ -256,7 +256,7 @@ namespace prism {
     // direction specifics
 
     std::size_t straightPosIndex;
-    std::string actionName, specialTransition; // if straight ahead is blocked 
+    std::string actionName, specialTransition; // if straight ahead is blocked
     std::array<std::size_t, ALL_POSS_DIRECTIONS> prob_piece_dir; // from north clockwise
 
     switch (direction)
@@ -367,7 +367,7 @@ namespace prism {
 
   std::ostream& PrismModulesPrinter::printRewards(std::ostream &os, const std::map<coordinates, float> &stateRewards, const cells &lava, const cells &goals) {
     os << "rewards \"NoBFS\"\n";
-    os << "\tAgentIsInGoalAndNotDone:  100;\n";
+    //os << "\tAgentIsInGoalAndNotDone:  100;\n";
     os << "\tAgentIsInLavaAndNotDone: -100;\n";
     os << "endrewards\n";
     os << "rewards \"WithBFS\"\n";
-- 
2.25.1