You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

172 lines
8.3 KiB

  1. #include "PrismFormulaPrinter.h"
  2. #include <map>
  3. #include <string>
  4. #include <algorithm>
  5. std::string oneOffToString(const int &offset) {
  6. return offset != 0 ? ( offset == 1 ? "+1" : "-1" ) : "";
  7. }
  8. std::string vectorToDisjunction(const std::vector<std::string> &formulae) {
  9. bool first = true;
  10. std::string disjunction = "";
  11. for(const auto &formula : formulae) {
  12. if(first) first = false;
  13. else disjunction += " | ";
  14. disjunction += formula;
  15. }
  16. return disjunction;
  17. }
  18. std::string cellToConjunction(const AgentName &agentName, const cell &c) {
  19. return "x" + agentName + "=" + std::to_string(c.column) + "&y" + agentName + "=" + std::to_string(c.row);
  20. }
  21. std::string coordinatesToConjunction(const AgentName &agentName, const coordinates &c, const ViewDirection viewDirection) {
  22. return "x" + agentName + "=" + std::to_string(c.first) + "&y" + agentName + "=" + std::to_string(c.second) + "&view" + agentName + "=" + std::to_string(viewDirection);
  23. }
  24. std::string objectPositionToConjunction(const AgentName &agentName, const std::string &identifier, const std::pair<int, int> &relativePosition, const ViewDirection viewDirection) {
  25. std::string xOffset = oneOffToString(relativePosition.first);
  26. std::string yOffset = oneOffToString(relativePosition.second);
  27. return "x" + agentName + xOffset + "=x" + identifier + "&y" + agentName + yOffset + "=y" + identifier + "&view" + agentName + "=" + std::to_string(viewDirection);
  28. }
  29. std::map<ViewDirection, coordinates> getSurroundingCells(const cell &c) {
  30. return {{1, c.getNorth()}, {2, c.getEast()}, {3, c.getSouth()}, {0, c.getWest()}};
  31. }
  32. std::map<ViewDirection, std::pair<int, int>> getRelativeSurroundingCells() {
  33. return { {1, {0,+1}}, {2, {-1,0}}, {3, {0,-1}}, {0, {+1,0}} };
  34. }
  35. namespace prism {
  36. PrismFormulaPrinter::PrismFormulaPrinter(std::ostream &os, const std::map<std::string, cells> &restrictions, 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)
  37. : os(os), restrictions(restrictions), boxes(boxes), balls(balls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), lava(lava), goals(goals)
  38. { }
  39. void PrismFormulaPrinter::print(const AgentName &agentName) {
  40. for(const auto& [direction, cells] : restrictions) {
  41. printRestrictionFormula(agentName, direction, cells);
  42. }
  43. for(const auto& [direction, cells] : slipperyTiles) {
  44. printIsOnFormula(agentName, "Slippery", cells, direction);
  45. }
  46. std::vector<std::string> allSlipperyDirections = {agentName + "IsOnSlipperyNorth", agentName + "IsOnSlipperyEast", agentName + "IsOnSlipperySouth", agentName + "IsOnSlipperyWest"};
  47. os << buildFormula(agentName + "IsOnSlippery", vectorToDisjunction(allSlipperyDirections));
  48. printIsOnFormula(agentName, "Lava", lava);
  49. printIsOnFormula(agentName, "Goal", goals);
  50. for(const auto& ball : balls) {
  51. std::string identifier = capitalize(ball.getColor()) + ball.getType();
  52. printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp");
  53. portableObjects.push_back(agentName + "Carrying" + identifier);
  54. for(auto const c : getSurroundingCells(ball)) {
  55. std::cout << ball << std::endl;
  56. std::cout << "dir:" << c.first << " column" << c.second.first << " row" << c.second.second << std::endl;
  57. }
  58. }
  59. for(const auto& box : boxes) {
  60. std::string identifier = capitalize(box.getColor()) + box.getType();
  61. printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp");
  62. portableObjects.push_back(agentName + "Carrying" + identifier);
  63. }
  64. for(const auto& key : keys) {
  65. std::string identifier = capitalize(key.getColor()) + key.getType();
  66. printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp");
  67. portableObjects.push_back(agentName + "Carrying" + identifier);
  68. }
  69. for(const auto& door : unlockedDoors) {
  70. std::string identifier = capitalize(door.getColor()) + door.getType();
  71. printRestrictionFormulaWithCondition(agentName, identifier, getSurroundingCells(door), "!" + identifier + "Open");
  72. printIsNextToFormula(agentName, identifier, getSurroundingCells(door));
  73. }
  74. for(const auto& door : lockedDoors) {
  75. std::string identifier = capitalize(door.getColor()) + door.getType();
  76. printRestrictionFormulaWithCondition(agentName, identifier, getSurroundingCells(door), "!" + identifier + "Open");
  77. printIsNextToFormula(agentName, identifier, getSurroundingCells(door));
  78. }
  79. if(conditionalMovementRestrictions.size() > 0) {
  80. os << buildFormula(agentName + "CannotMoveConditionally", vectorToDisjunction(conditionalMovementRestrictions));
  81. os << buildFormula(agentName + "IsCarrying", vectorToDisjunction(portableObjects));
  82. }
  83. }
  84. void PrismFormulaPrinter::printRestrictionFormula(const AgentName &agentName, const std::string &direction, const cells &grid_cells) {
  85. os << buildFormula(agentName + "CannotMove" + direction + "Wall", buildDisjunction(agentName, grid_cells));
  86. }
  87. void PrismFormulaPrinter::printIsOnFormula(const AgentName &agentName, const std::string &type, const cells &grid_cells, const std::string &direction) {
  88. os << buildFormula(agentName + "IsOn" + type + direction, buildDisjunction(agentName, grid_cells));
  89. }
  90. void PrismFormulaPrinter::printIsNextToFormula(const AgentName &agentName, const std::string &type, const std::map<ViewDirection, coordinates> &coordinates) {
  91. os << buildFormula(agentName + "IsNextTo" + type, buildDisjunction(agentName, coordinates));
  92. }
  93. void PrismFormulaPrinter::printRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::map<ViewDirection, coordinates> &coordinates, const std::string &condition) {
  94. os << buildFormula(agentName + "CannotMove" + reason, "(" + buildDisjunction(agentName, coordinates) + ") & " + condition);
  95. conditionalMovementRestrictions.push_back(agentName + "CannotMove" + reason);
  96. }
  97. void PrismFormulaPrinter::printRelativeRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::string &condition) {
  98. os << buildFormula(agentName + "CannotMove" + reason, "(" + buildDisjunction(agentName, reason) + ") & " + condition);
  99. conditionalMovementRestrictions.push_back(agentName + "CannotMove" + reason);
  100. }
  101. std::string PrismFormulaPrinter::buildFormula(const std::string &formulaName, const std::string &formula) {
  102. return "formula " + formulaName + " = " + formula + ";\n";
  103. }
  104. std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const std::map<ViewDirection, coordinates> &cells) {
  105. if(cells.size() == 0) return "false";
  106. bool first = true;
  107. std::string disjunction = "";
  108. for(const auto [viewDirection, coordinates] : cells) {
  109. if(first) first = false;
  110. else disjunction += " | ";
  111. disjunction += "(" + coordinatesToConjunction(agentName, coordinates, viewDirection) + ")";
  112. }
  113. return disjunction;
  114. }
  115. std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const cells &cells, const std::vector<std::string> &conditions) {
  116. if(cells.size() == 0) return "false";
  117. bool first = true;
  118. std::string disjunction = "";
  119. if(!conditions.empty()) {
  120. for(uint index = 0; index < cells.size(); index++) {
  121. if(first) first = false;
  122. else disjunction += " | ";
  123. disjunction += "(" + cellToConjunction(agentName, cells.at(index)) + "&" + conditions.at(index) + ")";
  124. }
  125. } else {
  126. for(auto const cell : cells) {
  127. if(first) first = false;
  128. else disjunction += " | ";
  129. disjunction += "(" + cellToConjunction(agentName, cell) + ")";
  130. }
  131. }
  132. return disjunction;
  133. }
  134. std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const std::string &reason) {
  135. std::string disjunction = "";
  136. bool first = true;
  137. for(auto const [viewDirection, relativePosition] : getRelativeSurroundingCells()) {
  138. if(first) first = false;
  139. else disjunction += " | ";
  140. disjunction += "(" + objectPositionToConjunction(agentName, reason, relativePosition, viewDirection) + ")";
  141. }
  142. return disjunction;
  143. }
  144. }