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