From d8c7e73a3246d9c6335fe4ef891f5958c0e84e35 Mon Sep 17 00:00:00 2001 From: sp Date: Wed, 10 Jan 2024 18:35:21 +0100 Subject: [PATCH 1/5] fixed some issues with formulas and semicolons --- util/PrismModulesPrinter.cpp | 234 +++++++++++++++++------------------ util/PrismModulesPrinter.h | 1 + 2 files changed, 118 insertions(+), 117 deletions(-) diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index 430dd3c..e9f4b0c 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -292,151 +292,151 @@ namespace prism { } void PrismModulesPrinter::printSlipperyMovementActionsForNorth(const AgentName &a) { - 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"; - actionStream << printSlipperyMovementGuard(a, "North", 3, {"!CanSlipNorth", "CanSlipNorthEast", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1/2, northUpdate(a)+"&"+eastUpdate(a)}, {1/2, northUpdate(a)+"&"+westUpdate(a)} }); - actionStream << printSlipperyMovementGuard(a, "North", 3, { "CanSlipNorth", "!CanSlipNorthEast", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, northUpdate(a)}, {(1 - probIntended), northUpdate(a)+"&"+westUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "North", 3, { "CanSlipNorth", "CanSlipNorthEast", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, northUpdate(a)}, {(1 - probIntended), northUpdate(a)+"&"+eastUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "North", 3, {"!CanSlipNorth", "!CanSlipNorthEast", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1, northUpdate(a)+"&"+westUpdate(a) } }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "North", 3, { "CanSlipNorth", "!CanSlipNorthEast", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1, northUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "North", 3, {"!CanSlipNorth", "CanSlipNorthEast", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1, northUpdate(a)+"&"+eastUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "North", 3, {"!CanSlipNorth", "!CanSlipNorthEast", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", {}) << "\n"; - - actionStream << printSlipperyMovementGuard(a, "North", 2, { "CanSlipWest", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, westUpdate(a) }, {1 - probIntended, westUpdate(a)+"&"+northUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "North", 2, {"!CanSlipWest", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1, westUpdate(a)+"&"+northUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "North", 2, { "CanSlipWest", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1, westUpdate(a) } }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "North", 2, {"!CanSlipWest", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", {}) << "\n"; - - actionStream << printSlipperyMovementGuard(a, "North", 0, { "CanSlipEast", "CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, eastUpdate(a) }, {1 - probIntended, eastUpdate(a)+"&"+northUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "North", 0, {"!CanSlipEast", "CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "North", { {1, eastUpdate(a)+"&"+northUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "North", 0, { "CanSlipEast", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "North", { {1, eastUpdate(a) } }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "North", 0, {"!CanSlipEast", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "North", {}) << "\n"; - - actionStream << printSlipperyMovementGuard(a, "North", 1, { "CanSlipSouth", "CanSlipNorth"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, southUpdate(a) }, {1 - probIntended, northUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "North", 1, {"!CanSlipSouth", "CanSlipNorth"}) << printSlipperyMovementUpdate(a, "North", { {1, northUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "North", 1, { "CanSlipSouth", "!CanSlipNorth"}) << printSlipperyMovementUpdate(a, "North", { {1, southUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "North", 1, {"!CanSlipSouth", "!CanSlipNorth"}) << printSlipperyMovementUpdate(a, "North", {}) << "\n"; + actionStream << printSlipperyMovementGuard(a, "North", 3, {"!"+a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, northUpdate(a)}, {(1 - probIntended) * 1/2, northUpdate(a)+"&"+eastUpdate(a)}, {(1 - probIntended) * 1/2, northUpdate(a)+"&"+westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "North", 3, { a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1/2, northUpdate(a)+"&"+eastUpdate(a)}, {1/2, northUpdate(a)+"&"+westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "North", 3, {"!"+a+"CannotSlipNorth", a+"CannotSlipNorthEast", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, northUpdate(a)}, {(1 - probIntended), northUpdate(a)+"&"+westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "North", 3, {"!"+a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast", a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, northUpdate(a)}, {(1 - probIntended), northUpdate(a)+"&"+eastUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "North", 3, { a+"CannotSlipNorth", a+"CannotSlipNorthEast", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1, northUpdate(a)+"&"+westUpdate(a) } }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "North", 3, {"!"+a+"CannotSlipNorth", a+"CannotSlipNorthEast", a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1, northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "North", 3, { a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast", a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1, northUpdate(a)+"&"+eastUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "North", 3, { a+"CannotSlipNorth", a+"CannotSlipNorthEast", a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", {}) << ";\n"; + + actionStream << printSlipperyMovementGuard(a, "North", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, westUpdate(a) }, {1 - probIntended, westUpdate(a)+"&"+northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "North", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1, westUpdate(a)+"&"+northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "North", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1, westUpdate(a) } }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "North", 2, { a+"CannotSlipWest", a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", {}) << ";\n"; + + actionStream << printSlipperyMovementGuard(a, "North", 0, {"!"+a+"CannotSlipEast", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, eastUpdate(a) }, {1 - probIntended, eastUpdate(a)+"&"+northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "North", 0, { a+"CannotSlipEast", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "North", { {1, eastUpdate(a)+"&"+northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "North", 0, {"!"+a+"CannotSlipEast", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "North", { {1, eastUpdate(a) } }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "North", 0, { a+"CannotSlipEast", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "North", {}) << ";\n"; + + actionStream << printSlipperyMovementGuard(a, "North", 1, {"!"+a+"CannotSlipSouth", "!"+a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, southUpdate(a) }, {1 - probIntended, northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "North", 1, { a+"CannotSlipSouth", "!"+a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "North", { {1, northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "North", 1, {"!"+a+"CannotSlipSouth", a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "North", { {1, southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "North", 1, { a+"CannotSlipSouth", a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "North", {}) << ";\n"; } void PrismModulesPrinter::printSlipperyMovementActionsForEast(const AgentName &a) { - 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"; - actionStream << printSlipperyMovementGuard(a, "East", 0, {"!CanSlipEast", "CanSlipSouthEast", "CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1/2, eastUpdate(a)+"&"+southUpdate(a)}, {1/2, eastUpdate(a)+"&"+northUpdate(a)} }); - actionStream << printSlipperyMovementGuard(a, "East", 0, { "CanSlipEast", "!CanSlipSouthEast", "CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a)}, {(1 - probIntended), eastUpdate(a)+"&"+northUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "East", 0, { "CanSlipEast", "CanSlipSouthEast", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a)}, {(1 - probIntended), eastUpdate(a)+"&"+southUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "East", 0, {"!CanSlipEast", "!CanSlipSouthEast", "CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)+"&"+northUpdate(a) } }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "East", 0, { "CanSlipEast", "!CanSlipSouthEast", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "East", 0, {"!CanSlipEast", "CanSlipSouthEast", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)+"&"+southUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "East", 0, {"!CanSlipEast", "!CanSlipSouthEast", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", {}) << "\n"; - - actionStream << printSlipperyMovementGuard(a, "East", 3, { "CanSlipNorth", "CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, northUpdate(a) }, {1 - probIntended, eastUpdate(a)+"&"+northUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "East", 3, {"!CanSlipNorth", "CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)+"&"+northUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "East", 3, { "CanSlipNorth", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, northUpdate(a) } }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "East", 3, {"!CanSlipNorth", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", {}) << "\n"; - - actionStream << printSlipperyMovementGuard(a, "East", 1, { "CanSlipSouth", "CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, southUpdate(a) }, {1 - probIntended, eastUpdate(a)+"&"+southUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "East", 1, {"!CanSlipSouth", "CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)+"&"+southUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "East", 1, { "CanSlipSouth", "!CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, southUpdate(a) } }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "East", 1, {"!CanSlipSouth", "!CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", {}) << "\n"; - - actionStream << printSlipperyMovementGuard(a, "East", 2, { "CanSlipWest", "CanSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a) }, {1 - probIntended, westUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "East", 2, {"!CanSlipWest", "CanSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "East", 2, { "CanSlipWest", "!CanSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {1, westUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "East", 2, {"!CanSlipWest", "!CanSlipEast"}) << printSlipperyMovementUpdate(a, "East", {}) << "\n"; + actionStream << printSlipperyMovementGuard(a, "East", 0, {"!"+a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a)}, {(1 - probIntended) * 1/2, eastUpdate(a)+"&"+southUpdate(a)}, {(1 - probIntended) * 1/2, eastUpdate(a)+"&"+northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "East", 0, { a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1/2, eastUpdate(a)+"&"+southUpdate(a)}, {1/2, eastUpdate(a)+"&"+northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "East", 0, {"!"+a+"CannotSlipEast", a+"CannotSlipSouthEast", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a)}, {(1 - probIntended), eastUpdate(a)+"&"+northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "East", 0, {"!"+a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a)}, {(1 - probIntended), eastUpdate(a)+"&"+southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "East", 0, { a+"CannotSlipEast", a+"CannotSlipSouthEast", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)+"&"+northUpdate(a) } }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "East", 0, {"!"+a+"CannotSlipEast", a+"CannotSlipSouthEast", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "East", 0, { a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)+"&"+southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "East", 0, { a+"CannotSlipEast", a+"CannotSlipSouthEast", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", {}) << ";\n"; + + actionStream << printSlipperyMovementGuard(a, "East", 3, {"!"+a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, northUpdate(a) }, {1 - probIntended, eastUpdate(a)+"&"+northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "East", 3, { a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)+"&"+northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "East", 3, {"!"+a+"CannotSlipNorth", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, northUpdate(a) } }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "East", 3, { a+"CannotSlipNorth", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", {}) << ";\n"; + + actionStream << printSlipperyMovementGuard(a, "East", 1, {"!"+a+"CannotSlipSouth", "!"+a+"CannotSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, southUpdate(a) }, {1 - probIntended, eastUpdate(a)+"&"+southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "East", 1, { a+"CannotSlipSouth", "!"+a+"CannotSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)+"&"+southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "East", 1, {"!"+a+"CannotSlipSouth", a+"CannotSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, southUpdate(a) } }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "East", 1, { a+"CannotSlipSouth", a+"CannotSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", {}) << ";\n"; + + actionStream << printSlipperyMovementGuard(a, "East", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a) }, {1 - probIntended, westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "East", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "East", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {1, westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "East", 2, { a+"CannotSlipWest", a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", {}) << ";\n"; } void PrismModulesPrinter::printSlipperyMovementActionsForSouth(const AgentName &a) { - 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"; - actionStream << printSlipperyMovementGuard(a, "South", 1, {"!CanSlipSouth", "CanSlipSouthEast", "CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1/2, southUpdate(a)+"&"+eastUpdate(a)}, {1/2, southUpdate(a)+"&"+westUpdate(a)} }); - actionStream << printSlipperyMovementGuard(a, "South", 1, { "CanSlipSouth", "!CanSlipSouthEast", "CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a)}, {(1 - probIntended), southUpdate(a)+"&"+westUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "South", 1, { "CanSlipSouth", "CanSlipSouthEast", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a)}, {(1 - probIntended), southUpdate(a)+"&"+eastUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "South", 1, {"!CanSlipSouth", "!CanSlipSouthEast", "CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1, southUpdate(a)+"&"+westUpdate(a) } }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "South", 1, { "CanSlipSouth", "!CanSlipSouthEast", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1, southUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "South", 1, {"!CanSlipSouth", "CanSlipSouthEast", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1, southUpdate(a)+"&"+eastUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "South", 1, {"!CanSlipSouth", "!CanSlipSouthEast", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", {}) << "\n"; - - actionStream << printSlipperyMovementGuard(a, "South", 2, { "CanSlipWest", "CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, westUpdate(a) }, {1 - probIntended, westUpdate(a)+"&"+southUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "South", 2, {"!CanSlipWest", "CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1, westUpdate(a)+"&"+southUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "South", 2, { "CanSlipWest", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1, westUpdate(a) } }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "South", 2, {"!CanSlipWest", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", {}) << "\n"; - - actionStream << printSlipperyMovementGuard(a, "South", 0, { "CanSlipEast", "CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, eastUpdate(a) }, {1 - probIntended, eastUpdate(a)+"&"+southUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "South", 0, {"!CanSlipEast", "CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "South", { {1, eastUpdate(a)+"&"+southUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "South", 0, { "CanSlipEast", "!CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "South", { {1, eastUpdate(a) } }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "South", 0, {"!CanSlipEast", "!CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "South", {}) << "\n"; - - actionStream << printSlipperyMovementGuard(a, "South", 3, { "CanSlipSouth", "CanSlipNorth"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a) }, {1 - probIntended, northUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "South", 3, {"!CanSlipSouth", "CanSlipNorth"}) << printSlipperyMovementUpdate(a, "South", { {1, northUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "South", 3, { "CanSlipSouth", "!CanSlipNorth"}) << printSlipperyMovementUpdate(a, "South", { {1, southUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "South", 3, {"!CanSlipSouth", "!CanSlipNorth"}) << printSlipperyMovementUpdate(a, "South", {}) << "\n"; + actionStream << printSlipperyMovementGuard(a, "South", 1, {"!"+a+"CannotSlipSouth", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a)}, {(1 - probIntended) * 1/2, southUpdate(a)+"&"+eastUpdate(a)}, {(1 - probIntended) * 1/2, southUpdate(a)+"&"+westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "South", 1, { a+"CannotSlipSouth", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1/2, southUpdate(a)+"&"+eastUpdate(a)}, {1/2, southUpdate(a)+"&"+westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "South", 1, {"!"+a+"CannotSlipSouth", a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a)}, {(1 - probIntended), southUpdate(a)+"&"+westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "South", 1, {"!"+a+"CannotSlipSouth", "!"+a+"CannotSlipSouthEast", a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a)}, {(1 - probIntended), southUpdate(a)+"&"+eastUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "South", 1, { a+"CannotSlipSouth", a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1, southUpdate(a)+"&"+westUpdate(a) } }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "South", 1, {"!"+a+"CannotSlipSouth", a+"CannotSlipSouthEast", a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1, southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "South", 1, { a+"CannotSlipSouth", "!"+a+"CannotSlipSouthEast", a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1, southUpdate(a)+"&"+eastUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "South", 1, { a+"CannotSlipSouth", a+"CannotSlipSouthEast", a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", {}) << ";\n"; + + actionStream << printSlipperyMovementGuard(a, "South", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, westUpdate(a) }, {1 - probIntended, westUpdate(a)+"&"+southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "South", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1, westUpdate(a)+"&"+southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "South", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1, westUpdate(a) } }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "South", 2, { a+"CannotSlipWest", a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", {}) << ";\n"; + + actionStream << printSlipperyMovementGuard(a, "South", 0, {"!"+a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, eastUpdate(a) }, {1 - probIntended, eastUpdate(a)+"&"+southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "South", 0, { a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast"}) << printSlipperyMovementUpdate(a, "South", { {1, eastUpdate(a)+"&"+southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "South", 0, {"!"+a+"CannotSlipEast", a+"CannotSlipSouthEast"}) << printSlipperyMovementUpdate(a, "South", { {1, eastUpdate(a) } }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "South", 0, { a+"CannotSlipEast", a+"CannotSlipSouthEast"}) << printSlipperyMovementUpdate(a, "South", {}) << ";\n"; + + actionStream << printSlipperyMovementGuard(a, "South", 3, {"!"+a+"CannotSlipSouth", "!"+a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a) }, {1 - probIntended, northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "South", 3, { a+"CannotSlipSouth", "!"+a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "South", { {1, northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "South", 3, {"!"+a+"CannotSlipSouth", a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "South", { {1, southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "South", 3, { a+"CannotSlipSouth", a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "South", {}) << ";\n"; } void PrismModulesPrinter::printSlipperyMovementActionsForWest(const AgentName &a) { - 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"; - actionStream << printSlipperyMovementGuard(a, "West", 2, {"!CanSlipWest", "CanSlipSouthWest", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1/2, westUpdate(a)+"&"+southUpdate(a)}, {1/2, westUpdate(a)+"&"+northUpdate(a)} }); - actionStream << printSlipperyMovementGuard(a, "West", 2, { "CanSlipWest", "!CanSlipSouthWest", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a)}, {(1 - probIntended), westUpdate(a)+"&"+northUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "West", 2, { "CanSlipWest", "CanSlipSouthWest", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a)}, {(1 - probIntended), westUpdate(a)+"&"+southUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "West", 2, {"!CanSlipWest", "!CanSlipSouthWest", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)+"&"+northUpdate(a) } }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "West", 2, { "CanSlipWest", "!CanSlipSouthWest", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "West", 2, {"!CanSlipWest", "CanSlipSouthWest", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)+"&"+southUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "West", 2, {"!CanSlipWest", "!CanSlipSouthWest", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", {}) << "\n"; - - actionStream << printSlipperyMovementGuard(a, "West", 3, { "CanSlipNorth", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, northUpdate(a) }, {1 - probIntended, westUpdate(a)+"&"+northUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "West", 3, {"!CanSlipNorth", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)+"&"+northUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "West", 3, { "CanSlipNorth", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a) } }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "West", 3, {"!CanSlipNorth", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", {}) << "\n"; - - actionStream << printSlipperyMovementGuard(a, "West", 1, { "CanSlipSouth", "CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, southUpdate(a) }, {1 - probIntended, westUpdate(a)+"&"+southUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "West", 1, {"!CanSlipSouth", "CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)+"&"+southUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "West", 1, { "CanSlipSouth", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, southUpdate(a) } }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "West", 1, {"!CanSlipSouth", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", {}) << "\n"; - - actionStream << printSlipperyMovementGuard(a, "West", 0, { "CanSlipEast", "CanSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a) }, {1 - probIntended, eastUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "West", 0, {"!CanSlipEast", "CanSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "West", 0, { "CanSlipEast", "!CanSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {1, eastUpdate(a)} }) << "\n"; - actionStream << printSlipperyMovementGuard(a, "West", 0, {"!CanSlipEast", "!CanSlipWest"}) << printSlipperyMovementUpdate(a, "West", {}) << "\n"; + actionStream << printSlipperyMovementGuard(a, "West", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipSouthWest", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a)}, {(1 - probIntended) * 1/2, westUpdate(a)+"&"+southUpdate(a)}, {(1 - probIntended) * 1/2, westUpdate(a)+"&"+northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "West", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipSouthWest", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1/2, westUpdate(a)+"&"+southUpdate(a)}, {1/2, westUpdate(a)+"&"+northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "West", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipSouthWest", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a)}, {(1 - probIntended), westUpdate(a)+"&"+northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "West", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipSouthWest", a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a)}, {(1 - probIntended), westUpdate(a)+"&"+southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "West", 2, { a+"CannotSlipWest", a+"CannotSlipSouthWest", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)+"&"+northUpdate(a) } }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "West", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipSouthWest", a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "West", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipSouthWest", a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)+"&"+southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "West", 2, { a+"CannotSlipWest", a+"CannotSlipSouthWest", a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", {}) << ";\n"; + + actionStream << printSlipperyMovementGuard(a, "West", 3, {"!"+a+"CannotSlipNorth", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, northUpdate(a) }, {1 - probIntended, westUpdate(a)+"&"+northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "West", 3, { a+"CannotSlipNorth", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)+"&"+northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "West", 3, {"!"+a+"CannotSlipNorth", a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a) } }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "West", 3, { a+"CannotSlipNorth", a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", {}) << ";\n"; + + actionStream << printSlipperyMovementGuard(a, "West", 1, {"!"+a+"CannotSlipSouth", "!"+a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, southUpdate(a) }, {1 - probIntended, westUpdate(a)+"&"+southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "West", 1, { a+"CannotSlipSouth", "!"+a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)+"&"+southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "West", 1, {"!"+a+"CannotSlipSouth", a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, southUpdate(a) } }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "West", 1, { a+"CannotSlipSouth", a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", {}) << ";\n"; + + actionStream << printSlipperyMovementGuard(a, "West", 0, {"!"+a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a) }, {1 - probIntended, eastUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "West", 0, { a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "West", 0, {"!"+a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {1, eastUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "West", 0, { a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", {}) << ";\n"; } void PrismModulesPrinter::printSlipperyTurnActionsForNorth(const AgentName &a) { - actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { "CanSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, northUpdate(a)} }) << "\n"; - actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!CanSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!"+a+"CannotSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { a+"CannotSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"-1)"}, {1 - probIntended, northUpdate(a)} }) << "\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"=3)"}, {1 - probIntended, northUpdate(a)} }) << "\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"=3)"} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n"; } void PrismModulesPrinter::printSlipperyTurnActionsForEast(const AgentName &a) { - actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { "CanSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, eastUpdate(a)} }) << "\n"; - actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!CanSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!"+a+"CannotSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, eastUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { a+"CannotSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"-1)"}, {1 - probIntended, eastUpdate(a)} }) << "\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"=3)"}, {1 - probIntended, eastUpdate(a)} }) << "\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"=3)"} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, eastUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, eastUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n"; } void PrismModulesPrinter::printSlipperyTurnActionsForSouth(const AgentName &a) { - actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { "CanSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, southUpdate(a)} }) << "\n"; - actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!CanSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!"+a+"CannotSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { a+"CannotSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"-1)"}, {1 - probIntended, southUpdate(a)} }) << "\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"=3)"}, {1 - probIntended, southUpdate(a)} }) << "\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"=3)"} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n"; } void PrismModulesPrinter::printSlipperyTurnActionsForWest(const AgentName &a) { - actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { "CanSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, westUpdate(a)} }) << "\n"; - actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!CanSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!"+a+"CannotSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { a+"CannotSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"-1)"}, {1 - probIntended, westUpdate(a)} }) << "\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"=3)"}, {1 - probIntended, westUpdate(a)} }) << "\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"=3)"} }) << "\n"; + actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n"; } std::string PrismModulesPrinter::printSlipperyMovementGuard(const AgentName &a, const std::string &direction, const ViewDirection &viewDirection, const std::vector &guards) { - std::string actionName = "[" + a + "_move_" + direction + "]"; + std::string actionName = "[" + a + "_move_" + viewDirectionToString.at(viewDirection) + "]"; agentNameActionMap.at(a).insert({FORWARD, actionName}); return "\t" + actionName + " " + viewVariable(a, viewDirection) + a + "IsOnSlippery" + direction + " & " + buildConjunction(a, guards) + " -> "; } diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h index a66d68f..368b667 100644 --- a/util/PrismModulesPrinter.h +++ b/util/PrismModulesPrinter.h @@ -105,6 +105,7 @@ namespace prism { float const probIntended; std::vector configuration; std::vector viewDirections = {0, 1, 2, 3}; + std::map viewDirectionToString = {{0, "East"}, {1, "South"}, {2, "West"}, {3, "North"}}; std::map>> agentNameActionMap; }; -- 2.20.1 From 7e932200caa3a63aca0d25577f8e2e8c7e198e1e Mon Sep 17 00:00:00 2001 From: sp Date: Wed, 10 Jan 2024 18:35:31 +0100 Subject: [PATCH 2/5] fixed additional semicolon in CannotSlip Formulas --- util/PrismFormulaPrinter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp index ef2f5a5..4f1d4d1 100644 --- a/util/PrismFormulaPrinter.cpp +++ b/util/PrismFormulaPrinter.cpp @@ -158,7 +158,7 @@ namespace prism { std::string identifier = capitalize(box.getColor()) + box.getType(); os << " | " << objectPositionToConjunction(agentName, identifier, slipCell); } - os << ";\n"; + if(!semicolon) os << ";\n"; } std::string PrismFormulaPrinter::buildFormula(const std::string &formulaName, const std::string &formula, const bool semicolon) { -- 2.20.1 From b50355deb976b4cf128a52980da2920eccbe12b5 Mon Sep 17 00:00:00 2001 From: sp Date: Wed, 10 Jan 2024 18:37:22 +0100 Subject: [PATCH 3/5] x and y start at 1 --- util/PrismModulesPrinter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index e9f4b0c..4adc004 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -167,8 +167,8 @@ namespace prism { void PrismModulesPrinter::printRobotModule(const AgentName &agentName, const coordinates &initialPosition) { os << "\nmodule " << agentName << std::endl; - os << "\tx" << agentName << " : [0.." << maxBoundaries.second << "] init " << initialPosition.second << ";\n"; - os << "\ty" << agentName << " : [0.." << maxBoundaries.first << "] init " << initialPosition.first << ";\n"; + os << "\tx" << agentName << " : [1.." << maxBoundaries.second << "] init " << initialPosition.second << ";\n"; + os << "\ty" << agentName << " : [1.." << maxBoundaries.first << "] init " << initialPosition.first << ";\n"; os << "\tview" << agentName << " : [0..3] init 1;\n"; printTurnActionsForRobot(agentName); -- 2.20.1 From 0a1f5ac40584f8712a4b59e950bafce8f88187a1 Mon Sep 17 00:00:00 2001 From: sp Date: Wed, 10 Jan 2024 18:47:30 +0100 Subject: [PATCH 4/5] switched to col and row instead of x and y --- util/PrismFormulaPrinter.cpp | 10 +++++----- util/PrismModulesPrinter.cpp | 12 ++++++------ 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp index 4f1d4d1..a873b38 100644 --- a/util/PrismFormulaPrinter.cpp +++ b/util/PrismFormulaPrinter.cpp @@ -20,26 +20,26 @@ std::string vectorToDisjunction(const std::vector &formulae) { } std::string cellToConjunction(const AgentName &agentName, const cell &c) { - return "x" + agentName + "=" + std::to_string(c.column) + "&y" + agentName + "=" + std::to_string(c.row); + return "col" + agentName + "=" + std::to_string(c.column) + "&row" + agentName + "=" + std::to_string(c.row); } std::string cellToConjunctionWithOffset(const AgentName &agentName, const cell &c, const std::string &xOffset, const std::string &yOffset){ - return "x" + agentName + xOffset + "=" + std::to_string(c.column) + "&y" + agentName + yOffset + "=" + std::to_string(c.row); + return "col" + agentName + xOffset + "=" + std::to_string(c.column) + "&row" + agentName + yOffset + "=" + std::to_string(c.row); } std::string coordinatesToConjunction(const AgentName &agentName, const coordinates &c, const ViewDirection viewDirection) { - return "x" + agentName + "=" + std::to_string(c.first) + "&y" + agentName + "=" + std::to_string(c.second) + "&view" + agentName + "=" + std::to_string(viewDirection); + return "col" + agentName + "=" + std::to_string(c.first) + "&row" + agentName + "=" + std::to_string(c.second) + "&view" + agentName + "=" + std::to_string(viewDirection); } std::string objectPositionToConjunction(const AgentName &agentName, const std::string &identifier, const std::pair &relativePosition) { std::string xOffset = oneOffToString(relativePosition.first); std::string yOffset = oneOffToString(relativePosition.second); - return "x" + agentName + xOffset + "=x" + identifier + "&y" + agentName + yOffset + "=y" + identifier; + return "col" + agentName + xOffset + "=col" + identifier + "&row" + agentName + yOffset + "=row" + identifier; } std::string objectPositionToConjunction(const AgentName &agentName, const std::string &identifier, const std::pair &relativePosition, const ViewDirection viewDirection) { std::string xOffset = oneOffToString(relativePosition.first); std::string yOffset = oneOffToString(relativePosition.second); - return "x" + agentName + xOffset + "=x" + identifier + "&y" + agentName + yOffset + "=y" + identifier + "&view" + agentName + "=" + std::to_string(viewDirection); + return "col" + agentName + xOffset + "=col" + identifier + "&row" + agentName + yOffset + "=row" + identifier + "&view" + agentName + "=" + std::to_string(viewDirection); } std::map getAdjacentCells(const cell &c) { diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index 4adc004..5c2020c 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -9,10 +9,10 @@ #define FORWARD 2 -std::string northUpdate(const AgentName &a) { return "(y"+a+"'=y"+a+"-1)"; } -std::string southUpdate(const AgentName &a) { return "(y"+a+"'=y"+a+"+1)"; } -std::string eastUpdate(const AgentName &a) { return "(x"+a+"'=x"+a+"+1)"; } -std::string westUpdate(const AgentName &a) { return "(x"+a+"'=x"+a+"-1)"; } +std::string northUpdate(const AgentName &a) { return "(row"+a+"'=row"+a+"-1)"; } +std::string southUpdate(const AgentName &a) { return "(row"+a+"'=row"+a+"+1)"; } +std::string eastUpdate(const AgentName &a) { return "(col"+a+"'=col"+a+"+1)"; } +std::string westUpdate(const AgentName &a) { return "(col"+a+"'=col"+a+"-1)"; } namespace prism { @@ -167,8 +167,8 @@ namespace prism { void PrismModulesPrinter::printRobotModule(const AgentName &agentName, const coordinates &initialPosition) { os << "\nmodule " << agentName << std::endl; - os << "\tx" << agentName << " : [1.." << maxBoundaries.second << "] init " << initialPosition.second << ";\n"; - os << "\ty" << agentName << " : [1.." << maxBoundaries.first << "] init " << initialPosition.first << ";\n"; + os << "\tcol" << agentName << " : [1.." << maxBoundaries.second << "] init " << initialPosition.second << ";\n"; + os << "\trow" << agentName << " : [1.." << maxBoundaries.first << "] init " << initialPosition.first << ";\n"; os << "\tview" << agentName << " : [0..3] init 1;\n"; printTurnActionsForRobot(agentName); -- 2.20.1 From bac91e7b5dc5fa05e6761a8a32ac5b820909686c Mon Sep 17 00:00:00 2001 From: sp Date: Wed, 10 Jan 2024 18:47:44 +0100 Subject: [PATCH 5/5] fixed bug in west slippery updates --- util/PrismModulesPrinter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index 5c2020c..9912f79 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -381,7 +381,7 @@ namespace prism { actionStream << printSlipperyMovementGuard(a, "West", 3, {"!"+a+"CannotSlipNorth", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, northUpdate(a) }, {1 - probIntended, westUpdate(a)+"&"+northUpdate(a)} }) << ";\n"; actionStream << printSlipperyMovementGuard(a, "West", 3, { a+"CannotSlipNorth", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)+"&"+northUpdate(a)} }) << ";\n"; - actionStream << printSlipperyMovementGuard(a, "West", 3, {"!"+a+"CannotSlipNorth", a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a) } }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "West", 3, {"!"+a+"CannotSlipNorth", a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, northUpdate(a) } }) << ";\n"; actionStream << printSlipperyMovementGuard(a, "West", 3, { a+"CannotSlipNorth", a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", {}) << ";\n"; actionStream << printSlipperyMovementGuard(a, "West", 1, {"!"+a+"CannotSlipSouth", "!"+a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, southUpdate(a) }, {1 - probIntended, westUpdate(a)+"&"+southUpdate(a)} }) << ";\n"; -- 2.20.1