From c6f7bb27be22a342ede8e8b08caa358c9f81dbde Mon Sep 17 00:00:00 2001 From: sp Date: Mon, 8 Jan 2024 14:06:13 +0100 Subject: [PATCH] added slippery turn actions --- util/PrismModulesPrinter.cpp | 52 +++++++++++++++++++++++++++++++++++- util/PrismModulesPrinter.h | 6 +++++ 2 files changed, 57 insertions(+), 1 deletion(-) diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index be92c2b..da7bb8a 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -285,15 +285,19 @@ namespace prism { void PrismModulesPrinter::printSlipperyMovementActionsForRobot(const AgentName &a) { if(!slipperyTiles.at("North").empty()) { printSlipperyMovementActionsForNorth(a); + printSlipperyTurnActionsForNorth(a); } if(!slipperyTiles.at("East").empty()) { printSlipperyMovementActionsForEast(a) ; + printSlipperyTurnActionsForEast(a); } if(!slipperyTiles.at("South").empty()) { printSlipperyMovementActionsForSouth(a); + printSlipperyTurnActionsForSouth(a); } if(!slipperyTiles.at("West").empty()) { printSlipperyMovementActionsForWest(a) ; + printSlipperyTurnActionsForWest(a); } } @@ -401,15 +405,61 @@ namespace prism { actionStream << printSlipperyMovementGuard(a, "West", 0, {"!CanSlipEast", "!CanSlipWest"}) << printSlipperyMovementUpdate(a, "West", {}) << "\n"; } + void PrismModulesPrinter::printSlipperyTurnActionsForNorth(const AgentName &a) { + actionStream << printSlipperyTurnGuard(a, "right", { "CanSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, northUpdate(a)} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "right", {"!CanSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n"; + + actionStream << printSlipperyTurnGuard(a, "left", { "CanSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"-1)"}, {1 - probIntended, northUpdate(a)} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "left", { "CanSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"=3)"}, {1 - probIntended, northUpdate(a)} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "left", {"!CanSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "left", {"!CanSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"=3)"} }) << "\n"; + } + + void PrismModulesPrinter::printSlipperyTurnActionsForEast(const AgentName &a) { + actionStream << printSlipperyTurnGuard(a, "right", { "CanSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, eastUpdate(a)} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "right", {"!CanSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n"; + + actionStream << printSlipperyTurnGuard(a, "left", { "CanSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"-1)"}, {1 - probIntended, eastUpdate(a)} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "left", { "CanSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"=3)"}, {1 - probIntended, eastUpdate(a)} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "left", {"!CanSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "left", {"!CanSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"=3)"} }) << "\n"; + } + + void PrismModulesPrinter::printSlipperyTurnActionsForSouth(const AgentName &a) { + actionStream << printSlipperyTurnGuard(a, "right", { "CanSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, southUpdate(a)} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "right", {"!CanSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n"; + + actionStream << printSlipperyTurnGuard(a, "left", { "CanSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"-1)"}, {1 - probIntended, southUpdate(a)} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "left", { "CanSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"=3)"}, {1 - probIntended, southUpdate(a)} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "left", {"!CanSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "left", {"!CanSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"=3)"} }) << "\n"; + } + + void PrismModulesPrinter::printSlipperyTurnActionsForWest(const AgentName &a) { + actionStream << printSlipperyTurnGuard(a, "right", { "CanSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, westUpdate(a)} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "right", {"!CanSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n"; + + actionStream << printSlipperyTurnGuard(a, "left", { "CanSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"-1)"}, {1 - probIntended, westUpdate(a)} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "left", { "CanSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"=3)"}, {1 - probIntended, westUpdate(a)} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "left", {"!CanSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "left", {"!CanSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"=3)"} }) << "\n"; + } std::string PrismModulesPrinter::printSlipperyMovementGuard(const AgentName &a, const std::string &direction, const ViewDirection &viewDirection, const std::vector &guards) const { - return "\t[" + a + "_move_" + direction + "]" + moveGuard(a) + viewVariable(a, viewDirection) + faultyBehaviourGuard(a, FORWARD) + a + "IsOnSlippery" + direction + " & " + buildConjunction(a, guards) + " -> "; + return "\t[" + a + "_move_" + direction + "] " + moveGuard(a) + viewVariable(a, viewDirection) + faultyBehaviourGuard(a, FORWARD) + a + "IsOnSlippery" + direction + " & " + buildConjunction(a, guards) + " -> "; } std::string PrismModulesPrinter::printSlipperyMovementUpdate(const AgentName &a, const std::string &direction, const updates &u) const { return updatesToString(u, a, FORWARD); } + std::string PrismModulesPrinter::printSlipperyTurnGuard(const AgentName &a, const std::string &direction, const std::vector &guards, const std::string &cond) const { + return "\t[" + a + "_turn_" + direction + "] " + buildConjunction(a, guards) + " & " + cond + " -> "; + } + + std::string PrismModulesPrinter::printSlipperyTurnUpdate(const AgentName &a, const updates &u) { + return updatesToString(u, a, NOFAULT); + } std::ostream& PrismModulesPrinter::printConfiguredActions(std::ostream &os, const AgentName &agentName) { for (auto& config : configuration) { diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h index 00f3836..1e71404 100644 --- a/util/PrismModulesPrinter.h +++ b/util/PrismModulesPrinter.h @@ -78,6 +78,10 @@ namespace prism { void printSlipperyMovementActionsForEast(const AgentName &a); void printSlipperyMovementActionsForSouth(const AgentName &a); void printSlipperyMovementActionsForWest(const AgentName &a); + void printSlipperyTurnActionsForNorth(const AgentName &a); + void printSlipperyTurnActionsForEast(const AgentName &a); + void printSlipperyTurnActionsForSouth(const AgentName &a); + void printSlipperyTurnActionsForWest(const AgentName &a); 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; @@ -85,6 +89,8 @@ namespace prism { std::string printTurnUpdate(const AgentName &a, const update &u, const ActionId &actionId) const; std::string printSlipperyMovementGuard(const AgentName &a, const std::string &direction, const ViewDirection &viewDirection, const std::vector &guards) const; std::string printSlipperyMovementUpdate(const AgentName &a, const std::string &direction, const updates &u) const; + std::string printSlipperyTurnGuard(const AgentName &a, const std::string &direction, const std::vector &guards, const std::string &cond) const; + std::string printSlipperyTurnUpdate(const AgentName &a, const updates &u); bool anyPortableObject() const; bool faultyBehaviour() const;