diff --git a/util/Grid.cpp b/util/Grid.cpp index 6ec9923..a429c80 100644 --- a/util/Grid.cpp +++ b/util/Grid.cpp @@ -97,7 +97,7 @@ cells Grid::getGridCells() { } bool Grid::isBlocked(coordinates p) { - return isWall(p) || isLockedDoor(p) || isKey(p); + return isWall(p); //|| isLockedDoor(p) || isKey(p); } bool Grid::isWall(coordinates p) { @@ -215,9 +215,11 @@ void Grid::printToPrism(std::ostream& os, std::vector& configurat } } } - + cells doors; + doors.insert(doors.end(), lockedDoors.begin(), lockedDoors.end()); + doors.insert(doors.end(), unlockedDoors.begin(), unlockedDoors.end()); 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, keys); + printer.printFormulas(os, agentNameAndPosition->first, northRestriction, eastRestriction, southRestriction, westRestriction, { slipperyNorth, slipperyEast, slipperySouth, slipperyWest }, lava, walls, noTurnFloor, slipperyNorth, slipperyEast, slipperySouth, slipperyWest, keys, doors); printer.printGoalLabel(os, agentNameAndPosition->first, goals); printer.printKeysLabels(os, agentNameAndPosition->first, keys); } @@ -237,7 +239,7 @@ void Grid::printToPrism(std::ostream& os, std::vector& configurat 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); + printer.printInitStruct(os, agentName, keys, lockedDoors, unlockedDoors); 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) { @@ -272,10 +274,17 @@ void Grid::printToPrism(std::ostream& os, std::vector& configurat printer.printConfiguration(os, configuration); } } - + // TODO CHANGE HANDLING + std::string agentName = agentNames.at(0); for (auto const & key : keys) { os << "\n"; - printer.printKeyModule(os, key, maxBoundaries); + printer.printKeyModule(os, key, maxBoundaries, agentName); + printer.printEndmodule(os); + } + + for (auto const& door : lockedDoors) { + os << "\n"; + printer.printDoorModule(os, door, maxBoundaries, agentName); printer.printEndmodule(os); } diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index e9d00b9..ef510ff 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -47,6 +47,7 @@ namespace prism { os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; } os << " | " << agentName << "CannotMove" << direction << "BecauseOfKey"; + os << " | " << agentName << "CannotMove" << direction << "BecauseOfDoor"; os << ";\n"; return os; } @@ -62,16 +63,16 @@ namespace prism { std::string yKey = "yKey" + keyColor; coordinates coords; - os << "!" << agentName << "_has_" << keyColor << "_key & "; + os << "(!" << agentName << "_has_" << keyColor << "_key & "; if (direction == "North") { - os << " (x" << agentName << " = " << xKey << "&y" << agentName << "-1 = " << yKey << ")"; + os << " x" << agentName << " = " << xKey << "&y" << agentName << "-1 = " << yKey << ")"; } else if (direction == "South") { - os << " (x" << agentName << " = " << xKey << "&y" << agentName << "+1 = " << yKey << ")"; + os << " x" << agentName << " = " << xKey << "&y" << agentName << "+1 = " << yKey << ")"; } else if (direction == "East") { - os << " (x" << agentName << "+1 = " << xKey << "&y" << agentName << " = " << yKey << ")"; + os << " x" << agentName << "+1 = " << xKey << "&y" << agentName << " = " << yKey << ")"; } else if (direction == "West") { - os << " (x" << agentName << "-1 = " << xKey << "&y" << agentName << " = " << yKey << ")"; + os << " x" << agentName << "-1 = " << xKey << "&y" << agentName << " = " << yKey << ")"; } else { os << "Invalid Direction! in Key Restriction"; } @@ -81,6 +82,38 @@ namespace prism { return os; } + std::ostream& PrismModulesPrinter::printDoorRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &doors) { + bool first = true; + + os << "formula " << agentName << "CannotMove" << direction << "BecauseOfDoor" << " = "; + + for (auto const& door : doors) { + if (first) first = false; + else os << " | "; + + std::string doorColor = door.getColor(); + size_t y = door.getCoordinates().first; + size_t x = door.getCoordinates().second; + + os << "(!Door" << doorColor << "open & "; + + if (direction == "North") { + os << " x" << agentName << " = " << x << "&y" << agentName << "-1 = " << y << ")"; + } else if (direction == "South") { + os << " x" << agentName << " = " << x << "&y" << agentName << "+1 = " << y << ")"; + } else if (direction == "East") { + os << " x" << agentName << "+1 = " << x << "&y" << agentName << " = " << y << ")"; + } else if (direction == "West") { + os << " x" << agentName << "-1 = " << y << "&y" << agentName << " = " << y << ")"; + } else { + os << "Invalid Direction! in Key Restriction"; + } + + } + + 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) { @@ -208,7 +241,8 @@ namespace prism { const cells &slipperyEast, const cells &slipperySouth, const cells &slipperyWest, - const cells &keys) { + const cells &keys, + const cells &doors) { printRestrictionFormula(os, agentName, "North", restrictionNorth); printRestrictionFormula(os, agentName, "East", restrictionEast); printRestrictionFormula(os, agentName, "South", restrictionSouth); @@ -220,6 +254,13 @@ namespace prism { printKeyRestrictionFormula(os, agentName, "South", keys); printKeyRestrictionFormula(os, agentName, "West", keys); } + + if (!doors.empty()) { + printDoorRestrictionFormula(os, agentName, "North", doors); + printDoorRestrictionFormula(os, agentName, "East", doors); + printDoorRestrictionFormula(os, agentName, "South", doors); + printDoorRestrictionFormula(os, agentName, "West", doors); + } printIsOnSlipperyFormula(os, agentName, slipperyCollection, slipperyNorth, slipperyEast, slipperySouth, slipperyWest); printIsInLavaFormula(os, agentName, lava); @@ -329,10 +370,10 @@ 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) + 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) ;"; - os << "\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) << "-> "; @@ -371,7 +412,7 @@ namespace prism { return os; } - std::ostream& PrismModulesPrinter::printInitStruct(std::ostream &os, const AgentName &agentName, const cells &keys) { + std::ostream& PrismModulesPrinter::printInitStruct(std::ostream &os, const AgentName &agentName, const cells &keys, const cells &lockedDoors, const cells &unlockedDoors) { os << "init\n"; os << "\t(!AgentIsInGoal & !AgentIsInLava & !AgentDone & !AgentIsOnWall)"; if(enforceOneWays) { @@ -386,6 +427,14 @@ namespace prism { os << " & ( yKey" << key.getColor() << "=" << key.row << ")"; } + for (auto const& locked : lockedDoors) { + os << " & (Door" << locked.getColor() << "locked & !Door" << locked.getColor() << "open)"; + } + + for (auto const& unlocked : unlockedDoors) { + os << " & (!Door" << unlocked.getColor() << "locked & !Door" << unlocked.getColor() << "open)"; + } + os << " & ( !" << agentName << "_is_carrying_object" << ")"; os << "\nendinit\n\n"; @@ -433,7 +482,7 @@ namespace prism { return os; } - std::ostream& PrismModulesPrinter::printKeyModule(std::ostream &os, const cell &key, const coordinates &boundaries) { + std::ostream& PrismModulesPrinter::printKeyModule(std::ostream &os, const cell &key, const coordinates &boundaries, AgentName agentName) { std::string keyIdentifier = "Key" + key.getColor(); os << "module " << keyIdentifier << "\n"; @@ -441,15 +490,14 @@ namespace prism { os << "\tx" << keyIdentifier << " : [1.." << boundaries.second << "];\n"; os << "\ty" << keyIdentifier << " : [1.." << boundaries.first << "];\n"; os << "\n"; - printKeyActions(os, key ,keyIdentifier); + printKeyActions(os, key ,keyIdentifier, agentName); os << "\n"; return os; } - std::ostream& PrismModulesPrinter::printKeyActions(std::ostream &os, const cell &key ,const std::string &keyIdentifier) { + std::ostream& PrismModulesPrinter::printKeyActions(std::ostream &os, const cell &key ,const std::string &keyIdentifier, AgentName agentName) { 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 << "(" << doorIdentifier << "locked'=false) & (" << doorIdentifier << "open'=true) ;\n"; + + os << "\t[" << "toggle_" << doorIdentifier << "]\t" << toggleGuard(agentName, door) << " -> "; + os << "(" << doorIdentifier << "open'=!" << doorIdentifier << "open) ;\n"; + + return os; + } + + std::string PrismModulesPrinter::unlockGuard(const AgentName &agentName, const cell& door) { + std::string doorColor = door.getColor(); + std::string ret; + ret += agentName + "_has_" + doorColor + "_key & "; + ret += "((" + viewVariable(agentName, 0, true) + "x" + agentName + "+ 1 = " + std::to_string(door.column) + " & y" + agentName + "= " + std::to_string(door.row) + ")"; + ret += " | (" + viewVariable(agentName, 1, true) + "x" + agentName + " = " + std::to_string(door.column) + " & y" + agentName + " + 1 = " + std::to_string(door.row) + ")"; + ret += " | (" + viewVariable(agentName, 2, true) + "x" + agentName + "- 1 = " + std::to_string(door.column) + " & y" + agentName + "= " + std::to_string(door.row) + ")"; + ret += " | (" + viewVariable(agentName, 3, true) + "x" + agentName + " = " + std::to_string(door.column) + " & y" + agentName + " - 1 = " + std::to_string(door.row) + "))"; + + + return ret; + } + + + std::string PrismModulesPrinter::toggleGuard(const AgentName &agentName, const cell& door) { + std::string doorColor = door.getColor(); + std::string ret; + + ret += "(" + viewVariable(agentName, 0, true) + "x" + agentName + "+ 1 = " + std::to_string(door.column) + " & y" + agentName + "= " + std::to_string(door.row) + ")"; + ret += " | (" + viewVariable(agentName, 1, true) + "x" + agentName + " = " + std::to_string(door.column) + " & y" + agentName + " + 1 = " + std::to_string(door.row) + ")"; + ret += " | (" + viewVariable(agentName, 2, true) + "x" + agentName + "- 1 = " + std::to_string(door.column) + " & y" + agentName + "= " + std::to_string(door.row) + ")"; + ret += " | (" + viewVariable(agentName, 3, true) + "x" + agentName + " = " + std::to_string(door.column) + " & y" + agentName + " - 1 = " + std::to_string(door.row) + ")"; + + + + return ret; + } + + std::ostream& PrismModulesPrinter::printConfiguredActions(std::ostream &os, const AgentName &agentName) { for (auto& config : configuration) { diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h index 9b208ff..01cccd7 100644 --- a/util/PrismModulesPrinter.h +++ b/util/PrismModulesPrinter.h @@ -13,6 +13,7 @@ namespace prism { 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& 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); std::ostream& printGoalLabel(std::ostream& os, const AgentName&agentName, const cells &goals); std::ostream& printCrashLabel(std::ostream &os, const std::vector agentNames); @@ -37,8 +38,15 @@ namespace prism { const cells &slipperyEast, const cells &slipperySouth, const cells &slipperyWest, - const cells &keys); - std::ostream& printKeyModule(std::ostream &os, const cell &key, const coordinates &boundaries); + const cells &keys, + const cells &doors); + + std::ostream& printKeyModule(std::ostream &os, const cell &key, const coordinates &boundaries, AgentName agentName); + std::ostream& printKeyActions(std::ostream &os, const cell& key ,const std::string &keyIdentifier, AgentName agentName); + + std::ostream& printDoorModule(std::ostream &os, const cell &door, const coordinates &boundaries, AgentName agentName); + std::ostream& printDoorActions(std::ostream &os, const cell &door ,const std::string &doorIdentifier, AgentName agentName); + /* * Representation for Slippery Tile. * -) North: Slips from North to South @@ -69,14 +77,13 @@ 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); + std::ostream& printInitStruct(std::ostream &os, const AgentName &agentName, const cells &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); 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); @@ -86,6 +93,8 @@ namespace prism { 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 unlockGuard(const AgentName &agentName, const cell& door); + std::string toggleGuard(const AgentName &agentName, const cell& door); std::string viewVariable(const AgentName &agentName, const size_t &agentDirection, const bool agentWithView);