From 389963a7c464421e19b5c74ea5e35ac37264996d Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Sun, 7 Jan 2024 19:30:21 +0100
Subject: [PATCH] added formulas to check where a robot can slip to
---
util/PrismFormulaPrinter.cpp | 95 ++++++++++++++++++++++++++----------
util/PrismFormulaPrinter.h | 13 ++++-
2 files changed, 81 insertions(+), 27 deletions(-)
diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp
index f28950a..3b4e0c9 100644
--- a/util/PrismFormulaPrinter.cpp
+++ b/util/PrismFormulaPrinter.cpp
@@ -23,10 +23,19 @@ std::string cellToConjunction(const AgentName &agentName, const cell &c) {
return "x" + agentName + "=" + std::to_string(c.column) + "&y" + agentName + "=" + std::to_string(c.row);
}
+std::string cellToConjunctionWithOffset(const AgentName &agentName, const cell &c, const std::string &xOffset, const std::string &yOffset){
+ return "x" + agentName + xOffset + "=" + std::to_string(c.column) + "&y" + agentName + yOffset + "=" + std::to_string(c.row);
+}
+
std::string coordinatesToConjunction(const AgentName &agentName, const coordinates &c, const ViewDirection viewDirection) {
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<int, int> &relativePosition) {
+ std::string xOffset = oneOffToString(relativePosition.first);
+ std::string yOffset = oneOffToString(relativePosition.second);
+ return "x" + agentName + xOffset + "=x" + identifier + "&y" + agentName + yOffset + "=y" + identifier;
+}
std::string objectPositionToConjunction(const AgentName &agentName, const std::string &identifier, const std::pair<int, int> &relativePosition, const ViewDirection viewDirection) {
std::string xOffset = oneOffToString(relativePosition.first);
std::string yOffset = oneOffToString(relativePosition.second);
@@ -41,6 +50,11 @@ std::map<ViewDirection, std::pair<int, int>> getRelativeAdjacentCells() {
return { {1, {0,+1}}, {2, {-1,0}}, {3, {0,-1}}, {0, {+1,0}} };
}
+std::map<std::string, std::pair<int, int>> getRelativeSurroundingCells() {
+ return { {"NorthWest", {-1,-1}}, {"North", { 0,-1}}, {"NorthEast", {+1,-1}},
+ {"West", {-1, 0}}, {"East", {+1, 0}},
+ {"SouthWest", {-1,+1}}, {"South", { 0,+1}}, {"SouthEast", {+1,+1}} };
+}
namespace prism {
PrismFormulaPrinter::PrismFormulaPrinter(std::ostream &os, const std::map<std::string, cells> &restrictions, const cells &walls, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const cells &lava, const cells &goals)
@@ -52,11 +66,17 @@ namespace prism {
printRestrictionFormula(agentName, direction, cells);
}
- for(const auto& [direction, cells] : slipperyTiles) {
- printIsOnFormula(agentName, "Slippery", cells, direction);
+ if(slipperyBehaviour()) {
+ for(const auto& [direction, cells] : slipperyTiles) {
+ printIsOnFormula(agentName, "Slippery", cells, direction);
+ }
+ std::vector<std::string> allSlipperyDirections = {agentName + "IsOnSlipperyNorth", agentName + "IsOnSlipperyEast", agentName + "IsOnSlipperySouth", agentName + "IsOnSlipperyWest"};
+ os << buildFormula(agentName + "IsOnSlippery", vectorToDisjunction(allSlipperyDirections));
+
+ for(const auto& [direction, relativePosition] : getRelativeSurroundingCells()) {
+ printSlipRestrictionFormula(agentName, direction);
+ }
}
- std::vector<std::string> allSlipperyDirections = {agentName + "IsOnSlipperyNorth", agentName + "IsOnSlipperyEast", agentName + "IsOnSlipperySouth", agentName + "IsOnSlipperyWest"};
- os << buildFormula(agentName + "IsOnSlippery", vectorToDisjunction(allSlipperyDirections));
printIsOnFormula(agentName, "Lava", lava);
printIsOnFormula(agentName, "Goal", goals);
@@ -64,11 +84,6 @@ 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 : getAdjacentCells(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) {
@@ -123,8 +138,27 @@ namespace prism {
conditionalMovementRestrictions.push_back(agentName + "CannotMove" + reason);
}
- std::string PrismFormulaPrinter::buildFormula(const std::string &formulaName, const std::string &formula) {
- return "formula " + formulaName + " = " + formula + ";\n";
+ void PrismFormulaPrinter::printSlipRestrictionFormula(const AgentName &agentName, const std::string &direction) {
+ std::pair<int, int> 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);
+ }
+ os << ";\n";
+ }
+
+ std::string PrismFormulaPrinter::buildFormula(const std::string &formulaName, const std::string &formula, const bool semicolon) {
+ return "formula " + formulaName + " = " + formula + (semicolon ? ";\n": "");
}
std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const std::map<ViewDirection, coordinates> &cells) {
@@ -139,23 +173,14 @@ namespace prism {
return disjunction;
}
- std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const cells &cells, const std::vector<std::string> &conditions) {
+ std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const cells &cells) {
if(cells.size() == 0) return "false";
bool first = true;
std::string disjunction = "";
- if(!conditions.empty()) {
- for(uint index = 0; index < cells.size(); index++) {
- if(first) first = false;
- else disjunction += " | ";
- disjunction += "(" + cellToConjunction(agentName, cells.at(index)) + "&" + conditions.at(index) + ")";
- }
-
- } else {
- for(auto const cell : cells) {
- if(first) first = false;
- else disjunction += " | ";
- disjunction += "(" + cellToConjunction(agentName, cell) + ")";
- }
+ for(auto const cell : cells) {
+ if(first) first = false;
+ else disjunction += " | ";
+ disjunction += "(" + cellToConjunction(agentName, cell) + ")";
}
return disjunction;
}
@@ -170,4 +195,24 @@ namespace prism {
}
return disjunction;
}
+
+ std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const cells &cells, const std::pair<int, int> &offset) {
+ std::string disjunction = "";
+ bool first = true;
+ std::string xOffset = oneOffToString(offset.first);
+ std::string yOffset = oneOffToString(offset.second);
+ for(auto const cell : cells) {
+ if(first) first = false;
+ else disjunction += " | ";
+ disjunction += "(" + cellToConjunctionWithOffset(agentName, cell, xOffset, yOffset) + ")";
+ }
+ return disjunction;
+ }
+
+ bool PrismFormulaPrinter::slipperyBehaviour() const {
+ 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();
+ }
}
diff --git a/util/PrismFormulaPrinter.h b/util/PrismFormulaPrinter.h
index f93406f..f1def2d 100644
--- a/util/PrismFormulaPrinter.h
+++ b/util/PrismFormulaPrinter.h
@@ -10,10 +10,13 @@
std::string oneOffToString(const int &offset);
std::string vectorToDisjunction(const std::vector<std::string> &formulae);
std::string cellToConjunction(const AgentName &agentName, const cell &c);
+std::string cellToConjunctionWithOffset(const AgentName &agentName, const cell &c, const std::string &xOffset, const std::string &yOffset);
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<int, int> &relativePosition);
std::string objectPositionToConjunction(const AgentName &agentName, const std::string &identifier, const std::pair<int, int> &relativePosition, const ViewDirection viewDirection);
std::map<ViewDirection, coordinates> getAdjacentCells(const cell &c);
std::map<ViewDirection, std::pair<int, int>> getRelativeAdjacentCells();
+std::map<std::string, std::pair<int, int>> getRelativeSurroundingCells();
namespace prism {
class PrismFormulaPrinter {
@@ -27,12 +30,18 @@ namespace prism {
void printIsNextToFormula(const AgentName &agentName, const std::string &type, const std::map<ViewDirection, coordinates> &coordinates);
void printRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::map<ViewDirection, coordinates> &coordinates, const std::string &condition);
void printRelativeRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::string &condition);
+ void printSlipRestrictionFormula(const AgentName &agentName, const std::string &direction);
private:
- std::string buildFormula(const std::string &formulaName, const std::string &formula);
+ std::string buildFormula(const std::string &formulaName, const std::string &formula, const bool semicolon = true);
std::string buildLabel(const std::string &labelName, const std::string &label);
std::string buildDisjunction(const AgentName &agentName, const std::map<ViewDirection, coordinates> &cells);
- std::string buildDisjunction(const AgentName &agentName, const cells &cells, const std::vector<std::string> &conditions = {});
+ std::string buildDisjunction(const AgentName &agentName, const cells &cells);
std::string buildDisjunction(const AgentName &agentName, const std::string &reason);
+ std::string buildDisjunction(const AgentName &agentName, const cells &cells, const std::pair<int, int> &offset);
+
+ bool slipperyBehaviour() const;
+ bool anyPortableObject() const;
+
std::ostream &os;
std::map<std::string, cells> restrictions;