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.

269 lines
13 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 "col" + agentName + "=" + std::to_string(c.column) + "&row" + agentName + "=" + std::to_string(c.row);
  20. }
  21. std::string cellToConjunctionWithOffset(const AgentName &agentName, const cell &c, const std::string &xOffset, const std::string &yOffset){
  22. return "col" + agentName + xOffset + "=" + std::to_string(c.column) + "&row" + agentName + yOffset + "=" + std::to_string(c.row);
  23. }
  24. std::string coordinatesToConjunction(const AgentName &agentName, const coordinates &c, const ViewDirection viewDirection) {
  25. return "col" + agentName + "=" + std::to_string(c.first) + "&row" + agentName + "=" + std::to_string(c.second) + "&view" + agentName + "=" + std::to_string(viewDirection);
  26. }
  27. std::string objectPositionToConjunction(const AgentName &agentName, const std::string &identifier, const std::pair<int, int> &relativePosition) {
  28. std::string xOffset = oneOffToString(relativePosition.first);
  29. std::string yOffset = oneOffToString(relativePosition.second);
  30. return "col" + agentName + xOffset + "=col" + identifier + "&row" + agentName + yOffset + "=row" + identifier;
  31. }
  32. std::string objectPositionToConjunction(const AgentName &agentName, const std::string &identifier, const std::pair<int, int> &relativePosition, const ViewDirection viewDirection) {
  33. std::string xOffset = oneOffToString(relativePosition.first);
  34. std::string yOffset = oneOffToString(relativePosition.second);
  35. return "col" + agentName + xOffset + "=col" + identifier + "&row" + agentName + yOffset + "=row" + identifier + "&view" + agentName + "=" + std::to_string(viewDirection);
  36. }
  37. std::map<ViewDirection, coordinates> getAdjacentCells(const cell &c) {
  38. return {{1, c.getNorth()}, {2, c.getEast()}, {3, c.getSouth()}, {0, c.getWest()}};
  39. }
  40. std::map<ViewDirection, std::pair<int, int>> getRelativeAdjacentCells() {
  41. return { {1, {0,+1}}, {2, {-1,0}}, {3, {0,-1}}, {0, {+1,0}} };
  42. }
  43. std::map<std::string, std::pair<int, int>> getRelativeSurroundingCells() {
  44. return { {"NorthWest", {-1,-1}}, {"North", { 0,-1}}, {"NorthEast", {+1,-1}},
  45. {"West", {-1, 0}}, {"East", {+1, 0}},
  46. {"SouthWest", {-1,+1}}, {"South", { 0,+1}}, {"SouthEast", {+1,+1}} };
  47. }
  48. namespace prism {
  49. 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, const AgentNameAndPositionMap &agentNameAndPositionMap, const bool faulty)
  50. : 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)
  51. { }
  52. void PrismFormulaPrinter::print(const AgentName &agentName) {
  53. conditionalMovementRestrictions.clear();
  54. for(const auto& [direction, cells] : restrictions) {
  55. printRestrictionFormula(agentName, direction, cells);
  56. }
  57. if(slipperyBehaviour()) {
  58. for(const auto& [direction, cells] : slipperyTiles) {
  59. printIsOnFormula(agentName, "Slippery", cells, direction);
  60. }
  61. std::vector<std::string> allSlipperyDirections = {agentName + "IsOnSlipperyNorth", agentName + "IsOnSlipperyEast", agentName + "IsOnSlipperySouth", agentName + "IsOnSlipperyWest"};
  62. os << buildFormula(agentName + "IsOnSlippery", vectorToDisjunction(allSlipperyDirections));
  63. for(const auto& [direction, relativePosition] : getRelativeSurroundingCells()) {
  64. printSlipRestrictionFormula(agentName, direction);
  65. }
  66. } else {
  67. os << buildFormula(agentName + "IsOnSlippery", "false");
  68. }
  69. if(!lava.empty()) printIsOnFormula(agentName, "Lava", lava);
  70. if(!goals.empty()) printIsOnFormula(agentName, "Goal", goals);
  71. for(const auto& ball : balls) {
  72. std::string identifier = capitalize(ball.getColor()) + ball.getType();
  73. printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp");
  74. portableObjects.push_back(agentName + "Carrying" + identifier);
  75. }
  76. for(const auto& box : boxes) {
  77. std::string identifier = capitalize(box.getColor()) + box.getType();
  78. printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp");
  79. portableObjects.push_back(agentName + "Carrying" + identifier);
  80. }
  81. for(const auto& key : keys) {
  82. std::string identifier = capitalize(key.getColor()) + key.getType();
  83. printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp");
  84. portableObjects.push_back(agentName + "Carrying" + identifier);
  85. }
  86. for(const auto& door : unlockedDoors) {
  87. std::string identifier = capitalize(door.getColor()) + door.getType();
  88. printRestrictionFormulaWithCondition(agentName, identifier, getAdjacentCells(door), "!" + identifier + "Open");
  89. printIsNextToFormula(agentName, identifier, getAdjacentCells(door));
  90. }
  91. for(const auto& door : lockedDoors) {
  92. std::string identifier = capitalize(door.getColor()) + door.getType();
  93. printRestrictionFormulaWithCondition(agentName, identifier, getAdjacentCells(door), "!" + identifier + "Open");
  94. printIsNextToFormula(agentName, identifier, getAdjacentCells(door));
  95. }
  96. if(conditionalMovementRestrictions.size() > 0) {
  97. os << buildFormula(agentName + "CannotMoveConditionally", vectorToDisjunction(conditionalMovementRestrictions));
  98. os << buildFormula(agentName + "IsCarrying", vectorToDisjunction(portableObjects));
  99. }
  100. }
  101. void PrismFormulaPrinter::printRestrictionFormula(const AgentName &agentName, const std::string &direction, const cells &grid_cells) {
  102. os << buildFormula(agentName + "CannotMove" + direction + "Wall", buildDisjunction(agentName, grid_cells));
  103. }
  104. void PrismFormulaPrinter::printIsOnFormula(const AgentName &agentName, const std::string &type, const cells &grid_cells, const std::string &direction) {
  105. os << buildFormula(agentName + "IsOn" + type + direction, buildDisjunction(agentName, grid_cells));
  106. }
  107. void PrismFormulaPrinter::printIsNextToFormula(const AgentName &agentName, const std::string &type, const std::map<ViewDirection, coordinates> &coordinates) {
  108. os << buildFormula(agentName + "IsNextTo" + type, buildDisjunction(agentName, coordinates));
  109. }
  110. void PrismFormulaPrinter::printRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::map<ViewDirection, coordinates> &coordinates, const std::string &condition) {
  111. os << buildFormula(agentName + "CannotMove" + reason, "(" + buildDisjunction(agentName, coordinates) + ") & " + condition);
  112. conditionalMovementRestrictions.push_back(agentName + "CannotMove" + reason);
  113. }
  114. void PrismFormulaPrinter::printRelativeRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::string &condition) {
  115. os << buildFormula(agentName + "CannotMove" + reason, "(" + buildDisjunction(agentName, reason) + ") & " + condition);
  116. conditionalMovementRestrictions.push_back(agentName + "CannotMove" + reason);
  117. }
  118. void PrismFormulaPrinter::printSlipRestrictionFormula(const AgentName &agentName, const std::string &direction) {
  119. std::pair<int, int> slipCell = getRelativeSurroundingCells().at(direction);
  120. bool semicolon = anyPortableObject() ? false : true;
  121. os << buildFormula(agentName + "CannotSlip" + direction, buildDisjunction(agentName, walls, slipCell), semicolon);
  122. for(auto const key : keys) {
  123. std::string identifier = capitalize(key.getColor()) + key.getType();
  124. os << " | " << objectPositionToConjunction(agentName, identifier, slipCell);
  125. }
  126. for(auto const ball : balls) {
  127. std::string identifier = capitalize(ball.getColor()) + ball.getType();
  128. os << " | " << objectPositionToConjunction(agentName, identifier, slipCell);
  129. }
  130. for(auto const box : boxes) {
  131. std::string identifier = capitalize(box.getColor()) + box.getType();
  132. os << " | " << objectPositionToConjunction(agentName, identifier, slipCell);
  133. }
  134. if(!semicolon) os << ";\n";
  135. }
  136. void PrismFormulaPrinter::printCollisionFormula(const AgentName &agentName) {
  137. if(!agentNameAndPositionMap.empty()) {
  138. os << "formula collision = ";
  139. bool first = true;
  140. for(auto const [name, coordinates] : agentNameAndPositionMap) {
  141. if(name == agentName) continue;
  142. if(first) first = false;
  143. else os << " | ";
  144. os << "(col"+agentName+"=col"+name+"&row"+agentName+"=row"+name+")";
  145. }
  146. os << ";\n";
  147. printCollisionLabel();
  148. }
  149. }
  150. void PrismFormulaPrinter::printCollisionLabel() {
  151. if(!agentNameAndPositionMap.empty()) {
  152. os << "label \"collision\" = collision;\n";
  153. }
  154. }
  155. void PrismFormulaPrinter::printInitStruct() {
  156. os << "init\n";
  157. bool first = true;
  158. for(auto const [a, coordinates] : agentNameAndPositionMap) {
  159. if(first) first = false;
  160. else os << " & ";
  161. os << "(col"+a+"="+std::to_string(coordinates.first)+"&row"+a+"="+std::to_string(coordinates.second)+" & ";
  162. os << "(view"+a+"=0|view"+a+"=1|view"+a+"=2|view"+a+"=3) ";
  163. if(faulty) os << " & previousAction"+a+"="+std::to_string(NOFAULT);
  164. os << ")";
  165. }
  166. for(auto const ball : balls) {
  167. std::string identifier = capitalize(ball.getColor()) + ball.getType();
  168. os << " & (col"+identifier+"="+std::to_string(ball.column)+"&row"+identifier+"="+std::to_string(ball.row)+"&"+identifier+"PickedUp=false) ";
  169. }
  170. for(auto const key : keys) {
  171. std::string identifier = capitalize(key.getColor()) + key.getType();
  172. os << " & (col"+identifier+"="+std::to_string(key.column)+"&row"+identifier+"="+std::to_string(key.row)+"&"+identifier+"PickedUp=false) ";
  173. }
  174. for(auto const box : boxes) {
  175. std::string identifier = capitalize(box.getColor()) + box.getType();
  176. os << " & (col"+identifier+"="+std::to_string(box.column)+"&row"+identifier+"="+std::to_string(box.row)+"&"+identifier+"PickedUp=false) ";
  177. }
  178. os << "endinit\n\n";
  179. }
  180. std::string PrismFormulaPrinter::buildFormula(const std::string &formulaName, const std::string &formula, const bool semicolon) {
  181. return "formula " + formulaName + " = " + formula + (semicolon ? ";\n": "");
  182. }
  183. std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const std::map<ViewDirection, coordinates> &cells) {
  184. if(cells.size() == 0) return "false";
  185. bool first = true;
  186. std::string disjunction = "";
  187. for(const auto [viewDirection, coordinates] : cells) {
  188. if(first) first = false;
  189. else disjunction += " | ";
  190. disjunction += "(" + coordinatesToConjunction(agentName, coordinates, viewDirection) + ")";
  191. }
  192. return disjunction;
  193. }
  194. std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const cells &cells) {
  195. if(cells.size() == 0) return "false";
  196. bool first = true;
  197. std::string disjunction = "";
  198. for(auto const cell : cells) {
  199. if(first) first = false;
  200. else disjunction += " | ";
  201. disjunction += "(" + cellToConjunction(agentName, cell) + ")";
  202. }
  203. return disjunction;
  204. }
  205. std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const std::string &reason) {
  206. std::string disjunction = "";
  207. bool first = true;
  208. for(auto const [viewDirection, relativePosition] : getRelativeAdjacentCells()) {
  209. if(first) first = false;
  210. else disjunction += " | ";
  211. disjunction += "(" + objectPositionToConjunction(agentName, reason, relativePosition, viewDirection) + ")";
  212. }
  213. return disjunction;
  214. }
  215. std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const cells &cells, const std::pair<int, int> &offset) {
  216. std::string disjunction = "";
  217. bool first = true;
  218. std::string xOffset = oneOffToString(offset.first);
  219. std::string yOffset = oneOffToString(offset.second);
  220. for(auto const cell : cells) {
  221. if(first) first = false;
  222. else disjunction += " | ";
  223. disjunction += "(" + cellToConjunctionWithOffset(agentName, cell, xOffset, yOffset) + ")";
  224. }
  225. return disjunction;
  226. }
  227. bool PrismFormulaPrinter::slipperyBehaviour() const {
  228. return !slipperyTiles.at("North").empty() || !slipperyTiles.at("East").empty() || !slipperyTiles.at("South").empty() || !slipperyTiles.at("West").empty();
  229. }
  230. bool PrismFormulaPrinter::anyPortableObject() const {
  231. return !keys.empty() || !boxes.empty() || !balls.empty();
  232. }
  233. }