From 48a90f07394b5c7dd7efe9eb16a1fb9562c7f367 Mon Sep 17 00:00:00 2001 From: sp Date: Sun, 7 Jan 2024 17:35:37 +0100 Subject: [PATCH] added walls to PrismFormulaPrinter also renamed methods for surrounding cells to adjacent --- util/Grid.cpp | 2 +- util/PrismFormulaPrinter.cpp | 21 +++++++++++---------- util/PrismFormulaPrinter.h | 7 ++++--- 3 files changed, 16 insertions(+), 14 deletions(-) diff --git a/util/Grid.cpp b/util/Grid.cpp index 4ccfd00..d3e2d49 100644 --- a/util/Grid.cpp +++ b/util/Grid.cpp @@ -158,7 +158,7 @@ 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, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, lava, goals); + prism::PrismFormulaPrinter formulas(os, wallRestrictions, walls, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, lava, goals); prism::PrismModulesPrinter modules(os, modelType, maxBoundaries, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, agentNameAndPositionMap, configuration, faultyProbability); modules.printModelType(modelType); diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp index 29e40c4..f28950a 100644 --- a/util/PrismFormulaPrinter.cpp +++ b/util/PrismFormulaPrinter.cpp @@ -33,17 +33,18 @@ std::string objectPositionToConjunction(const AgentName &agentName, const std::s return "x" + agentName + xOffset + "=x" + identifier + "&y" + agentName + yOffset + "=y" + identifier + "&view" + agentName + "=" + std::to_string(viewDirection); } -std::map getSurroundingCells(const cell &c) { +std::map getAdjacentCells(const cell &c) { return {{1, c.getNorth()}, {2, c.getEast()}, {3, c.getSouth()}, {0, c.getWest()}}; } -std::map> getRelativeSurroundingCells() { +std::map> getRelativeAdjacentCells() { 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) + 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) + : os(os), restrictions(restrictions), walls(walls), boxes(boxes), balls(balls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), lava(lava), goals(goals) { } void PrismFormulaPrinter::print(const AgentName &agentName) { @@ -63,7 +64,7 @@ namespace prism { std::string identifier = capitalize(ball.getColor()) + ball.getType(); printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp"); portableObjects.push_back(agentName + "Carrying" + identifier); - for(auto const c : getSurroundingCells(ball)) { + for(auto const c : getAdjacentCells(ball)) { std::cout << ball << std::endl; std::cout << "dir:" << c.first << " column" << c.second.first << " row" << c.second.second << std::endl; @@ -84,14 +85,14 @@ namespace prism { for(const auto& door : unlockedDoors) { std::string identifier = capitalize(door.getColor()) + door.getType(); - printRestrictionFormulaWithCondition(agentName, identifier, getSurroundingCells(door), "!" + identifier + "Open"); - printIsNextToFormula(agentName, identifier, getSurroundingCells(door)); + printRestrictionFormulaWithCondition(agentName, identifier, getAdjacentCells(door), "!" + identifier + "Open"); + printIsNextToFormula(agentName, identifier, getAdjacentCells(door)); } for(const auto& door : lockedDoors) { std::string identifier = capitalize(door.getColor()) + door.getType(); - printRestrictionFormulaWithCondition(agentName, identifier, getSurroundingCells(door), "!" + identifier + "Open"); - printIsNextToFormula(agentName, identifier, getSurroundingCells(door)); + printRestrictionFormulaWithCondition(agentName, identifier, getAdjacentCells(door), "!" + identifier + "Open"); + printIsNextToFormula(agentName, identifier, getAdjacentCells(door)); } if(conditionalMovementRestrictions.size() > 0) { @@ -162,7 +163,7 @@ namespace prism { std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const std::string &reason) { std::string disjunction = ""; bool first = true; - for(auto const [viewDirection, relativePosition] : getRelativeSurroundingCells()) { + for(auto const [viewDirection, relativePosition] : getRelativeAdjacentCells()) { if(first) first = false; else disjunction += " | "; disjunction += "(" + objectPositionToConjunction(agentName, reason, relativePosition, viewDirection) + ")"; diff --git a/util/PrismFormulaPrinter.h b/util/PrismFormulaPrinter.h index e932587..f93406f 100644 --- a/util/PrismFormulaPrinter.h +++ b/util/PrismFormulaPrinter.h @@ -12,13 +12,13 @@ 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(); +std::map getAdjacentCells(const cell &c); +std::map> getRelativeAdjacentCells(); namespace prism { class PrismFormulaPrinter { public: - 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); + 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); void print(const AgentName &agentName); @@ -36,6 +36,7 @@ namespace prism { std::ostream &os; std::map restrictions; + cells walls; cells boxes; cells balls; cells lockedDoors;