From e4cddbe9de3cec9a34f5201e93ee40ac0f45a53a Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Fri, 22 Sep 2023 09:34:24 +0200 Subject: [PATCH] init struct handling changs --- util/Grid.cpp | 34 ++++++++----- util/Grid.h | 1 + util/PrismModulesPrinter.cpp | 97 ++++++++++++++++++++++-------------- util/PrismModulesPrinter.h | 4 +- util/PrismPrinter.h | 2 + 5 files changed, 86 insertions(+), 52 deletions(-) diff --git a/util/Grid.cpp b/util/Grid.cpp index a429c80..e47ea2f 100644 --- a/util/Grid.cpp +++ b/util/Grid.cpp @@ -37,13 +37,7 @@ 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), [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"); - } - } - + std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(keys), [this](cell c) { return c.type == Type::Key; }); std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(boxes), [](cell c) { @@ -70,6 +64,18 @@ Grid::Grid(cells gridCells, cells background, const GridOptions &gridOptions, co throw; } } + for(auto const& key : keys) { + std::string color = key.getColor(); + try { + auto success = keyNameAndPositionMap.insert({color, key.getCoordinates() }); + if (!success.second) { + throw std::logic_error("Multiple keys with same color not supported " + color + "\n"); + } + } catch(const std::logic_error& e) { + std::cerr << "Expected key colors to be different. Key with color : '" << color << "' already present." << std::endl; + throw; + } + } for(auto const& color : allColors) { cells cellsOfColor; std::copy_if(background.begin(), background.end(), std::back_inserter(cellsOfColor), [&color](cell c) { @@ -233,13 +239,16 @@ void Grid::printToPrism(std::ostream& os, std::vector& configurat printer.printCrashLabel(os, agentNames); } size_t agentIndex = 0; + + printer.printInitStruct(os, agentNameAndPositionMap, keyNameAndPositionMap, lockedDoors, unlockedDoors); + + for(auto agentNameAndPosition = agentNameAndPositionMap.begin(); agentNameAndPosition != agentNameAndPositionMap.end(); ++agentNameAndPosition, agentIndex++) { AgentName agentName = agentNameAndPosition->first; //std::cout << "Agent Name: " << agentName << std::endl; bool agentWithView = std::find(gridOptions.agentsWithView.begin(), gridOptions.agentsWithView.end(), agentName) != gridOptions.agentsWithView.end(); bool agentWithProbabilisticBehaviour = std::find(gridOptions.agentsWithProbabilisticBehaviour.begin(), gridOptions.agentsWithProbabilisticBehaviour.end(), agentName) != gridOptions.agentsWithProbabilisticBehaviour.end(); - std::set slipperyActions; - printer.printInitStruct(os, agentName, keys, lockedDoors, unlockedDoors); + std::set slipperyActions; // TODO AGENT POSITION INITIALIZATIN if(agentWithProbabilisticBehaviour) printer.printModule(os, agentName, agentIndex, maxBoundaries, agentNameAndPosition->second, keys, backgroundTiles, agentWithView, gridOptions.probabilitiesForActions); else printer.printModule(os, agentName, agentIndex, maxBoundaries, agentNameAndPosition->second, keys, backgroundTiles, agentWithView); for(auto const& c : slipperyNorth) { @@ -270,9 +279,10 @@ void Grid::printToPrism(std::ostream& os, std::vector& configurat printer.printRewards(os, agentName, stateRewards, lava, goals, backgroundTiles); //} - if (!configuration.empty()) { - printer.printConfiguration(os, configuration); - } + } + + if (!configuration.empty()) { + printer.printConfiguration(os, configuration); } // TODO CHANGE HANDLING std::string agentName = agentNames.at(0); diff --git a/util/Grid.h b/util/Grid.h index a7c5667..c869945 100644 --- a/util/Grid.h +++ b/util/Grid.h @@ -46,6 +46,7 @@ class Grid { cell agent; cells adversaries; AgentNameAndPositionMap agentNameAndPositionMap; + KeyNameAndPositionMap keyNameAndPositionMap; cells walls; cells floor; diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index ef510ff..4688b59 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -38,16 +38,22 @@ namespace prism { return os; } - std::ostream& PrismModulesPrinter::printRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &cells) { + std::ostream& PrismModulesPrinter::printRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &grid_cells, const cells &keys, const cells &doors) { bool first = true; os << "formula " << agentName << "CannotMove" << direction << " = " ; - for(auto const& cell : cells) { + for(auto const& cell : grid_cells) { if(first) first = false; else os << " | "; os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; } - os << " | " << agentName << "CannotMove" << direction << "BecauseOfKey"; - os << " | " << agentName << "CannotMove" << direction << "BecauseOfDoor"; + + if (!keys.empty()) { + os << " | " << agentName << "CannotMove" << direction << "BecauseOfKey"; + } + if (!doors.empty()) { + os << " | " << agentName << "CannotMove" << direction << "BecauseOfDoor"; + } + os << ";\n"; return os; } @@ -205,7 +211,7 @@ namespace prism { os << "formula " << agentName << "SlipperyTurnLeftAllowed = true;\n"; os << "formula " << agentName << "SlipperyTurnRightAllowed = true;\n"; os << "formula " << agentName << "SlipperyMoveForwardAllowed = true;\n"; - os << "label \"FixedStates\" = " << agentName << "IsFixed | !" << agentName << "SlipperyTurnRightAllowed | !" << agentName << "SlipperyTurnLeftAllowed | !" << agentName << "SlipperyMoveForwardAllowed | " << agentName << "IsInGoal | " << agentName << "IsInLava"; + os << "label \"FixedStates" << agentName << "\" = " << agentName << "IsFixed | !" << agentName << "SlipperyTurnRightAllowed | !" << agentName << "SlipperyTurnLeftAllowed | !" << agentName << "SlipperyMoveForwardAllowed | " << agentName << "IsInGoal | " << agentName << "IsInLava"; if(enforceOneWays) { os << " | " << agentName << "CannotTurn"; } @@ -243,10 +249,10 @@ namespace prism { const cells &slipperyWest, const cells &keys, const cells &doors) { - printRestrictionFormula(os, agentName, "North", restrictionNorth); - printRestrictionFormula(os, agentName, "East", restrictionEast); - printRestrictionFormula(os, agentName, "South", restrictionSouth); - printRestrictionFormula(os, agentName, "West", restrictionWest); + printRestrictionFormula(os, agentName, "North", restrictionNorth, keys, doors); + printRestrictionFormula(os, agentName, "East", restrictionEast, keys, doors); + printRestrictionFormula(os, agentName, "South", restrictionSouth, keys, doors); + printRestrictionFormula(os, agentName, "West", restrictionWest, keys, doors); if (!keys.empty()) { printKeyRestrictionFormula(os, agentName, "North", keys); @@ -373,7 +379,7 @@ namespace prism { os << "\n"; std::string keyColor = key.getColor(); os << "\t[pickup_" << keyColor << "_key]\t" << pickupGuard(agentName, keyColor) << "-> "; - os << "(" << agentName << "_has_" << keyColor << "_key'=true) & (" << agentName << "_is_carrying_object'=true) ;\n"; + os << "(" << agentName << "_has_" << keyColor << "_key'=true) & (" << agentName << "_is_carrying_object'=true);\n"; os << "\n"; os << "\t[drop_" << keyColor << "_key_north]\t" << dropGuard(agentName, keyColor, 3) << "-> "; @@ -412,19 +418,31 @@ namespace prism { return os; } - std::ostream& PrismModulesPrinter::printInitStruct(std::ostream &os, const AgentName &agentName, const cells &keys, const cells &lockedDoors, const cells &unlockedDoors) { + std::ostream& PrismModulesPrinter::printInitStruct(std::ostream &os, const AgentNameAndPositionMap &agents, const KeyNameAndPositionMap &keys, const cells &lockedDoors, const cells &unlockedDoors) { os << "init\n"; - os << "\t(!AgentIsInGoal & !AgentIsInLava & !AgentDone & !AgentIsOnWall)"; - if(enforceOneWays) { - os << " & ( !AgentCannotTurn ) "; - } else { - os << " & ( !AgentIsOnSlippery ) "; - } + os << "\t"; + + bool first = true; + for (auto const& agent : agents) { + if (first) first = false; + else os << " & "; + os << "(!" << agent.first << "IsInGoal & !" << agent.first << "IsInLava & !" << agent.first << "Done & !" << agent.first << "IsOnWall & "; + os << "x" << agent.first << "=" << agent.second.second << " & y" << agent.first << "=" << agent.second.first << ")"; + os << " & !" << agent.first << "_is_carrying_object"; + if(enforceOneWays) { + os << " & ( !AgentCannotTurn ) "; + } else { + os << " & ( !AgentIsOnSlippery ) "; + } + for (auto const& key : keys) { + os << " & ( !" << agent.first << "_has_" << key.first << "_key )"; + } + } + for (auto const& key : keys) { - os << " & ( !" << agentName << "_has_" << key.getColor() << "_key )"; - os << " & ( xKey" << key.getColor() << "="<< key.column << ")"; - os << " & ( yKey" << key.getColor() << "=" << key.row << ")"; + os << " & ( xKey" << key.first << "="<< key.second.second<< ")"; + os << " & ( yKey" << key.first << "=" << key.second.first << ")"; } for (auto const& locked : lockedDoors) { @@ -435,7 +453,7 @@ namespace prism { os << " & (!Door" << unlocked.getColor() << "locked & !Door" << unlocked.getColor() << "open)"; } - os << " & ( !" << agentName << "_is_carrying_object" << ")"; + // os << " & ( !" << agentName << "_is_carrying_object" << ")"; os << "\nendinit\n\n"; @@ -487,8 +505,8 @@ namespace prism { os << "module " << keyIdentifier << "\n"; - os << "\tx" << keyIdentifier << " : [1.." << boundaries.second << "];\n"; - os << "\ty" << keyIdentifier << " : [1.." << boundaries.first << "];\n"; + os << "\tx" << keyIdentifier << " : [-1.." << boundaries.second << "];\n"; + os << "\ty" << keyIdentifier << " : [-1.." << boundaries.first << "];\n"; os << "\n"; printKeyActions(os, key ,keyIdentifier, agentName); @@ -498,7 +516,10 @@ namespace prism { std::ostream& PrismModulesPrinter::printKeyActions(std::ostream &os, const cell &key ,const std::string &keyIdentifier, AgentName agentName) { std::string keyColor = key.getColor(); - + + os << "\t[pickup_" << keyColor << "key]\t" << pickupGuard(agentName, keyColor) << "-> "; + os << "(xKey" << keyColor << "'=-1) & (yKey" << keyColor << "'=-1)" << ";\n"; + os << "\t[drop_" << keyColor << "_key_north]\t" << dropGuard(agentName, keyColor, 3) << "-> "; os << "(xKey" << keyColor << "'=x" << agentName << ") & (yKey" << keyColor << "'=y" < &stateRewards, const cells &lava, const cells &goals, const std::map &backgroundTiles) { if(lava.size() != 0) { - os << "rewards \"SafetyNoBFS\"\n"; - os << "\tAgentIsInLavaAndNotDone: -100;\n"; + os << "rewards \"" << agentName << "SafetyNoBFS\"\n"; + os << "\t" < 0) { - os << "rewards \"SafetyWithBFS\"\n"; - if(lava.size() != 0) os << "\tAgentIsInLavaAndNotDone: -100;\n"; + os << "rewards \"" << agentName << "SafetyWithBFS\"\n"; + if(lava.size() != 0) os << "\t" << agentName << "IsInLavaAndNotDone: -100;\n"; for(auto const [coordinates, reward] : stateRewards) { os << "\txAgent=" << coordinates.first << "&yAgent=" << coordinates.second << " : " << reward << ";\n"; } os << "endrewards\n"; } if(stateRewards.size() > 0) { - os << "rewards \"SafetyWithBFSAndGoal\"\n"; + os << "rewards \"" << agentName << "SafetyWithBFSAndGoal\"\n"; if(goals.size() != 0) os << "\tAgentIsInGoalAndNotDone: 100;\n"; if(lava.size() != 0) os << "\tAgentIsInLavaAndNotDone: -100;\n"; for(auto const [coordinates, reward] : stateRewards) { diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h index 01cccd7..dd57a8c 100644 --- a/util/PrismModulesPrinter.h +++ b/util/PrismModulesPrinter.h @@ -11,7 +11,7 @@ namespace prism { public: 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& printRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &grid_cells, const cells& keys, const cells& doors); std::ostream& printKeyRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &keys); std::ostream& printDoorRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &doors); 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); @@ -77,7 +77,7 @@ namespace prism { std::ostream& printActionsForKeys(std::ostream &os, const AgentName &agentName, const cells &keys); std::ostream& printBooleansForBackground(std::ostream &os, const AgentName &agentName, const std::map &backgroundTiles); std::ostream& printActionsForBackground(std::ostream &os, const AgentName &agentName, const std::map &backgroundTiles); - std::ostream& printInitStruct(std::ostream &os, const AgentName &agentName, const cells &keys, const cells &lockedDoors, const cells &unlockedDoors); + std::ostream& printInitStruct(std::ostream &os, const AgentNameAndPositionMap &agents, const KeyNameAndPositionMap &keys, const cells &lockedDoors, const cells &unlockedDoors); std::ostream& printModule(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const coordinates &boundaries, const coordinates& initialPosition, const cells &keys, const std::map &backgroundTiles, const bool agentWithView, const std::vector &probabilities = {}); std::ostream& printMovementActions(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const bool agentWithView, const float &probability = 1.0); std::ostream& printDoneActions(std::ostream &os, const AgentName &agentName, const size_t &agentIndex); diff --git a/util/PrismPrinter.h b/util/PrismPrinter.h index ed12126..55f4ada 100644 --- a/util/PrismPrinter.h +++ b/util/PrismPrinter.h @@ -6,7 +6,9 @@ typedef std::string AgentName; typedef std::pair AgentNameAndPosition; +typedef AgentNameAndPosition KeyNameAndPosition; typedef std::map AgentNameAndPositionMap; +typedef std::map KeyNameAndPositionMap; namespace prism { enum class ModelType {