diff --git a/main.cpp b/main.cpp index 8228deb..fc78157 100644 --- a/main.cpp +++ b/main.cpp @@ -3,6 +3,7 @@ #include "util/Grid.h" #include "util/ConfigYaml.h" +#include #include #include #include @@ -163,7 +164,7 @@ int main(int argc, char* argv[]) { setProbability(properties, parsed_properties, probTurnIntendedIdentifier, probTurnIntended); } if(ok) { - Grid grid(contentCells, backgroundCells, stateRewards, probIntended, faultyProbability); + Grid grid(contentCells, backgroundCells, stateRewards, probIntended, probTurnIntended, faultyProbability); auto modelTypeIter = std::find_if(parsed_properties.begin(), parsed_properties.end(), [](const Property& obj) -> bool {return obj.property == "modeltype";}); prism::ModelType modelType = prism::ModelType::MDP;; @@ -176,7 +177,7 @@ int main(int argc, char* argv[]) { grid.setModelType(modelType); } - + //grid.printToPrism(std::cout, configurations); diff --git a/util/Grid.cpp b/util/Grid.cpp index c80570c..d276c7b 100644 --- a/util/Grid.cpp +++ b/util/Grid.cpp @@ -3,15 +3,15 @@ #include -Grid::Grid(cells gridCells, cells background, const std::map &stateRewards, const float probIntended, const float faultyProbability) - : allGridCells(gridCells), background(background), stateRewards(stateRewards), probIntended(probIntended), faultyProbability(faultyProbability) +Grid::Grid(cells gridCells, cells background, const std::map &stateRewards, const float probIntended, const float probTurnIntended, const float faultyProbability) + : allGridCells(gridCells), background(background), stateRewards(stateRewards), probIntended(probIntended), probTurnIntended(probTurnIntended), faultyProbability(faultyProbability) { cell max = allGridCells.at(allGridCells.size() - 1); maxBoundaries = std::make_pair(max.column - 1, max.row - 1); std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(walls), [](cell c) { return c.type == Type::Wall; }); std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(lava), [](cell c) { return c.type == Type::Lava; }); std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(floor), [](cell c) { return c.type == Type::Floor; }); // TODO CHECK IF ALL AGENTS ARE ADDED TO FLOOR - std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(slippery), [](cell c) { return c.type == Type::Slippery; }); + std::copy_if(background.begin(), background.end(), std::back_inserter(slippery), [](cell c) { return c.type == Type::Slippery; }); std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyNorth), [](cell c) { return c.type == Type::SlipperyNorth; }); std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyEast), [](cell c) { return c.type == Type::SlipperyEast; }); std::copy_if(background.begin(), background.end(), std::back_inserter(slipperySouth), [](cell c) { return c.type == Type::SlipperySouth; }); @@ -173,7 +173,7 @@ void Grid::printToPrism(std::ostream& os, std::vector& configurat std::string agentName = agentNames.at(0); prism::PrismFormulaPrinter formulas(os, wallRestrictions, walls, lockedDoors, unlockedDoors, keys, slipperyTiles, lava, goals, agentNameAndPositionMap, faultyProbability > 0.0); - prism::PrismModulesPrinter modules(os, modelType, maxBoundaries, lockedDoors, unlockedDoors, keys, slipperyTiles, agentNameAndPositionMap, configuration, probIntended, faultyProbability, !lava.empty(), !goals.empty()); + prism::PrismModulesPrinter modules(os, modelType, maxBoundaries, lockedDoors, unlockedDoors, keys, slipperyTiles, agentNameAndPositionMap, configuration, probIntended, probTurnIntended, faultyProbability, !lava.empty(), !goals.empty()); modules.printModelType(modelType); for(const auto &agentName : agentNames) { diff --git a/util/Grid.h b/util/Grid.h index 74e4e9f..298ec26 100644 --- a/util/Grid.h +++ b/util/Grid.h @@ -13,7 +13,7 @@ class Grid { public: - Grid(cells gridCells, cells background, const std::map &stateRewards = {}, const float probIntended = 1.0, const float faultyProbability = 0); + Grid(cells gridCells, cells background, const std::map &stateRewards = {}, const float probIntended = 1.0, const float probTurnIntended = 1.0, const float faultyProbability = 0); cells getGridCells(); @@ -64,5 +64,6 @@ class Grid { std::map stateRewards; const float probIntended; + const float probTurnIntended; const float faultyProbability; }; diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index fdd8df2..a2855da 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -12,8 +12,8 @@ std::string westUpdate(const AgentName &a) { return "(col"+a+"'=col"+a+"-1)"; } namespace prism { - PrismModulesPrinter::PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector config, const float probIntended, const float faultyProbability, const bool anyLava, const bool anyGoals) - : os(os), modelType(modelType), maxBoundaries(maxBoundaries), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), agentNameAndPositionMap(agentNameAndPositionMap), configuration(config), probIntended(probIntended), faultyProbability(faultyProbability), anyLava(anyLava), anyGoals(anyGoals) { + PrismModulesPrinter::PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector config, const float probIntended, const float probTurnIntended, const float faultyProbability, const bool anyLava, const bool anyGoals) + : os(os), modelType(modelType), maxBoundaries(maxBoundaries), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), agentNameAndPositionMap(agentNameAndPositionMap), configuration(config), probIntended(probIntended), probTurnIntended(probTurnIntended), faultyProbability(faultyProbability), anyLava(anyLava), anyGoals(anyGoals) { numberOfPlayer = agentNameAndPositionMap.size(); size_t index = 0; for(auto begin = agentNameAndPositionMap.begin(); begin != agentNameAndPositionMap.end(); begin++, index++) { @@ -283,6 +283,10 @@ namespace prism { } void PrismModulesPrinter::printSlipperyMovementActionsForRobot(const AgentName &a) { + if(!slipperyTiles.at("Slippery").empty()) { + printSlipperyMovementActionsForSlippery(a); + printSlipperyTurnActionsForSlippery(a); + } if(!slipperyTiles.at("North").empty()) { printSlipperyMovementActionsForNorth(a); printSlipperyTurnActionsForNorth(a); @@ -316,10 +320,47 @@ namespace prism { printSlipperyTurnActionsForSouthWest(a); } } + void PrismModulesPrinter::printSlipperyMovementActionsForSlippery(const AgentName &a) { + actionStream << printSlipperyMovementGuard(a, "Slippery", 0, {"!"+a+"CannotSlipEast", "!"+a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {probIntended, eastUpdate(a)}, {(1 - probIntended) * 0.5, northUpdate(a)}, {(1 - probIntended) * 0.5, southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 0, { a+"CannotSlipEast", "!"+a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {0.5 , northUpdate(a)}, {0.5 , southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 0, {"!"+a+"CannotSlipEast", a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, eastUpdate(a)}, {(1 - probIntended) * 0.5, southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 0, {"!"+a+"CannotSlipEast", "!"+a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, eastUpdate(a)}, {(1 - probIntended) * 0.5, northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 0, { a+"CannotSlipEast", a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { { 1 , southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 0, {"!"+a+"CannotSlipEast", a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {1 , eastUpdate(a)}, }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 0, { a+"CannotSlipEast", "!"+a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {1 , northUpdate(a)}, }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 0, { a+"CannotSlipEast", a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { }) << ";\n"; + + actionStream << printSlipperyMovementGuard(a, "Slippery", 1, {"!"+a+"CannotSlipSouth", "!"+a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {probIntended, southUpdate(a)}, {(1 - probIntended) * 0.5, eastUpdate(a)}, {(1 - probIntended) * 0.5, westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 1, { a+"CannotSlipSouth", "!"+a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {0.5 , eastUpdate(a)}, {0.5 , westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 1, {"!"+a+"CannotSlipSouth", a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, southUpdate(a)}, {(1 - probIntended) * 0.5, westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 1, {"!"+a+"CannotSlipSouth", "!"+a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, southUpdate(a)}, {(1 - probIntended) * 0.5, eastUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 1, { a+"CannotSlipSouth", a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { { 1 , westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 1, {"!"+a+"CannotSlipSouth", a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {1 , southUpdate(a)}, }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 1, { a+"CannotSlipSouth", "!"+a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {1 , eastUpdate(a)}, }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 1, { a+"CannotSlipSouth", a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { }) << ";\n"; + + actionStream << printSlipperyMovementGuard(a, "Slippery", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {probIntended, westUpdate(a)}, {(1 - probIntended) * 0.5, northUpdate(a)}, {(1 - probIntended) * 0.5, southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {0.5 , northUpdate(a)}, {0.5 , southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, westUpdate(a)}, {(1 - probIntended) * 0.5, southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, westUpdate(a)}, {(1 - probIntended) * 0.5, northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 2, { a+"CannotSlipWest", a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { { 1 , southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {1 , westUpdate(a)}, }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {1 , northUpdate(a)}, }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 2, { a+"CannotSlipWest", a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { }) << ";\n"; + + actionStream << printSlipperyMovementGuard(a, "Slippery", 3, {"!"+a+"CannotSlipNorth", "!"+a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {probIntended, northUpdate(a)}, {(1 - probIntended) * 0.5, eastUpdate(a)}, {(1 - probIntended) * 0.5, westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 3, { a+"CannotSlipNorth", "!"+a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {0.5 , eastUpdate(a)}, {0.5 , westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 3, {"!"+a+"CannotSlipNorth", a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, northUpdate(a)}, {(1 - probIntended) * 0.5, westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 3, {"!"+a+"CannotSlipNorth", "!"+a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, northUpdate(a)}, {(1 - probIntended) * 0.5, eastUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 3, { a+"CannotSlipNorth", a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { { 1 , westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 3, {"!"+a+"CannotSlipNorth", a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {1 , northUpdate(a)}, }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 3, { a+"CannotSlipNorth", "!"+a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {1 , eastUpdate(a)}, }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "Slippery", 3, { a+"CannotSlipNorth", a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { }) << ";\n"; + } void PrismModulesPrinter::printSlipperyMovementActionsForNorth(const AgentName &a) { - 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) * 0.5, northUpdate(a)+"&"+eastUpdate(a)}, {(1 - probIntended) * 0.5, northUpdate(a)+"&"+westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "North", 3, { a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {0.5, northUpdate(a)+"&"+eastUpdate(a)}, {0.5, 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"; @@ -342,8 +383,8 @@ namespace prism { } void PrismModulesPrinter::printSlipperyMovementActionsForEast(const AgentName &a) { - 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) * 0.5, eastUpdate(a)+"&"+southUpdate(a)}, {(1 - probIntended) * 0.5, eastUpdate(a)+"&"+northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "East", 0, { a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {0.5, eastUpdate(a)+"&"+southUpdate(a)}, {0.5, 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"; @@ -361,13 +402,13 @@ namespace prism { 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+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a) }, {1 - probIntended, "true"} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "East", 2, {"!"+a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, westUpdate(a) }, {1 - probIntended, "true"} }) << ";\n"; actionStream << printSlipperyMovementGuard(a, "East", 2, { a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {1, "true"} }) << ";\n"; } void PrismModulesPrinter::printSlipperyMovementActionsForSouth(const AgentName &a) { - 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) * 0.5, southUpdate(a)+"&"+eastUpdate(a)}, {(1 - probIntended) * 0.5, southUpdate(a)+"&"+westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "South", 1, { a+"CannotSlipSouth", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {0.5, southUpdate(a)+"&"+eastUpdate(a)}, {0.5, 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"; @@ -390,8 +431,8 @@ namespace prism { } void PrismModulesPrinter::printSlipperyMovementActionsForWest(const AgentName &a) { - 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) * 0.5, westUpdate(a)+"&"+southUpdate(a)}, {(1 - probIntended) * 0.5, westUpdate(a)+"&"+northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "West", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipSouthWest", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {0.5, westUpdate(a)+"&"+southUpdate(a)}, {0.5, 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"; @@ -409,46 +450,52 @@ namespace prism { 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+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a) }, {1 - probIntended, "true"} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "West", 0, {"!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, eastUpdate(a) }, {1 - probIntended, "true"} }) << ";\n"; actionStream << printSlipperyMovementGuard(a, "West", 0, { a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", {{1, "true"}}) << ";\n"; } + void PrismModulesPrinter::printSlipperyTurnActionsForSlippery(const AgentName &a) { + actionStream << printSlipperyTurnGuard(a, "right", "Slippery", RIGHT, {}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "Slippery", LEFT, {}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "Slippery", LEFT, {}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n"; + } + void PrismModulesPrinter::printSlipperyTurnActionsForNorth(const AgentName &a) { - actionStream << printSlipperyTurnGuard(a, "right", "North", RIGHT, {"!"+a+"CannotSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "right", "North", RIGHT, {"!"+a+"CannotSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probTurnIntended, northUpdate(a)} }) << ";\n"; actionStream << printSlipperyTurnGuard(a, "right", "North", RIGHT, { a+"CannotSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, {"!"+a+"CannotSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, northUpdate(a)} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, {"!"+a+"CannotSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, {"!"+a+"CannotSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probTurnIntended, northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, {"!"+a+"CannotSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=3)"}, {1 - probTurnIntended, northUpdate(a)} }) << ";\n"; actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, { a+"CannotSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n"; actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, { a+"CannotSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n"; } void PrismModulesPrinter::printSlipperyTurnActionsForEast(const AgentName &a) { - actionStream << printSlipperyTurnGuard(a, "right", "East", RIGHT, {"!"+a+"CannotSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, eastUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "right", "East", RIGHT, {"!"+a+"CannotSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probTurnIntended, eastUpdate(a)} }) << ";\n"; actionStream << printSlipperyTurnGuard(a, "right", "East", RIGHT, { a+"CannotSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, {"!"+a+"CannotSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, eastUpdate(a)} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, {"!"+a+"CannotSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, eastUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, {"!"+a+"CannotSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probTurnIntended, eastUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, {"!"+a+"CannotSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=3)"}, {1 - probTurnIntended, eastUpdate(a)} }) << ";\n"; actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, { a+"CannotSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n"; actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, { a+"CannotSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n"; } void PrismModulesPrinter::printSlipperyTurnActionsForSouth(const AgentName &a) { - actionStream << printSlipperyTurnGuard(a, "right", "South", RIGHT, {"!"+a+"CannotSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "right", "South", RIGHT, {"!"+a+"CannotSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probTurnIntended, southUpdate(a)} }) << ";\n"; actionStream << printSlipperyTurnGuard(a, "right", "South", RIGHT, { a+"CannotSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, {"!"+a+"CannotSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, southUpdate(a)} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, {"!"+a+"CannotSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, {"!"+a+"CannotSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probTurnIntended, southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, {"!"+a+"CannotSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=3)"}, {1 - probTurnIntended, southUpdate(a)} }) << ";\n"; actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, { a+"CannotSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n"; actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, { a+"CannotSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n"; } void PrismModulesPrinter::printSlipperyTurnActionsForWest(const AgentName &a) { - actionStream << printSlipperyTurnGuard(a, "right", "West", RIGHT, {"!"+a+"CannotSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "right", "West", RIGHT, {"!"+a+"CannotSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probTurnIntended, westUpdate(a)} }) << ";\n"; actionStream << printSlipperyTurnGuard(a, "right", "West", RIGHT, { a+"CannotSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, {"!"+a+"CannotSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, westUpdate(a)} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, {"!"+a+"CannotSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, {"!"+a+"CannotSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probTurnIntended, westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, {"!"+a+"CannotSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=3)"}, {1 - probTurnIntended, westUpdate(a)} }) << ";\n"; actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, { a+"CannotSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n"; actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, { a+"CannotSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n"; } @@ -720,7 +767,7 @@ namespace prism { } bool PrismModulesPrinter::slipperyBehaviour() const { - return !slipperyTiles.at("North").empty() || !slipperyTiles.at("East").empty() || !slipperyTiles.at("South").empty() || !slipperyTiles.at("West").empty(); + return !slipperyTiles.at("Slippery").empty() || !slipperyTiles.at("North").empty() || !slipperyTiles.at("East").empty() || !slipperyTiles.at("South").empty() || !slipperyTiles.at("West").empty(); } bool PrismModulesPrinter::isGame() const { diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h index af7601b..2178d44 100644 --- a/util/PrismModulesPrinter.h +++ b/util/PrismModulesPrinter.h @@ -16,7 +16,7 @@ std::string westUpdate(const AgentName &a); namespace prism { class PrismModulesPrinter { public: - PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector config, const float probIntended, const float faultyProbability, const bool anyLava, const bool anyGoals); + PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector config, const float probIntended, const float probTurnIntended, const float faultyProbability, const bool anyLava, const bool anyGoals); std::ostream& print(); @@ -40,10 +40,12 @@ namespace prism { void printTurnActionsForRobot(const std::string &a); void printNonMovementActionsForRobot(const AgentName &agentName); void printSlipperyMovementActionsForRobot(const AgentName &a); + void printSlipperyMovementActionsForSlippery(const AgentName &a); void printSlipperyMovementActionsForNorth(const AgentName &a); void printSlipperyMovementActionsForEast(const AgentName &a); void printSlipperyMovementActionsForSouth(const AgentName &a); void printSlipperyMovementActionsForWest(const AgentName &a); + void printSlipperyTurnActionsForSlippery(const AgentName &a); void printSlipperyTurnActionsForNorth(const AgentName &a); void printSlipperyTurnActionsForEast(const AgentName &a); void printSlipperyTurnActionsForSouth(const AgentName &a); @@ -113,6 +115,7 @@ namespace prism { size_t numberOfPlayer; float const faultyProbability; float const probIntended; + float const probTurnIntended; std::vector configuration; std::vector viewDirections = {0, 1, 2, 3}; std::map viewDirectionToString = {{0, "East"}, {1, "South"}, {2, "West"}, {3, "North"}};