diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index 7886c89..968d46c 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -3,9 +3,14 @@ #include #include +#define NOFAULT -1 +#define LEFT 0 +#define RIGHT 1 +#define FORWARD 2 + namespace prism { - 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 AgentNameAndPositionMap &agentNameAndPositionMap, std::vector config, const float &faultyProbability) + 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 AgentNameAndPositionMap &agentNameAndPositionMap, std::vector config, const float faultyProbability) : os(os), modelType(modelType), maxBoundaries(maxBoundaries), boxes(boxes), balls(balls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), agentNameAndPositionMap(agentNameAndPositionMap), configuration(config), faultyProbability(faultyProbability), viewDirectionMapping({{0, "East"}, {1, "South"}, {2, "West"}, {3, "North"}}) { numberOfPlayer = agentNameAndPositionMap.size(); size_t index = 0; @@ -68,70 +73,6 @@ namespace prism { return os; } - - std::ostream& PrismModulesPrinter::printBooleansForKeys(std::ostream &os, const AgentName &agentName, const cells &keys) { - for(auto const& key : keys) { - os << "\t" << agentName << "_has_"<< key.getColor() << "_key : bool;\n";//init false;\n"; - } - os << "\n"; - return os; - } - - std::ostream& PrismModulesPrinter::printBooleansForBackground(std::ostream &os, const AgentName &agentName, const std::map &backgroundTiles) { - for(auto const& [color, cells] : backgroundTiles) { - if(cells.size() == 0) continue; - std::string c = getColor(color); - c.at(0) = std::toupper(c.at(0)); - os << "\t" << agentName << "_picked_up_" << c << " : bool init false;\n"; - } - os << "\n"; - return os; - } - - std::ostream& PrismModulesPrinter::printActionsForKeys(std::ostream &os, const AgentName &agentName, const cells &keys) { - for(auto const& key : keys) { // TODO ADD Drop action and enforce that pickup only possible if pockets empty (nothing picked up already) - os << "\n"; - std::string keyColor = key.getColor(); - os << "\t[pickup_" << keyColor << "_key]\t" << pickupGuard(agentName, keyColor) << "-> "; - os << "(" << agentName << "_has_" << keyColor << "_key'=true) & (" << agentName << "_is_carrying_object'=true);\n"; - os << "\n"; - - os << "\t[drop_" << keyColor << "_key_north]\t" << dropGuard(agentName, keyColor, 3) << "-> "; - os << "(" << agentName << "_has_" << keyColor << "_key'=false) & (" << agentName << "_is_carrying_object'=false);\n"; - - os << "\t[drop_" << keyColor << "_key_west]\t" << dropGuard(agentName, keyColor, 2) << "-> "; - os << "(" << agentName << "_has_" << keyColor << "_key'=false) & (" << agentName << "_is_carrying_object'=false);\n"; - - os << "\t[drop_" << keyColor << "_key_south]\t" << dropGuard(agentName, keyColor, 1) << "-> "; - os << "(" << agentName << "_has_" << keyColor << "_key'=false) & (" << agentName << "_is_carrying_object'=false);\n"; - - os << "\t[drop_" << keyColor << "_key_east]\t" << dropGuard(agentName, keyColor, 0) << "-> "; - os << "(" << agentName << "_has_" << keyColor << "_key'=false) & (" << agentName << "_is_carrying_object'=false);\n"; - } - - return os; - } - - std::string PrismModulesPrinter::pickupGuard(const AgentName &agentName, const std::string keyColor ) { - return "!" + agentName + "_is_carrying_object &\t" + agentName + "CanPickUp" + keyColor + "Key "; - } - - std::string PrismModulesPrinter::dropGuard(const AgentName &agentName, const std::string keyColor, size_t view) { - return viewVariable(agentName, view, true) + "\t!" + agentName + "CannotMove" + viewDirectionMapping.at(view) + "\t&\t" + agentName + "_has_" + keyColor + "_key\t"; - } - - std::ostream& PrismModulesPrinter::printActionsForBackground(std::ostream &os, const AgentName &agentName, const std::map &backgroundTiles) { - for(auto const& [color, cells] : backgroundTiles) { - if(cells.size() == 0) continue; - std::string c = getColor(color); - c.at(0) = std::toupper(c.at(0)); - os << "\t[" << agentName << "_pickup_" << c << "] " << agentName << "On" << c << " & !" << agentName << "_picked_up_" << c << " -> "; - os << "(" << agentName << "_picked_up_" << c << "'=true);\n"; - } - os << "\n"; - return os; - } - std::ostream& PrismModulesPrinter::printInitStruct(std::ostream &os, const AgentNameAndPositionMap &agents, const KeyNameAndPositionMap &keys, const cells &lockedDoors, const cells &unlockedDoors, prism::ModelType modelType) { /* os << "init\n"; @@ -176,7 +117,7 @@ namespace prism { return os; } - std::ostream& PrismModulesPrinter::printModule(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const coordinates &boundaries, const coordinates& initialPosition, const cells &keys, const std::map &backgroundTiles, const bool agentWithView, const std::vector &probabilities, const double faultyProbability) { + std::ostream& PrismModulesPrinter::printModule(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const coordinates &boundaries, const coordinates& initialPosition, const cells &keys, const std::map &backgroundTiles, const bool agentWithView, const std::vector &probabilities, const float faultyProbability) { /* os << "module " << agentName << "\n"; os << "\tx" << agentName << " : [1.." << boundaries.second << "];\n"; @@ -276,6 +217,9 @@ namespace prism { os << "\ty" << agentName << " : [0.." << maxBoundaries.first << "] init " << initialPosition.first << ";\n"; os << "\tview" << agentName << " : [0..3] init 1;\n"; + if(faultyBehaviour()) os << "\tpreviousAction" << agentName << " : [-1..2] init -1;\n"; + + printTurnActionsForRobot(agentName); printMovementActionsForRobot(agentName); for(const auto &door : unlockedDoors) { @@ -295,51 +239,83 @@ namespace prism { printPortableObjectActionsForRobot(agentName, identifier); } + for(const auto &ball : balls) { + std::string identifier = capitalize(ball.getColor()) + ball.getType(); + os << "\t" << agentName << "Carrying" << identifier << " : bool init false;\n"; + printPortableObjectActionsForRobot(agentName, identifier); + } + + for(const auto &box : boxes) { + std::string identifier = capitalize(box.getColor()) + box.getType(); + os << "\t" << agentName << "Carrying" << identifier << " : bool init false;\n"; + printPortableObjectActionsForRobot(agentName, identifier); + } + os << "\n" << actionStream.str(); actionStream.str(std::string()); os << "endmodule\n\n"; } void PrismModulesPrinter::printPortableObjectActionsForRobot(const std::string &a, const std::string &i) { - actionStream << "\t[" << a << "_pickup_" << i << "] " << a << "CannotMove" << i << " -> (" << a << "Carrying" << i << "'=true);\n"; - actionStream << "\t[" << a << "_drop_" << i << "_north]\t" << a << "Carrying" << i << " & view" << a << "=3 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveNorthWall -> (" << a << "Carrying" << i << "'=false);\n"; - actionStream << "\t[" << a << "_drop_" << i << "_west] \t" << a << "Carrying" << i << " & view" << a << "=2 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveWestWall -> (" << a << "Carrying" << i << "'=false);\n"; - actionStream << "\t[" << a << "_drop_" << i << "_south]\t" << a << "Carrying" << i << " & view" << a << "=1 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveSouthWall -> (" << a << "Carrying" << i << "'=false);\n"; - actionStream << "\t[" << a << "_drop_" << i << "_east] \t" << a << "Carrying" << i << " & view" << a << "=0 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveEastWall -> (" << a << "Carrying" << i << "'=false);\n"; + actionStream << "\t[" << a << "_pickup_" << i << "] " << faultyBehaviourGuard(a, NOFAULT) << moveGuard(a) << " !" << a << "IsCarrying & " << a << "CannotMove" << i << " -> (" << a << "Carrying" << i << "'=true);\n"; + actionStream << "\t[" << a << "_drop_" << i << "_north]\t" << faultyBehaviourGuard(a, NOFAULT) << moveGuard(a) << a << "Carrying" << i << " & view" << a << "=3 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveNorthWall -> (" << a << "Carrying" << i << "'=false);\n"; + actionStream << "\t[" << a << "_drop_" << i << "_west] \t" << faultyBehaviourGuard(a, NOFAULT) << moveGuard(a) << a << "Carrying" << i << " & view" << a << "=2 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveWestWall -> (" << a << "Carrying" << i << "'=false);\n"; + actionStream << "\t[" << a << "_drop_" << i << "_south]\t" << faultyBehaviourGuard(a, NOFAULT) << moveGuard(a) << a << "Carrying" << i << " & view" << a << "=1 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveSouthWall -> (" << a << "Carrying" << i << "'=false);\n"; + actionStream << "\t[" << a << "_drop_" << i << "_east] \t" << faultyBehaviourGuard(a, NOFAULT) << moveGuard(a) << a << "Carrying" << i << " & view" << a << "=0 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveEastWall -> (" << a << "Carrying" << i << "'=false);\n"; actionStream << "\n"; } void PrismModulesPrinter::printUnlockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier) { - actionStream << "\t[" << agentName << "_open_" << identifier << "] " << agentName << "CannotMove" << identifier << " -> true;\n"; - actionStream << "\t[" << agentName << "_close_" << identifier << "] " << agentName << "IsNextTo" << identifier << " -> true;\n"; + actionStream << "\t[" << agentName << "_open_" << identifier << "] " << faultyBehaviourGuard(agentName, NOFAULT) << moveGuard(agentName) << agentName << "CannotMove" << identifier << " -> true;\n"; + actionStream << "\t[" << agentName << "_close_" << identifier << "] " << faultyBehaviourGuard(agentName, NOFAULT) << moveGuard(agentName) << agentName << "IsNextTo" << identifier << " -> true;\n"; actionStream << "\n"; } void PrismModulesPrinter::printLockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier, const std::string &key) { - actionStream << "\t[" << agentName << "_unlock_" << identifier << "] " << agentName << "CannotMove" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n"; - actionStream << "\t[" << agentName << "_close_" << identifier << "] " << agentName << "IsNextTo" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n"; + actionStream << "\t[" << agentName << "_unlock_" << identifier << "] " << faultyBehaviourGuard(agentName, NOFAULT) << moveGuard(agentName) << agentName << "CannotMove" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n"; + actionStream << "\t[" << agentName << "_close_" << identifier << "] " << faultyBehaviourGuard(agentName, NOFAULT) << moveGuard(agentName) << agentName << "IsNextTo" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n"; actionStream << "\n"; } - void PrismModulesPrinter::printTurningActionsForRobot(const AgentName &a) { - + void PrismModulesPrinter::printTurnActionsForRobot(const AgentName &a) { + actionStream << printTurnGuard(a, "right", RIGHT, "true") << printTurnUpdate(a, {1.0, "(view"+a+"'=mod(view"+a+"+1,4))"}, RIGHT); + actionStream << printTurnGuard(a, "left", LEFT, "view"+a+">0") << printTurnUpdate(a, {1.0, "(view"+a+"'=view"+a+"-1)"}, LEFT); + actionStream << printTurnGuard(a, "left", LEFT, "view"+a+"=0") << printTurnUpdate(a, {1.0, "(view"+a+"'=3)"}, LEFT); } void PrismModulesPrinter::printMovementActionsForRobot(const AgentName &a) { - if(faultyProbability <= 0.0) { - actionStream << printMovementGuard(a, "North", 3) << printMovementUpdate(a, "y" + a + "'=y" + a + "-1"); - actionStream << printMovementGuard(a, "East", 0) << printMovementUpdate(a, "x" + a + "'=x" + a + "+1"); - actionStream << printMovementGuard(a, "South", 1) << printMovementUpdate(a, "y" + a + "'=y" + a + "+1"); - actionStream << printMovementGuard(a, "West", 2) << printMovementUpdate(a, "x" + a + "'=x" + a + "-1"); + actionStream << printMovementGuard(a, "North", 3) << printMovementUpdate(a, {1.0, "(y"+a+"'=y"+a+"-1)"}); + actionStream << printMovementGuard(a, "East", 0) << printMovementUpdate(a, {1.0, "(x"+a+"'=x"+a+"+1)"}); + actionStream << printMovementGuard(a, "South", 1) << printMovementUpdate(a, {1.0, "(y"+a+"'=y"+a+"+1)"}); + actionStream << printMovementGuard(a, "West", 2) << printMovementUpdate(a, {1.0, "(x"+a+"'=x"+a+"-1)"}); + } + + std::string PrismModulesPrinter::printMovementGuard(const AgentName &a, const std::string &direction, const size_t &viewDirection) const { + return "\t[" + a + "_move_" + direction + "]" + moveGuard(a) + viewVariable(a, 3) + faultyBehaviourGuard(a, FORWARD) + " !" + a + "IsOnSlippery & !" + a + "IsOnLava & !" + a + "IsOnGoal & !" + a + "CannotMove" + direction + "Wall -> "; + } + + std::string PrismModulesPrinter::printMovementUpdate(const AgentName &a, const update &u) const { + if(!faultyBehaviour()) { + return updateToString(u) + ";\n"; + } else { + update nonFaultyUpdate = {u.first - faultyProbability, u.second + " & " + faultyBehaviourUpdate(a, NOFAULT)}; + update faultyUpdate = {faultyProbability, u.second + " & " + faultyBehaviourUpdate(a, FORWARD)}; + return updateToString(nonFaultyUpdate) + " + " + updateToString(faultyUpdate) + ";\n"; } } - std::string PrismModulesPrinter::printMovementGuard(const AgentName &a, const std::string &direction, const size_t &viewDirection) { - return "\t[" + a + "_move_" + direction + "]" + moveGuard(a) + viewVariable(a, 3) + " !" + a + "IsOnSlippery & !" + a + "IsOnLava & !" + a + "IsOnGoal & !" + a + "CannotMove" + direction + "Wall -> "; + std::string PrismModulesPrinter::printTurnGuard(const AgentName &a, const std::string &direction, const ActionId &actionId, const std::string &cond) const { + return "\t[" + a + "_turn_" + direction + "]" + moveGuard(a) + faultyBehaviourGuard(a, actionId) + cond + " -> "; } - std::string PrismModulesPrinter::printMovementUpdate(const AgentName &a, const std::string &update) { - return "(" + update + ") & " + moveUpdate(a) + ";\n"; + std::string PrismModulesPrinter::printTurnUpdate(const AgentName &a, const update &u, const ActionId &actionId) const { + if(!faultyBehaviour()) { + return updateToString(u) + ";\n"; + } else { + update nonFaultyUpdate = {u.first - faultyProbability, u.second + " & " + faultyBehaviourUpdate(a, NOFAULT)}; + update faultyUpdate = {faultyProbability, u.second + " & " + faultyBehaviourUpdate(a, actionId)}; + return updateToString(nonFaultyUpdate) + " + " + updateToString(faultyUpdate) + ";\n"; + } } std::ostream& PrismModulesPrinter::printConfiguredActions(std::ostream &os, const AgentName &agentName) { @@ -817,12 +793,24 @@ namespace prism { return os; } - std::string PrismModulesPrinter::moveGuard(const AgentName &agentName) { - return isGame() ? " move=" + std::to_string(agentIndexMap[agentName]) + " & " : " "; + std::string PrismModulesPrinter::moveGuard(const AgentName &agentName) const { + return isGame() ? " move=" + std::to_string(agentIndexMap.at(agentName)) + " & " : " "; + } + + std::string PrismModulesPrinter::faultyBehaviourGuard(const AgentName &agentName, const ActionId &actionId) const { + if(actionId == NOFAULT) { + return "(previousAction" + agentName + "=" + std::to_string(NOFAULT) + ") & "; + } else { + return "(previousAction" + agentName + "=" + std::to_string(NOFAULT) + " | previousAction" + agentName + "=" + std::to_string(actionId) + ") & "; + } } - std::string PrismModulesPrinter::moveUpdate(const AgentName &agentName) { - size_t agentIndex = agentIndexMap[agentName]; + std::string PrismModulesPrinter::faultyBehaviourUpdate(const AgentName &agentName, const ActionId &actionId) const { + return "(previousAction" + agentName + "'=" + std::to_string(actionId) + ")"; + } + + std::string PrismModulesPrinter::moveUpdate(const AgentName &agentName) const { + size_t agentIndex = agentIndexMap.at(agentName); return isGame() ? (agentIndex == numberOfPlayer - 1) ? " & (move'=0) " : @@ -830,10 +818,22 @@ namespace prism { ""; } - std::string PrismModulesPrinter::viewVariable(const AgentName &agentName, const size_t &agentDirection, const bool agentWithView) { + std::string PrismModulesPrinter::updateToString(const update &u) const { + return std::to_string(u.first) + ": " + u.second; + } + + std::string PrismModulesPrinter::viewVariable(const AgentName &agentName, const size_t &agentDirection, const bool agentWithView) const { return agentWithView ? " view" + agentName + "=" + std::to_string(agentDirection) + " & " : " "; } + bool PrismModulesPrinter::anyPortableObject() const { + return !keys.empty() || !boxes.empty() || !balls.empty(); + } + + bool PrismModulesPrinter::faultyBehaviour() const { + return faultyProbability > 0.0f; + } + bool PrismModulesPrinter::isGame() const { return modelType == ModelType::SMG; } diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h index 626d06c..425283e 100644 --- a/util/PrismModulesPrinter.h +++ b/util/PrismModulesPrinter.h @@ -9,7 +9,7 @@ namespace prism { class PrismModulesPrinter { public: - 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 AgentNameAndPositionMap &agentNameAndPositionMap, std::vector config, const float &faultyProbability); + 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 AgentNameAndPositionMap &agentNameAndPositionMap, std::vector config, const float faultyProbability); std::ostream& print(); @@ -24,12 +24,10 @@ namespace prism { void printRobotModule(const AgentName &agentName, const coordinates &initialPosition); void printPortableObjectActionsForRobot(const std::string &agentName, const std::string &identifier); - void printUnlockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier); void printLockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier, const std::string &key); - void printMovementActionsForRobot(const std::string &a); - void printTurningActionsForRobot(const std::string &a); + void printTurnActionsForRobot(const std::string &a); std::ostream& printConstants(std::ostream &os, const std::vector &constants); /* @@ -57,10 +55,6 @@ namespace prism { */ std::ostream& printSlipperyTurn(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const coordinates &c, std::set &slipperyActions, const std::array& neighborhood, SlipperyType orientation); - std::ostream& printBooleansForKeys(std::ostream &os, const AgentName &agentName, const cells &keys); - std::ostream& printActionsForKeys(std::ostream &os, const AgentName &agentName, const cells &keys); - std::ostream& printBooleansForBackground(std::ostream &os, const AgentName &agentName, const std::map &backgroundTiles); - std::ostream& printActionsForBackground(std::ostream &os, const AgentName &agentName, const std::map &backgroundTiles); std::ostream& printInitStruct(std::ostream &os, const AgentNameAndPositionMap &agents, const KeyNameAndPositionMap &keys, const cells &lockedDoors, const cells &unlockedDoors, prism::ModelType modelType); std::ostream& printModule(std::ostream &os, const AgentName &agentName, @@ -71,7 +65,7 @@ namespace prism { const std::map &backgroundTiles, const bool agentWithView, const std::vector &probabilities = {}, - const double faultyProbability = 0); + const float faultyProbability = 0); std::ostream& printMovementActions(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const bool agentWithView, const float &probability = 1.0, const double &stickyProbability = 0.0); std::ostream& printDoneActions(std::ostream &os, const AgentName &agentName); std::ostream& printEndmodule(std::ostream &os); @@ -82,17 +76,23 @@ namespace prism { std::ostream& printConfiguration(std::ostream &os, const std::vector& configurations); std::ostream& printConfiguredActions(std::ostream &os, const AgentName &agentName); - std::string moveGuard(const AgentName &agentName); - std::string pickupGuard(const AgentName &agentName, const std::string keyColor); - std::string dropGuard(const AgentName &agentName, const std::string keyColor, size_t view); - std::string moveUpdate(const AgentName &agentName); - - std::string viewVariable(const AgentName &agentName, const size_t &agentDirection, const bool agentWithView = true); bool isGame() const; private: - std::string printMovementGuard(const AgentName &a, const std::string &direction, const size_t &viewDirection); - std::string printMovementUpdate(const AgentName &a, const std::string &update); + std::string printMovementGuard(const AgentName &a, const std::string &direction, const size_t &viewDirection) const; + std::string printMovementUpdate(const AgentName &a, const update &update) const; + std::string printTurnGuard(const AgentName &a, const std::string &direction, const ActionId &actionId, const std::string &cond = "") const; + std::string printTurnUpdate(const AgentName &a, const update &u, const ActionId &actionId) const; + + bool anyPortableObject() const; + bool faultyBehaviour() const; + std::string moveGuard(const AgentName &agentName) const; + std::string faultyBehaviourGuard(const AgentName &agentName, const ActionId &actionId) const; + std::string faultyBehaviourUpdate(const AgentName &agentName, const ActionId &actionId) const; + std::string moveUpdate(const AgentName &agentName) const; + std::string updateToString(const update &u) const; + + std::string viewVariable(const AgentName &agentName, const size_t &agentDirection, const bool agentWithView = true) const; std::ostream &os; @@ -110,7 +110,7 @@ namespace prism { AgentNameAndPositionMap agentNameAndPositionMap; std::map agentIndexMap; size_t numberOfPlayer; - float const &faultyProbability; + float const faultyProbability; std::vector configuration; std::map viewDirectionMapping; };