From 8cc2b0c4da9abcc17edf54d9414fed0cb6da225e Mon Sep 17 00:00:00 2001 From: sp Date: Sat, 20 Jan 2024 13:09:22 +0100 Subject: [PATCH] portable objects are now traversable This is also changes keys to not be dropable anymore. --- util/Grid.cpp | 4 +-- util/PrismFormulaPrinter.cpp | 44 ++++------------------- util/PrismFormulaPrinter.h | 6 ++-- util/PrismModulesPrinter.cpp | 70 +++++++++++++++--------------------- util/PrismModulesPrinter.h | 8 ++--- 5 files changed, 41 insertions(+), 91 deletions(-) diff --git a/util/Grid.cpp b/util/Grid.cpp index 91366b2..8f83703 100644 --- a/util/Grid.cpp +++ b/util/Grid.cpp @@ -154,8 +154,8 @@ void Grid::printToPrism(std::ostream& os, std::vector& configurat [](const std::map::value_type &pair){return pair.first;}); std::string agentName = agentNames.at(0); - prism::PrismFormulaPrinter formulas(os, wallRestrictions, walls, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, lava, goals, agentNameAndPositionMap, faultyProbability > 0.0); - prism::PrismModulesPrinter modules(os, modelType, maxBoundaries, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, agentNameAndPositionMap, configuration, probIntended, faultyProbability, !lava.empty(), !goals.empty()); + prism::PrismFormulaPrinter formulas(os, wallRestrictions, walls, lockedDoors, unlockedDoors, keys, slipperyTiles, lava, goals, agentNameAndPositionMap, faultyProbability > 0.0); + prism::PrismModulesPrinter modules(os, modelType, maxBoundaries, lockedDoors, unlockedDoors, keys, slipperyTiles, agentNameAndPositionMap, configuration, probIntended, faultyProbability, !lava.empty(), !goals.empty()); modules.printModelType(modelType); for(const auto &agentName : agentNames) { diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp index e50b2f4..bbb9a0c 100644 --- a/util/PrismFormulaPrinter.cpp +++ b/util/PrismFormulaPrinter.cpp @@ -57,8 +57,8 @@ std::map> getRelativeSurroundingCells() { } namespace prism { - PrismFormulaPrinter::PrismFormulaPrinter(std::ostream &os, const std::map &restrictions, const cells &walls, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map &slipperyTiles, const cells &lava, const cells &goals, const AgentNameAndPositionMap &agentNameAndPositionMap, const bool faulty) - : os(os), restrictions(restrictions), walls(walls), boxes(boxes), balls(balls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), lava(lava), goals(goals), agentNameAndPositionMap(agentNameAndPositionMap), faulty(faulty) + PrismFormulaPrinter::PrismFormulaPrinter(std::ostream &os, const std::map &restrictions, const cells &walls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map &slipperyTiles, const cells &lava, const cells &goals, const AgentNameAndPositionMap &agentNameAndPositionMap, const bool faulty) + : os(os), restrictions(restrictions), walls(walls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), lava(lava), goals(goals), agentNameAndPositionMap(agentNameAndPositionMap), faulty(faulty) { } void PrismFormulaPrinter::print(const AgentName &agentName) { @@ -83,21 +83,10 @@ namespace prism { if(!lava.empty()) printIsOnFormula(agentName, "Lava", lava); if(!goals.empty()) printIsOnFormula(agentName, "Goal", goals); - for(const auto& ball : balls) { - std::string identifier = capitalize(ball.getColor()) + ball.getType(); - printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp"); - portableObjects.push_back(agentName + "Carrying" + identifier); - } - - for(const auto& box : boxes) { - std::string identifier = capitalize(box.getColor()) + box.getType(); - printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp"); - portableObjects.push_back(agentName + "Carrying" + identifier); - } for(const auto& key : keys) { std::string identifier = capitalize(key.getColor()) + key.getType(); - printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp"); + printRelativeIsInFrontOfFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp"); portableObjects.push_back(agentName + "Carrying" + identifier); } @@ -136,27 +125,14 @@ namespace prism { conditionalMovementRestrictions.push_back(agentName + "CannotMove" + reason); } - void PrismFormulaPrinter::printRelativeRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::string &condition) { - os << buildFormula(agentName + "CannotMove" + reason, "(" + buildDisjunction(agentName, reason) + ") & " + condition); - conditionalMovementRestrictions.push_back(agentName + "CannotMove" + reason); + void PrismFormulaPrinter::printRelativeIsInFrontOfFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::string &condition) { + os << buildFormula(agentName + "IsInFrontOf" + reason, "(" + buildDisjunction(agentName, reason) + ") & " + condition); } void PrismFormulaPrinter::printSlipRestrictionFormula(const AgentName &agentName, const std::string &direction) { std::pair slipCell = getRelativeSurroundingCells().at(direction); bool semicolon = anyPortableObject() ? false : true; os << buildFormula(agentName + "CannotSlip" + direction, buildDisjunction(agentName, walls, slipCell), semicolon); - for(auto const key : keys) { - std::string identifier = capitalize(key.getColor()) + key.getType(); - os << " | " << objectPositionToConjunction(agentName, identifier, slipCell); - } - for(auto const ball : balls) { - std::string identifier = capitalize(ball.getColor()) + ball.getType(); - os << " | " << objectPositionToConjunction(agentName, identifier, slipCell); - } - for(auto const box : boxes) { - std::string identifier = capitalize(box.getColor()) + box.getType(); - os << " | " << objectPositionToConjunction(agentName, identifier, slipCell); - } if(!semicolon) os << ";\n"; } @@ -192,18 +168,10 @@ namespace prism { if(faulty) os << " & previousAction"+a+"="+std::to_string(NOFAULT); os << ")"; } - for(auto const ball : balls) { - std::string identifier = capitalize(ball.getColor()) + ball.getType(); - os << " & (col"+identifier+"="+std::to_string(ball.column)+"&row"+identifier+"="+std::to_string(ball.row)+"&"+identifier+"PickedUp=false) "; - } for(auto const key : keys) { std::string identifier = capitalize(key.getColor()) + key.getType(); os << " & (col"+identifier+"="+std::to_string(key.column)+"&row"+identifier+"="+std::to_string(key.row)+"&"+identifier+"PickedUp=false) "; } - for(auto const box : boxes) { - std::string identifier = capitalize(box.getColor()) + box.getType(); - os << " & (col"+identifier+"="+std::to_string(box.column)+"&row"+identifier+"="+std::to_string(box.row)+"&"+identifier+"PickedUp=false) "; - } os << "endinit\n\n"; } @@ -264,6 +232,6 @@ namespace prism { return !slipperyTiles.at("North").empty() || !slipperyTiles.at("East").empty() || !slipperyTiles.at("South").empty() || !slipperyTiles.at("West").empty(); } bool PrismFormulaPrinter::anyPortableObject() const { - return !keys.empty() || !boxes.empty() || !balls.empty(); + return !keys.empty(); } } diff --git a/util/PrismFormulaPrinter.h b/util/PrismFormulaPrinter.h index 8e24578..e0c5a62 100644 --- a/util/PrismFormulaPrinter.h +++ b/util/PrismFormulaPrinter.h @@ -21,7 +21,7 @@ std::map> getRelativeSurroundingCells(); namespace prism { class PrismFormulaPrinter { public: - PrismFormulaPrinter(std::ostream &os, const std::map &restrictions, const cells &walls, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map &slipperyTiles, const cells &lava, const cells &goals, const AgentNameAndPositionMap &agentNameAndPositionMap, const bool faulty); + PrismFormulaPrinter(std::ostream &os, const std::map &restrictions, const cells &walls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map &slipperyTiles, const cells &lava, const cells &goals, const AgentNameAndPositionMap &agentNameAndPositionMap, const bool faulty); void print(const AgentName &agentName); @@ -29,7 +29,7 @@ namespace prism { void printIsOnFormula(const AgentName &agentName, const std::string &type, const cells &grid_cells, const std::string &direction = ""); void printIsNextToFormula(const AgentName &agentName, const std::string &type, const std::map &coordinates); void printRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::map &coordinates, const std::string &condition); - void printRelativeRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::string &condition); + void printRelativeIsInFrontOfFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::string &condition); void printSlipRestrictionFormula(const AgentName &agentName, const std::string &direction); void printCollisionFormula(const std::string &agentName); @@ -51,8 +51,6 @@ namespace prism { std::ostream &os; std::map restrictions; cells walls; - cells boxes; - cells balls; cells lockedDoors; cells unlockedDoors; cells keys; diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index 5b6ddd1..01c8431 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -11,8 +11,8 @@ std::string westUpdate(const AgentName &a) { return "(col"+a+"'=col"+a+"-1)"; } namespace prism { - 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 std::map &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector config, const float probIntended, const float faultyProbability, const bool anyLava, const bool anyGoals) - : os(os), modelType(modelType), maxBoundaries(maxBoundaries), boxes(boxes), balls(balls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), agentNameAndPositionMap(agentNameAndPositionMap), configuration(config), probIntended(probIntended), faultyProbability(faultyProbability), anyLava(anyLava), anyGoals(anyGoals) { + PrismModulesPrinter::PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector config, const float probIntended, const float faultyProbability, const bool anyLava, const bool anyGoals) + : os(os), modelType(modelType), maxBoundaries(maxBoundaries), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), agentNameAndPositionMap(agentNameAndPositionMap), configuration(config), probIntended(probIntended), faultyProbability(faultyProbability), anyLava(anyLava), anyGoals(anyGoals) { numberOfPlayer = agentNameAndPositionMap.size(); size_t index = 0; for(auto begin = agentNameAndPositionMap.begin(); begin != agentNameAndPositionMap.end(); begin++, index++) { @@ -40,12 +40,6 @@ namespace prism { for(const auto &key : keys) { printPortableObjectModule(key); } - for(const auto &ball : balls) { - printPortableObjectModule(ball); - } - for(const auto &box : boxes) { - printPortableObjectModule(box); - } for(const auto &door : unlockedDoors) { printDoorModule(door, true); } @@ -110,22 +104,24 @@ namespace prism { os << "endmodule\n\n"; } - void PrismModulesPrinter::printPortableObjectActions(const std::string &agentName, const std::string &identifier) { + void PrismModulesPrinter::printPortableObjectActions(const std::string &agentName, const std::string &identifier, const bool canBeDroped) { std::string actionName = "[" + agentName + "_pickup_" + identifier + "]"; - agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); + agentNameActionMap.at(agentName).insert({PICKUP, actionName}); os << " " << actionName << " true -> (col" << identifier << "'=-1) & (row" << identifier << "'=-1) & (" << identifier << "PickedUp'=true);\n"; - actionName = "[" + agentName + "_drop_" + identifier + "_north]"; - agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); - os << " " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << ") & (row" << identifier << "'=row" << agentName << "-1) & (" << identifier << "PickedUp'=false);\n"; - actionName = "[" + agentName + "_drop_" + identifier + "_west]"; - agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); - os << " " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << "-1) & (row" << identifier << "'=row" << agentName << ") & (" << identifier << "PickedUp'=false);\n"; - actionName = "[" + agentName + "_drop_" + identifier + "_south]"; - agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); - os << " " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << ") & (row" << identifier << "'=row" << agentName << "+1) & (" << identifier << "PickedUp'=false);\n"; - actionName = "[" + agentName + "_drop_" + identifier + "_east]"; - agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); - os << " " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << "+1) & (row" << identifier << "'=row" << agentName << ") & (" << identifier << "PickedUp'=false);\n"; + if(canBeDroped) { + actionName = "[" + agentName + "_drop_" + identifier + "_north]"; + agentNameActionMap.at(agentName).insert({DROP, actionName}); + os << " " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << ") & (row" << identifier << "'=row" << agentName << "-1) & (" << identifier << "PickedUp'=false);\n"; + actionName = "[" + agentName + "_drop_" + identifier + "_west]"; + agentNameActionMap.at(agentName).insert({DROP, actionName}); + os << " " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << "-1) & (row" << identifier << "'=row" << agentName << ") & (" << identifier << "PickedUp'=false);\n"; + actionName = "[" + agentName + "_drop_" + identifier + "_south]"; + agentNameActionMap.at(agentName).insert({DROP, actionName}); + os << " " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << ") & (row" << identifier << "'=row" << agentName << "+1) & (" << identifier << "PickedUp'=false);\n"; + actionName = "[" + agentName + "_drop_" + identifier + "_east]"; + agentNameActionMap.at(agentName).insert({DROP, actionName}); + os << " " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << "+1) & (row" << identifier << "'=row" << agentName << ") & (" << identifier << "PickedUp'=false);\n"; + } } void PrismModulesPrinter::printDoorModule(const cell &door, const bool &opened) { @@ -191,18 +187,6 @@ namespace prism { printPortableObjectActionsForRobot(agentName, identifier); } - for(const auto &ball : balls) { - std::string identifier = capitalize(ball.getColor()) + ball.getType(); - os << " " << agentName << "Carrying" << identifier << " : bool;\n"; - printPortableObjectActionsForRobot(agentName, identifier); - } - - for(const auto &box : boxes) { - std::string identifier = capitalize(box.getColor()) + box.getType(); - os << " " << agentName << "Carrying" << identifier << " : bool;\n"; - printPortableObjectActionsForRobot(agentName, identifier); - } - printNonMovementActionsForRobot(agentName); @@ -213,13 +197,15 @@ namespace prism { os << "endmodule\n\n"; } - void PrismModulesPrinter::printPortableObjectActionsForRobot(const std::string &a, const std::string &i) { - actionStream << " [" << a << "_pickup_" << i << "] " << " !" << a << "IsCarrying & " << a << "CannotMove" << i << " -> (" << a << "Carrying" << i << "'=true);\n"; - actionStream << " [" << a << "_drop_" << i << "_north]\t" << a << "Carrying" << i << " & view" << a << "=3 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveNorthWall -> (" << a << "Carrying" << i << "'=false);\n"; - actionStream << " [" << a << "_drop_" << i << "_west] \t" << a << "Carrying" << i << " & view" << a << "=2 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveWestWall -> (" << a << "Carrying" << i << "'=false);\n"; - actionStream << " [" << a << "_drop_" << i << "_south]\t" << a << "Carrying" << i << " & view" << a << "=1 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveSouthWall -> (" << a << "Carrying" << i << "'=false);\n"; - actionStream << " [" << a << "_drop_" << i << "_east] \t" << a << "Carrying" << i << " & view" << a << "=0 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveEastWall -> (" << a << "Carrying" << i << "'=false);\n"; - actionStream << "\n"; + void PrismModulesPrinter::printPortableObjectActionsForRobot(const std::string &a, const std::string &i, const bool canBeDroped) { + actionStream << " [" << a << "_pickup_" << i << "] " << " !" << a << "IsCarrying & " << a << "IsInFrontOf" << i << " -> (" << a << "Carrying" << i << "'=true);\n"; + if(canBeDroped) { + actionStream << " [" << a << "_drop_" << i << "_north]\t" << a << "Carrying" << i << " & view" << a << "=3 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveNorthWall -> (" << a << "Carrying" << i << "'=false);\n"; + actionStream << " [" << a << "_drop_" << i << "_west] \t" << a << "Carrying" << i << " & view" << a << "=2 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveWestWall -> (" << a << "Carrying" << i << "'=false);\n"; + actionStream << " [" << a << "_drop_" << i << "_south]\t" << a << "Carrying" << i << " & view" << a << "=1 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveSouthWall -> (" << a << "Carrying" << i << "'=false);\n"; + actionStream << " [" << a << "_drop_" << i << "_east] \t" << a << "Carrying" << i << " & view" << a << "=0 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveEastWall -> (" << a << "Carrying" << i << "'=false);\n"; + actionStream << "\n"; + } } void PrismModulesPrinter::printUnlockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier) { @@ -636,7 +622,7 @@ namespace prism { } bool PrismModulesPrinter::anyPortableObject() const { - return !keys.empty() || !boxes.empty() || !balls.empty(); + return !keys.empty(); } bool PrismModulesPrinter::faultyBehaviour() const { diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h index 16d562b..618833a 100644 --- a/util/PrismModulesPrinter.h +++ b/util/PrismModulesPrinter.h @@ -16,7 +16,7 @@ std::string westUpdate(const AgentName &a); namespace prism { class PrismModulesPrinter { public: - 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 std::map &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector config, const float probIntended, const float faultyProbability, const bool anyLava, const bool anyGoals); + PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector config, const float probIntended, const float faultyProbability, const bool anyLava, const bool anyGoals); std::ostream& print(); @@ -26,14 +26,14 @@ namespace prism { bool isGame() const; private: void printPortableObjectModule(const cell &object); - void printPortableObjectActions(const std::string &agentName, const std::string &identifier); + void printPortableObjectActions(const std::string &agentName, const std::string &identifier, const bool canBeDroped = false); 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 printPortableObjectActionsForRobot(const std::string &agentName, const std::string &identifier, const bool canBeDroped = false); void printUnlockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier); void printLockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier, const std::string &key); void printMovementActionsForRobot(const std::string &a); @@ -92,8 +92,6 @@ namespace prism { ModelType const &modelType; coordinates const &maxBoundaries; AgentName agentName; - cells boxes; - cells balls; cells lockedDoors; cells unlockedDoors; cells keys;