From b16e348acb31268322a1e9c9a0e92fb7350d9fd5 Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Tue, 19 Sep 2023 12:13:35 +0200 Subject: [PATCH] continued key support --- util/Grid.cpp | 8 +++- util/MinigridGrammar.h | 1 - util/PrismModulesPrinter.cpp | 90 ++++++++++++++++++++---------------- util/PrismModulesPrinter.h | 1 + 4 files changed, 58 insertions(+), 42 deletions(-) diff --git a/util/Grid.cpp b/util/Grid.cpp index bc7773b..6ec9923 100644 --- a/util/Grid.cpp +++ b/util/Grid.cpp @@ -37,7 +37,13 @@ Grid::Grid(cells gridCells, cells background, const GridOptions &gridOptions, co std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(goals), [](cell c) { return c.type == Type::Goal; }); - std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(keys), [](cell c) { + std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(keys), [this](cell c) { + for (auto const& key : keys) { + if (key.color == c.color && key.type == c.type) { + throw std::logic_error("Multiple keys with same color not supported " + key.getColor() + "\n"); + } + } + return c.type == Type::Key; }); std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(boxes), [](cell c) { diff --git a/util/MinigridGrammar.h b/util/MinigridGrammar.h index f92d05a..e2cfddc 100644 --- a/util/MinigridGrammar.h +++ b/util/MinigridGrammar.h @@ -75,7 +75,6 @@ template ("P", Color::Purple) ("Y", Color::Yellow) (" ", Color::None); - //TODO Enforce keys different color cell_ = type_ > color_; diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index 8fbfc59..e9d00b9 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -6,7 +6,7 @@ namespace prism { PrismModulesPrinter::PrismModulesPrinter(const ModelType &modelType, const size_t &numberOfPlayer, std::vector config, const bool enforceOneWays) - : modelType(modelType), numberOfPlayer(numberOfPlayer), enforceOneWays(enforceOneWays), configuration(config) { + : modelType(modelType), numberOfPlayer(numberOfPlayer), enforceOneWays(enforceOneWays), configuration(config), viewDirectionMapping({{0, "East"}, {1, "South"}, {2, "West"}, {3, "North"}}) { } std::ostream& PrismModulesPrinter::printModel(std::ostream &os, const ModelType &modelType) { @@ -57,24 +57,26 @@ namespace prism { for (auto const& key : keys) { if(first) first = false; else os << " | "; - os << "((!" << agentName << "_has_" << key.getColor() << "_key) & "; - + std::string keyColor = key.getColor(); + std::string xKey = "xKey" + keyColor; + std::string yKey = "yKey" + keyColor; coordinates coords; + + os << "!" << agentName << "_has_" << keyColor << "_key & "; if (direction == "North") { - coords = key.getSouth(); + os << " (x" << agentName << " = " << xKey << "&y" << agentName << "-1 = " << yKey << ")"; } else if (direction == "South") { - coords = key.getNorth(); + os << " (x" << agentName << " = " << xKey << "&y" << agentName << "+1 = " << yKey << ")"; } else if (direction == "East") { - coords = key.getWest(); + os << " (x" << agentName << "+1 = " << xKey << "&y" << agentName << " = " << yKey << ")"; } else if (direction == "West") { - coords = key.getEast(); + os << " (x" << agentName << "-1 = " << xKey << "&y" << agentName << " = " << yKey << ")"; } else { - *((size_t*)0); + os << "Invalid Direction! in Key Restriction"; } - - os << "(x" << agentName << "=" << coords.first << "&y" << agentName << "=" << coords.second << "))"; } + os << ";\n"; return os; } @@ -208,7 +210,7 @@ namespace prism { const cells &slipperyWest, const cells &keys) { printRestrictionFormula(os, agentName, "North", restrictionNorth); - printRestrictionFormula(os, agentName, "East ", restrictionEast); + printRestrictionFormula(os, agentName, "East", restrictionEast); printRestrictionFormula(os, agentName, "South", restrictionSouth); printRestrictionFormula(os, agentName, "West", restrictionWest); @@ -294,10 +296,10 @@ namespace prism { 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) |"; - os << " (x" << agentName << "+1 = " << xKey << "&y" << agentName << " = " << yKey << "&view" << agentName << " = 3) |"; - os << " (x" << agentName << " = " << xKey << "&y" << agentName << "-1 = " << yKey << "&view" << agentName << " = 0) |"; - os << " (x" << agentName << " = " << xKey << "&y" << agentName << "+1 = " << yKey << "&view" << agentName << " = 2) ) &"; + os << "((x" << agentName << "-1 = " << xKey << "&y" << agentName << " = " << yKey << "&view" << agentName << " = 2) |"; + os << " (x" << agentName << "+1 = " << xKey << "&y" << agentName << " = " << yKey << "&view" << agentName << " = 0) |"; + os << " (x" << agentName << " = " << xKey << "&y" << agentName << "-1 = " << yKey << "&view" << agentName << " = 3) |"; + os << " (x" << agentName << " = " << xKey << "&y" << agentName << "+1 = " << yKey << "&view" << agentName << " = 1) ) &"; os << "!" << agentName << "_has_" << keyColor << "_key;"; } os << "\n"; @@ -328,30 +330,24 @@ namespace prism { std::ostream& PrismModulesPrinter::printActionsForKeys(std::ostream &os, const AgentName &agentName, const cells &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] " << pickupGuard(agentName, keyColor) << "-> "; - os << "(" << agentName << "_has_" << keyColor << "_key'=true) & (" << agentName << "_is_carrying_object'=true)\n"; + os << "\t[pickup_" << keyColor << "_key]\t" << pickupGuard(agentName, keyColor) << "-> "; + os << "(" << agentName << "_has_" << keyColor << "_key'=true) & (" << agentName << "_is_carrying_object'=true) ;"; + os << "\n"; + os << "\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" < "; + os << "(" << agentName << "_has_" << keyColor << "_key'=false) & (" << agentName << "_is_carrying_object'=false);\n"; + + os << "\t[drop_" << keyColor << "_key_west]\t" << dropGuard(agentName, keyColor, 2) << "-> "; + os << "(" << agentName << "_has_" << keyColor << "_key'=false) & (" << agentName << "_is_carrying_object'=false);\n"; + + os << "\t[drop_" << keyColor << "_key_south]\t" << dropGuard(agentName, keyColor, 1) << "-> "; + os << "(" << agentName << "_has_" << keyColor << "_key'=false) & (" << agentName << "_is_carrying_object'=false);\n"; + + os << "\t[drop_" << keyColor << "_key_east]\t" << dropGuard(agentName, keyColor, 0) << "-> "; + os << "(" << agentName << "_has_" << keyColor << "_key'=false) & (" << agentName << "_is_carrying_object'=false);\n"; } - os << "\n"; + return os; } @@ -360,7 +356,7 @@ namespace prism { } std::string PrismModulesPrinter::dropGuard(const AgentName &agentName, const std::string keyColor, size_t view) { - return viewVariable(agentName, view, true) + agentName + "_has_" + keyColor + "_key\t"; + return viewVariable(agentName, view, true) + "\t!" + agentName + "CannotMove" + viewDirectionMapping.at(view) + "\t&\t" + agentName + "_has_" + keyColor + "_key\t"; } std::ostream& PrismModulesPrinter::printActionsForBackground(std::ostream &os, const AgentName &agentName, const std::map &backgroundTiles) { @@ -444,7 +440,7 @@ namespace prism { os << "\tx" << keyIdentifier << " : [1.." << boundaries.second << "];\n"; os << "\ty" << keyIdentifier << " : [1.." << boundaries.first << "];\n"; - + os << "\n"; printKeyActions(os, key ,keyIdentifier); os << "\n"; @@ -452,7 +448,21 @@ namespace prism { } std::ostream& PrismModulesPrinter::printKeyActions(std::ostream &os, const cell &key ,const std::string &keyIdentifier) { - + std::string keyColor = key.getColor(); + std::string agentName = "Agent"; + + os << "\t[drop_" << keyColor << "_key_north]\t" << dropGuard(agentName, keyColor, 3) << "-> "; + os << "(xKey" << keyColor << "'=x" << agentName << ") & (yKey" << keyColor << "'=y" < "; + os << "(xKey" << keyColor << "'=x" << agentName << "-1) & (yKey" << keyColor << "'=y" < "; + os << "(xKey" << keyColor << "'=x" << agentName << ") & (yKey" << keyColor << "'=y" < "; + os << "(xKey" << keyColor << "'=x" << agentName << "+1) & (yKey" << keyColor << "'=y" < configuration; + std::map viewDirectionMapping; }; }