From d42c62e71370a59f650e9e9f21fa763811ea9343 Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Mon, 18 Sep 2023 16:06:21 +0200 Subject: [PATCH] changed key handling --- util/Grid.cpp | 28 +++++++-- util/MinigridGrammar.h | 3 +- util/PrismModulesPrinter.cpp | 110 ++++++++++++++++++++++++++++++++--- util/PrismModulesPrinter.h | 10 +++- 4 files changed, 136 insertions(+), 15 deletions(-) diff --git a/util/Grid.cpp b/util/Grid.cpp index 9f11f0c..bc7773b 100644 --- a/util/Grid.cpp +++ b/util/Grid.cpp @@ -158,14 +158,17 @@ void Grid::printToPrism(std::ostream& os, std::vector& configurat cells southRestriction; cells westRestriction; cells walkable = floor; + cells conditionallyWalkable; + walkable.insert(walkable.end(), goals.begin(), goals.end()); walkable.insert(walkable.end(), boxes.begin(), boxes.end()); walkable.push_back(agent); walkable.insert(walkable.end(), adversaries.begin(), adversaries.end()); walkable.insert(walkable.end(), lava.begin(), lava.end()); - walkable.insert(walkable.end(), keys.begin(), keys.end()); - walkable.insert(walkable.end(), lockedDoors.begin(), lockedDoors.end()); - walkable.insert(walkable.end(), unlockedDoors.begin(), unlockedDoors.end()); + + conditionallyWalkable.insert(conditionallyWalkable.end(), keys.begin(), keys.end()); + conditionallyWalkable.insert(conditionallyWalkable.end(), lockedDoors.begin(), lockedDoors.end()); + conditionallyWalkable.insert(conditionallyWalkable.end(), unlockedDoors.begin(), unlockedDoors.end()); for(auto const& c : walkable) { if(isBlocked(c.getNorth())) northRestriction.push_back(c); @@ -173,6 +176,15 @@ void Grid::printToPrism(std::ostream& os, std::vector& configurat if(isBlocked(c.getSouth())) southRestriction.push_back(c); if(isBlocked(c.getWest())) westRestriction.push_back(c); } + // TODO Add doors here (list of doors keys etc) + // walkable.insert(walkable.end(), lockedDoors.begin(), lockedDoors.end()); + // walkable.insert(walkable.end(), unlockedDoors.begin(), unlockedDoors.end()); + for(auto const& c : conditionallyWalkable) { + if(isBlocked(c.getNorth())) northRestriction.push_back(c); + if(isBlocked(c.getEast())) eastRestriction.push_back(c); + if(isBlocked(c.getSouth())) southRestriction.push_back(c); + if(isBlocked(c.getWest())) westRestriction.push_back(c); + } prism::PrismModulesPrinter printer(modelType, agentNameAndPositionMap.size(), configuration, gridOptions.enforceOneWays); printer.printModel(os, modelType); @@ -199,7 +211,7 @@ void Grid::printToPrism(std::ostream& os, std::vector& configurat } for(auto agentNameAndPosition = agentNameAndPositionMap.begin(); agentNameAndPosition != agentNameAndPositionMap.end(); ++agentNameAndPosition) { - printer.printFormulas(os, agentNameAndPosition->first, northRestriction, eastRestriction, southRestriction, westRestriction, { slipperyNorth, slipperyEast, slipperySouth, slipperyWest }, lava, walls, noTurnFloor, slipperyNorth, slipperyEast, slipperySouth, slipperyWest); + printer.printFormulas(os, agentNameAndPosition->first, northRestriction, eastRestriction, southRestriction, westRestriction, { slipperyNorth, slipperyEast, slipperySouth, slipperyWest }, lava, walls, noTurnFloor, slipperyNorth, slipperyEast, slipperySouth, slipperyWest, keys); printer.printGoalLabel(os, agentNameAndPosition->first, goals); printer.printKeysLabels(os, agentNameAndPosition->first, keys); } @@ -241,6 +253,7 @@ void Grid::printToPrism(std::ostream& os, std::vector& configurat } printer.printEndmodule(os); + if(modelType == prism::ModelType::SMG) { if(agentWithProbabilisticBehaviour) printer.printPlayerStruct(os, agentNameAndPosition->first, agentWithView, gridOptions.probabilitiesForActions, slipperyActions); else printer.printPlayerStruct(os, agentNameAndPosition->first, agentWithView, {}, slipperyActions); @@ -253,6 +266,13 @@ void Grid::printToPrism(std::ostream& os, std::vector& configurat printer.printConfiguration(os, configuration); } } + + for (auto const & key : keys) { + os << "\n"; + printer.printKeyModule(os, key, maxBoundaries); + printer.printEndmodule(os); + } + } diff --git a/util/MinigridGrammar.h b/util/MinigridGrammar.h index 79684a5..f92d05a 100644 --- a/util/MinigridGrammar.h +++ b/util/MinigridGrammar.h @@ -75,7 +75,8 @@ template ("P", Color::Purple) ("Y", Color::Yellow) (" ", Color::None); - + //TODO Enforce keys different color + cell_ = type_ > color_; row_ = (cell_ % -qi::char_("\n")); diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index 8ad82f5..8fbfc59 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -46,9 +46,40 @@ namespace prism { else os << " | "; os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; } + os << " | " << agentName << "CannotMove" << direction << "BecauseOfKey"; os << ";\n"; return os; } + + std::ostream& PrismModulesPrinter::printKeyRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &keys) { + bool first = true; + os << "formula " << agentName << "CannotMove" << direction << "BecauseOfKey" << " = "; + for (auto const& key : keys) { + if(first) first = false; + else os << " | "; + os << "((!" << agentName << "_has_" << key.getColor() << "_key) & "; + + coordinates coords; + + if (direction == "North") { + coords = key.getSouth(); + } else if (direction == "South") { + coords = key.getNorth(); + } else if (direction == "East") { + coords = key.getWest(); + } else if (direction == "West") { + coords = key.getEast(); + } else { + *((size_t*)0); + } + + os << "(x" << agentName << "=" << coords.first << "&y" << agentName << "=" << coords.second << "))"; + } + os << ";\n"; + return os; + } + + std::ostream& PrismModulesPrinter::printIsOnSlipperyFormula(std::ostream& os, const AgentName &agentName, const std::vector> &slipperyCollection, const cells &slipperyNorth, const cells &slipperyEast, const cells &slipperySouth, const cells &slipperyWest) { if(std::find_if(slipperyCollection.cbegin(), slipperyCollection.cend(), [=](const std::reference_wrapper& c) { return !c.get().empty(); }) == slipperyCollection.cend()) { @@ -174,11 +205,20 @@ namespace prism { const cells &slipperyNorth, const cells &slipperyEast, const cells &slipperySouth, - const cells &slipperyWest) { + const cells &slipperyWest, + const cells &keys) { printRestrictionFormula(os, agentName, "North", restrictionNorth); printRestrictionFormula(os, agentName, "East ", restrictionEast); printRestrictionFormula(os, agentName, "South", restrictionSouth); - printRestrictionFormula(os, agentName, "West ", restrictionWest); + printRestrictionFormula(os, agentName, "West", restrictionWest); + + if (!keys.empty()) { + printKeyRestrictionFormula(os, agentName, "North", keys); + printKeyRestrictionFormula(os, agentName, "East", keys); + printKeyRestrictionFormula(os, agentName, "South", keys); + printKeyRestrictionFormula(os, agentName, "West", keys); + } + printIsOnSlipperyFormula(os, agentName, slipperyCollection, slipperyNorth, slipperyEast, slipperySouth, slipperyWest); printIsInLavaFormula(os, agentName, lava); printWallFormula(os, agentName, walls); @@ -249,9 +289,9 @@ namespace prism { if(keys.size() == 0) return os; for(auto const& key : keys) { - int xKey = key.getCoordinates().first; - int yKey = key.getCoordinates().second; std::string keyColor = key.getColor(); + std::string xKey = "xKey" + keyColor; + std::string yKey = "yKey" + keyColor; os << "label \"" << agentName << "PickedUp" << keyColor << "Key\" = " << agentName << "_has_" << keyColor << "_key = true;\n"; os << "formula " << agentName << "CanPickUp" << keyColor << "Key = "; os << "((x" << agentName << "-1 = " << xKey << "&y" << agentName << " = " << yKey << "&view" << agentName << " = 1) |"; @@ -268,6 +308,8 @@ namespace prism { for(auto const& key : keys) { os << "\t" << agentName << "_has_"<< key.getColor() << "_key : bool;\n";//init false;\n"; } + + os << "\n"; return os; } @@ -284,15 +326,43 @@ namespace prism { } std::ostream& PrismModulesPrinter::printActionsForKeys(std::ostream &os, const AgentName &agentName, const cells &keys) { - for(auto const& key : keys) { + for(auto const& key : keys) { // TODO ADD Drop action and enforce that pickup only possible if pockets empty (nothing picked up already) std::string keyColor = key.getColor(); - os << "\t[pickup_" << keyColor << "_key] " << agentName << "CanPickUp" << keyColor << "Key -> "; - os << "(" << agentName << "_has_" << keyColor << "_key'=true);"; + os << "\t[pickup_" << keyColor << "_key] " << pickupGuard(agentName, keyColor) << "-> "; + os << "(" << agentName << "_has_" << keyColor << "_key'=true) & (" << agentName << "_is_carrying_object'=true)\n"; + + viewVariable(agentName, 3, true); + os << "\t[drop_" << keyColor << "_key_north] " << dropGuard(agentName, keyColor, 3) << "-> "; + os << "(" << agentName << "_has_" << keyColor << "_key'=false) & (" << agentName << "_is_carrying_object'=false)"; + os << " & (xKey" << keyColor << "'=x" << agentName << ") & (yKey" << keyColor << "'=y" < "; + os << "(" << agentName << "_has_" << keyColor << "_key'=false) & (" << agentName << "_is_carrying_object'=false)"; + os << " & (xKey" << keyColor << "'=x" << agentName << "-1) & (yKey" << keyColor << "'=y" < "; + os << "(" << agentName << "_has_" << keyColor << "_key'=false) & (" << agentName << "_is_carrying_object'=false)"; + os << " & (xKey" << keyColor << "'=x" << agentName << ") & (yKey" << keyColor << "'=y" < "; + os << "(" << agentName << "_has_" << keyColor << "_key'=false) & (" << agentName << "_is_carrying_object'=false)"; + os << " & (xKey" << keyColor << "'=x" << agentName << "+1) & (yKey" << keyColor << "'=y" < &backgroundTiles) { for(auto const& [color, cells] : backgroundTiles) { if(cells.size() == 0) continue; @@ -316,8 +386,12 @@ namespace prism { for (auto const& key : keys) { os << " & ( !" << agentName << "_has_" << key.getColor() << "_key )"; + os << " & ( xKey" << key.getColor() << "="<< key.column << ")"; + os << " & ( yKey" << key.getColor() << "=" << key.row << ")"; } + os << " & ( !" << agentName << "_is_carrying_object" << ")"; + os << "\nendinit\n\n"; @@ -328,6 +402,8 @@ namespace prism { os << "module " << agentName << "\n"; os << "\tx" << agentName << " : [1.." << boundaries.second << "];\n"; os << "\ty" << agentName << " : [1.." << boundaries.first << "];\n"; + os << "\t" << agentName << "_is_carrying_object : bool;\n"; + printBooleansForKeys(os, agentName, keys); printBooleansForBackground(os, agentName, backgroundTiles); os << "\t" << agentName << "Done : bool;\n"; @@ -361,6 +437,26 @@ namespace prism { return os; } + std::ostream& PrismModulesPrinter::printKeyModule(std::ostream &os, const cell &key, const coordinates &boundaries) { + std::string keyIdentifier = "Key" + key.getColor(); + + os << "module " << keyIdentifier << "\n"; + + os << "\tx" << keyIdentifier << " : [1.." << boundaries.second << "];\n"; + os << "\ty" << keyIdentifier << " : [1.." << boundaries.first << "];\n"; + + printKeyActions(os, key ,keyIdentifier); + + os << "\n"; + return os; + } + + std::ostream& PrismModulesPrinter::printKeyActions(std::ostream &os, const cell &key ,const std::string &keyIdentifier) { + + return os; + } + + std::ostream& PrismModulesPrinter::printConfiguredActions(std::ostream &os, const AgentName &agentName) { for (auto& config : configuration) { if (config.type_ == ConfigType::Module && !config.overwrite_ && agentName == config.module_) { diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h index 85483ab..8e2d50a 100644 --- a/util/PrismModulesPrinter.h +++ b/util/PrismModulesPrinter.h @@ -12,6 +12,7 @@ namespace prism { PrismModulesPrinter(const ModelType &modelType, const size_t &numberOfPlayer, std::vector config ,const bool enforceOneWays = false); std::ostream& printRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &cells); + std::ostream& printKeyRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &keys); std::ostream& printIsOnSlipperyFormula(std::ostream& os, const AgentName &agentName, const std::vector> &slipperyCollection, const cells &slipperyNorth, const cells &slipperyEast, const cells &slipperySouth, const cells &slipperyWest); std::ostream& printGoalLabel(std::ostream& os, const AgentName&agentName, const cells &goals); std::ostream& printCrashLabel(std::ostream &os, const std::vector agentNames); @@ -35,8 +36,9 @@ namespace prism { const cells &slipperyNorth, const cells &slipperyEast, const cells &slipperySouth, - const cells &slipperyWest); - + const cells &slipperyWest, + const cells &keys); + std::ostream& printKeyModule(std::ostream &os, const cell &key, const coordinates &boundaries); /* * Representation for Slippery Tile. * -) North: Slips from North to South @@ -74,13 +76,15 @@ namespace prism { std::ostream& printEndmodule(std::ostream &os); std::ostream& printPlayerStruct(std::ostream &os, const AgentName &agentName, const bool agentWithView, const std::vector &probabilities = {}, const std::set &slipperyActions = {}); std::ostream& printGlobalMoveVariable(std::ostream &os, const size_t &numberOfPlayer); - + std::ostream& printKeyActions(std::ostream &os, const cell& key ,const std::string &keyIdentifier); std::ostream& printRewards(std::ostream &os, const AgentName &agentName, const std::map &stateRewards, const cells &lava, const cells &goals, const std::map &backgroundTiles); std::ostream& printConfiguration(std::ostream &os, const std::vector& configurations); std::ostream& printConfiguredActions(std::ostream &os, const AgentName &agentName); std::string moveGuard(const size_t &agentIndex); + std::string pickupGuard(const AgentName &agentName, const std::string keyColor); + std::string dropGuard(const AgentName &agentName, const std::string keyColor, size_t view); std::string moveUpdate(const size_t &agentIndex); std::string viewVariable(const AgentName &agentName, const size_t &agentDirection, const bool agentWithView);