diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp index 99ba5eb..29e40c4 100644 --- a/util/PrismFormulaPrinter.cpp +++ b/util/PrismFormulaPrinter.cpp @@ -4,6 +4,10 @@ #include #include +std::string oneOffToString(const int &offset) { + return offset != 0 ? ( offset == 1 ? "+1" : "-1" ) : ""; +} + std::string vectorToDisjunction(const std::vector &formulae) { bool first = true; std::string disjunction = ""; @@ -23,10 +27,20 @@ std::string coordinatesToConjunction(const AgentName &agentName, const coordinat return "x" + agentName + "=" + std::to_string(c.first) + "&y" + agentName + "=" + std::to_string(c.second) + "&view" + agentName + "=" + std::to_string(viewDirection); } +std::string objectPositionToConjunction(const AgentName &agentName, const std::string &identifier, const std::pair &relativePosition, const ViewDirection viewDirection) { + std::string xOffset = oneOffToString(relativePosition.first); + std::string yOffset = oneOffToString(relativePosition.second); + return "x" + agentName + xOffset + "=x" + identifier + "&y" + agentName + yOffset + "=y" + identifier + "&view" + agentName + "=" + std::to_string(viewDirection); +} + std::map getSurroundingCells(const cell &c) { return {{1, c.getNorth()}, {2, c.getEast()}, {3, c.getSouth()}, {0, c.getWest()}}; } +std::map> getRelativeSurroundingCells() { + return { {1, {0,+1}}, {2, {-1,0}}, {3, {0,-1}}, {0, {+1,0}} }; +} + namespace prism { PrismFormulaPrinter::PrismFormulaPrinter(std::ostream &os, const std::map &restrictions, 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) : os(os), restrictions(restrictions), boxes(boxes), balls(balls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), lava(lava), goals(goals) @@ -47,19 +61,24 @@ namespace prism { for(const auto& ball : balls) { std::string identifier = capitalize(ball.getColor()) + ball.getType(); - printRestrictionFormulaWithCondition(agentName, identifier, getSurroundingCells(ball), "!" + identifier + "PickedUp"); + printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp"); portableObjects.push_back(agentName + "Carrying" + identifier); + for(auto const c : getSurroundingCells(ball)) { + std::cout << ball << std::endl; + std::cout << "dir:" << c.first << " column" << c.second.first << " row" << c.second.second << std::endl; + + } } for(const auto& box : boxes) { std::string identifier = capitalize(box.getColor()) + box.getType(); - printRestrictionFormulaWithCondition(agentName, identifier, getSurroundingCells(box), "!" + identifier + "PickedUp"); + printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp"); portableObjects.push_back(agentName + "Carrying" + identifier); } for(const auto& key : keys) { std::string identifier = capitalize(key.getColor()) + key.getType(); - printRestrictionFormulaWithCondition(agentName, identifier, getSurroundingCells(key), "!" + identifier + "PickedUp"); + printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp"); portableObjects.push_back(agentName + "Carrying" + identifier); } @@ -98,6 +117,11 @@ 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); + } + std::string PrismFormulaPrinter::buildFormula(const std::string &formulaName, const std::string &formula) { return "formula " + formulaName + " = " + formula + ";\n"; } @@ -134,4 +158,15 @@ namespace prism { } return disjunction; } + + std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const std::string &reason) { + std::string disjunction = ""; + bool first = true; + for(auto const [viewDirection, relativePosition] : getRelativeSurroundingCells()) { + if(first) first = false; + else disjunction += " | "; + disjunction += "(" + objectPositionToConjunction(agentName, reason, relativePosition, viewDirection) + ")"; + } + return disjunction; + } } diff --git a/util/PrismFormulaPrinter.h b/util/PrismFormulaPrinter.h index d1ead81..e932587 100644 --- a/util/PrismFormulaPrinter.h +++ b/util/PrismFormulaPrinter.h @@ -7,10 +7,13 @@ #include "ConfigYaml.h" +std::string oneOffToString(const int &offset); std::string vectorToDisjunction(const std::vector &formulae); std::string cellToConjunction(const AgentName &agentName, const cell &c); std::string coordinatesToConjunction(const AgentName &agentName, const coordinates &c, const ViewDirection viewDirection); +std::string objectPositionToConjunction(const AgentName &agentName, const std::string &identifier, const std::pair &relativePosition, const ViewDirection viewDirection); std::map getSurroundingCells(const cell &c); +std::map> getRelativeSurroundingCells(); namespace prism { class PrismFormulaPrinter { @@ -23,11 +26,13 @@ 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); private: std::string buildFormula(const std::string &formulaName, const std::string &formula); std::string buildLabel(const std::string &labelName, const std::string &label); std::string buildDisjunction(const AgentName &agentName, const std::map &cells); std::string buildDisjunction(const AgentName &agentName, const cells &cells, const std::vector &conditions = {}); + std::string buildDisjunction(const AgentName &agentName, const std::string &reason); std::ostream &os; std::map restrictions;