From ca70595b58fdb3cbd8e5ccc98d9c9687d8d67c09 Mon Sep 17 00:00:00 2001 From: sp Date: Sat, 6 Jan 2024 18:35:59 +0100 Subject: [PATCH] WIP major rework of PrismModulesPrinter will probably get squashed, otw summary in later commit --- util/PrismModulesPrinter.cpp | 576 ++++++++--------------------------- util/PrismModulesPrinter.h | 72 ++--- 2 files changed, 161 insertions(+), 487 deletions(-) diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index 9b20dc0..1f26d89 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -5,11 +5,12 @@ 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), viewDirectionMapping({{0, "East"}, {1, "South"}, {2, "West"}, {3, "North"}}) { + PrismModulesPrinter::PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector config, const bool enforceOneWays) + : os(os), modelType(modelType), maxBoundaries(maxBoundaries), boxes(boxes), balls(balls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), agentNameAndPositionMap(agentNameAndPositionMap), enforceOneWays(enforceOneWays), configuration(config), viewDirectionMapping({{0, "East"}, {1, "South"}, {2, "West"}, {3, "North"}}) { + numberOfPlayer = agentNameAndPositionMap.size(); } - std::ostream& PrismModulesPrinter::printModel(std::ostream &os, const ModelType &modelType) { + std::ostream& PrismModulesPrinter::printModelType(const ModelType &modelType) { switch(modelType) { case(ModelType::MDP): os << "mdp"; @@ -22,394 +23,52 @@ namespace prism { return os; } - std::ostream& PrismModulesPrinter::printBackgroundLabels(std::ostream &os, const AgentName &agentName, const std::pair &backgroundTiles) { - if(backgroundTiles.second.size() == 0) return os; - - bool first = true; - std::string color = getColor(backgroundTiles.first); - color.at(0) = std::toupper(color.at(0)); - os << "formula " << agentName << "On" << color << " = "; - for(auto const& cell : backgroundTiles.second) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; - } - os << ";\n"; - os << "label \"" << agentName << "On" << color << "\" = " << agentName << "On" << color << ";\n"; - return os; - } - - 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 : grid_cells) { - if(first) first = false; - else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; - } - - if (!keys.empty()) { - os << " | " << agentName << "CannotMove" << direction << "BecauseOfKey"; - } - if (!doors.empty()) { - os << " | " << agentName << "CannotMove" << direction << "BecauseOfDoor"; - } - - 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 << " | "; - 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") { - os << " x" << agentName << " = " << xKey << "&y" << agentName << "-1 = " << yKey << ")"; - } else if (direction == "South") { - os << " x" << agentName << " = " << xKey << "&y" << agentName << "+1 = " << yKey << ")"; - } else if (direction == "East") { - os << " x" << agentName << "+1 = " << xKey << "&y" << agentName << " = " << yKey << ")"; - } else if (direction == "West") { - os << " x" << agentName << "-1 = " << xKey << "&y" << agentName << " = " << yKey << ")"; - } else { - os << "Invalid Direction! in Key Restriction"; - } - } - - os << ";\n"; - 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) { - if(std::find_if(slipperyCollection.cbegin(), slipperyCollection.cend(), [=](const std::reference_wrapper& c) { return !c.get().empty(); }) == slipperyCollection.cend()) { - os << "formula " << agentName << "IsOnSlippery = false;\n"; - return os; - } - - bool first = true; - if (!slipperyNorth.empty()) { - os << "formula " << agentName << "IsOnSlipperyNorth = "; - for (const auto& cell : slipperyNorth) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; - } - os << ";\n"; - } - - if (!slipperyEast.empty()) { - first = true; - os << "formula " << agentName << "IsOnSlipperyEast = "; - for (const auto& cell : slipperyEast) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; - } - os << ";\n"; - + std::ostream& PrismModulesPrinter::print() { + for(const auto &key : keys) { + printPortableObjectModule(key); } - - if (!slipperySouth.empty()) { - first = true; - os << "formula " << agentName << "IsOnSlipperySouth = "; - for (const auto& cell : slipperySouth) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; - } - os << ";\n"; - } - - if (!slipperyWest.empty()) { - first = true; - os << "formula " << agentName << "IsOnSlipperyWest = "; - for (const auto& cell : slipperyWest) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; - } - os << ";\n"; - } - - first = true; - os << "formula " << agentName << "IsOnSlippery = "; - - for (const auto& slippery: slipperyCollection) { - for(const auto& cell : slippery.get()) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; - } - } - os << ";\n"; - if(enforceOneWays) { - first = true; - os << "formula " << agentName << "IsOnSlipperyNorth = "; - - for (const auto& cell: slipperyNorth) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; - } - os << ";\n"; - first = true; - os << "formula " << agentName << "IsOnSlipperyEast = "; - - for (const auto& cell: slipperyEast) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; - } - os << ";\n"; - first = true; - os << "formula " << agentName << "IsOnSlipperySouth = "; - - for (const auto& cell: slipperySouth) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; - } - os << ";\n"; - first = true; - os << "formula " << agentName << "IsOnSlipperyWest = "; - for (const auto& cell: slipperyWest) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; - } - os << ";\n"; - } - return os; - } - - std::ostream& PrismModulesPrinter::printIsInLavaFormula(std::ostream& os, const AgentName &agentName, const cells &lava) { - if(lava.size() == 0) { - os << "formula " << agentName << "IsInLava = false;\n"; - return os; - } - bool first = true; - os << "formula " << agentName << "IsInLava = "; - for(auto const& cell : lava) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; - } - os << ";\n"; - os << "formula " << agentName << "IsInLavaAndNotDone = " << agentName << "IsInLava & !" << agentName << "Done;\n"; - os << "label \"" << agentName << "IsInLavaAndNotDone\" = " << agentName << "IsInLava & !" << agentName << "Done;\n"; - return os; - } - - std::ostream& PrismModulesPrinter::printTurningNotAllowedFormulas(std::ostream& os, const AgentName &agentName, const cells &noTurnFloor) { - if( (!enforceOneWays or noTurnFloor.size() == 0) or (noTurnFloor.size() == 0) ) { - os << "formula " << agentName << "CannotTurn = false;\n"; - return os; - } - bool first = true; - os << "formula " << agentName << "CannotTurn = "; - for(auto const& cell : noTurnFloor) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; - } - os << " | " << agentName << "IsOnSlippery;\n"; - return os; - } - - std::ostream& PrismModulesPrinter::printIsFixedFormulas(std::ostream& os, const AgentName &agentName) { - os << "formula " << agentName << "IsFixed = false;\n"; - os << "formula " << agentName << "SlipperyTurnLeftAllowed = true;\n"; - os << "formula " << agentName << "SlipperyTurnRightAllowed = true;\n"; - os << "formula " << agentName << "SlipperyMoveForwardAllowed = true;\n"; - os << "label \"FixedStates" << agentName << "\" = " << agentName << "IsFixed | !" << agentName << "SlipperyTurnRightAllowed | !" << agentName << "SlipperyTurnLeftAllowed | !" << agentName << "SlipperyMoveForwardAllowed | " << agentName << "IsInGoal | " << agentName << "IsInLava"; - if(enforceOneWays) { - os << " | " << agentName << "CannotTurn"; - } - os << ";\n"; - //os << "label \"FixedStates\" = " << agentName << "IsFixed | " << agentName << "IsOnSlippery | " << agentName << "IsInGoal | " << agentName << "IsInLava;\n"; - - return os; - } - - - std::ostream& PrismModulesPrinter::printWallFormula(std::ostream& os, const AgentName &agentName, const cells &walls) { - os << "formula " << agentName << "IsOnWall = "; - bool first = true; - for(auto const& cell : walls) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; + for(const auto &ball : balls) { + printPortableObjectModule(ball); } - os << ";\n"; - return os; - } - - std::ostream& PrismModulesPrinter::printFormulas(std::ostream& os, - const AgentName &agentName, - const cells &restrictionNorth, - const cells &restrictionEast, - const cells &restrictionSouth, - const cells &restrictionWest, - const std::vector> &slipperyCollection, - const cells &lava, - const cells &walls, - const cells &noTurnFloor, - const cells &slipperyNorth, - const cells &slipperyEast, - const cells &slipperySouth, - const cells &slipperyWest, - const cells &keys, - const cells &doors) { - 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); - printKeyRestrictionFormula(os, agentName, "East", keys); - printKeyRestrictionFormula(os, agentName, "South", keys); - printKeyRestrictionFormula(os, agentName, "West", keys); + for(const auto &box : boxes) { + printPortableObjectModule(box); } - - if (!doors.empty()) { - printDoorRestrictionFormula(os, agentName, "North", doors); - printDoorRestrictionFormula(os, agentName, "East", doors); - printDoorRestrictionFormula(os, agentName, "South", doors); - printDoorRestrictionFormula(os, agentName, "West", doors); + for(const auto &door : unlockedDoors) { + printDoorModule(door, true); } - - printIsOnSlipperyFormula(os, agentName, slipperyCollection, slipperyNorth, slipperyEast, slipperySouth, slipperyWest); - printIsInLavaFormula(os, agentName, lava); - printWallFormula(os, agentName, walls); - printTurningNotAllowedFormulas(os, agentName, noTurnFloor); - printIsFixedFormulas(os, agentName); - os << "\n"; - return os; - } - - std::ostream& PrismModulesPrinter::printGoalLabel(std::ostream& os, const AgentName &agentName, const cells &goals) { - if(goals.size() == 0) { - os << "formula " << agentName << "IsInGoal = false;\n"; - return os; + for(const auto &door : lockedDoors) { + printDoorModule(door, false); } - bool first = true; - os << "formula " << agentName << "IsInGoal = "; - for(auto const& cell : goals) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; + for(const auto [agentName, initialPosition] : agentNameAndPositionMap) { + printRobotModule(agentName, initialPosition); } - os << ";\n"; - os << "formula " << agentName << "IsInGoalAndNotDone = " << agentName << "IsInGoal & !" << agentName << "Done;\n"; - os << "label \"" << agentName << "IsInGoalAndNotDone\" = " << agentName << "IsInGoal & !" << agentName << "Done;\n"; return os; } - std::ostream& PrismModulesPrinter::printCrashLabel(std::ostream &os, const std::vector agentNames) { - os << "label crash = "; - bool first = true; - for(auto const& agentName : agentNames) { - if(agentName == "Agent") continue; - if(first) first = false; else os << " | "; - os << "(xAgent=x" << agentName << ")&(yAgent=y" << agentName << ")"; - } - os << ";\n\n"; - return os; - } std::ostream& PrismModulesPrinter::printConfiguration(std::ostream& os, const std::vector& configurations) { - for (auto& configuration : configurations) { if (configuration.overwrite_ || configuration.type_ == ConfigType::Module) { continue; } - os << configuration.expression_ << std::endl; } - return os; } std::ostream& PrismModulesPrinter::printConstants(std::ostream &os, const std::vector &constants) { - for (auto& constant : constants) { os << constant << std::endl; } - - return os; - } - - - std::ostream& PrismModulesPrinter::printAvoidanceLabel(std::ostream &os, const std::vector agentNames, const int &distance) { - os << "label avoidance = "; - bool first = true; - for(auto const& agentName : agentNames) { - if(agentName == "Agent") continue; - if(first) first = false; else os << " | "; - os << "max(xAgent-x" << agentName << ",x" << agentName << "-xAgent)+"; - os << "max(yAgent-y" << agentName << ",y" << agentName << "-yAgent) "; - } - os << ";\n\n"; return os; } - // TODO this does not account for multiple agents yet, i.e. key can be picked up multiple times - std::ostream& PrismModulesPrinter::printKeysLabels(std::ostream& os, const AgentName &agentName, const cells &keys) { - if(keys.size() == 0) return os; - - for(auto const& key : keys) { - 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 << " = 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"; - return os; - } std::ostream& PrismModulesPrinter::printBooleansForKeys(std::ostream &os, const AgentName &agentName, const cells &keys) { for(auto const& key : keys) { os << "\t" << agentName << "_has_"<< key.getColor() << "_key : bool;\n";//init false;\n"; } - - os << "\n"; return os; } @@ -432,7 +91,7 @@ namespace prism { os << "\t[pickup_" << keyColor << "_key]\t" << pickupGuard(agentName, keyColor) << "-> "; 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) << "-> "; os << "(" << agentName << "_has_" << keyColor << "_key'=false) & (" << agentName << "_is_carrying_object'=false);\n"; @@ -472,7 +131,7 @@ namespace prism { std::ostream& PrismModulesPrinter::printInitStruct(std::ostream &os, const AgentNameAndPositionMap &agents, const KeyNameAndPositionMap &keys, const cells &lockedDoors, const cells &unlockedDoors, prism::ModelType modelType) { os << "init\n"; os << "\t"; - + bool first = true; for (auto const& agent : agents) { if (first) first = false; @@ -483,14 +142,14 @@ namespace prism { if(enforceOneWays) { os << " & ( !AgentCannotTurn ) "; } else { - // os << " & ( !AgentIsOnSlippery ) "; + // os << " & ( !AgentIsOnSlippery ) "; } for (auto const& key : keys) { os << " & ( !" << agent.first << "_has_" << key.first << "_key )"; } } - + for (auto const& key : keys) { os << " & ( xKey" << key.first << "="<< key.second.second<< ")"; os << " & ( yKey" << key.first << "=" << key.second.first << ")"; @@ -505,13 +164,13 @@ namespace prism { } if (modelType == ModelType::SMG) { - os << " & move=0"; + os << " & move=0"; } os << "\nendinit\n\n"; - + return os; } @@ -529,9 +188,9 @@ namespace prism { os << "\n"; if (faultyProbability != 0.0) { os << "\t[" << agentName << "_turn_right] " << moveGuard(agentIndex) << " !" << agentName << "CannotTurn & " << " !" << agentName << "IsFixed & " << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & !" << agentName << "IsOnSlippery -> " << 100 - faultyProbability << "/100:" << "(view" << agentName << "'=mod(view" << agentName << " + 1, 4))" << moveUpdate(agentIndex) << "\n + " << faultyProbability << "/100:" << "(view" << agentName << "'=mod(view" << agentName << " + 2, 4))" << ";\n"; - os << "\t[" << agentName << "_turn_left] " << moveGuard(agentIndex) << " !" << agentName << "CannotTurn & " << " !" << agentName << "IsFixed & " << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & !" << agentName << "IsOnSlippery & view" << agentName << ">1 -> " << 100 - faultyProbability << "/100:" << "(view" << agentName << "'=mod(view" << agentName << " - 1, 4))" << moveUpdate(agentIndex) << "\n + " << faultyProbability << "/100:" << "(view" << agentName << "'=mod(view" << agentName << " - 2, 4))" << ";\n"; - os << "\t[" << agentName << "_turn_left] " << moveGuard(agentIndex) << " !" << agentName << "CannotTurn & " << " !" << agentName << "IsFixed & " << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & !" << agentName << "IsOnSlippery & view" << agentName << "=0 -> " << 100 - faultyProbability << "/100:" << "(view" << agentName << "'=3)" << moveUpdate(agentIndex) << "\n + " << faultyProbability << "/100:" << "(view" << agentName << "'=2)" << ";\n"; - os << "\t[" << agentName << "_turn_left] " << moveGuard(agentIndex) << " !" << agentName << "CannotTurn & " << " !" << agentName << "IsFixed & " << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & !" << agentName << "IsOnSlippery & view" << agentName << "=1 -> " << 100 - faultyProbability << "/100:" << "(view" << agentName << "'=0)" << moveUpdate(agentIndex) << "\n + " << faultyProbability << "/100:" << "(view" << agentName << "'=3)" << ";\n"; + os << "\t[" << agentName << "_turn_left] " << moveGuard(agentIndex) << " !" << agentName << "CannotTurn & " << " !" << agentName << "IsFixed & " << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & !" << agentName << "IsOnSlippery & view" << agentName << ">1 -> " << 100 - faultyProbability << "/100:" << "(view" << agentName << "'=mod(view" << agentName << " - 1, 4))" << moveUpdate(agentIndex) << "\n + " << faultyProbability << "/100:" << "(view" << agentName << "'=mod(view" << agentName << " - 2, 4))" << ";\n"; + os << "\t[" << agentName << "_turn_left] " << moveGuard(agentIndex) << " !" << agentName << "CannotTurn & " << " !" << agentName << "IsFixed & " << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & !" << agentName << "IsOnSlippery & view" << agentName << "=0 -> " << 100 - faultyProbability << "/100:" << "(view" << agentName << "'=3)" << moveUpdate(agentIndex) << "\n + " << faultyProbability << "/100:" << "(view" << agentName << "'=2)" << ";\n"; + os << "\t[" << agentName << "_turn_left] " << moveGuard(agentIndex) << " !" << agentName << "CannotTurn & " << " !" << agentName << "IsFixed & " << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & !" << agentName << "IsOnSlippery & view" << agentName << "=1 -> " << 100 - faultyProbability << "/100:" << "(view" << agentName << "'=0)" << moveUpdate(agentIndex) << "\n + " << faultyProbability << "/100:" << "(view" << agentName << "'=3)" << ";\n"; } else { os << "\t[" << agentName << "_turn_right] " << moveGuard(agentIndex) << " !" << agentName << "CannotTurn & " << " !" << agentName << "IsFixed & " << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & !" << agentName << "IsOnSlippery -> (view" << agentName << "'=mod(view" << agentName << " + 1, 4)) " << moveUpdate(agentIndex) << ";\n"; os << "\t[" << agentName << "_turn_left] " << moveGuard(agentIndex) << " !" << agentName << "CannotTurn & " << " !" << agentName << "IsFixed & " << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & !" << agentName << "IsOnSlippery & view" << agentName << ">0 -> (view" << agentName << "'=view" << agentName << " - 1) " << moveUpdate(agentIndex) << ";\n"; @@ -562,93 +221,118 @@ namespace prism { return os; } - 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"; - - os << "\tx" << keyIdentifier << " : [-1.." << boundaries.second << "];\n"; - os << "\ty" << keyIdentifier << " : [-1.." << boundaries.first << "];\n"; + void PrismModulesPrinter::printPortableObjectModule(const cell &object) { + std::string identifier = capitalize(object.getColor()) + object.getType(); + os << "\nmodule " << identifier << std::endl; + os << "\tx" << identifier << " : [-1.." << maxBoundaries.second << "] init " << object.column << ";\n"; + os << "\ty" << identifier << " : [-1.." << maxBoundaries.first << "] init " << object.row << ";\n"; + os << "\t" << identifier << "PickedUp : bool;\n"; os << "\n"; - printKeyActions(os, key ,keyIdentifier, agentName); - os << "\n"; - return os; + for(const auto [name, position] : agentNameAndPositionMap) { + printPortableObjectActions(name, identifier); + } + os << "endmodule\n\n"; } - - 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"; + void PrismModulesPrinter::printPortableObjectActions(const std::string &agentName, const std::string &identifier) { + os << "\t[" << agentName << "_pickup_" << identifier << "]\ttrue -> (x" << identifier << "'=-1) & (y" << identifier << "'=-1) & (" << identifier << "PickedUp'=true);\n"; + os << "\t[" << agentName << "_drop_" << identifier << "_north]\ttrue -> (x" << identifier << "'=x" << agentName << ") & (y" << identifier << "'=y" << agentName << "-1) & (" << identifier << "PickedUp'=false);\n"; + os << "\t[" << agentName << "_drop_" << identifier << "_west]\ttrue -> (x" << identifier << "'=x" << agentName << "-1) & (y" << identifier << "'=y" << agentName << ") & (" << identifier << "PickedUp'=false);\n"; + os << "\t[" << agentName << "_drop_" << identifier << "_south]\ttrue -> (x" << identifier << "'=x" << agentName << ") & (y" << identifier << "'=y" << agentName << "+1) & (" << identifier << "PickedUp'=false);\n"; + os << "\t[" << agentName << "_drop_" << identifier << "_east]\ttrue -> (x" << identifier << "'=x" << agentName << "+1) & (y" << identifier << "'=y" << agentName << ") & (" << identifier << "PickedUp'=false);\n"; + } - 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" < (" << identifier << "Open'=true);\n"; + os << "\t[" << agentName << "_close_" << identifier << "] " << identifier << "Open -> (" << identifier << "Open'=false);\n"; + } - return os; + void PrismModulesPrinter::printUnlockedDoorActions(const std::string &agentName, const std::string &identifier) { + os << "\t[" << agentName << "_open_" << identifier << "] !" << identifier << "Open -> (" << identifier << "Open'=true);\n"; + os << "\t[" << agentName << "_close_" << identifier << "] " << identifier << "Open -> (" << identifier << "Open'=false);\n"; } - std::ostream& PrismModulesPrinter::printDoorModule(std::ostream &os, const cell &door, const coordinates &boundaries, AgentName agent) { - std::string doorIdentifier = "Door" + door.getColor(); - os << "module " << doorIdentifier << "\n"; - - os << "\t" << doorIdentifier << "locked : bool;\n"; - os << "\t" << doorIdentifier << "open : bool;\n"; + void PrismModulesPrinter::printRobotModule(const AgentName &agentName, const coordinates &initialPosition) { + os << "\nmodule " << agentName << std::endl; + os << "\tx" << agentName << " : [0.." << maxBoundaries.second << "] init " << initialPosition.second << ";\n"; + os << "\ty" << agentName << " : [0.." << maxBoundaries.first << "] init " << initialPosition.first << ";\n"; + os << "\tview" << agentName << " : [0..3] init 1;\n"; - printDoorActions(os, door, doorIdentifier, agent); - - return os; - } + for(const auto &door : unlockedDoors) { + std::string identifier = capitalize(door.getColor()) + door.getType(); + printUnlockedDoorActionsForRobot(agentName, identifier); + } - std::ostream& PrismModulesPrinter::printDoorActions(std::ostream &os, const cell &door ,const std::string &doorIdentifier, AgentName agentName) { - os << "\t[" << "unlock_" << doorIdentifier << "]\t" << unlockGuard(agentName, door) << " -> "; - os << "(" << doorIdentifier << "locked'=false) & (" << doorIdentifier << "open'=true) ;\n"; + for(const auto &door : lockedDoors) { + std::string identifier = capitalize(door.getColor()) + door.getType(); + std::string key = capitalize(door.getColor()) + "Key"; + printLockedDoorActionsForRobot(agentName, identifier, key); + } - os << "\t[" << "toggle_" << doorIdentifier << "]\t" << toggleGuard(agentName, door) << " -> "; - os << "(" << doorIdentifier << "open'=!" << doorIdentifier << "open) ;\n"; + for(const auto &key : keys) { + std::string identifier = capitalize(key.getColor()) + key.getType(); + os << "\tCarrying" << identifier << " : bool init false;\n"; + printPortableObjectActionsForRobot(agentName, identifier); + } - return os; + os << "\n" << actionStream.str(); + os << "endmodule\n\n"; } - 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; + void PrismModulesPrinter::printPortableObjectActionsForRobot(const std::string &a, const std::string &i) { + actionStream << "\t[" << a << "_pickup_" << i << "] " << a << "CannotMove" << i << " -> (Carrying" << i << "'=true);\n"; + actionStream << "\t[" << a << "_drop_" << i << "_north]\tCarrying" << i << " & view" << a << "=3 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveNorthWall -> (Carrying" << i << "'=false);\n"; + actionStream << "\t[" << a << "_drop_" << i << "_west] \tCarrying" << i << " & view" << a << "=2 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveWestWall -> (Carrying" << i << "'=false);\n"; + actionStream << "\t[" << a << "_drop_" << i << "_south]\tCarrying" << i << " & view" << a << "=1 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveSouthWall -> (Carrying" << i << "'=false);\n"; + actionStream << "\t[" << a << "_drop_" << i << "_east] \tCarrying" << i << " & view" << a << "=0 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveEastWall -> (Carrying" << i << "'=false);\n"; + actionStream << "\n"; } + void PrismModulesPrinter::printUnlockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier) { + actionStream << "\t[" << agentName << "_open_" << identifier << "] " << agentName << "CannotMove" << identifier << " -> true;\n"; + actionStream << "\t[" << agentName << "_close_" << identifier << "] " << agentName << "IsNextTo" << identifier << " -> true;\n"; + actionStream << "\n"; + } - std::string PrismModulesPrinter::toggleGuard(const AgentName &agentName, const cell& door) { - std::string doorColor = door.getColor(); - std::string ret; - ret += "!Door" + doorColor + "locked & ("; - 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; + void PrismModulesPrinter::printLockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier, const std::string &key) { + actionStream << "\t[" << agentName << "_unlock_" << identifier << "] " << agentName << "CannotMove" << identifier << " & Carrying" << key << " -> true;\n"; + actionStream << "\t[" << agentName << "_close_" << identifier << "] " << agentName << "IsNextTo" << identifier << " & Carrying" << key << " -> true;\n"; + actionStream << "\n"; } + + + + + + + + + + + std::ostream& PrismModulesPrinter::printConfiguredActions(std::ostream &os, const AgentName &agentName) { for (auto& config : configuration) { if (config.type_ == ConfigType::Module && !config.overwrite_ && agentName == config.module_) { @@ -661,7 +345,7 @@ namespace prism { return os; } - std::ostream& PrismModulesPrinter::printMovementActions(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const bool agentWithView, const float &probability, const double &stickyProbability) { + std::ostream& PrismModulesPrinter::printMovementActions(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const bool agentWithView, const float &probability, const double &stickyProbability) { if(stickyProbability != 0.0) { os << "\t[" << agentName << "_move_north]" << moveGuard(agentIndex) << viewVariable(agentName, 3, agentWithView) << " !" << agentName << "IsFixed & " << " !" << agentName << "IsOnSlippery & !" << agentName << "IsInLava &!" << agentName << "IsInGoal & !" << agentName << "CannotMoveNorth -> " << (100 - stickyProbability) << "/100:" << "(y" << agentName << "'=y" << agentName << "-1)" << moveUpdate(agentIndex) << "\n+ " << (stickyProbability) << "/100:" << "(y" << agentName << "'=max(y" << agentName << "-2, 1 ))" << moveUpdate(agentIndex) << ";\n"; os << "\t[" << agentName << "_move_east] " << moveGuard(agentIndex) << viewVariable(agentName, 0, agentWithView) << " !" << agentName << "IsFixed & " << " !" << agentName << "IsOnSlippery & !" << agentName << "IsInLava &!" << agentName << "IsInGoal & !" << agentName << "CannotMoveEast -> " << (100 - stickyProbability) << "/100:" << "(x" << agentName << "'=x" << agentName << "+1)" << moveUpdate(agentIndex) << "\n+ " << (stickyProbability) << "/100:" << "(x" << agentName << "'=min(x" << agentName << "+2, width))" << moveUpdate(agentIndex) << ";\n"; @@ -835,7 +519,7 @@ namespace prism { std::array prob_piece_dir_constants_agent_east; std::array prob_piece_dir_constants_agent_south; std::array prob_piece_dir_constants_agent_west; - + switch (orientation) { case SlipperyType::North: @@ -849,12 +533,12 @@ namespace prism { prob_piece_dir_agent_west = { 0, 0, 0, 0, 0, 2, 0 /* <- R */, 0 }; prob_piece_dir_constants = { "prop_zero", "prop_zero", "prop_displacement * 1/2", "prop_displacement", "prop_zero" /* <- R */, "prop_displacement", "prop_displacement * 1/2", "prop_zero" }; - + prob_piece_dir_constants_agent_north = { "prop_zero", "prop_zero", "prop_zero", "prop_displacement * 1/2", "prop_zero" /* <- R */, "prop_displacement * 1/2", "prop_zero", "prop_zero" }; prob_piece_dir_constants_agent_east = { "prop_zero", "prop_zero", "prop_zero", "prop_displacement", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" }; prob_piece_dir_constants_agent_south = { "prop_displacement", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" } ; prob_piece_dir_constants_agent_west ={ "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_displacement", "prop_zero", "prop_zero" } ; - + straightPosIndex = 4; straightPosIndex_east = 2; @@ -868,25 +552,25 @@ namespace prism { case SlipperyType::South: actionName = "\t[" + agentName + "move_on_slip_south]"; positionGuard = "\t" + agentName + "IsOnSlipperySouth"; - + prob_piece_dir = { 0 /* <- R */, 2, 1, 0, 0, 0, 1, 2 }; // { n, ne, e, se, s, sw, w, nw } prob_piece_dir_agent_north = { 0 /*n <- R */, 1, 0, 0, 0, 0, 0, 1}; prob_piece_dir_agent_east = { 0, 2, 0 /*e <- R */, 0, 0, 0, 0, 0 }; prob_piece_dir_agent_south = { 2, 0, 0, 0, 0 /*s <- R */, 0, 0, 0 }; prob_piece_dir_agent_west = { 0, 0, 0, 0, 0, 0, 0 /* <- R */, 2 }; - + prob_piece_dir_constants = { "prop_zero" /* <- R */, "prop_displacement", "prop_displacement * 1/2", "prop_zero", "prop_zero", "prop_zero", "prop_displacement * 1/2", "prop_displacement" }; - + prob_piece_dir_constants_agent_north = { "prop_zero", "prop_displacement * 1/2", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_displacement * 1/2" }; prob_piece_dir_constants_agent_east = { "prop_zero", "prop_displacement", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" }; prob_piece_dir_constants_agent_south = { "prop_displacement", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" } ; prob_piece_dir_constants_agent_west ={ "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_displacement" } ; - + straightPosIndex = 0; // always north straightPosIndex_east = 2; - straightPosIndex_south = 4; + straightPosIndex_south = 4; straightPosIndex_west = 6; straightPosIndex_north = 0; specialTransition = "(y" + agentName + "'=y" + agentName + (!neighborhood.at(straightPosIndex) ? ")" : "-1)"); @@ -911,10 +595,10 @@ namespace prism { prob_piece_dir_constants_agent_south = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_displacement * 1/2", "prop_displacement * 1/2", "prop_zero" } ; prob_piece_dir_constants_agent_west ={ "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_displacement * 1/2", "prop_zero", "prop_displacement * 1/2" } ; - + straightPosIndex = 6; straightPosIndex_east = 2; - straightPosIndex_south = 4; + straightPosIndex_south = 4; straightPosIndex_west = 6; straightPosIndex_north = 0; @@ -934,7 +618,7 @@ namespace prism { prob_piece_dir_agent_west = { 0, 0, 0, 0, 0, 0, 0 /* <- R */, 2 }; prob_piece_dir_constants = {"prop_displacement * 1/2", "prop_displacement", "prop_zero" /* <- R */, "prop_displacement", "prop_displacement * 1/2", "prop_zero","prop_zero", "prop_zero" }; - + prob_piece_dir_constants_agent_north = { "prop_zero", "prop_displacement * 1/2", "prop_displacement * 1/2", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" }; prob_piece_dir_constants_agent_east = { "prop_zero", "prop_displacement * 1/2", "prop_zero", "prop_displacement * 1/2", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" }; prob_piece_dir_constants_agent_south = { "prop_zero", "prop_zero", "prop_displacement * 1/2", "prop_displacement * 1/2", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" } ; @@ -943,7 +627,7 @@ namespace prism { straightPosIndex = 2; straightPosIndex_east = 2; - straightPosIndex_south = 4; + straightPosIndex_south = 4; straightPosIndex_west = 6; straightPosIndex_north = 0; specialTransition = "(x" + agentName + "'=x" + agentName + (!neighborhood.at(straightPosIndex) ? ")" : "+1)"); @@ -988,14 +672,14 @@ namespace prism { // generic output (for every view and every possible view direction) size_t current_dir = 0; // East os << actionName << moveGuard(agentIndex) << " x" << agentName << "=" << c.second << " & y" << agentName << "=" << c.first << " & " << agentName << "SlipperyMoveForwardAllowed " << "& " << "view" << agentName << "=" << current_dir; - + for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS; i++) { os << (i == 0 ? " -> " : " + ") << prob_piece_dir_constants_agent_east.at(i) << " : " << positionTransition.at(i) << moveUpdate(agentIndex) << (i == ALL_POSS_DIRECTIONS - 1 ? ";\n" : "\n"); } current_dir = 1; // South os << actionName << moveGuard(agentIndex) << " x" << agentName << "=" << c.second << " & y" << agentName << "=" << c.first << " & " << agentName << "SlipperyMoveForwardAllowed " << "& " << "view" << agentName << "=" << current_dir; - + for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS; i++) { os << (i == 0 ? " -> " : " + ") << prob_piece_dir_constants_agent_south.at(i) << " : " << positionTransition.at(i) << moveUpdate(agentIndex) << (i == ALL_POSS_DIRECTIONS - 1 ? ";\n" : "\n"); } @@ -1009,7 +693,7 @@ namespace prism { current_dir = 3; // North - + os << actionName << moveGuard(agentIndex) << " x" << agentName << "=" << c.second << " & y" << agentName << "=" << c.first << " & " << agentName << "SlipperyMoveForwardAllowed " << "& " << "view" << agentName << "=" << current_dir; for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS; i++) { os << (i == 0 ? " -> " : " + ") << prob_piece_dir_constants_agent_north.at(i) << " : " << positionTransition.at(i) << moveUpdate(agentIndex) << (i == ALL_POSS_DIRECTIONS - 1 ? ";\n" : "\n"); diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h index 9e5936c..460aa67 100644 --- a/util/PrismModulesPrinter.h +++ b/util/PrismModulesPrinter.h @@ -9,43 +9,25 @@ namespace prism { class PrismModulesPrinter { 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 &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); - std::ostream& printGoalLabel(std::ostream& os, const AgentName&agentName, const cells &goals); - std::ostream& printCrashLabel(std::ostream &os, const std::vector agentNames); - std::ostream& printAvoidanceLabel(std::ostream &os, const std::vector agentNames, const int &distance); - std::ostream& printKeysLabels(std::ostream& os, const AgentName&agentName, const cells &keys); - std::ostream& printBackgroundLabels(std::ostream &os, const AgentName &agentName, const std::pair &backgroundTiles); - std::ostream& printIsInLavaFormula(std::ostream& os, const AgentName &agentName, const cells &lava); - std::ostream& printIsFixedFormulas(std::ostream& os, const AgentName &agentName); - std::ostream& printTurningNotAllowedFormulas(std::ostream& os, const AgentName &agentName, const cells &floor); - std::ostream& printWallFormula(std::ostream& os, const AgentName &agentName, const cells &walls); - std::ostream& printFormulas(std::ostream& os, - const AgentName&agentName, - const cells &restrictionNorth, - const cells &restrictionEast, - const cells &restrictionSouth, - const cells &restrictionWest, - const std::vector> &slipperyCollection, - const cells &lava, - const cells &walls, - const cells &noTurnFloor, - const cells &slipperyNorth, - const cells &slipperyEast, - const cells &slipperySouth, - const cells &slipperyWest, - 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); + PrismModulesPrinter(std::ostream &os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector config, const bool enforceOneWays = false); + + std::ostream& print(); + + std::ostream& printModelType(const ModelType &modelType); + + void printPortableObjectModule(const cell &object); + void printPortableObjectActions(const std::string &agentName, const std::string &identifier); + + void printDoorModule(const cell &object, const bool &opened); + void printLockedDoorActions(const std::string &agentName, const std::string &identifier); + void printUnlockedDoorActions(const std::string &agentName, const std::string &identifier); + + void printRobotModule(const AgentName &agentName, const coordinates &initialPosition); + void printPortableObjectActionsForRobot(const std::string &agentName, const std::string &identifier); + + void printUnlockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier); + void printLockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier, const std::string &key); + std::ostream& printConstants(std::ostream &os, const std::vector &constants); /* * Representation for Slippery Tile. @@ -72,7 +54,6 @@ namespace prism { */ std::ostream& printSlipperyTurn(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const coordinates &c, std::set &slipperyActions, const std::array& neighborhood, SlipperyType orientation); - std::ostream& printModel(std::ostream &os, const ModelType &modelType); std::ostream& printBooleansForKeys(std::ostream &os, const AgentName &agentName, const cells &keys); 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); @@ -102,16 +83,25 @@ 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); bool isGame() const; private: + std::ostream &os; + std::stringstream actionStream; ModelType const& modelType; - const size_t numberOfPlayer; + coordinates const& maxBoundaries; + AgentName agentName; + cells boxes; + cells balls; + cells lockedDoors; + cells unlockedDoors; + cells keys; + + AgentNameAndPositionMap agentNameAndPositionMap; + size_t numberOfPlayer; bool enforceOneWays; std::vector configuration; std::map viewDirectionMapping;