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.

658 lines
46 KiB

10 months ago
10 months ago
10 months ago
10 months ago
10 months ago
  1. #include "PrismModulesPrinter.h"
  2. #include <map>
  3. #include <string>
  4. #define NOFAULT -1
  5. #define LEFT 0
  6. #define RIGHT 1
  7. #define FORWARD 2
  8. std::string northUpdate(const AgentName &a) { return "(y"+a+"'=y"+a+"-1)"; }
  9. std::string southUpdate(const AgentName &a) { return "(y"+a+"'=y"+a+"+1)"; }
  10. std::string eastUpdate(const AgentName &a) { return "(x"+a+"'=x"+a+"+1)"; }
  11. std::string westUpdate(const AgentName &a) { return "(x"+a+"'=x"+a+"-1)"; }
  12. namespace prism {
  13. PrismModulesPrinter::PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector<Configuration> config, const float probIntended, const float faultyProbability)
  14. : os(os), modelType(modelType), maxBoundaries(maxBoundaries), boxes(boxes), balls(balls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), agentNameAndPositionMap(agentNameAndPositionMap), configuration(config), probIntended(probIntended), faultyProbability(faultyProbability) {
  15. numberOfPlayer = agentNameAndPositionMap.size();
  16. size_t index = 0;
  17. for(auto begin = agentNameAndPositionMap.begin(); begin != agentNameAndPositionMap.end(); begin++, index++) {
  18. agentIndexMap[begin->first] = index;
  19. }
  20. }
  21. void PrismModulesPrinter::printModelType(const ModelType &modelType) {
  22. switch(modelType) {
  23. case(ModelType::MDP):
  24. os << "mdp";
  25. break;
  26. case(ModelType::SMG):
  27. os << "smg";
  28. break;
  29. }
  30. os << "\n\n";
  31. }
  32. std::ostream& PrismModulesPrinter::print() {
  33. for(const auto [agentName, initialPosition] : agentNameAndPositionMap) {
  34. agentNameActionMap[agentName] = {};
  35. }
  36. for(const auto &key : keys) {
  37. printPortableObjectModule(key);
  38. }
  39. for(const auto &ball : balls) {
  40. printPortableObjectModule(ball);
  41. }
  42. for(const auto &box : boxes) {
  43. printPortableObjectModule(box);
  44. }
  45. for(const auto &door : unlockedDoors) {
  46. printDoorModule(door, true);
  47. }
  48. for(const auto &door : lockedDoors) {
  49. printDoorModule(door, false);
  50. }
  51. for(const auto [agentName, initialPosition] : agentNameAndPositionMap) {
  52. printRobotModule(agentName, initialPosition);
  53. }
  54. if(faultyBehaviour()) {
  55. for(const auto [agentName, initialPosition] : agentNameAndPositionMap) {
  56. printFaultyMovementModule(agentName);
  57. }
  58. }
  59. return os;
  60. }
  61. void PrismModulesPrinter::printConfiguration(const std::vector<Configuration>& configurations) {
  62. for (auto& configuration : configurations) {
  63. if (configuration.overwrite_ || configuration.type_ == ConfigType::Module) {
  64. continue;
  65. }
  66. os << configuration.expression_ << std::endl;
  67. }
  68. }
  69. void PrismModulesPrinter::printConstants(const std::vector<std::string> &constants) {
  70. for (auto& constant : constants) {
  71. os << constant << std::endl;
  72. }
  73. }
  74. void PrismModulesPrinter::printPortableObjectModule(const cell &object) {
  75. std::string identifier = capitalize(object.getColor()) + object.getType();
  76. os << "\nmodule " << identifier << std::endl;
  77. os << "\tx" << identifier << " : [-1.." << maxBoundaries.second << "] init " << object.column << ";\n";
  78. os << "\ty" << identifier << " : [-1.." << maxBoundaries.first << "] init " << object.row << ";\n";
  79. os << "\t" << identifier << "PickedUp : bool;\n";
  80. os << "\n";
  81. for(const auto [name, position] : agentNameAndPositionMap) {
  82. printPortableObjectActions(name, identifier);
  83. }
  84. os << "endmodule\n\n";
  85. }
  86. void PrismModulesPrinter::printPortableObjectActions(const std::string &agentName, const std::string &identifier) {
  87. std::string actionName = "[" + agentName + "_pickup_" + identifier + "]";
  88. agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
  89. os << "\t" << actionName << " true -> (x" << identifier << "'=-1) & (y" << identifier << "'=-1) & (" << identifier << "PickedUp'=true);\n";
  90. actionName = "[" + agentName + "_drop_" + identifier + "_north]";
  91. agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
  92. os << "\t" << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << ") & (y" << identifier << "'=y" << agentName << "-1) & (" << identifier << "PickedUp'=false);\n";
  93. actionName = "[" + agentName + "_drop_" + identifier + "_west]";
  94. agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
  95. os << "\t" << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << "-1) & (y" << identifier << "'=y" << agentName << ") & (" << identifier << "PickedUp'=false);\n";
  96. actionName = "[" + agentName + "_drop_" + identifier + "_south]";
  97. agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
  98. os << "\t" << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << ") & (y" << identifier << "'=y" << agentName << "+1) & (" << identifier << "PickedUp'=false);\n";
  99. actionName = "[" + agentName + "_drop_" + identifier + "_east]";
  100. agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
  101. os << "\t" << actionName << " " << " ttrue -> (x" << identifier << "'=x" << agentName << "+1) & (y" << identifier << "'=y" << agentName << ") & (" << identifier << "PickedUp'=false);\n";
  102. }
  103. void PrismModulesPrinter::printDoorModule(const cell &door, const bool &opened) {
  104. std::string identifier = capitalize(door.getColor()) + door.getType();
  105. os << "\nmodule " << identifier << std::endl;
  106. os << "\t" << identifier << "Open : bool init false;\n";
  107. os << "\n";
  108. if(opened) {
  109. for(const auto [name, position] : agentNameAndPositionMap) {
  110. printUnlockedDoorActions(name, identifier);
  111. }
  112. } else {
  113. for(const auto [name, position] : agentNameAndPositionMap) {
  114. printLockedDoorActions(name, identifier);
  115. }
  116. }
  117. os << "endmodule\n\n";
  118. }
  119. void PrismModulesPrinter::printLockedDoorActions(const std::string &agentName, const std::string &identifier) {
  120. std::string actionName = "[" + agentName + "_unlock_" + identifier + "]";
  121. agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
  122. os << "\t" << actionName << " !" << identifier << "Open -> (" << identifier << "Open'=true);\n";
  123. actionName = "[" + agentName + "_close_" + identifier + "]";
  124. agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
  125. os << "\t" << actionName << " " << identifier << "Open -> (" << identifier << "Open'=false);\n";
  126. }
  127. void PrismModulesPrinter::printUnlockedDoorActions(const std::string &agentName, const std::string &identifier) {
  128. std::string actionName = "[" + agentName + "_open_" + identifier + "]";
  129. agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
  130. os << "\t !" << identifier << "Open -> (" << identifier << "Open'=true);\n";
  131. actionName = "[" + agentName + "_close_" + identifier + "]";
  132. agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
  133. os << "\t" << agentName << " " << identifier << "Open -> (" << identifier << "Open'=false);\n";
  134. }
  135. void PrismModulesPrinter::printRobotModule(const AgentName &agentName, const coordinates &initialPosition) {
  136. os << "\nmodule " << agentName << std::endl;
  137. os << "\tx" << agentName << " : [0.." << maxBoundaries.second << "] init " << initialPosition.second << ";\n";
  138. os << "\ty" << agentName << " : [0.." << maxBoundaries.first << "] init " << initialPosition.first << ";\n";
  139. os << "\tview" << agentName << " : [0..3] init 1;\n";
  140. printTurnActionsForRobot(agentName);
  141. printMovementActionsForRobot(agentName);
  142. if(slipperyBehaviour()) printSlipperyMovementActionsForRobot(agentName);
  143. for(const auto &door : unlockedDoors) {
  144. std::string identifier = capitalize(door.getColor()) + door.getType();
  145. printUnlockedDoorActionsForRobot(agentName, identifier);
  146. }
  147. for(const auto &door : lockedDoors) {
  148. std::string identifier = capitalize(door.getColor()) + door.getType();
  149. std::string key = capitalize(door.getColor()) + "Key";
  150. printLockedDoorActionsForRobot(agentName, identifier, key);
  151. }
  152. for(const auto &key : keys) {
  153. std::string identifier = capitalize(key.getColor()) + key.getType();
  154. os << "\t" << agentName << "Carrying" << identifier << " : bool init false;\n";
  155. printPortableObjectActionsForRobot(agentName, identifier);
  156. }
  157. for(const auto &ball : balls) {
  158. std::string identifier = capitalize(ball.getColor()) + ball.getType();
  159. os << "\t" << agentName << "Carrying" << identifier << " : bool init false;\n";
  160. printPortableObjectActionsForRobot(agentName, identifier);
  161. }
  162. for(const auto &box : boxes) {
  163. std::string identifier = capitalize(box.getColor()) + box.getType();
  164. os << "\t" << agentName << "Carrying" << identifier << " : bool init false;\n";
  165. printPortableObjectActionsForRobot(agentName, identifier);
  166. }
  167. os << "\n" << actionStream.str();
  168. actionStream.str(std::string());
  169. os << "endmodule\n\n";
  170. }
  171. void PrismModulesPrinter::printPortableObjectActionsForRobot(const std::string &a, const std::string &i) {
  172. actionStream << "\t[" << a << "_pickup_" << i << "] " << " !" << a << "IsCarrying & " << a << "CannotMove" << i << " -> (" << a << "Carrying" << i << "'=true);\n";
  173. actionStream << "\t[" << a << "_drop_" << i << "_north]\t" << a << "Carrying" << i << " & view" << a << "=3 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveNorthWall -> (" << a << "Carrying" << i << "'=false);\n";
  174. actionStream << "\t[" << a << "_drop_" << i << "_west] \t" << a << "Carrying" << i << " & view" << a << "=2 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveWestWall -> (" << a << "Carrying" << i << "'=false);\n";
  175. actionStream << "\t[" << a << "_drop_" << i << "_south]\t" << a << "Carrying" << i << " & view" << a << "=1 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveSouthWall -> (" << a << "Carrying" << i << "'=false);\n";
  176. actionStream << "\t[" << a << "_drop_" << i << "_east] \t" << a << "Carrying" << i << " & view" << a << "=0 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveEastWall -> (" << a << "Carrying" << i << "'=false);\n";
  177. actionStream << "\n";
  178. }
  179. void PrismModulesPrinter::printUnlockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier) {
  180. actionStream << "\t[" << agentName << "_open_" << identifier << "] " << agentName << "CannotMove" << identifier << " -> true;\n";
  181. actionStream << "\t[" << agentName << "_close_" << identifier << "] " << agentName << "IsNextTo" << identifier << " -> true;\n";
  182. actionStream << "\n";
  183. }
  184. void PrismModulesPrinter::printLockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier, const std::string &key) {
  185. actionStream << "\t[" << agentName << "_unlock_" << identifier << "] " << agentName << "CannotMove" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n";
  186. actionStream << "\t[" << agentName << "_close_" << identifier << "] " << agentName << "IsNextTo" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n";
  187. actionStream << "\n";
  188. }
  189. void PrismModulesPrinter::printTurnActionsForRobot(const AgentName &a) {
  190. actionStream << printTurnGuard(a, "right", RIGHT, "true") << printTurnUpdate(a, {1.0, "(view"+a+"'=mod(view"+a+"+1,4))"}, RIGHT);
  191. actionStream << printTurnGuard(a, "left", LEFT, "view"+a+">0") << printTurnUpdate(a, {1.0, "(view"+a+"'=view"+a+"-1)"}, LEFT);
  192. actionStream << printTurnGuard(a, "left", LEFT, "view"+a+"=0") << printTurnUpdate(a, {1.0, "(view"+a+"'=3)"}, LEFT);
  193. }
  194. void PrismModulesPrinter::printMovementActionsForRobot(const AgentName &a) {
  195. actionStream << printMovementGuard(a, "North", 3) << printMovementUpdate(a, {1.0, "(y"+a+"'=y"+a+"-1)"});
  196. actionStream << printMovementGuard(a, "East", 0) << printMovementUpdate(a, {1.0, "(x"+a+"'=x"+a+"+1)"});
  197. actionStream << printMovementGuard(a, "South", 1) << printMovementUpdate(a, {1.0, "(y"+a+"'=y"+a+"+1)"});
  198. actionStream << printMovementGuard(a, "West", 2) << printMovementUpdate(a, {1.0, "(x"+a+"'=x"+a+"-1)"});
  199. }
  200. std::string PrismModulesPrinter::printMovementGuard(const AgentName &a, const std::string &direction, const size_t &viewDirection) {
  201. std::string actionName = "[" + a + "_move_" + direction + "]";
  202. agentNameActionMap.at(a).insert({FORWARD, actionName});
  203. return "\t" + actionName + " " + viewVariable(a, viewDirection) + " !" + a + "IsOnSlippery & !" + a + "IsOnLava & !" + a + "IsOnGoal & !" + a + "CannotMove" + direction + "Wall &!" + a + "CannotMoveConditionally -> ";
  204. }
  205. std::string PrismModulesPrinter::printMovementUpdate(const AgentName &a, const update &u) const {
  206. return updateToString(u) + ";\n";
  207. }
  208. std::string PrismModulesPrinter::printTurnGuard(const AgentName &a, const std::string &direction, const ActionId &actionId, const std::string &cond) {
  209. std::string actionName = "[" + a + "_turn_" + direction + "]";
  210. agentNameActionMap.at(a).insert({actionId, actionName});
  211. return "\t" + actionName + " " + cond + " -> ";
  212. }
  213. std::string PrismModulesPrinter::printTurnUpdate(const AgentName &a, const update &u, const ActionId &actionId) const {
  214. return updateToString(u) + ";\n";
  215. }
  216. void PrismModulesPrinter::printSlipperyMovementActionsForRobot(const AgentName &a) {
  217. if(!slipperyTiles.at("North").empty()) {
  218. printSlipperyMovementActionsForNorth(a);
  219. printSlipperyTurnActionsForNorth(a);
  220. }
  221. if(!slipperyTiles.at("East").empty()) {
  222. printSlipperyMovementActionsForEast(a) ;
  223. printSlipperyTurnActionsForEast(a);
  224. }
  225. if(!slipperyTiles.at("South").empty()) {
  226. printSlipperyMovementActionsForSouth(a);
  227. printSlipperyTurnActionsForSouth(a);
  228. }
  229. if(!slipperyTiles.at("West").empty()) {
  230. printSlipperyMovementActionsForWest(a) ;
  231. printSlipperyTurnActionsForWest(a);
  232. }
  233. }
  234. void PrismModulesPrinter::printSlipperyMovementActionsForNorth(const AgentName &a) {
  235. actionStream << printSlipperyMovementGuard(a, "North", 3, { "CanSlipNorth", "CanSlipNorthEast", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, northUpdate(a)}, {(1 - probIntended) * 1/2, northUpdate(a)+"&"+eastUpdate(a)}, {(1 - probIntended) * 1/2, northUpdate(a)+"&"+westUpdate(a)} }) << "\n";
  236. actionStream << printSlipperyMovementGuard(a, "North", 3, {"!CanSlipNorth", "CanSlipNorthEast", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1/2, northUpdate(a)+"&"+eastUpdate(a)}, {1/2, northUpdate(a)+"&"+westUpdate(a)} });
  237. actionStream << printSlipperyMovementGuard(a, "North", 3, { "CanSlipNorth", "!CanSlipNorthEast", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, northUpdate(a)}, {(1 - probIntended), northUpdate(a)+"&"+westUpdate(a)} }) << "\n";
  238. actionStream << printSlipperyMovementGuard(a, "North", 3, { "CanSlipNorth", "CanSlipNorthEast", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, northUpdate(a)}, {(1 - probIntended), northUpdate(a)+"&"+eastUpdate(a)} }) << "\n";
  239. actionStream << printSlipperyMovementGuard(a, "North", 3, {"!CanSlipNorth", "!CanSlipNorthEast", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1, northUpdate(a)+"&"+westUpdate(a) } }) << "\n";
  240. actionStream << printSlipperyMovementGuard(a, "North", 3, { "CanSlipNorth", "!CanSlipNorthEast", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1, northUpdate(a)} }) << "\n";
  241. actionStream << printSlipperyMovementGuard(a, "North", 3, {"!CanSlipNorth", "CanSlipNorthEast", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1, northUpdate(a)+"&"+eastUpdate(a)} }) << "\n";
  242. actionStream << printSlipperyMovementGuard(a, "North", 3, {"!CanSlipNorth", "!CanSlipNorthEast", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", {}) << "\n";
  243. actionStream << printSlipperyMovementGuard(a, "North", 2, { "CanSlipWest", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, westUpdate(a) }, {1 - probIntended, westUpdate(a)+"&"+northUpdate(a)} }) << "\n";
  244. actionStream << printSlipperyMovementGuard(a, "North", 2, {"!CanSlipWest", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1, westUpdate(a)+"&"+northUpdate(a)} }) << "\n";
  245. actionStream << printSlipperyMovementGuard(a, "North", 2, { "CanSlipWest", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1, westUpdate(a) } }) << "\n";
  246. actionStream << printSlipperyMovementGuard(a, "North", 2, {"!CanSlipWest", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", {}) << "\n";
  247. actionStream << printSlipperyMovementGuard(a, "North", 0, { "CanSlipEast", "CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, eastUpdate(a) }, {1 - probIntended, eastUpdate(a)+"&"+northUpdate(a)} }) << "\n";
  248. actionStream << printSlipperyMovementGuard(a, "North", 0, {"!CanSlipEast", "CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "North", { {1, eastUpdate(a)+"&"+northUpdate(a)} }) << "\n";
  249. actionStream << printSlipperyMovementGuard(a, "North", 0, { "CanSlipEast", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "North", { {1, eastUpdate(a) } }) << "\n";
  250. actionStream << printSlipperyMovementGuard(a, "North", 0, {"!CanSlipEast", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "North", {}) << "\n";
  251. actionStream << printSlipperyMovementGuard(a, "North", 1, { "CanSlipSouth", "CanSlipNorth"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, southUpdate(a) }, {1 - probIntended, northUpdate(a)} }) << "\n";
  252. actionStream << printSlipperyMovementGuard(a, "North", 1, {"!CanSlipSouth", "CanSlipNorth"}) << printSlipperyMovementUpdate(a, "North", { {1, northUpdate(a)} }) << "\n";
  253. actionStream << printSlipperyMovementGuard(a, "North", 1, { "CanSlipSouth", "!CanSlipNorth"}) << printSlipperyMovementUpdate(a, "North", { {1, southUpdate(a)} }) << "\n";
  254. actionStream << printSlipperyMovementGuard(a, "North", 1, {"!CanSlipSouth", "!CanSlipNorth"}) << printSlipperyMovementUpdate(a, "North", {}) << "\n";
  255. }
  256. void PrismModulesPrinter::printSlipperyMovementActionsForEast(const AgentName &a) {
  257. actionStream << printSlipperyMovementGuard(a, "East", 0, { "CanSlipEast", "CanSlipSouthEast", "CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a)}, {(1 - probIntended) * 1/2, eastUpdate(a)+"&"+southUpdate(a)}, {(1 - probIntended) * 1/2, eastUpdate(a)+"&"+northUpdate(a)} }) << "\n";
  258. actionStream << printSlipperyMovementGuard(a, "East", 0, {"!CanSlipEast", "CanSlipSouthEast", "CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1/2, eastUpdate(a)+"&"+southUpdate(a)}, {1/2, eastUpdate(a)+"&"+northUpdate(a)} });
  259. actionStream << printSlipperyMovementGuard(a, "East", 0, { "CanSlipEast", "!CanSlipSouthEast", "CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a)}, {(1 - probIntended), eastUpdate(a)+"&"+northUpdate(a)} }) << "\n";
  260. actionStream << printSlipperyMovementGuard(a, "East", 0, { "CanSlipEast", "CanSlipSouthEast", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a)}, {(1 - probIntended), eastUpdate(a)+"&"+southUpdate(a)} }) << "\n";
  261. actionStream << printSlipperyMovementGuard(a, "East", 0, {"!CanSlipEast", "!CanSlipSouthEast", "CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)+"&"+northUpdate(a) } }) << "\n";
  262. actionStream << printSlipperyMovementGuard(a, "East", 0, { "CanSlipEast", "!CanSlipSouthEast", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)} }) << "\n";
  263. actionStream << printSlipperyMovementGuard(a, "East", 0, {"!CanSlipEast", "CanSlipSouthEast", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)+"&"+southUpdate(a)} }) << "\n";
  264. actionStream << printSlipperyMovementGuard(a, "East", 0, {"!CanSlipEast", "!CanSlipSouthEast", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", {}) << "\n";
  265. actionStream << printSlipperyMovementGuard(a, "East", 3, { "CanSlipNorth", "CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, northUpdate(a) }, {1 - probIntended, eastUpdate(a)+"&"+northUpdate(a)} }) << "\n";
  266. actionStream << printSlipperyMovementGuard(a, "East", 3, {"!CanSlipNorth", "CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)+"&"+northUpdate(a)} }) << "\n";
  267. actionStream << printSlipperyMovementGuard(a, "East", 3, { "CanSlipNorth", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, northUpdate(a) } }) << "\n";
  268. actionStream << printSlipperyMovementGuard(a, "East", 3, {"!CanSlipNorth", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", {}) << "\n";
  269. actionStream << printSlipperyMovementGuard(a, "East", 1, { "CanSlipSouth", "CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, southUpdate(a) }, {1 - probIntended, eastUpdate(a)+"&"+southUpdate(a)} }) << "\n";
  270. actionStream << printSlipperyMovementGuard(a, "East", 1, {"!CanSlipSouth", "CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)+"&"+southUpdate(a)} }) << "\n";
  271. actionStream << printSlipperyMovementGuard(a, "East", 1, { "CanSlipSouth", "!CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, southUpdate(a) } }) << "\n";
  272. actionStream << printSlipperyMovementGuard(a, "East", 1, {"!CanSlipSouth", "!CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", {}) << "\n";
  273. actionStream << printSlipperyMovementGuard(a, "East", 2, { "CanSlipWest", "CanSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a) }, {1 - probIntended, westUpdate(a)} }) << "\n";
  274. actionStream << printSlipperyMovementGuard(a, "East", 2, {"!CanSlipWest", "CanSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)} }) << "\n";
  275. actionStream << printSlipperyMovementGuard(a, "East", 2, { "CanSlipWest", "!CanSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {1, westUpdate(a)} }) << "\n";
  276. actionStream << printSlipperyMovementGuard(a, "East", 2, {"!CanSlipWest", "!CanSlipEast"}) << printSlipperyMovementUpdate(a, "East", {}) << "\n";
  277. }
  278. void PrismModulesPrinter::printSlipperyMovementActionsForSouth(const AgentName &a) {
  279. actionStream << printSlipperyMovementGuard(a, "South", 1, { "CanSlipSouth", "CanSlipSouthEast", "CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a)}, {(1 - probIntended) * 1/2, southUpdate(a)+"&"+eastUpdate(a)}, {(1 - probIntended) * 1/2, southUpdate(a)+"&"+westUpdate(a)} }) << "\n";
  280. actionStream << printSlipperyMovementGuard(a, "South", 1, {"!CanSlipSouth", "CanSlipSouthEast", "CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1/2, southUpdate(a)+"&"+eastUpdate(a)}, {1/2, southUpdate(a)+"&"+westUpdate(a)} });
  281. actionStream << printSlipperyMovementGuard(a, "South", 1, { "CanSlipSouth", "!CanSlipSouthEast", "CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a)}, {(1 - probIntended), southUpdate(a)+"&"+westUpdate(a)} }) << "\n";
  282. actionStream << printSlipperyMovementGuard(a, "South", 1, { "CanSlipSouth", "CanSlipSouthEast", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a)}, {(1 - probIntended), southUpdate(a)+"&"+eastUpdate(a)} }) << "\n";
  283. actionStream << printSlipperyMovementGuard(a, "South", 1, {"!CanSlipSouth", "!CanSlipSouthEast", "CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1, southUpdate(a)+"&"+westUpdate(a) } }) << "\n";
  284. actionStream << printSlipperyMovementGuard(a, "South", 1, { "CanSlipSouth", "!CanSlipSouthEast", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1, southUpdate(a)} }) << "\n";
  285. actionStream << printSlipperyMovementGuard(a, "South", 1, {"!CanSlipSouth", "CanSlipSouthEast", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1, southUpdate(a)+"&"+eastUpdate(a)} }) << "\n";
  286. actionStream << printSlipperyMovementGuard(a, "South", 1, {"!CanSlipSouth", "!CanSlipSouthEast", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", {}) << "\n";
  287. actionStream << printSlipperyMovementGuard(a, "South", 2, { "CanSlipWest", "CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, westUpdate(a) }, {1 - probIntended, westUpdate(a)+"&"+southUpdate(a)} }) << "\n";
  288. actionStream << printSlipperyMovementGuard(a, "South", 2, {"!CanSlipWest", "CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1, westUpdate(a)+"&"+southUpdate(a)} }) << "\n";
  289. actionStream << printSlipperyMovementGuard(a, "South", 2, { "CanSlipWest", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1, westUpdate(a) } }) << "\n";
  290. actionStream << printSlipperyMovementGuard(a, "South", 2, {"!CanSlipWest", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", {}) << "\n";
  291. actionStream << printSlipperyMovementGuard(a, "South", 0, { "CanSlipEast", "CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, eastUpdate(a) }, {1 - probIntended, eastUpdate(a)+"&"+southUpdate(a)} }) << "\n";
  292. actionStream << printSlipperyMovementGuard(a, "South", 0, {"!CanSlipEast", "CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "South", { {1, eastUpdate(a)+"&"+southUpdate(a)} }) << "\n";
  293. actionStream << printSlipperyMovementGuard(a, "South", 0, { "CanSlipEast", "!CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "South", { {1, eastUpdate(a) } }) << "\n";
  294. actionStream << printSlipperyMovementGuard(a, "South", 0, {"!CanSlipEast", "!CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "South", {}) << "\n";
  295. actionStream << printSlipperyMovementGuard(a, "South", 3, { "CanSlipSouth", "CanSlipNorth"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a) }, {1 - probIntended, northUpdate(a)} }) << "\n";
  296. actionStream << printSlipperyMovementGuard(a, "South", 3, {"!CanSlipSouth", "CanSlipNorth"}) << printSlipperyMovementUpdate(a, "South", { {1, northUpdate(a)} }) << "\n";
  297. actionStream << printSlipperyMovementGuard(a, "South", 3, { "CanSlipSouth", "!CanSlipNorth"}) << printSlipperyMovementUpdate(a, "South", { {1, southUpdate(a)} }) << "\n";
  298. actionStream << printSlipperyMovementGuard(a, "South", 3, {"!CanSlipSouth", "!CanSlipNorth"}) << printSlipperyMovementUpdate(a, "South", {}) << "\n";
  299. }
  300. void PrismModulesPrinter::printSlipperyMovementActionsForWest(const AgentName &a) {
  301. actionStream << printSlipperyMovementGuard(a, "West", 2, { "CanSlipWest", "CanSlipSouthWest", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a)}, {(1 - probIntended) * 1/2, westUpdate(a)+"&"+southUpdate(a)}, {(1 - probIntended) * 1/2, westUpdate(a)+"&"+northUpdate(a)} }) << "\n";
  302. actionStream << printSlipperyMovementGuard(a, "West", 2, {"!CanSlipWest", "CanSlipSouthWest", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1/2, westUpdate(a)+"&"+southUpdate(a)}, {1/2, westUpdate(a)+"&"+northUpdate(a)} });
  303. actionStream << printSlipperyMovementGuard(a, "West", 2, { "CanSlipWest", "!CanSlipSouthWest", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a)}, {(1 - probIntended), westUpdate(a)+"&"+northUpdate(a)} }) << "\n";
  304. actionStream << printSlipperyMovementGuard(a, "West", 2, { "CanSlipWest", "CanSlipSouthWest", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a)}, {(1 - probIntended), westUpdate(a)+"&"+southUpdate(a)} }) << "\n";
  305. actionStream << printSlipperyMovementGuard(a, "West", 2, {"!CanSlipWest", "!CanSlipSouthWest", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)+"&"+northUpdate(a) } }) << "\n";
  306. actionStream << printSlipperyMovementGuard(a, "West", 2, { "CanSlipWest", "!CanSlipSouthWest", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)} }) << "\n";
  307. actionStream << printSlipperyMovementGuard(a, "West", 2, {"!CanSlipWest", "CanSlipSouthWest", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)+"&"+southUpdate(a)} }) << "\n";
  308. actionStream << printSlipperyMovementGuard(a, "West", 2, {"!CanSlipWest", "!CanSlipSouthWest", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", {}) << "\n";
  309. actionStream << printSlipperyMovementGuard(a, "West", 3, { "CanSlipNorth", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, northUpdate(a) }, {1 - probIntended, westUpdate(a)+"&"+northUpdate(a)} }) << "\n";
  310. actionStream << printSlipperyMovementGuard(a, "West", 3, {"!CanSlipNorth", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)+"&"+northUpdate(a)} }) << "\n";
  311. actionStream << printSlipperyMovementGuard(a, "West", 3, { "CanSlipNorth", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a) } }) << "\n";
  312. actionStream << printSlipperyMovementGuard(a, "West", 3, {"!CanSlipNorth", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", {}) << "\n";
  313. actionStream << printSlipperyMovementGuard(a, "West", 1, { "CanSlipSouth", "CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, southUpdate(a) }, {1 - probIntended, westUpdate(a)+"&"+southUpdate(a)} }) << "\n";
  314. actionStream << printSlipperyMovementGuard(a, "West", 1, {"!CanSlipSouth", "CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)+"&"+southUpdate(a)} }) << "\n";
  315. actionStream << printSlipperyMovementGuard(a, "West", 1, { "CanSlipSouth", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, southUpdate(a) } }) << "\n";
  316. actionStream << printSlipperyMovementGuard(a, "West", 1, {"!CanSlipSouth", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", {}) << "\n";
  317. actionStream << printSlipperyMovementGuard(a, "West", 0, { "CanSlipEast", "CanSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a) }, {1 - probIntended, eastUpdate(a)} }) << "\n";
  318. actionStream << printSlipperyMovementGuard(a, "West", 0, {"!CanSlipEast", "CanSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)} }) << "\n";
  319. actionStream << printSlipperyMovementGuard(a, "West", 0, { "CanSlipEast", "!CanSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {1, eastUpdate(a)} }) << "\n";
  320. actionStream << printSlipperyMovementGuard(a, "West", 0, {"!CanSlipEast", "!CanSlipWest"}) << printSlipperyMovementUpdate(a, "West", {}) << "\n";
  321. }
  322. void PrismModulesPrinter::printSlipperyTurnActionsForNorth(const AgentName &a) {
  323. actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { "CanSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, northUpdate(a)} }) << "\n";
  324. actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!CanSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n";
  325. actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"-1)"}, {1 - probIntended, northUpdate(a)} }) << "\n";
  326. actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"=3)"}, {1 - probIntended, northUpdate(a)} }) << "\n";
  327. actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n";
  328. actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"=3)"} }) << "\n";
  329. }
  330. void PrismModulesPrinter::printSlipperyTurnActionsForEast(const AgentName &a) {
  331. actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { "CanSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, eastUpdate(a)} }) << "\n";
  332. actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!CanSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n";
  333. actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"-1)"}, {1 - probIntended, eastUpdate(a)} }) << "\n";
  334. actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"=3)"}, {1 - probIntended, eastUpdate(a)} }) << "\n";
  335. actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n";
  336. actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"=3)"} }) << "\n";
  337. }
  338. void PrismModulesPrinter::printSlipperyTurnActionsForSouth(const AgentName &a) {
  339. actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { "CanSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, southUpdate(a)} }) << "\n";
  340. actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!CanSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n";
  341. actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"-1)"}, {1 - probIntended, southUpdate(a)} }) << "\n";
  342. actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"=3)"}, {1 - probIntended, southUpdate(a)} }) << "\n";
  343. actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n";
  344. actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"=3)"} }) << "\n";
  345. }
  346. void PrismModulesPrinter::printSlipperyTurnActionsForWest(const AgentName &a) {
  347. actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { "CanSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, westUpdate(a)} }) << "\n";
  348. actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!CanSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n";
  349. actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"-1)"}, {1 - probIntended, westUpdate(a)} }) << "\n";
  350. actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"=3)"}, {1 - probIntended, westUpdate(a)} }) << "\n";
  351. actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n";
  352. actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"=3)"} }) << "\n";
  353. }
  354. std::string PrismModulesPrinter::printSlipperyMovementGuard(const AgentName &a, const std::string &direction, const ViewDirection &viewDirection, const std::vector<std::string> &guards) {
  355. std::string actionName = "[" + a + "_move_" + direction + "]";
  356. agentNameActionMap.at(a).insert({FORWARD, actionName});
  357. return "\t" + actionName + " " + viewVariable(a, viewDirection) + a + "IsOnSlippery" + direction + " & " + buildConjunction(a, guards) + " -> ";
  358. }
  359. std::string PrismModulesPrinter::printSlipperyMovementUpdate(const AgentName &a, const std::string &direction, const updates &u) const {
  360. return updatesToString(u);
  361. }
  362. std::string PrismModulesPrinter::printSlipperyTurnGuard(const AgentName &a, const std::string &direction, const ActionId &actionId, const std::vector<std::string> &guards, const std::string &cond) {
  363. std::string actionName = "[" + a + "_turn_" + direction + "]";
  364. agentNameActionMap.at(a).insert({actionId, actionName});
  365. return "\t" + actionName + " " + buildConjunction(a, guards) + " & " + cond + " -> ";
  366. }
  367. std::string PrismModulesPrinter::printSlipperyTurnUpdate(const AgentName &a, const updates &u) {
  368. return updatesToString(u);
  369. }
  370. void PrismModulesPrinter::printFaultyMovementModule(const AgentName &a) {
  371. os << "\nmodule " << a << "FaultyBehaviour" << std::endl;
  372. os << "\tpreviousAction" << a << " : [-1..2] init -1;\n";
  373. for(const auto [actionId, actionName] : agentNameActionMap.at(a)) {
  374. os << "\t" << actionName << faultyBehaviourGuard(a, actionId) << " -> " << faultyBehaviourUpdate(a, actionId) << ";\n";
  375. }
  376. os << "endmodule\n\n";
  377. }
  378. void PrismModulesPrinter::printMoveModule() {
  379. os << "\nmodule " << "Arbiter" << std::endl;
  380. os << "\tclock : [0.." << agentIndexMap.size() - 1 << "] init 0;\n";
  381. for(const auto [agentName, actions] : agentNameActionMap) {
  382. for(const auto [actionId, actionName] : actions) {
  383. os << "\t" << actionName << " " << moveGuard(agentName) << " -> " << moveUpdate(agentName) << ";\n";
  384. }
  385. }
  386. os << "endmodule\n\n";
  387. }
  388. void PrismModulesPrinter::printConfiguredActions(const AgentName &agentName) {
  389. for (auto& config : configuration) {
  390. if (config.type_ == ConfigType::Module && !config.overwrite_ && agentName == config.module_) {
  391. os << config.expression_ ;
  392. }
  393. }
  394. os << "\n";
  395. return os;
  396. }
  397. std::ostream& PrismModulesPrinter::printDoneActions(std::ostream &os, const AgentName &agentName) {
  398. os << "\t[" << agentName << "_done]" << moveGuard(agentName) << agentName << "IsInGoal | " << agentName << "IsInLava -> (" << agentName << "Done'=true);\n";
  399. return os;
  400. }
  401. std::ostream& PrismModulesPrinter::printPlayerStruct(std::ostream &os, const AgentName &agentName, const bool agentWithView, const std::vector<float> &probabilities, const std::set<std::string> &slipperyActions) {
  402. os << "player " << agentName << "\n\t";
  403. bool first = true;
  404. std::list<std::string> allActions = { "_move_north", "_move_east", "_move_south", "_move_west" };
  405. std::list<std::string> movementActions = allActions;
  406. for(auto const& probability : probabilities) {
  407. std::string percentageString = std::to_string((int)(100 * probability));
  408. for(auto const& movement : movementActions) {
  409. allActions.push_back(movement + "_" + percentageString);
  410. }
  411. }
  412. if(agentWithView) {
  413. allActions.push_back("_turn_left");
  414. allActions.push_back("_turn_right");
  415. } else {
  416. allActions.push_back("_turns");
  417. }
  418. for(auto const& action : allActions) {
  419. if(first) first = false; else os << ", ";
  420. os << "[" << agentName << action << "]";
  421. }
  422. for(auto const& action : slipperyActions) {
  423. os << ", " << action;
  424. }
  425. os << ", [" << agentName << "_done]";
  426. os << "\nendplayer\n";
  427. return os;
  428. }
  429. std::ostream& PrismModulesPrinter::printGlobalMoveVariable(std::ostream &os, const size_t &numberOfPlayer) {
  430. os << "\nglobal move : [0.." << std::to_string(numberOfPlayer - 1) << "];\n\n";
  431. return os;
  432. }
  433. std::ostream& PrismModulesPrinter::printRewards(std::ostream &os, const AgentName &agentName, const std::map<coordinates, float> &stateRewards, const cells &lava, const cells &goals, const std::map<Color, cells> &backgroundTiles) {
  434. if(lava.size() != 0) {
  435. os << "rewards \"" << agentName << "SafetyNoBFS\"\n";
  436. os << "\t" <<agentName << "IsInLavaAndNotDone: -100;\n";
  437. os << "endrewards\n";
  438. }
  439. if (!goals.empty() || !lava.empty()) {
  440. os << "rewards \"" << agentName << "SafetyNoBFSAndGoal\"\n";
  441. if(goals.size() != 0) os << "\t" << agentName << "IsInGoalAndNotDone: 100;\n";
  442. if(lava.size() != 0) os << "\t" << agentName << "IsInLavaAndNotDone: -100;\n";
  443. os << "endrewards\n";
  444. }
  445. os << "rewards \"" << agentName << "Time\"\n";
  446. os << "\t!" << agentName << "IsInGoal : -1;\n";
  447. if(goals.size() != 0) os << "\t" << agentName << "IsInGoalAndNotDone: 100;\n";
  448. if(lava.size() != 0) os << "\t" << agentName << "IsInLavaAndNotDone: -100;\n";
  449. os << "endrewards\n";
  450. if(stateRewards.size() > 0) {
  451. os << "rewards \"" << agentName << "SafetyWithBFS\"\n";
  452. if(lava.size() != 0) os << "\t" << agentName << "IsInLavaAndNotDone: -100;\n";
  453. for(auto const [coordinates, reward] : stateRewards) {
  454. os << "\txAgent=" << coordinates.first << "&yAgent=" << coordinates.second << " : " << reward << ";\n";
  455. }
  456. os << "endrewards\n";
  457. }
  458. if(stateRewards.size() > 0) {
  459. os << "rewards \"" << agentName << "SafetyWithBFSAndGoal\"\n";
  460. if(goals.size() != 0) os << "\tAgentIsInGoalAndNotDone: 100;\n";
  461. if(lava.size() != 0) os << "\tAgentIsInLavaAndNotDone: -100;\n";
  462. for(auto const [coordinates, reward] : stateRewards) {
  463. os << "\txAgent=" << coordinates.first << "&yAgent=" << coordinates.second << " : " << reward << ";\n";
  464. }
  465. os << "endrewards\n";
  466. }
  467. for(auto const entry : backgroundTiles)
  468. {
  469. std::cout << getColor(entry.first) << " ";
  470. for(auto const cell : entry.second){
  471. std::cout << cell.getCoordinates().first << " " << cell.getCoordinates().second << std::endl;
  472. }
  473. }
  474. if(backgroundTiles.size() > 0) {
  475. os << "rewards \"TaxiReward\"\n";
  476. os << "\t!AgentIsInGoal : -1;\n";
  477. std::string allPassengersPickedUp = "";
  478. bool first = true;
  479. for(auto const [color, cells] : backgroundTiles) {
  480. if(cells.size() == 0) continue;
  481. if(first) first = false; else allPassengersPickedUp += "&";
  482. std::string c = getColor(color);
  483. c.at(0) = std::toupper(c.at(0));
  484. std::string visitedLabel = agentName + "_picked_up_" + c;
  485. allPassengersPickedUp += visitedLabel;
  486. os << "[" << agentName << "_pickup_" << c << "] true : 100;\n";
  487. }
  488. if(goals.size() != 0) os << "\tAgentIsInGoalAndNotDone & " << allPassengersPickedUp << " : 100;\n";
  489. if(goals.size() != 0) os << "\tAgentIsInGoalAndNotDone & !(" << allPassengersPickedUp << ") : -100;\n";
  490. os << "endrewards";
  491. }
  492. return os;
  493. }
  494. std::string PrismModulesPrinter::faultyBehaviourGuard(const AgentName &agentName, const ActionId &actionId) const {
  495. if(faultyBehaviour()) {
  496. if(actionId == NOFAULT) {
  497. return "(previousAction" + agentName + "=" + std::to_string(NOFAULT) + ") ";
  498. } else {
  499. return "(previousAction" + agentName + "=" + std::to_string(NOFAULT) + " | previousAction" + agentName + "=" + std::to_string(actionId) + ") ";
  500. }
  501. } else {
  502. return "";
  503. }
  504. }
  505. std::string PrismModulesPrinter::faultyBehaviourUpdate(const AgentName &agentName, const ActionId &actionId) const {
  506. if(actionId != NOFAULT) {
  507. return updatesToString({ {1 - faultyProbability, "(previousAction" + agentName + "'=" + std::to_string(NOFAULT) + ")"}, {faultyProbability, "(previousAction" + agentName + "'=" + std::to_string(actionId) + ")" } });
  508. } else {
  509. return "true";
  510. }
  511. }
  512. std::string PrismModulesPrinter::moveGuard(const AgentName &agentName) const {
  513. return "clock=" + std::to_string(agentIndexMap.at(agentName));
  514. }
  515. std::string PrismModulesPrinter::moveUpdate(const AgentName &agentName) const {
  516. size_t agentIndex = agentIndexMap.at(agentName);
  517. return (agentIndex == numberOfPlayer - 1) ? " & (clock'=0) " : " & (clock'=" + std::to_string(agentIndex + 1) + ") ";
  518. }
  519. std::string PrismModulesPrinter::updatesToString(const updates &updates) const {
  520. if(updates.empty()) return "true";
  521. std::string updatesString = "";
  522. bool first = true;
  523. for(auto const update : updates) {
  524. if(first) first = false;
  525. else updatesString += " + ";
  526. updatesString += updateToString(update);
  527. }
  528. return updatesString;
  529. }
  530. std::string PrismModulesPrinter::updateToString(const update &u) const {
  531. return std::to_string(u.first) + ": " + u.second;
  532. }
  533. std::string PrismModulesPrinter::viewVariable(const AgentName &agentName, const size_t &agentDirection, const bool agentWithView) const {
  534. return agentWithView ? " view" + agentName + "=" + std::to_string(agentDirection) + " & " : " ";
  535. }
  536. bool PrismModulesPrinter::anyPortableObject() const {
  537. return !keys.empty() || !boxes.empty() || !balls.empty();
  538. }
  539. bool PrismModulesPrinter::faultyBehaviour() const {
  540. return faultyProbability > 0.0f;
  541. }
  542. bool PrismModulesPrinter::slipperyBehaviour() const {
  543. return !slipperyTiles.at("North").empty() || !slipperyTiles.at("East").empty() || !slipperyTiles.at("South").empty() || !slipperyTiles.at("West").empty();
  544. }
  545. bool PrismModulesPrinter::isGame() const {
  546. return modelType == ModelType::SMG;
  547. }
  548. std::string PrismModulesPrinter::buildConjunction(const AgentName &a, std::vector<std::string> formulae) const {
  549. if(formulae.empty()) return "true";
  550. std::string conjunction = "";
  551. bool first = true;
  552. for(auto const formula : formulae) {
  553. if(first) first = false;
  554. else conjunction += " & ";
  555. conjunction += formula;
  556. }
  557. return conjunction;
  558. }
  559. }