diff --git a/CMakeLists.txt b/CMakeLists.txt index 1a7c5c1..0392819 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,24 +1,26 @@ -include(util/CMakeLists.txt) - -set(CMAKE_CXX_STANDARD 20) - -set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D__FILENAME__='\"$(subst ${CMAKE_SOURCE_DIR}/,,$(abspath $<))\"'") -add_definitions(-DLOG_DEBUG) - cmake_minimum_required(VERSION 3.0...3.22) - -set(CMAKE_BUILD_TYPE Debug) - project( Minigrid2PRISM VERSION 0.1 LANGUAGES CXX) +set(CMAKE_CXX_STANDARD 20) -find_package(yaml-cpp) - -add_executable(main - ${SRCS} - main.cpp - ) - -target_link_libraries(main pthread yaml-cpp) +include(util/CMakeLists.txt) +include(FetchContent) + +FetchContent_Declare( + yaml-cpp + GIT_REPOSITORY https://github.com/jbeder/yaml-cpp.git + GIT_TAG master + OVERRIDE_FIND_PACKAGE +) +FetchContent_GetProperties(yaml-cpp) +if(NOT yaml-cpp_POPULATED) + message(STATUS "Fetching yaml-cpp...") + FetchContent_Populate(yaml-cpp) + add_subdirectory(${yaml-cpp_SOURCE_DIR} ${yaml-cpp_BINARY_DIR}) +endif() +FetchContent_MakeAvailable(yaml-cpp) + +add_executable(main ${SRCS} main.cpp) +target_link_libraries(main pthread yaml-cpp::yaml-cpp) diff --git a/main.cpp b/main.cpp index 37b3a36..be33399 100644 --- a/main.cpp +++ b/main.cpp @@ -144,12 +144,13 @@ int main(int argc, char* argv[]) { pos_iterator_t backgroundIter = backgroundFirst; pos_iterator_t backgroundLast(background.end()); MinigridParser backgroundParser(backgroundFirst); - + cells contentCells; cells backgroundCells; std::vector configurations; std::map stateRewards; - double faultyProbability; + float faultyProbability = 0.0; + float probIntended = 0.9; try { bool ok = phrase_parse(contentIter, contentLast, contentParser, qi::space, contentCells); @@ -157,7 +158,7 @@ int main(int argc, char* argv[]) { ok &= phrase_parse(backgroundIter, backgroundLast, backgroundParser, qi::space, backgroundCells); // TODO } if (configFilename->is_set()) { - YamlConfigParser parser(configFilename->value(0)); + YamlConfigParser parser(configFilename->value(0)); configurations = parser.parseConfiguration(); } @@ -181,8 +182,9 @@ int main(int argc, char* argv[]) { } } if(ok) { - Grid grid(contentCells, backgroundCells, gridOptions, stateRewards, faultyProbability); - //grid.printToPrism(std::cout, prism::ModelType::MDP); + Grid grid(contentCells, backgroundCells, gridOptions, stateRewards, probIntended, faultyProbability); + + grid.printToPrism(std::cout, configurations , gridOptions.getModelType()); std::stringstream ss; // grid.printToPrism(file, configurations ,prism::ModelType::MDP); grid.printToPrism(ss, configurations , gridOptions.getModelType()); diff --git a/util/CMakeLists.txt b/util/CMakeLists.txt index 877fde4..2325d92 100644 --- a/util/CMakeLists.txt +++ b/util/CMakeLists.txt @@ -2,7 +2,9 @@ list(APPEND SRCS ${CMAKE_CURRENT_LIST_DIR}/cell.cpp ${CMAKE_CURRENT_LIST_DIR}/MinigridGrammar.h ${CMAKE_CURRENT_LIST_DIR}/Grid.cpp + ${CMAKE_CURRENT_LIST_DIR}/PrismPrinter.cpp ${CMAKE_CURRENT_LIST_DIR}/PrismModulesPrinter.cpp + ${CMAKE_CURRENT_LIST_DIR}/PrismFormulaPrinter.cpp ${CMAKE_CURRENT_LIST_DIR}/popl.hpp ${CMAKE_CURRENT_LIST_DIR}/OptionParser.cpp ${CMAKE_CURRENT_LIST_DIR}/ConfigYaml.cpp diff --git a/util/Grid.cpp b/util/Grid.cpp index d14a3a0..294ddd1 100644 --- a/util/Grid.cpp +++ b/util/Grid.cpp @@ -3,62 +3,36 @@ #include -prism::ModelType GridOptions::getModelType() const +prism::ModelType GridOptions::getModelType() const { if (agentsWithView.size() > 1) { return prism::ModelType::SMG; - } - + } return prism::ModelType::MDP; } -Grid::Grid(cells gridCells, cells background, const GridOptions &gridOptions, const std::map &stateRewards, const double faultyProbability) - : allGridCells(gridCells), background(background), gridOptions(gridOptions), stateRewards(stateRewards), faultyProbability(faultyProbability) +Grid::Grid(cells gridCells, cells background, const GridOptions &gridOptions, const std::map &stateRewards, const float probIntended, const float faultyProbability) + : allGridCells(gridCells), background(background), gridOptions(gridOptions), stateRewards(stateRewards), probIntended(probIntended), faultyProbability(faultyProbability) { cell max = allGridCells.at(allGridCells.size() - 1); maxBoundaries = std::make_pair(max.row - 1, max.column - 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; - }); - 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; - }); - std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyWest), [](cell c) { - return c.type == Type::SlipperyWest; - }); - std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(lockedDoors), [](cell c) { - return c.type == Type::LockedDoor; - }); - std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(unlockedDoors), [](cell c) { - return c.type == Type::Door; - }); - std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(goals), [](cell c) { - return c.type == Type::Goal; - }); - std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(keys), [this](cell c) { - return c.type == Type::Key; - }); - std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(boxes), [](cell c) { - return c.type == Type::Box; - }); - agent = *std::find_if(gridCells.begin(), gridCells.end(), [](cell c) { - return c.type == Type::Agent; - }); - std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(adversaries), [](cell c) { - return c.type == Type::Adversary; - }); + 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(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; }); + std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyWest), [](cell c) { return c.type == Type::SlipperyWest; }); + std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(lockedDoors), [](cell c) { return c.type == Type::LockedDoor; }); + std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(unlockedDoors), [](cell c) { return c.type == Type::Door; }); + std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(goals), [](cell c) { return c.type == Type::Goal; }); + std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(keys), [](cell c) { return c.type == Type::Key; }); + std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(boxes), [](cell c) { return c.type == Type::Box; }); + std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(balls), [](cell c) { return c.type == Type::Ball; }); + std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(adversaries), [](cell c) { return c.type == Type::Adversary; }); + agent = *std::find_if(gridCells.begin(), gridCells.end(), [](cell c) { return c.type == Type::Agent; }); + floor.push_back(agent); + agentNameAndPositionMap.insert({ "Agent", agent.getCoordinates() }); for(auto const& adversary : adversaries) { std::string color = adversary.getColor(); @@ -66,6 +40,7 @@ Grid::Grid(cells gridCells, cells background, const GridOptions &gridOptions, co try { if(gridOptions.agentsToBeConsidered.size() != 0 && std::find(gridOptions.agentsToBeConsidered.begin(), gridOptions.agentsToBeConsidered.end(), color) == gridOptions.agentsToBeConsidered.end()) continue; auto success = agentNameAndPositionMap.insert({ color, adversary.getCoordinates() }); + floor.push_back(adversary); if(!success.second) { throw std::logic_error("Agent with " + color + " already present\n"); } @@ -113,43 +88,16 @@ cells Grid::getGridCells() { } bool Grid::isBlocked(coordinates p) { - return isWall(p); //|| isLockedDoor(p) || isKey(p); + return isWall(p); } bool Grid::isWall(coordinates p) { return std::find_if(walls.begin(), walls.end(), [p](cell cell) { - return cell.row == p.first && cell.column == p.second; + return cell.row == p.second && cell.column == p.first; }) != walls.end(); } -bool Grid::isLockedDoor(coordinates p) { - return std::find_if(lockedDoors.begin(), lockedDoors.end(), - [p](cell cell) { - return cell.row == p.first && cell.column == p.second; - }) != lockedDoors.end(); -} - -bool Grid::isUnlockedDoor(coordinates p) { - return std::find_if(unlockedDoors.begin(), unlockedDoors.end(), - [p](cell cell) { - return cell.row == p.first && cell.column == p.second; - }) != unlockedDoors.end(); -} - -bool Grid::isKey(coordinates p) { - return std::find_if(keys.begin(), keys.end(), - [p](cell cell) { - return cell.row == p.first && cell.column == p.second; - }) != keys.end(); -} - -bool Grid::isBox(coordinates p) { - return std::find_if(boxes.begin(), boxes.end(), - [p](cell cell) { - return cell.row == p.first && cell.column == p.second; - }) != boxes.end(); -} void Grid::applyOverwrites(std::string& str, std::vector& configuration) { for (auto& config : configuration) { @@ -157,7 +105,7 @@ void Grid::applyOverwrites(std::string& str, std::vector& configu continue; } size_t start_pos; - + if (config.type_ == ConfigType::Formula) { start_pos = str.find("formula " + config.identifier_); } else if (config.type_ == ConfigType::Label) { @@ -177,168 +125,64 @@ void Grid::applyOverwrites(std::string& str, std::vector& configu size_t end_pos = str.find(';', start_pos) + 1; std::string expression = config.expression_; - + str.replace(start_pos, end_pos - start_pos , expression); } } - void Grid::printToPrism(std::ostream& os, std::vector& configuration ,const prism::ModelType& modelType) { - cells northRestriction; - cells eastRestriction; - cells southRestriction; - cells westRestriction; - cells walkable = floor; - cells conditionallyWalkable; + cells northRestriction, eastRestriction, southRestriction, westRestriction; + cells walkable = floor; walkable.insert(walkable.end(), goals.begin(), goals.end()); walkable.insert(walkable.end(), boxes.begin(), boxes.end()); - walkable.push_back(agent); - walkable.insert(walkable.end(), adversaries.begin(), adversaries.end()); walkable.insert(walkable.end(), lava.begin(), lava.end()); - - conditionallyWalkable.insert(conditionallyWalkable.end(), keys.begin(), keys.end()); - conditionallyWalkable.insert(conditionallyWalkable.end(), lockedDoors.begin(), lockedDoors.end()); - conditionallyWalkable.insert(conditionallyWalkable.end(), unlockedDoors.begin(), unlockedDoors.end()); + walkable.insert(walkable.end(), keys.begin(), keys.end()); + walkable.insert(walkable.end(), balls.begin(), balls.end()); for(auto const& c : walkable) { - if(isBlocked(c.getNorth())) northRestriction.push_back(c); - if(isBlocked(c.getEast())) eastRestriction.push_back(c); - if(isBlocked(c.getSouth())) southRestriction.push_back(c); - if(isBlocked(c.getWest())) westRestriction.push_back(c); - } - // TODO Add doors here (list of doors keys etc) - // walkable.insert(walkable.end(), lockedDoors.begin(), lockedDoors.end()); - // walkable.insert(walkable.end(), unlockedDoors.begin(), unlockedDoors.end()); - for(auto const& c : conditionallyWalkable) { - if(isBlocked(c.getNorth())) northRestriction.push_back(c); - if(isBlocked(c.getEast())) eastRestriction.push_back(c); - if(isBlocked(c.getSouth())) southRestriction.push_back(c); - if(isBlocked(c.getWest())) westRestriction.push_back(c); + if(isWall(c.getNorth())) northRestriction.push_back(c); + if(isWall(c.getEast())) eastRestriction.push_back(c); + if(isWall(c.getSouth())) southRestriction.push_back(c); + if(isWall(c.getWest())) westRestriction.push_back(c); } - prism::PrismModulesPrinter printer(modelType, agentNameAndPositionMap.size(), configuration, gridOptions.enforceOneWays); - printer.printModel(os, modelType); - if(modelType == prism::ModelType::SMG) { - printer.printGlobalMoveVariable(os, agentNameAndPositionMap.size()); - } - for(auto const &backgroundTilesOfColor : backgroundTiles) { - for(auto agentNameAndPosition = agentNameAndPositionMap.begin(); agentNameAndPosition != agentNameAndPositionMap.end(); ++agentNameAndPosition) { - printer.printBackgroundLabels(os, agentNameAndPosition->first, backgroundTilesOfColor); - } - } - cells noTurnFloor; - if(gridOptions.enforceOneWays) { - for(auto const& c : floor) { - cell east = c.getEast(allGridCells); - cell south = c.getSouth(allGridCells); - cell west = c.getWest(allGridCells); - cell north = c.getNorth(allGridCells); - if( (east.type == Type::Wall && west.type == Type::Wall) or - (north.type == Type::Wall && south.type == Type::Wall) ) { - noTurnFloor.push_back(c); - } - } - } - cells doors; - doors.insert(doors.end(), lockedDoors.begin(), lockedDoors.end()); - doors.insert(doors.end(), unlockedDoors.begin(), unlockedDoors.end()); - for(auto agentNameAndPosition = agentNameAndPositionMap.begin(); agentNameAndPosition != agentNameAndPositionMap.end(); ++agentNameAndPosition) { - printer.printFormulas(os, agentNameAndPosition->first, northRestriction, eastRestriction, southRestriction, westRestriction, { slipperyNorth, slipperyEast, slipperySouth, slipperyWest }, lava, walls, noTurnFloor, slipperyNorth, slipperyEast, slipperySouth, slipperyWest, keys, doors); - printer.printGoalLabel(os, agentNameAndPosition->first, goals); - printer.printKeysLabels(os, agentNameAndPosition->first, keys); - } - std::vector constants {"const double prop_zero = 0/9;", - "const double prop_intended = 6/9;", - "const double prop_turn_intended = 6/9;", - "const double prop_displacement = 3/9;", - "const double prop_turn_displacement = 3/9;", - "const int width = " + std::to_string(maxBoundaries.first) + ";", - "const int height = " + std::to_string(maxBoundaries.second) + ";" - }; - printer.printConstants(os, constants); + std::map wallRestrictions = {{"North", northRestriction}, {"East", eastRestriction}, {"South", southRestriction}, {"West", westRestriction}}; + std::map slipperyTiles = {{"North", slipperyNorth}, {"East", slipperyEast}, {"South", slipperySouth}, {"West", slipperyWest}}; std::vector agentNames; std::transform(agentNameAndPositionMap.begin(), agentNameAndPositionMap.end(), std::back_inserter(agentNames), [](const std::map::value_type &pair){return pair.first;}); - if(modelType == prism::ModelType::SMG) { - printer.printCrashLabel(os, agentNames); - } - size_t agentIndex = 0; - - printer.printInitStruct(os, agentNameAndPositionMap, keyNameAndPositionMap, lockedDoors, unlockedDoors, modelType); - - - for(auto agentNameAndPosition = agentNameAndPositionMap.begin(); agentNameAndPosition != agentNameAndPositionMap.end(); ++agentNameAndPosition, agentIndex++) { - AgentName agentName = agentNameAndPosition->first; - //std::cout << "Agent Name: " << agentName << std::endl; - bool agentWithView = std::find(gridOptions.agentsWithView.begin(), gridOptions.agentsWithView.end(), agentName) != gridOptions.agentsWithView.end(); - bool agentWithProbabilisticBehaviour = std::find(gridOptions.agentsWithProbabilisticBehaviour.begin(), gridOptions.agentsWithProbabilisticBehaviour.end(), agentName) != gridOptions.agentsWithProbabilisticBehaviour.end(); - std::set slipperyActions; // TODO AGENT POSITION INITIALIZATIN - if(agentWithProbabilisticBehaviour) printer.printModule(os, agentName, agentIndex, maxBoundaries, agentNameAndPosition->second, keys, backgroundTiles, agentWithView, gridOptions.probabilitiesForActions); - else printer.printModule(os, agentName, agentIndex, maxBoundaries, agentNameAndPosition->second, keys, backgroundTiles, agentWithView, {} ,faultyProbability); - for(auto const& c : slipperyNorth) { - printer.printSlipperyMove(os, agentName, agentIndex, c.getCoordinates(), slipperyActions, getWalkableDirOf8Neighborhood(c), prism::PrismModulesPrinter::SlipperyType::North); - if(!gridOptions.enforceOneWays) printer.printSlipperyTurn(os, agentName, agentIndex, c.getCoordinates(), slipperyActions, getWalkableDirOf8Neighborhood(c), prism::PrismModulesPrinter::SlipperyType::North); - - } - for(auto const& c : slipperyEast) { - printer.printSlipperyMove(os, agentName, agentIndex, c.getCoordinates(), slipperyActions, getWalkableDirOf8Neighborhood(c), prism::PrismModulesPrinter::SlipperyType::East); - if(!gridOptions.enforceOneWays) printer.printSlipperyTurn(os, agentName, agentIndex, c.getCoordinates(), slipperyActions, getWalkableDirOf8Neighborhood(c), prism::PrismModulesPrinter::SlipperyType::East); - } - for(auto const& c : slipperySouth) { - printer.printSlipperyMove(os, agentName, agentIndex, c.getCoordinates(), slipperyActions, getWalkableDirOf8Neighborhood(c), prism::PrismModulesPrinter::SlipperyType::South); - if(!gridOptions.enforceOneWays) printer.printSlipperyTurn(os, agentName, agentIndex, c.getCoordinates(), slipperyActions, getWalkableDirOf8Neighborhood(c), prism::PrismModulesPrinter::SlipperyType::South); - } - for(auto const& c : slipperyWest) { - printer.printSlipperyMove(os, agentName, agentIndex, c.getCoordinates(), slipperyActions, getWalkableDirOf8Neighborhood(c), prism::PrismModulesPrinter::SlipperyType::West); - if(!gridOptions.enforceOneWays) printer.printSlipperyTurn(os, agentName, agentIndex, c.getCoordinates(), slipperyActions, getWalkableDirOf8Neighborhood(c), prism::PrismModulesPrinter::SlipperyType::West); - } - - printer.printEndmodule(os); + std::string agentName = agentNames.at(0); - if(modelType == prism::ModelType::SMG) { - if(agentWithProbabilisticBehaviour) printer.printPlayerStruct(os, agentNameAndPosition->first, agentWithView, gridOptions.probabilitiesForActions, slipperyActions); - else printer.printPlayerStruct(os, agentNameAndPosition->first, agentWithView, {}, slipperyActions); - } - //if(!stateRewards.empty()) { - printer.printRewards(os, agentName, stateRewards, lava, goals, backgroundTiles); - //} + prism::PrismFormulaPrinter formulas(os, wallRestrictions, walls, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, lava, goals); + prism::PrismModulesPrinter modules(os, modelType, maxBoundaries, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, agentNameAndPositionMap, configuration, probIntended, faultyProbability); + modules.printModelType(modelType); + for(const auto &agentName : agentNames) { + formulas.print(agentName); } + //std::vector constants {"const double prop_zero = 0/9;", + // "const double prop_intended = 6/9;", + // "const double prop_turn_intended = 6/9;", + // "const double prop_displacement = 3/9;", + // "const double prop_turn_displacement = 3/9;", + // "const int width = " + std::to_string(maxBoundaries.first) + ";", + // "const int height = " + std::to_string(maxBoundaries.second) + ";" + // }; + //modules.printConstants(os, constants); + modules.print(); - if (!configuration.empty()) { - printer.printConfiguration(os, configuration); - } - // TODO CHANGE HANDLING - std::string agentName = agentNames.at(0); - for (auto const & key : keys) { - os << "\n"; - printer.printKeyModule(os, key, maxBoundaries, agentName); - printer.printEndmodule(os); - } - for (auto const& door : lockedDoors) { - os << "\n"; - printer.printDoorModule(os, door, maxBoundaries, agentName); - printer.printEndmodule(os); - } -} + //if(!stateRewards.empty()) { + // modules.printRewards(os, agentName, stateRewards, lava, goals, backgroundTiles); + //} -std::array Grid::getWalkableDirOf8Neighborhood(cell c) /* const */ { - return (std::array) - { - !isBlocked(c.getNorth()), - !isBlocked(c.getNorth(allGridCells).getEast()), - !isBlocked(c.getEast()), - !isBlocked(c.getSouth(allGridCells).getEast()), - !isBlocked(c.getSouth()), - !isBlocked(c.getSouth(allGridCells).getWest()), - !isBlocked(c.getWest()), - !isBlocked(c.getNorth(allGridCells).getWest()) - }; + //if (!configuration.empty()) { + // modules.printConfiguration(os, configuration); + //} } diff --git a/util/Grid.h b/util/Grid.h index 29e9e20..eb95437 100644 --- a/util/Grid.h +++ b/util/Grid.h @@ -7,6 +7,7 @@ #include "MinigridGrammar.h" #include "PrismModulesPrinter.h" +#include "PrismFormulaPrinter.h" #include "ConfigYaml.h" struct GridOptions { @@ -21,16 +22,12 @@ struct GridOptions { class Grid { public: - Grid(cells gridCells, cells background, const GridOptions &gridOptions, const std::map &stateRewards = {}, const double faultyProbability = 0); + Grid(cells gridCells, cells background, const GridOptions &gridOptions, const std::map &stateRewards = {}, const float probIntended = 1.0, const float faultyProbability = 0); cells getGridCells(); bool isBlocked(coordinates p); bool isWall(coordinates p); - bool isLockedDoor(coordinates p); - bool isUnlockedDoor(coordinates p); - bool isKey(coordinates p); - bool isBox(coordinates p); void printToPrism(std::ostream &os, std::vector& configuration, const prism::ModelType& modelType); void applyOverwrites(std::string& str, std::vector& configuration); @@ -59,6 +56,7 @@ class Grid { cells lockedDoors; cells unlockedDoors; cells boxes; + cells balls; cells lava; cells goals; @@ -67,5 +65,6 @@ class Grid { std::map backgroundTiles; std::map stateRewards; - double faultyProbability; + const float probIntended; + const float faultyProbability; }; diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp new file mode 100644 index 0000000..ef2f5a5 --- /dev/null +++ b/util/PrismFormulaPrinter.cpp @@ -0,0 +1,222 @@ +#include "PrismFormulaPrinter.h" + +#include +#include +#include + +std::string oneOffToString(const int &offset) { + return offset != 0 ? ( offset == 1 ? "+1" : "-1" ) : ""; +} + +std::string vectorToDisjunction(const std::vector &formulae) { + bool first = true; + std::string disjunction = ""; + for(const auto &formula : formulae) { + if(first) first = false; + else disjunction += " | "; + disjunction += formula; + } + return disjunction; +} + +std::string cellToConjunction(const AgentName &agentName, const cell &c) { + return "x" + agentName + "=" + std::to_string(c.column) + "&y" + 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); +} + +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); +} + +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; +} +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); +} + +std::map getAdjacentCells(const cell &c) { + return {{1, c.getNorth()}, {2, c.getEast()}, {3, c.getSouth()}, {0, c.getWest()}}; +} + +std::map> getRelativeAdjacentCells() { + return { {1, {0,+1}}, {2, {-1,0}}, {3, {0,-1}}, {0, {+1,0}} }; +} + +std::map> getRelativeSurroundingCells() { + return { {"NorthWest", {-1,-1}}, {"North", { 0,-1}}, {"NorthEast", {+1,-1}}, + {"West", {-1, 0}}, {"East", {+1, 0}}, + {"SouthWest", {-1,+1}}, {"South", { 0,+1}}, {"SouthEast", {+1,+1}} }; +} + +namespace prism { + PrismFormulaPrinter::PrismFormulaPrinter(std::ostream &os, const std::map &restrictions, const cells &walls, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map &slipperyTiles, const cells &lava, const cells &goals) + : os(os), restrictions(restrictions), walls(walls), boxes(boxes), balls(balls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), lava(lava), goals(goals) + { } + + void PrismFormulaPrinter::print(const AgentName &agentName) { + for(const auto& [direction, cells] : restrictions) { + printRestrictionFormula(agentName, direction, cells); + } + + if(slipperyBehaviour()) { + for(const auto& [direction, cells] : slipperyTiles) { + printIsOnFormula(agentName, "Slippery", cells, direction); + } + std::vector allSlipperyDirections = {agentName + "IsOnSlipperyNorth", agentName + "IsOnSlipperyEast", agentName + "IsOnSlipperySouth", agentName + "IsOnSlipperyWest"}; + os << buildFormula(agentName + "IsOnSlippery", vectorToDisjunction(allSlipperyDirections)); + + for(const auto& [direction, relativePosition] : getRelativeSurroundingCells()) { + printSlipRestrictionFormula(agentName, direction); + } + } else { + os << buildFormula(agentName + "IsOnSlippery", "false"); + } + printIsOnFormula(agentName, "Lava", lava); + printIsOnFormula(agentName, "Goal", goals); + + for(const auto& ball : balls) { + std::string identifier = capitalize(ball.getColor()) + ball.getType(); + printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp"); + portableObjects.push_back(agentName + "Carrying" + identifier); + } + + for(const auto& box : boxes) { + std::string identifier = capitalize(box.getColor()) + box.getType(); + printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp"); + portableObjects.push_back(agentName + "Carrying" + identifier); + } + + for(const auto& key : keys) { + std::string identifier = capitalize(key.getColor()) + key.getType(); + printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp"); + portableObjects.push_back(agentName + "Carrying" + identifier); + } + + for(const auto& door : unlockedDoors) { + std::string identifier = capitalize(door.getColor()) + door.getType(); + printRestrictionFormulaWithCondition(agentName, identifier, getAdjacentCells(door), "!" + identifier + "Open"); + printIsNextToFormula(agentName, identifier, getAdjacentCells(door)); + } + + for(const auto& door : lockedDoors) { + std::string identifier = capitalize(door.getColor()) + door.getType(); + printRestrictionFormulaWithCondition(agentName, identifier, getAdjacentCells(door), "!" + identifier + "Open"); + printIsNextToFormula(agentName, identifier, getAdjacentCells(door)); + } + + if(conditionalMovementRestrictions.size() > 0) { + os << buildFormula(agentName + "CannotMoveConditionally", vectorToDisjunction(conditionalMovementRestrictions)); + os << buildFormula(agentName + "IsCarrying", vectorToDisjunction(portableObjects)); + } else { + os << buildFormula(agentName + "CannotMoveConditionally", "false"); + } + } + + void PrismFormulaPrinter::printRestrictionFormula(const AgentName &agentName, const std::string &direction, const cells &grid_cells) { + os << buildFormula(agentName + "CannotMove" + direction + "Wall", buildDisjunction(agentName, grid_cells)); + } + + void PrismFormulaPrinter::printIsOnFormula(const AgentName &agentName, const std::string &type, const cells &grid_cells, const std::string &direction) { + os << buildFormula(agentName + "IsOn" + type + direction, buildDisjunction(agentName, grid_cells)); + } + + void PrismFormulaPrinter::printIsNextToFormula(const AgentName &agentName, const std::string &type, const std::map &coordinates) { + os << buildFormula(agentName + "IsNextTo" + type, buildDisjunction(agentName, coordinates)); + } + + void PrismFormulaPrinter::printRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::map &coordinates, const std::string &condition) { + os << buildFormula(agentName + "CannotMove" + reason, "(" + buildDisjunction(agentName, coordinates) + ") & " + condition); + conditionalMovementRestrictions.push_back(agentName + "CannotMove" + reason); + } + + void PrismFormulaPrinter::printRelativeRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::string &condition) { + os << buildFormula(agentName + "CannotMove" + reason, "(" + buildDisjunction(agentName, reason) + ") & " + condition); + conditionalMovementRestrictions.push_back(agentName + "CannotMove" + reason); + } + + void PrismFormulaPrinter::printSlipRestrictionFormula(const AgentName &agentName, const std::string &direction) { + std::pair slipCell = getRelativeSurroundingCells().at(direction); + bool semicolon = anyPortableObject() ? false : true; + os << buildFormula(agentName + "CannotSlip" + direction, buildDisjunction(agentName, walls, slipCell), semicolon); + for(auto const key : keys) { + std::string identifier = capitalize(key.getColor()) + key.getType(); + os << " | " << objectPositionToConjunction(agentName, identifier, slipCell); + } + for(auto const ball : balls) { + std::string identifier = capitalize(ball.getColor()) + ball.getType(); + os << " | " << objectPositionToConjunction(agentName, identifier, slipCell); + } + for(auto const box : boxes) { + std::string identifier = capitalize(box.getColor()) + box.getType(); + os << " | " << objectPositionToConjunction(agentName, identifier, slipCell); + } + os << ";\n"; + } + + std::string PrismFormulaPrinter::buildFormula(const std::string &formulaName, const std::string &formula, const bool semicolon) { + return "formula " + formulaName + " = " + formula + (semicolon ? ";\n": ""); + } + + std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const std::map &cells) { + if(cells.size() == 0) return "false"; + bool first = true; + std::string disjunction = ""; + for(const auto [viewDirection, coordinates] : cells) { + if(first) first = false; + else disjunction += " | "; + disjunction += "(" + coordinatesToConjunction(agentName, coordinates, viewDirection) + ")"; + } + return disjunction; + } + + std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const cells &cells) { + if(cells.size() == 0) return "false"; + bool first = true; + std::string disjunction = ""; + for(auto const cell : cells) { + if(first) first = false; + else disjunction += " | "; + disjunction += "(" + cellToConjunction(agentName, cell) + ")"; + } + return disjunction; + } + + std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const std::string &reason) { + std::string disjunction = ""; + bool first = true; + for(auto const [viewDirection, relativePosition] : getRelativeAdjacentCells()) { + if(first) first = false; + else disjunction += " | "; + disjunction += "(" + objectPositionToConjunction(agentName, reason, relativePosition, viewDirection) + ")"; + } + return disjunction; + } + + std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const cells &cells, const std::pair &offset) { + std::string disjunction = ""; + bool first = true; + std::string xOffset = oneOffToString(offset.first); + std::string yOffset = oneOffToString(offset.second); + for(auto const cell : cells) { + if(first) first = false; + else disjunction += " | "; + disjunction += "(" + cellToConjunctionWithOffset(agentName, cell, xOffset, yOffset) + ")"; + } + return disjunction; + } + + bool PrismFormulaPrinter::slipperyBehaviour() const { + return !slipperyTiles.at("North").empty() || !slipperyTiles.at("East").empty() || !slipperyTiles.at("South").empty() || !slipperyTiles.at("West").empty(); + } + bool PrismFormulaPrinter::anyPortableObject() const { + return !keys.empty() || !boxes.empty() || !balls.empty(); + } +} diff --git a/util/PrismFormulaPrinter.h b/util/PrismFormulaPrinter.h new file mode 100644 index 0000000..f1def2d --- /dev/null +++ b/util/PrismFormulaPrinter.h @@ -0,0 +1,61 @@ +#pragma once + +#include +#include +#include "MinigridGrammar.h" +#include "PrismPrinter.h" +#include "ConfigYaml.h" + + +std::string oneOffToString(const int &offset); +std::string vectorToDisjunction(const std::vector &formulae); +std::string cellToConjunction(const AgentName &agentName, const cell &c); +std::string cellToConjunctionWithOffset(const AgentName &agentName, const cell &c, const std::string &xOffset, const std::string &yOffset); +std::string coordinatesToConjunction(const AgentName &agentName, const coordinates &c, const ViewDirection viewDirection); +std::string objectPositionToConjunction(const AgentName &agentName, const std::string &identifier, const std::pair &relativePosition); +std::string objectPositionToConjunction(const AgentName &agentName, const std::string &identifier, const std::pair &relativePosition, const ViewDirection viewDirection); +std::map getAdjacentCells(const cell &c); +std::map> getRelativeAdjacentCells(); +std::map> getRelativeSurroundingCells(); + +namespace prism { + class PrismFormulaPrinter { + public: + PrismFormulaPrinter(std::ostream &os, const std::map &restrictions, const cells &walls, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map &slipperyTiles, const cells &lava, const cells &goals); + + void print(const AgentName &agentName); + + void printRestrictionFormula(const AgentName &agentName, const std::string &direction, const cells &grid_cells); + void printIsOnFormula(const AgentName &agentName, const std::string &type, const cells &grid_cells, const std::string &direction = ""); + void printIsNextToFormula(const AgentName &agentName, const std::string &type, const std::map &coordinates); + void printRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::map &coordinates, const std::string &condition); + void printRelativeRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::string &condition); + void printSlipRestrictionFormula(const AgentName &agentName, const std::string &direction); + private: + std::string buildFormula(const std::string &formulaName, const std::string &formula, const bool semicolon = true); + std::string buildLabel(const std::string &labelName, const std::string &label); + std::string buildDisjunction(const AgentName &agentName, const std::map &cells); + std::string buildDisjunction(const AgentName &agentName, const cells &cells); + std::string buildDisjunction(const AgentName &agentName, const std::string &reason); + std::string buildDisjunction(const AgentName &agentName, const cells &cells, const std::pair &offset); + + bool slipperyBehaviour() const; + bool anyPortableObject() const; + + + std::ostream &os; + std::map restrictions; + cells walls; + cells boxes; + cells balls; + cells lockedDoors; + cells unlockedDoors; + cells keys; + std::map slipperyTiles; + cells lava; + cells goals; + + std::vector conditionalMovementRestrictions; + std::vector portableObjects; + }; +} diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index 9b20dc0..430dd3c 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -3,13 +3,29 @@ #include #include +#define NOFAULT -1 +#define LEFT 0 +#define RIGHT 1 +#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)"; } + namespace prism { - PrismModulesPrinter::PrismModulesPrinter(const ModelType &modelType, const size_t &numberOfPlayer, std::vector config, const bool enforceOneWays) - : modelType(modelType), numberOfPlayer(numberOfPlayer), enforceOneWays(enforceOneWays), configuration(config), viewDirectionMapping({{0, "East"}, {1, "South"}, {2, "West"}, {3, "North"}}) { + PrismModulesPrinter::PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector config, const float probIntended, const float faultyProbability) + : os(os), modelType(modelType), maxBoundaries(maxBoundaries), boxes(boxes), balls(balls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), agentNameAndPositionMap(agentNameAndPositionMap), configuration(config), probIntended(probIntended), faultyProbability(faultyProbability) { + numberOfPlayer = agentNameAndPositionMap.size(); + size_t index = 0; + for(auto begin = agentNameAndPositionMap.begin(); begin != agentNameAndPositionMap.end(); begin++, index++) { + agentIndexMap[begin->first] = index; + } } - std::ostream& PrismModulesPrinter::printModel(std::ostream &os, const ModelType &modelType) { + void PrismModulesPrinter::printModelType(const ModelType &modelType) { switch(modelType) { case(ModelType::MDP): os << "mdp"; @@ -19,1048 +35,474 @@ namespace prism { break; } os << "\n\n"; - return os; } - std::ostream& PrismModulesPrinter::printBackgroundLabels(std::ostream &os, const AgentName &agentName, const std::pair &backgroundTiles) { - if(backgroundTiles.second.size() == 0) return os; - - bool first = true; - std::string color = getColor(backgroundTiles.first); - color.at(0) = std::toupper(color.at(0)); - os << "formula " << agentName << "On" << color << " = "; - for(auto const& cell : backgroundTiles.second) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; + std::ostream& PrismModulesPrinter::print() { + for(const auto [agentName, initialPosition] : agentNameAndPositionMap) { + agentNameActionMap[agentName] = {}; } - os << ";\n"; - os << "label \"" << agentName << "On" << color << "\" = " << agentName << "On" << color << ";\n"; - return os; - } - std::ostream& PrismModulesPrinter::printRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &grid_cells, const cells &keys, const cells &doors) { - bool first = true; - os << "formula " << agentName << "CannotMove" << direction << " = " ; - for(auto const& cell : grid_cells) { - if(first) first = false; - else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; + for(const auto &key : keys) { + printPortableObjectModule(key); } - - if (!keys.empty()) { - os << " | " << agentName << "CannotMove" << direction << "BecauseOfKey"; + for(const auto &ball : balls) { + printPortableObjectModule(ball); } - if (!doors.empty()) { - os << " | " << agentName << "CannotMove" << direction << "BecauseOfDoor"; + for(const auto &box : boxes) { + printPortableObjectModule(box); } - - os << ";\n"; - return os; - } - - std::ostream& PrismModulesPrinter::printKeyRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &keys) { - bool first = true; - os << "formula " << agentName << "CannotMove" << direction << "BecauseOfKey" << " = "; - for (auto const& key : keys) { - if(first) first = false; - else os << " | "; - std::string keyColor = key.getColor(); - std::string xKey = "xKey" + keyColor; - std::string yKey = "yKey" + keyColor; - coordinates coords; - - os << "(!" << agentName << "_has_" << keyColor << "_key & "; - - if (direction == "North") { - os << " x" << agentName << " = " << xKey << "&y" << agentName << "-1 = " << yKey << ")"; - } else if (direction == "South") { - os << " x" << agentName << " = " << xKey << "&y" << agentName << "+1 = " << yKey << ")"; - } else if (direction == "East") { - os << " x" << agentName << "+1 = " << xKey << "&y" << agentName << " = " << yKey << ")"; - } else if (direction == "West") { - os << " x" << agentName << "-1 = " << xKey << "&y" << agentName << " = " << yKey << ")"; - } else { - os << "Invalid Direction! in Key Restriction"; - } + for(const auto &door : unlockedDoors) { + printDoorModule(door, true); } - - os << ";\n"; - return os; - } - - std::ostream& PrismModulesPrinter::printDoorRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &doors) { - bool first = true; - - os << "formula " << agentName << "CannotMove" << direction << "BecauseOfDoor" << " = "; - - for (auto const& door : doors) { - if (first) first = false; - else os << " | "; - - std::string doorColor = door.getColor(); - size_t y = door.getCoordinates().first; - size_t x = door.getCoordinates().second; - - os << "(!Door" << doorColor << "open & "; - - if (direction == "North") { - os << " x" << agentName << " = " << x << "&y" << agentName << "-1 = " << y << ")"; - } else if (direction == "South") { - os << " x" << agentName << " = " << x << "&y" << agentName << "+1 = " << y << ")"; - } else if (direction == "East") { - os << " x" << agentName << "+1 = " << x << "&y" << agentName << " = " << y << ")"; - } else if (direction == "West") { - os << " x" << agentName << "-1 = " << y << "&y" << agentName << " = " << y << ")"; - } else { - os << "Invalid Direction! in Key Restriction"; - } - + for(const auto &door : lockedDoors) { + printDoorModule(door, false); } - os << ";\n"; - return os; - } - - - std::ostream& PrismModulesPrinter::printIsOnSlipperyFormula(std::ostream& os, const AgentName &agentName, const std::vector> &slipperyCollection, const cells &slipperyNorth, const cells &slipperyEast, const cells &slipperySouth, const cells &slipperyWest) { - if(std::find_if(slipperyCollection.cbegin(), slipperyCollection.cend(), [=](const std::reference_wrapper& c) { return !c.get().empty(); }) == slipperyCollection.cend()) { - os << "formula " << agentName << "IsOnSlippery = false;\n"; - return os; - } - - bool first = true; - if (!slipperyNorth.empty()) { - os << "formula " << agentName << "IsOnSlipperyNorth = "; - for (const auto& cell : slipperyNorth) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; - } - os << ";\n"; + for(const auto [agentName, initialPosition] : agentNameAndPositionMap) { + printRobotModule(agentName, initialPosition); } - if (!slipperyEast.empty()) { - first = true; - os << "formula " << agentName << "IsOnSlipperyEast = "; - for (const auto& cell : slipperyEast) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; - } - os << ";\n"; - + if(agentNameAndPositionMap.size() > 1) { + printMoveModule(); } - if (!slipperySouth.empty()) { - first = true; - os << "formula " << agentName << "IsOnSlipperySouth = "; - for (const auto& cell : slipperySouth) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; + if(faultyBehaviour()) { + for(const auto [agentName, initialPosition] : agentNameAndPositionMap) { + printFaultyMovementModule(agentName); } - os << ";\n"; } - if (!slipperyWest.empty()) { - first = true; - os << "formula " << agentName << "IsOnSlipperyWest = "; - for (const auto& cell : slipperyWest) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; + if(agentNameAndPositionMap.size() > 1) { + for(const auto [agentName, index] : agentIndexMap) { + printPlayerStruct(agentName); } - os << ";\n"; } - first = true; - os << "formula " << agentName << "IsOnSlippery = "; - - for (const auto& slippery: slipperyCollection) { - for(const auto& cell : slippery.get()) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; - } - } - os << ";\n"; - if(enforceOneWays) { - first = true; - os << "formula " << agentName << "IsOnSlipperyNorth = "; - - for (const auto& cell: slipperyNorth) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; - } - os << ";\n"; - first = true; - os << "formula " << agentName << "IsOnSlipperyEast = "; + return os; + } - for (const auto& cell: slipperyEast) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; - } - os << ";\n"; - first = true; - os << "formula " << agentName << "IsOnSlipperySouth = "; - for (const auto& cell: slipperySouth) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; - } - os << ";\n"; - first = true; - os << "formula " << agentName << "IsOnSlipperyWest = "; - for (const auto& cell: slipperyWest) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; + void PrismModulesPrinter::printConfiguration(const std::vector& configurations) { + for (auto& configuration : configurations) { + if (configuration.overwrite_ || configuration.type_ == ConfigType::Module) { + continue; } - os << ";\n"; + os << configuration.expression_ << std::endl; } - return os; } - std::ostream& PrismModulesPrinter::printIsInLavaFormula(std::ostream& os, const AgentName &agentName, const cells &lava) { - if(lava.size() == 0) { - os << "formula " << agentName << "IsInLava = false;\n"; - return os; - } - bool first = true; - os << "formula " << agentName << "IsInLava = "; - for(auto const& cell : lava) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; + void PrismModulesPrinter::printConstants(const std::vector &constants) { + for (auto& constant : constants) { + os << constant << std::endl; } - os << ";\n"; - os << "formula " << agentName << "IsInLavaAndNotDone = " << agentName << "IsInLava & !" << agentName << "Done;\n"; - os << "label \"" << agentName << "IsInLavaAndNotDone\" = " << agentName << "IsInLava & !" << agentName << "Done;\n"; - return os; } - std::ostream& PrismModulesPrinter::printTurningNotAllowedFormulas(std::ostream& os, const AgentName &agentName, const cells &noTurnFloor) { - if( (!enforceOneWays or noTurnFloor.size() == 0) or (noTurnFloor.size() == 0) ) { - os << "formula " << agentName << "CannotTurn = false;\n"; - return os; - } - bool first = true; - os << "formula " << agentName << "CannotTurn = "; - for(auto const& cell : noTurnFloor) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; - } - os << " | " << agentName << "IsOnSlippery;\n"; - return os; - } + void PrismModulesPrinter::printPortableObjectModule(const cell &object) { + std::string identifier = capitalize(object.getColor()) + object.getType(); + os << "\nmodule " << identifier << std::endl; + os << "\tx" << identifier << " : [-1.." << maxBoundaries.second << "] init " << object.column << ";\n"; + os << "\ty" << identifier << " : [-1.." << maxBoundaries.first << "] init " << object.row << ";\n"; + os << "\t" << identifier << "PickedUp : bool;\n"; + os << "\n"; - std::ostream& PrismModulesPrinter::printIsFixedFormulas(std::ostream& os, const AgentName &agentName) { - os << "formula " << agentName << "IsFixed = false;\n"; - os << "formula " << agentName << "SlipperyTurnLeftAllowed = true;\n"; - os << "formula " << agentName << "SlipperyTurnRightAllowed = true;\n"; - os << "formula " << agentName << "SlipperyMoveForwardAllowed = true;\n"; - os << "label \"FixedStates" << agentName << "\" = " << agentName << "IsFixed | !" << agentName << "SlipperyTurnRightAllowed | !" << agentName << "SlipperyTurnLeftAllowed | !" << agentName << "SlipperyMoveForwardAllowed | " << agentName << "IsInGoal | " << agentName << "IsInLava"; - if(enforceOneWays) { - os << " | " << agentName << "CannotTurn"; - } - os << ";\n"; - //os << "label \"FixedStates\" = " << agentName << "IsFixed | " << agentName << "IsOnSlippery | " << agentName << "IsInGoal | " << agentName << "IsInLava;\n"; + for(const auto [name, position] : agentNameAndPositionMap) { + printPortableObjectActions(name, identifier); + } + os << "endmodule\n\n"; + } + + void PrismModulesPrinter::printPortableObjectActions(const std::string &agentName, const std::string &identifier) { + std::string actionName = "[" + agentName + "_pickup_" + identifier + "]"; + agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); + os << "\t" << actionName << " true -> (x" << identifier << "'=-1) & (y" << identifier << "'=-1) & (" << identifier << "PickedUp'=true);\n"; + actionName = "[" + agentName + "_drop_" + identifier + "_north]"; + agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); + os << "\t" << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << ") & (y" << identifier << "'=y" << agentName << "-1) & (" << identifier << "PickedUp'=false);\n"; + actionName = "[" + agentName + "_drop_" + identifier + "_west]"; + agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); + os << "\t" << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << "-1) & (y" << identifier << "'=y" << agentName << ") & (" << identifier << "PickedUp'=false);\n"; + actionName = "[" + agentName + "_drop_" + identifier + "_south]"; + agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); + os << "\t" << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << ") & (y" << identifier << "'=y" << agentName << "+1) & (" << identifier << "PickedUp'=false);\n"; + actionName = "[" + agentName + "_drop_" + identifier + "_east]"; + agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); + os << "\t" << actionName << " " << " ttrue -> (x" << identifier << "'=x" << agentName << "+1) & (y" << identifier << "'=y" << agentName << ") & (" << identifier << "PickedUp'=false);\n"; + } + + void PrismModulesPrinter::printDoorModule(const cell &door, const bool &opened) { + std::string identifier = capitalize(door.getColor()) + door.getType(); + os << "\nmodule " << identifier << std::endl; + os << "\t" << identifier << "Open : bool init false;\n"; + os << "\n"; - return os; + if(opened) { + for(const auto [name, position] : agentNameAndPositionMap) { + printUnlockedDoorActions(name, identifier); + } + } else { + for(const auto [name, position] : agentNameAndPositionMap) { + printLockedDoorActions(name, identifier); + } + } + os << "endmodule\n\n"; } + void PrismModulesPrinter::printLockedDoorActions(const std::string &agentName, const std::string &identifier) { + std::string actionName = "[" + agentName + "_unlock_" + identifier + "]"; + agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); + os << "\t" << actionName << " !" << identifier << "Open -> (" << identifier << "Open'=true);\n"; + actionName = "[" + agentName + "_close_" + identifier + "]"; + agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); + os << "\t" << actionName << " " << identifier << "Open -> (" << identifier << "Open'=false);\n"; + } - std::ostream& PrismModulesPrinter::printWallFormula(std::ostream& os, const AgentName &agentName, const cells &walls) { - os << "formula " << agentName << "IsOnWall = "; - bool first = true; - for(auto const& cell : walls) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; - } - os << ";\n"; - return os; + void PrismModulesPrinter::printUnlockedDoorActions(const std::string &agentName, const std::string &identifier) { + std::string actionName = "[" + agentName + "_open_" + identifier + "]"; + agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); + os << "\t !" << identifier << "Open -> (" << identifier << "Open'=true);\n"; + actionName = "[" + agentName + "_close_" + identifier + "]"; + agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); + os << "\t" << agentName << " " << identifier << "Open -> (" << identifier << "Open'=false);\n"; } - std::ostream& PrismModulesPrinter::printFormulas(std::ostream& os, - const AgentName &agentName, - const cells &restrictionNorth, - const cells &restrictionEast, - const cells &restrictionSouth, - const cells &restrictionWest, - const std::vector> &slipperyCollection, - const cells &lava, - const cells &walls, - const cells &noTurnFloor, - const cells &slipperyNorth, - const cells &slipperyEast, - const cells &slipperySouth, - const cells &slipperyWest, - const cells &keys, - const cells &doors) { - printRestrictionFormula(os, agentName, "North", restrictionNorth, keys, doors); - printRestrictionFormula(os, agentName, "East", restrictionEast, keys, doors); - printRestrictionFormula(os, agentName, "South", restrictionSouth, keys, doors); - printRestrictionFormula(os, agentName, "West", restrictionWest, keys, doors); - - if (!keys.empty()) { - printKeyRestrictionFormula(os, agentName, "North", keys); - printKeyRestrictionFormula(os, agentName, "East", keys); - printKeyRestrictionFormula(os, agentName, "South", keys); - printKeyRestrictionFormula(os, agentName, "West", keys); - } + 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 << "\tview" << agentName << " : [0..3] init 1;\n"; - if (!doors.empty()) { - printDoorRestrictionFormula(os, agentName, "North", doors); - printDoorRestrictionFormula(os, agentName, "East", doors); - printDoorRestrictionFormula(os, agentName, "South", doors); - printDoorRestrictionFormula(os, agentName, "West", doors); - } - - printIsOnSlipperyFormula(os, agentName, slipperyCollection, slipperyNorth, slipperyEast, slipperySouth, slipperyWest); - printIsInLavaFormula(os, agentName, lava); - printWallFormula(os, agentName, walls); - printTurningNotAllowedFormulas(os, agentName, noTurnFloor); - printIsFixedFormulas(os, agentName); - os << "\n"; - return os; - } + printTurnActionsForRobot(agentName); + printMovementActionsForRobot(agentName); + if(slipperyBehaviour()) printSlipperyMovementActionsForRobot(agentName); - std::ostream& PrismModulesPrinter::printGoalLabel(std::ostream& os, const AgentName &agentName, const cells &goals) { - if(goals.size() == 0) { - os << "formula " << agentName << "IsInGoal = false;\n"; - return os; + for(const auto &door : unlockedDoors) { + std::string identifier = capitalize(door.getColor()) + door.getType(); + printUnlockedDoorActionsForRobot(agentName, identifier); } - bool first = true; - os << "formula " << agentName << "IsInGoal = "; - for(auto const& cell : goals) { - if(first) first = false; else os << " | "; - os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")"; + for(const auto &door : lockedDoors) { + std::string identifier = capitalize(door.getColor()) + door.getType(); + std::string key = capitalize(door.getColor()) + "Key"; + printLockedDoorActionsForRobot(agentName, identifier, key); } - os << ";\n"; - os << "formula " << agentName << "IsInGoalAndNotDone = " << agentName << "IsInGoal & !" << agentName << "Done;\n"; - os << "label \"" << agentName << "IsInGoalAndNotDone\" = " << agentName << "IsInGoal & !" << agentName << "Done;\n"; - return os; - } - std::ostream& PrismModulesPrinter::printCrashLabel(std::ostream &os, const std::vector agentNames) { - os << "label crash = "; - bool first = true; - for(auto const& agentName : agentNames) { - if(agentName == "Agent") continue; - if(first) first = false; else os << " | "; - os << "(xAgent=x" << agentName << ")&(yAgent=y" << agentName << ")"; + for(const auto &key : keys) { + std::string identifier = capitalize(key.getColor()) + key.getType(); + os << "\t" << agentName << "Carrying" << identifier << " : bool init false;\n"; + printPortableObjectActionsForRobot(agentName, identifier); } - os << ";\n\n"; - return os; - } - std::ostream& PrismModulesPrinter::printConfiguration(std::ostream& os, const std::vector& configurations) { - - for (auto& configuration : configurations) { - if (configuration.overwrite_ || configuration.type_ == ConfigType::Module) { - continue; - } - - os << configuration.expression_ << std::endl; + for(const auto &ball : balls) { + std::string identifier = capitalize(ball.getColor()) + ball.getType(); + os << "\t" << agentName << "Carrying" << identifier << " : bool init false;\n"; + printPortableObjectActionsForRobot(agentName, identifier); } - return os; - } - - std::ostream& PrismModulesPrinter::printConstants(std::ostream &os, const std::vector &constants) { - - for (auto& constant : constants) { - os << constant << std::endl; + for(const auto &box : boxes) { + std::string identifier = capitalize(box.getColor()) + box.getType(); + os << "\t" << agentName << "Carrying" << identifier << " : bool init false;\n"; + printPortableObjectActionsForRobot(agentName, identifier); } - return os; + os << "\n" << actionStream.str(); + actionStream.str(std::string()); + os << "endmodule\n\n"; } - - std::ostream& PrismModulesPrinter::printAvoidanceLabel(std::ostream &os, const std::vector agentNames, const int &distance) { - os << "label avoidance = "; - bool first = true; - for(auto const& agentName : agentNames) { - if(agentName == "Agent") continue; - if(first) first = false; else os << " | "; - os << "max(xAgent-x" << agentName << ",x" << agentName << "-xAgent)+"; - os << "max(yAgent-y" << agentName << ",y" << agentName << "-yAgent) "; - } - os << ";\n\n"; - return os; + void PrismModulesPrinter::printPortableObjectActionsForRobot(const std::string &a, const std::string &i) { + actionStream << "\t[" << a << "_pickup_" << i << "] " << " !" << a << "IsCarrying & " << a << "CannotMove" << i << " -> (" << a << "Carrying" << i << "'=true);\n"; + actionStream << "\t[" << a << "_drop_" << i << "_north]\t" << a << "Carrying" << i << " & view" << a << "=3 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveNorthWall -> (" << a << "Carrying" << i << "'=false);\n"; + actionStream << "\t[" << a << "_drop_" << i << "_west] \t" << a << "Carrying" << i << " & view" << a << "=2 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveWestWall -> (" << a << "Carrying" << i << "'=false);\n"; + actionStream << "\t[" << a << "_drop_" << i << "_south]\t" << a << "Carrying" << i << " & view" << a << "=1 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveSouthWall -> (" << a << "Carrying" << i << "'=false);\n"; + actionStream << "\t[" << a << "_drop_" << i << "_east] \t" << a << "Carrying" << i << " & view" << a << "=0 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveEastWall -> (" << a << "Carrying" << i << "'=false);\n"; + actionStream << "\n"; } - // TODO this does not account for multiple agents yet, i.e. key can be picked up multiple times - std::ostream& PrismModulesPrinter::printKeysLabels(std::ostream& os, const AgentName &agentName, const cells &keys) { - if(keys.size() == 0) return os; - - for(auto const& key : keys) { - std::string keyColor = key.getColor(); - std::string xKey = "xKey" + keyColor; - std::string yKey = "yKey" + keyColor; - os << "label \"" << agentName << "PickedUp" << keyColor << "Key\" = " << agentName << "_has_" << keyColor << "_key = true;\n"; - os << "formula " << agentName << "CanPickUp" << keyColor << "Key = "; - os << "((x" << agentName << "-1 = " << xKey << "&y" << agentName << " = " << yKey << "&view" << agentName << " = 2) |"; - os << " (x" << agentName << "+1 = " << xKey << "&y" << agentName << " = " << yKey << "&view" << agentName << " = 0) |"; - os << " (x" << agentName << " = " << xKey << "&y" << agentName << "-1 = " << yKey << "&view" << agentName << " = 3) |"; - os << " (x" << agentName << " = " << xKey << "&y" << agentName << "+1 = " << yKey << "&view" << agentName << " = 1) ) &"; - os << "!" << agentName << "_has_" << keyColor << "_key;"; - } - os << "\n"; - return os; + void PrismModulesPrinter::printUnlockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier) { + actionStream << "\t[" << agentName << "_open_" << identifier << "] " << agentName << "CannotMove" << identifier << " -> true;\n"; + actionStream << "\t[" << agentName << "_close_" << identifier << "] " << agentName << "IsNextTo" << identifier << " -> true;\n"; + actionStream << "\n"; } - std::ostream& PrismModulesPrinter::printBooleansForKeys(std::ostream &os, const AgentName &agentName, const cells &keys) { - for(auto const& key : keys) { - os << "\t" << agentName << "_has_"<< key.getColor() << "_key : bool;\n";//init false;\n"; - } - - - os << "\n"; - return os; + void PrismModulesPrinter::printLockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier, const std::string &key) { + actionStream << "\t[" << agentName << "_unlock_" << identifier << "] " << agentName << "CannotMove" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n"; + actionStream << "\t[" << agentName << "_close_" << identifier << "] " << agentName << "IsNextTo" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n"; + actionStream << "\n"; } - std::ostream& PrismModulesPrinter::printBooleansForBackground(std::ostream &os, const AgentName &agentName, const std::map &backgroundTiles) { - for(auto const& [color, cells] : backgroundTiles) { - if(cells.size() == 0) continue; - std::string c = getColor(color); - c.at(0) = std::toupper(c.at(0)); - os << "\t" << agentName << "_picked_up_" << c << " : bool init false;\n"; - } - os << "\n"; - return os; + void PrismModulesPrinter::printTurnActionsForRobot(const AgentName &a) { + actionStream << printTurnGuard(a, "right", RIGHT, "true") << printTurnUpdate(a, {1.0, "(view"+a+"'=mod(view"+a+"+1,4))"}, RIGHT); + actionStream << printTurnGuard(a, "left", LEFT, "view"+a+">0") << printTurnUpdate(a, {1.0, "(view"+a+"'=view"+a+"-1)"}, LEFT); + actionStream << printTurnGuard(a, "left", LEFT, "view"+a+"=0") << printTurnUpdate(a, {1.0, "(view"+a+"'=3)"}, LEFT); } - std::ostream& PrismModulesPrinter::printActionsForKeys(std::ostream &os, const AgentName &agentName, const cells &keys) { - for(auto const& key : keys) { // TODO ADD Drop action and enforce that pickup only possible if pockets empty (nothing picked up already) - os << "\n"; - std::string keyColor = key.getColor(); - os << "\t[pickup_" << keyColor << "_key]\t" << pickupGuard(agentName, keyColor) << "-> "; - os << "(" << agentName << "_has_" << keyColor << "_key'=true) & (" << agentName << "_is_carrying_object'=true);\n"; - os << "\n"; - - os << "\t[drop_" << keyColor << "_key_north]\t" << dropGuard(agentName, keyColor, 3) << "-> "; - os << "(" << agentName << "_has_" << keyColor << "_key'=false) & (" << agentName << "_is_carrying_object'=false);\n"; - - os << "\t[drop_" << keyColor << "_key_west]\t" << dropGuard(agentName, keyColor, 2) << "-> "; - os << "(" << agentName << "_has_" << keyColor << "_key'=false) & (" << agentName << "_is_carrying_object'=false);\n"; - - os << "\t[drop_" << keyColor << "_key_south]\t" << dropGuard(agentName, keyColor, 1) << "-> "; - os << "(" << agentName << "_has_" << keyColor << "_key'=false) & (" << agentName << "_is_carrying_object'=false);\n"; - - os << "\t[drop_" << keyColor << "_key_east]\t" << dropGuard(agentName, keyColor, 0) << "-> "; - os << "(" << agentName << "_has_" << keyColor << "_key'=false) & (" << agentName << "_is_carrying_object'=false);\n"; + void PrismModulesPrinter::printMovementActionsForRobot(const AgentName &a) { + actionStream << printMovementGuard(a, "North", 3) << printMovementUpdate(a, {1.0, northUpdate(a)}); + actionStream << printMovementGuard(a, "East", 0) << printMovementUpdate(a, {1.0, eastUpdate(a)}); + actionStream << printMovementGuard(a, "South", 1) << printMovementUpdate(a, {1.0, southUpdate(a)}); + actionStream << printMovementGuard(a, "West", 2) << printMovementUpdate(a, {1.0, westUpdate(a)}); + if(faultyBehaviour()) { + std::string actionName = "[" + a + "_stuck]"; + agentNameActionMap.at(a).insert({FORWARD, actionName}); + actionStream << "\t" << actionName << " " << "previousAction" << a << "=" << std::to_string(FORWARD); + actionStream << " & ((view" << a << "=0 & " << a << "CannotMoveEastWall) |"; + actionStream << " (view" << a << "=1 & " << a << "CannotMoveSouthWall) |"; + actionStream << " (view" << a << "=2 & " << a << "CannotMoveWestWall) |"; + actionStream << " (view" << a << "=3 & " << a << "CannotMoveNorthWall) ) -> true;\n"; } - - return os; } - std::string PrismModulesPrinter::pickupGuard(const AgentName &agentName, const std::string keyColor ) { - return "!" + agentName + "_is_carrying_object &\t" + agentName + "CanPickUp" + keyColor + "Key "; + std::string PrismModulesPrinter::printMovementGuard(const AgentName &a, const std::string &direction, const size_t &viewDirection) { + std::string actionName = "[" + a + "_move_" + direction + "]"; + agentNameActionMap.at(a).insert({FORWARD, actionName}); + return "\t" + actionName + " " + viewVariable(a, viewDirection) + " !" + a + "IsOnSlippery & !" + a + "IsOnLava & !" + a + "IsOnGoal & !" + a + "CannotMove" + direction + "Wall &!" + a + "CannotMoveConditionally -> "; } - std::string PrismModulesPrinter::dropGuard(const AgentName &agentName, const std::string keyColor, size_t view) { - return viewVariable(agentName, view, true) + "\t!" + agentName + "CannotMove" + viewDirectionMapping.at(view) + "\t&\t" + agentName + "_has_" + keyColor + "_key\t"; + std::string PrismModulesPrinter::printMovementUpdate(const AgentName &a, const update &u) const { + return updateToString(u) + ";\n"; } - std::ostream& PrismModulesPrinter::printActionsForBackground(std::ostream &os, const AgentName &agentName, const std::map &backgroundTiles) { - for(auto const& [color, cells] : backgroundTiles) { - if(cells.size() == 0) continue; - std::string c = getColor(color); - c.at(0) = std::toupper(c.at(0)); - os << "\t[" << agentName << "_pickup_" << c << "] " << agentName << "On" << c << " & !" << agentName << "_picked_up_" << c << " -> "; - os << "(" << agentName << "_picked_up_" << c << "'=true);\n"; - } - os << "\n"; - return os; + std::string PrismModulesPrinter::printTurnGuard(const AgentName &a, const std::string &direction, const ActionId &actionId, const std::string &cond) { + std::string actionName = "[" + a + "_turn_" + direction + "]"; + agentNameActionMap.at(a).insert({actionId, actionName}); + return "\t" + actionName + " " + cond + " -> "; } - std::ostream& PrismModulesPrinter::printInitStruct(std::ostream &os, const AgentNameAndPositionMap &agents, const KeyNameAndPositionMap &keys, const cells &lockedDoors, const cells &unlockedDoors, prism::ModelType modelType) { - os << "init\n"; - os << "\t"; - - bool first = true; - for (auto const& agent : agents) { - if (first) first = false; - else os << " & "; - os << "(!" << agent.first << "IsInGoal & !" << agent.first << "IsInLava & !" << agent.first << "Done & !" << agent.first << "IsOnWall & "; - os << "x" << agent.first << "=" << agent.second.second << " & y" << agent.first << "=" << agent.second.first << ")"; - os << " & !" << agent.first << "_is_carrying_object"; - if(enforceOneWays) { - os << " & ( !AgentCannotTurn ) "; - } else { - // os << " & ( !AgentIsOnSlippery ) "; - } + std::string PrismModulesPrinter::printTurnUpdate(const AgentName &a, const update &u, const ActionId &actionId) const { + return updateToString(u) + ";\n"; + } - for (auto const& key : keys) { - os << " & ( !" << agent.first << "_has_" << key.first << "_key )"; - } + void PrismModulesPrinter::printSlipperyMovementActionsForRobot(const AgentName &a) { + if(!slipperyTiles.at("North").empty()) { + printSlipperyMovementActionsForNorth(a); + printSlipperyTurnActionsForNorth(a); } - - for (auto const& key : keys) { - os << " & ( xKey" << key.first << "="<< key.second.second<< ")"; - os << " & ( yKey" << key.first << "=" << key.second.first << ")"; - } - - for (auto const& locked : lockedDoors) { - os << " & (Door" << locked.getColor() << "locked & !Door" << locked.getColor() << "open)"; + if(!slipperyTiles.at("East").empty()) { + printSlipperyMovementActionsForEast(a) ; + printSlipperyTurnActionsForEast(a); } - - for (auto const& unlocked : unlockedDoors) { - os << " & (!Door" << unlocked.getColor() << "locked & !Door" << unlocked.getColor() << "open)"; + if(!slipperyTiles.at("South").empty()) { + printSlipperyMovementActionsForSouth(a); + printSlipperyTurnActionsForSouth(a); } - - if (modelType == ModelType::SMG) { - os << " & move=0"; + if(!slipperyTiles.at("West").empty()) { + printSlipperyMovementActionsForWest(a) ; + printSlipperyTurnActionsForWest(a); } + } + 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"; - os << "\nendinit\n\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"; - - return os; + 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"; } - std::ostream& PrismModulesPrinter::printModule(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const coordinates &boundaries, const coordinates& initialPosition, const cells &keys, const std::map &backgroundTiles, const bool agentWithView, const std::vector &probabilities, const double faultyProbability) { - os << "module " << agentName << "\n"; - os << "\tx" << agentName << " : [1.." << boundaries.second << "];\n"; - os << "\ty" << agentName << " : [1.." << boundaries.first << "];\n"; - os << "\t" << agentName << "_is_carrying_object : bool;\n"; - - printBooleansForKeys(os, agentName, keys); - printBooleansForBackground(os, agentName, backgroundTiles); - os << "\t" << agentName << "Done : bool;\n"; - if(agentWithView) { - os << "\tview" << agentName << " : [0..3];\n"; - os << "\n"; - if (faultyProbability != 0.0) { - os << "\t[" << agentName << "_turn_right] " << moveGuard(agentIndex) << " !" << agentName << "CannotTurn & " << " !" << agentName << "IsFixed & " << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & !" << agentName << "IsOnSlippery -> " << 100 - faultyProbability << "/100:" << "(view" << agentName << "'=mod(view" << agentName << " + 1, 4))" << moveUpdate(agentIndex) << "\n + " << faultyProbability << "/100:" << "(view" << agentName << "'=mod(view" << agentName << " + 2, 4))" << ";\n"; - os << "\t[" << agentName << "_turn_left] " << moveGuard(agentIndex) << " !" << agentName << "CannotTurn & " << " !" << agentName << "IsFixed & " << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & !" << agentName << "IsOnSlippery & view" << agentName << ">1 -> " << 100 - faultyProbability << "/100:" << "(view" << agentName << "'=mod(view" << agentName << " - 1, 4))" << moveUpdate(agentIndex) << "\n + " << faultyProbability << "/100:" << "(view" << agentName << "'=mod(view" << agentName << " - 2, 4))" << ";\n"; - os << "\t[" << agentName << "_turn_left] " << moveGuard(agentIndex) << " !" << agentName << "CannotTurn & " << " !" << agentName << "IsFixed & " << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & !" << agentName << "IsOnSlippery & view" << agentName << "=0 -> " << 100 - faultyProbability << "/100:" << "(view" << agentName << "'=3)" << moveUpdate(agentIndex) << "\n + " << faultyProbability << "/100:" << "(view" << agentName << "'=2)" << ";\n"; - os << "\t[" << agentName << "_turn_left] " << moveGuard(agentIndex) << " !" << agentName << "CannotTurn & " << " !" << agentName << "IsFixed & " << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & !" << agentName << "IsOnSlippery & view" << agentName << "=1 -> " << 100 - faultyProbability << "/100:" << "(view" << agentName << "'=0)" << moveUpdate(agentIndex) << "\n + " << faultyProbability << "/100:" << "(view" << agentName << "'=3)" << ";\n"; - } else { - os << "\t[" << agentName << "_turn_right] " << moveGuard(agentIndex) << " !" << agentName << "CannotTurn & " << " !" << agentName << "IsFixed & " << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & !" << agentName << "IsOnSlippery -> (view" << agentName << "'=mod(view" << agentName << " + 1, 4)) " << moveUpdate(agentIndex) << ";\n"; - os << "\t[" << agentName << "_turn_left] " << moveGuard(agentIndex) << " !" << agentName << "CannotTurn & " << " !" << agentName << "IsFixed & " << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & !" << agentName << "IsOnSlippery & view" << agentName << ">0 -> (view" << agentName << "'=view" << agentName << " - 1) " << moveUpdate(agentIndex) << ";\n"; - os << "\t[" << agentName << "_turn_left] " << moveGuard(agentIndex) << " !" << agentName << "CannotTurn & " << " !" << agentName << "IsFixed & " << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & !" << agentName << "IsOnSlippery & view" << agentName << "=0 -> (view" << agentName << "'=3) " << moveUpdate(agentIndex) << ";\n"; - } - if(enforceOneWays) { - os << "\t[" << agentName << "_stuck] !" << agentName << "IsFixed & " << agentName << "CannotTurn & view" << agentName << " = 0 & " << agentName << "CannotMoveEast -> true;\n"; - os << "\t[" << agentName << "_stuck] !" << agentName << "IsFixed & " << agentName << "CannotTurn & view" << agentName << " = 1 & " << agentName << "CannotMoveSouth -> true;\n"; - os << "\t[" << agentName << "_stuck] !" << agentName << "IsFixed & " << agentName << "CannotTurn & view" << agentName << " = 2 & " << agentName << "CannotMoveWest -> true;\n"; - os << "\t[" << agentName << "_stuck] !" << agentName << "IsFixed & " << agentName << "CannotTurn & view" << agentName << " = 3 & " << agentName << "CannotMoveNorth -> true;\n"; - } - } else { - os << "\t[" << agentName << "_turns] " << " !" << agentName << "CannotTurn & " << " !" << agentName << "IsFixed & " << moveGuard(agentIndex) << " true -> (x" << agentName << "'=x" << agentName << ")" << moveUpdate(agentIndex) << ";\n"; - } - printActionsForKeys(os, agentName, keys); - printActionsForBackground(os, agentName, backgroundTiles); - os << "\n"; - - printMovementActions(os, agentName, agentIndex, agentWithView, 1.0, faultyProbability); - for(auto const& probability : probabilities) { - printMovementActions(os, agentName, agentIndex, agentWithView, probability); - } - printDoneActions(os, agentName, agentIndex); - - printConfiguredActions(os, agentName); + 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"; - os << "\n"; - return os; + 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"; } - std::ostream& PrismModulesPrinter::printKeyModule(std::ostream &os, const cell &key, const coordinates &boundaries, AgentName agentName) { - std::string keyIdentifier = "Key" + key.getColor(); + 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"; - os << "module " << keyIdentifier << "\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"; - os << "\tx" << keyIdentifier << " : [-1.." << boundaries.second << "];\n"; - os << "\ty" << keyIdentifier << " : [-1.." << boundaries.first << "];\n"; - os << "\n"; - printKeyActions(os, key ,keyIdentifier, agentName); + 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"; - os << "\n"; - return os; + 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"; } - - std::ostream& PrismModulesPrinter::printKeyActions(std::ostream &os, const cell &key ,const std::string &keyIdentifier, AgentName agentName) { - std::string keyColor = key.getColor(); - - os << "\t[pickup_" << keyColor << "key]\t" << pickupGuard(agentName, keyColor) << "-> "; - os << "(xKey" << keyColor << "'=-1) & (yKey" << keyColor << "'=-1)" << ";\n"; - - os << "\t[drop_" << keyColor << "_key_north]\t" << dropGuard(agentName, keyColor, 3) << "-> "; - os << "(xKey" << keyColor << "'=x" << agentName << ") & (yKey" << keyColor << "'=y" < "; - os << "(xKey" << keyColor << "'=x" << agentName << "-1) & (yKey" << keyColor << "'=y" < "; - os << "(xKey" << keyColor << "'=x" << agentName << ") & (yKey" << keyColor << "'=y" < "; - os << "(xKey" << keyColor << "'=x" << agentName << "+1) & (yKey" << keyColor << "'=y" <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"; } - std::ostream& PrismModulesPrinter::printDoorActions(std::ostream &os, const cell &door ,const std::string &doorIdentifier, AgentName agentName) { - os << "\t[" << "unlock_" << doorIdentifier << "]\t" << unlockGuard(agentName, door) << " -> "; - os << "(" << doorIdentifier << "locked'=false) & (" << doorIdentifier << "open'=true) ;\n"; - - os << "\t[" << "toggle_" << doorIdentifier << "]\t" << toggleGuard(agentName, door) << " -> "; - os << "(" << doorIdentifier << "open'=!" << doorIdentifier << "open) ;\n"; - - return os; - } + 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"; - std::string PrismModulesPrinter::unlockGuard(const AgentName &agentName, const cell& door) { - std::string doorColor = door.getColor(); - std::string ret; - ret += agentName + "_has_" + doorColor + "_key & "; - ret += "((" + viewVariable(agentName, 0, true) + "x" + agentName + "+ 1 = " + std::to_string(door.column) + " & y" + agentName + "= " + std::to_string(door.row) + ")"; - ret += " | (" + viewVariable(agentName, 1, true) + "x" + agentName + " = " + std::to_string(door.column) + " & y" + agentName + " + 1 = " + std::to_string(door.row) + ")"; - ret += " | (" + viewVariable(agentName, 2, true) + "x" + agentName + "- 1 = " + std::to_string(door.column) + " & y" + agentName + "= " + std::to_string(door.row) + ")"; - ret += " | (" + viewVariable(agentName, 3, true) + "x" + agentName + " = " + std::to_string(door.column) + " & y" + agentName + " - 1 = " + std::to_string(door.row) + "))"; - - - return ret; + 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"; } + 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"; - std::string PrismModulesPrinter::toggleGuard(const AgentName &agentName, const cell& door) { - std::string doorColor = door.getColor(); - std::string ret; - ret += "!Door" + doorColor + "locked & ("; - ret += "(" + viewVariable(agentName, 0, true) + "x" + agentName + "+ 1 = " + std::to_string(door.column) + " & y" + agentName + "= " + std::to_string(door.row) + ")"; - ret += " | (" + viewVariable(agentName, 1, true) + "x" + agentName + " = " + std::to_string(door.column) + " & y" + agentName + " + 1 = " + std::to_string(door.row) + ")"; - ret += " | (" + viewVariable(agentName, 2, true) + "x" + agentName + "- 1 = " + std::to_string(door.column) + " & y" + agentName + "= " + std::to_string(door.row) + ")"; - ret += " | (" + viewVariable(agentName, 3, true) + "x" + agentName + " = " + std::to_string(door.column) + " & y" + agentName + " - 1 = " + std::to_string(door.row) + "))"; - - - - return ret; + 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"; } + 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"; - - std::ostream& PrismModulesPrinter::printConfiguredActions(std::ostream &os, const AgentName &agentName) { - for (auto& config : configuration) { - if (config.type_ == ConfigType::Module && !config.overwrite_ && agentName == config.module_) { - os << config.expression_ ; - } - } - - os << "\n"; - - return os; + 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"; } - std::ostream& PrismModulesPrinter::printMovementActions(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const bool agentWithView, const float &probability, const double &stickyProbability) { - if(stickyProbability != 0.0) { - os << "\t[" << agentName << "_move_north]" << moveGuard(agentIndex) << viewVariable(agentName, 3, agentWithView) << " !" << agentName << "IsFixed & " << " !" << agentName << "IsOnSlippery & !" << agentName << "IsInLava &!" << agentName << "IsInGoal & !" << agentName << "CannotMoveNorth -> " << (100 - stickyProbability) << "/100:" << "(y" << agentName << "'=y" << agentName << "-1)" << moveUpdate(agentIndex) << "\n+ " << (stickyProbability) << "/100:" << "(y" << agentName << "'=max(y" << agentName << "-2, 1 ))" << moveUpdate(agentIndex) << ";\n"; - os << "\t[" << agentName << "_move_east] " << moveGuard(agentIndex) << viewVariable(agentName, 0, agentWithView) << " !" << agentName << "IsFixed & " << " !" << agentName << "IsOnSlippery & !" << agentName << "IsInLava &!" << agentName << "IsInGoal & !" << agentName << "CannotMoveEast -> " << (100 - stickyProbability) << "/100:" << "(x" << agentName << "'=x" << agentName << "+1)" << moveUpdate(agentIndex) << "\n+ " << (stickyProbability) << "/100:" << "(x" << agentName << "'=min(x" << agentName << "+2, width))" << moveUpdate(agentIndex) << ";\n"; - os << "\t[" << agentName << "_move_south]" << moveGuard(agentIndex) << viewVariable(agentName, 1, agentWithView) << " !" << agentName << "IsFixed & " << " !" << agentName << "IsOnSlippery & !" << agentName << "IsInLava &!" << agentName << "IsInGoal & !" << agentName << "CannotMoveSouth -> " << (100 - stickyProbability) << "/100:" << "(y" << agentName << "'=y" << agentName << "+1)" << moveUpdate(agentIndex) << "\n+ " << (stickyProbability) << "/100:" << "(y" << agentName << "'=min(y" << agentName << "+2, height))" << moveUpdate(agentIndex) << ";\n"; - os << "\t[" << agentName << "_move_west] " << moveGuard(agentIndex) << viewVariable(agentName, 2, agentWithView) << " !" << agentName << "IsFixed & " << " !" << agentName << "IsOnSlippery & !" << agentName << "IsInLava &!" << agentName << "IsInGoal & !" << agentName << "CannotMoveWest -> " << (100 - stickyProbability) << "/100:" << "(x" << agentName << "'=x" << agentName << "-1)" << moveUpdate(agentIndex) << "\n+ " << (stickyProbability) << "/100:" << "(x" << agentName << "'=max(x" << agentName << "-1, 1))" << moveUpdate(agentIndex) << ";\n"; - } - else if(probability >= 1) { - os << "\t[" << agentName << "_move_north]" << moveGuard(agentIndex) << viewVariable(agentName, 3, agentWithView) << " !" << agentName << "IsFixed & " << " !" << agentName << "IsOnSlippery & !" << agentName << "IsInLava &!" << agentName << "IsInGoal & !" << agentName << "CannotMoveNorth -> (y" << agentName << "'=y" << agentName << "-1)" << moveUpdate(agentIndex) << ";\n"; - os << "\t[" << agentName << "_move_east] " << moveGuard(agentIndex) << viewVariable(agentName, 0, agentWithView) << " !" << agentName << "IsFixed & " << " !" << agentName << "IsOnSlippery & !" << agentName << "IsInLava &!" << agentName << "IsInGoal & !" << agentName << "CannotMoveEast -> (x" << agentName << "'=x" << agentName << "+1)" << moveUpdate(agentIndex) << ";\n"; - os << "\t[" << agentName << "_move_south]" << moveGuard(agentIndex) << viewVariable(agentName, 1, agentWithView) << " !" << agentName << "IsFixed & " << " !" << agentName << "IsOnSlippery & !" << agentName << "IsInLava &!" << agentName << "IsInGoal & !" << agentName << "CannotMoveSouth -> (y" << agentName << "'=y" << agentName << "+1)" << moveUpdate(agentIndex) << ";\n"; - os << "\t[" << agentName << "_move_west] " << moveGuard(agentIndex) << viewVariable(agentName, 2, agentWithView) << " !" << agentName << "IsFixed & " << " !" << agentName << "IsOnSlippery & !" << agentName << "IsInLava &!" << agentName << "IsInGoal & !" << agentName << "CannotMoveWest -> (x" << agentName << "'=x" << agentName << "-1)" << moveUpdate(agentIndex) << ";\n"; - } else { - std::string probabilityString = std::to_string(probability); - std::string percentageString = std::to_string((int)(100 * probability)); - std::string complementProbabilityString = std::to_string(1 - probability); - os << "\t[" << agentName << "_move_north_" << percentageString << "] "; - os << moveGuard(agentIndex) << viewVariable(agentName, 3, agentWithView) << " !" << agentName << "IsFixed & " << " !" << agentName << "IsOnSlippery & !" << agentName << "IsInLava & !" << agentName << "CannotMoveNorth -> "; - os << probabilityString << ": (y" << agentName << "'=y" << agentName << "-1)" << moveUpdate(agentIndex) << " + "; - os << complementProbabilityString << ": (y" << agentName << "'=y" << agentName << ") " << moveUpdate(agentIndex) << ";\n"; - - os << "\t[" << agentName << "_move_east_" << percentageString << "] "; - os << moveGuard(agentIndex) << viewVariable(agentName, 0, agentWithView) << " !" << agentName << "IsFixed & " << " !" << agentName << "IsOnSlippery & !" << agentName << "IsInLava & !" << agentName << "CannotMoveEast -> "; - os << probabilityString << ": (x" << agentName << "'=x" << agentName << "+1)" << moveUpdate(agentIndex) << " + "; - os << complementProbabilityString << ": (x" << agentName << "'=x" << agentName << ") " << moveUpdate(agentIndex) << ";\n"; - - os << "\t[" << agentName << "_move_south_" << percentageString << "] "; - os << moveGuard(agentIndex) << viewVariable(agentName, 1, agentWithView) << " !" << agentName << "IsFixed & " << " !" << agentName << "IsOnSlippery & !" << agentName << "IsInLava & !" << agentName << "CannotMoveSouth -> "; - os << probabilityString << ": (y" << agentName << "'=y" << agentName << "+1)" << moveUpdate(agentIndex) << " + "; - os << complementProbabilityString << ": (y" << agentName << "'=y" << agentName << ") " << moveUpdate(agentIndex) << ";\n"; - - os << "\t[" << agentName << "_move_west_" << percentageString << "] "; - os << moveGuard(agentIndex) << viewVariable(agentName, 2, agentWithView) << " !" << agentName << "IsFixed & " << " !" << agentName << "IsOnSlippery & !" << agentName << "IsInLava & !" << agentName << "CannotMoveWest -> "; - os << probabilityString << ": (x" << agentName << "'=x" << agentName << "-1)" << moveUpdate(agentIndex) << " + "; - os << complementProbabilityString << ": (x" << agentName << "'=x" << agentName << ") " << moveUpdate(agentIndex) << ";\n"; - } - return os; + std::string PrismModulesPrinter::printSlipperyMovementGuard(const AgentName &a, const std::string &direction, const ViewDirection &viewDirection, const std::vector &guards) { + std::string actionName = "[" + a + "_move_" + direction + "]"; + agentNameActionMap.at(a).insert({FORWARD, actionName}); + return "\t" + actionName + " " + viewVariable(a, viewDirection) + a + "IsOnSlippery" + direction + " & " + buildConjunction(a, guards) + " -> "; } - std::ostream& PrismModulesPrinter::printDoneActions(std::ostream &os, const AgentName &agentName, const size_t &agentIndex) { - os << "\t[" << agentName << "_done]" << moveGuard(agentIndex) << agentName << "IsInGoal | " << agentName << "IsInLava -> (" << agentName << "Done'=true);\n"; - return os; + std::string PrismModulesPrinter::printSlipperyMovementUpdate(const AgentName &a, const std::string &direction, const updates &u) const { + return updatesToString(u); } - std::ostream& PrismModulesPrinter::printSlipperyTurn(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const coordinates &c, std::set &slipperyActions, const std::array& neighborhood, SlipperyType orientation) { - constexpr std::size_t PROB_PIECES = 9, ALL_POSS_DIRECTIONS = 9; - - std::array positionTransition = { - /* north */ "(y" + agentName + "'=y" + agentName + "-1)", - /* north east */ "(x" + agentName + "'=x" + agentName + "+1) & (y" + agentName + "'=y" + agentName + "-1)", - /* east */ "(x" + agentName + "'=x" + agentName + "+1)", - /* east south */ "(x" + agentName + "'=x" + agentName + "+1) & (y" + agentName + "'=y" + agentName + "+1)", - /* south */ "(y" + agentName + "'=y" + agentName + "+1)", - /* south west */ "(x" + agentName + "'=x" + agentName + "-1) & (y" + agentName + "'=y" + agentName + "+1)", - /* west */ "(x" + agentName + "'=x" + agentName + "-1)", - /* north west */ "(x" + agentName + "'=x" + agentName + "-1) & (y" + agentName + "'=y" + agentName + "-1)", - /* own position */ "(x" + agentName + "'=x" + agentName + ") & (y" + agentName + "'=y" + agentName + ")" - }; - - // view transition appdx in form (guard, update part) - // IMPORTANT: No mod() usage for turn left due to bug in mod() function for decrement - - - std::array, 3> viewTransition = { - std::make_tuple(" & " + agentName + "SlipperyTurnRightAllowed ", " & (view" + agentName + "'=mod(view" + agentName + " + 1, 4))", "_right]"), - std::make_tuple(" & " + agentName + "SlipperyTurnLeftAllowed & view" + agentName + ">0", " & (view" + agentName + "'=view" + agentName + " - 1)", "_left]"), - std::make_tuple(" & " + agentName + "SlipperyTurnLeftAllowed & view" + agentName + "=0", " & (view" + agentName + "'=3)", "_left]") - }; - - // direction specifics - - std::string actionName; - std::string positionGuard; - std::size_t remainPosIndex = 8; - std::array prob_piece_dir; // { n, ne, e, se, s, sw, w, nw, CURRENT POS } - std::array prob_piece_dir_constants; - - switch (orientation) - { - case SlipperyType::North: - actionName = "\t[" + agentName + "turn_at_slip_north"; - positionGuard = "\t" + agentName + "IsOnSlipperyNorth"; - prob_piece_dir = { 0, 0, 0, 0, 1, 0, 0, 0, 0 /* <- R */ }; - prob_piece_dir_constants = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_turn_displacement" /* <- R */, "prop_zero", "prop_zero", "prop_zero","prop_zero" }; - break; - - case SlipperyType::South: - actionName = "\t[" + agentName + "turn_at_slip_south"; - positionGuard = "\t" + agentName + "IsOnSlipperySouth"; - prob_piece_dir = { 1, 0, 0, 0, 0, 0, 0, 0, 0 /* <- R */ }; - prob_piece_dir_constants = { "prop_turn_displacement", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" }; - break; - - case SlipperyType::East: - actionName = "\t[" + agentName + "turn_at_slip_east"; - positionGuard = "\t" + agentName + "IsOnSlipperyEast"; - prob_piece_dir = { 0, 0, 0, 0, 0, 0, 1, 0, 0 /* <- R */ }; - prob_piece_dir_constants = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_turn_displacement", "prop_zero", "prop_zero" }; - break; - - case SlipperyType::West: - actionName = "\t[" + agentName + "turn_at_slip_west"; - positionGuard = "\t" + agentName + "IsOnSlipperyWest"; - prob_piece_dir = { 0, 0, 1, 0, 0, 0, 0, 0, 0 /* <- R */ }; - prob_piece_dir_constants = { "prop_zero", "prop_zero", "prop_turn_displacement", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" }; - break; - } - - slipperyActions.insert(actionName + "_left]"); - slipperyActions.insert(actionName + "_right]"); - - // override probability to 0 if corresp. direction is blocked - - for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS - 1; i++) { - if (!neighborhood.at(i)) - prob_piece_dir.at(i) = 0; - } - - // determine residual probability (R) by replacing 0 with (1 - overall sum) - - prob_piece_dir.at(remainPosIndex) = PROB_PIECES - std::accumulate(prob_piece_dir.begin(), prob_piece_dir.end(), 0); - prob_piece_dir_constants.at(remainPosIndex) = "prop_turn_intended"; - // - { - assert(prob_piece_dir.at(remainPosIndex) <= 9 && prob_piece_dir.at(remainPosIndex) >= 6 && "Value not in Range!"); - assert(std::accumulate(prob_piece_dir.begin(), prob_piece_dir.end(), 0) == PROB_PIECES && "Does not sum up to 1!"); - } - // - - // generic output (for every view transition) - for (std::size_t v = 0; v < viewTransition.size(); v++) { - os << actionName << std::get<2>(viewTransition.at(v)) << moveGuard(agentIndex) << " x" << agentName << "=" << c.second << " & y" << agentName << "=" << c.first << std::get<0>(viewTransition.at(v)); - for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS; i++) { - if (i == remainPosIndex) { - os << (i == 0 ? " -> " : " + ") << prob_piece_dir_constants.at(i) << " : " << positionTransition.at(i) << std::get<1>(viewTransition.at(v)) << moveUpdate(agentIndex) << (i == ALL_POSS_DIRECTIONS - 1 ? ";\n" : "\n"); - } else { - os << (i == 0 ? " -> " : " + ") << prob_piece_dir_constants.at(i) << " : " << positionTransition.at(i) << moveUpdate(agentIndex) << (i == ALL_POSS_DIRECTIONS - 1 ? ";\n" : "\n"); - } - } - } - - return os; + std::string PrismModulesPrinter::printSlipperyTurnGuard(const AgentName &a, const std::string &direction, const ActionId &actionId, const std::vector &guards, const std::string &cond) { + std::string actionName = "[" + a + "_turn_" + direction + "]"; + agentNameActionMap.at(a).insert({actionId, actionName}); + return "\t" + actionName + " " + buildConjunction(a, guards) + " & " + cond + " -> "; } - std::ostream& PrismModulesPrinter::printSlipperyMove(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const coordinates &c, std::set &slipperyActions, const std::array& neighborhood, SlipperyType orientation) { - constexpr std::size_t PROB_PIECES = 9, ALL_POSS_DIRECTIONS = 8; - - std::array positionTransition = { - /* north */ "(y" + agentName + "'=y" + agentName + "-1)", - /* north east */ "(x" + agentName + "'=x" + agentName + "+1) & (y" + agentName + "'=y" + agentName + "-1)", - /* east */ "(x" + agentName + "'=x" + agentName + "+1)", - /* east south */ "(x" + agentName + "'=x" + agentName + "+1) & (y" + agentName + "'=y" + agentName + "+1)", - /* south */ "(y" + agentName + "'=y" + agentName + "+1)", - /* south west */ "(x" + agentName + "'=x" + agentName + "-1) & (y" + agentName + "'=y" + agentName + "+1)", - /* west */ "(x" + agentName + "'=x" + agentName + "-1)", - /* north west */ "(x" + agentName + "'=x" + agentName + "-1) & (y" + agentName + "'=y" + agentName + "-1)" - }; - - // direction specifics - - std::size_t straightPosIndex, straightPosIndex_east, straightPosIndex_south, straightPosIndex_west, straightPosIndex_north; - std::string actionName, specialTransition; // if straight ahead is blocked - std::string positionGuard; - std::array prob_piece_dir; // { n, ne, e, se, s, sw, w, nw } - std::array prob_piece_dir_agent_north; // { n, ne, e, se, s, sw, w, nw } - std::array prob_piece_dir_agent_east; // { n, ne, e, se, s, sw, w, nw } - std::array prob_piece_dir_agent_south; // { n, ne, e, se, s, sw, w, nw } - std::array prob_piece_dir_agent_west; // { n, ne, e, se, s, sw, w, nw } - - std::array prob_piece_dir_constants; - std::array prob_piece_dir_constants_agent_north; - std::array prob_piece_dir_constants_agent_east; - std::array prob_piece_dir_constants_agent_south; - std::array prob_piece_dir_constants_agent_west; - - switch (orientation) - { - case SlipperyType::North: - actionName = "\t[" + agentName + "move_on_slip_north]"; - positionGuard = "\t" + agentName + "IsOnSlipperyNorth"; - prob_piece_dir = { 0, 0, 1, 2, 0 /* <- R */, 2, 1, 0 }; - - prob_piece_dir_agent_south = { 0 , 0, 0, 1, 0 /*s <- R */, 1, 0, 0}; - prob_piece_dir_agent_east = { 0, 0, 0 /*e <- R */, 2, 0, 0, 0, 0 }; - prob_piece_dir_agent_north = { 0 /*n <- R */, 0, 0, 0, 2 , 0, 0, 0 }; - prob_piece_dir_agent_west = { 0, 0, 0, 0, 0, 2, 0 /* <- R */, 0 }; - - prob_piece_dir_constants = { "prop_zero", "prop_zero", "prop_displacement * 1/2", "prop_displacement", "prop_zero" /* <- R */, "prop_displacement", "prop_displacement * 1/2", "prop_zero" }; - - prob_piece_dir_constants_agent_north = { "prop_zero", "prop_zero", "prop_zero", "prop_displacement * 1/2", "prop_zero" /* <- R */, "prop_displacement * 1/2", "prop_zero", "prop_zero" }; - prob_piece_dir_constants_agent_east = { "prop_zero", "prop_zero", "prop_zero", "prop_displacement", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" }; - prob_piece_dir_constants_agent_south = { "prop_displacement", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" } ; - prob_piece_dir_constants_agent_west ={ "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_displacement", "prop_zero", "prop_zero" } ; - - - straightPosIndex = 4; - straightPosIndex_east = 2; - straightPosIndex_south = 4; - straightPosIndex_west = 6; - straightPosIndex_north = 0; - - specialTransition = "(y" + agentName + "'=y" + agentName + (!neighborhood.at(straightPosIndex) ? ")" : "+1)"); - break; - - case SlipperyType::South: - actionName = "\t[" + agentName + "move_on_slip_south]"; - positionGuard = "\t" + agentName + "IsOnSlipperySouth"; - - prob_piece_dir = { 0 /* <- R */, 2, 1, 0, 0, 0, 1, 2 }; - // { n, ne, e, se, s, sw, w, nw } - prob_piece_dir_agent_north = { 0 /*n <- R */, 1, 0, 0, 0, 0, 0, 1}; - prob_piece_dir_agent_east = { 0, 2, 0 /*e <- R */, 0, 0, 0, 0, 0 }; - prob_piece_dir_agent_south = { 2, 0, 0, 0, 0 /*s <- R */, 0, 0, 0 }; - prob_piece_dir_agent_west = { 0, 0, 0, 0, 0, 0, 0 /* <- R */, 2 }; - - prob_piece_dir_constants = { "prop_zero" /* <- R */, "prop_displacement", "prop_displacement * 1/2", "prop_zero", "prop_zero", "prop_zero", "prop_displacement * 1/2", "prop_displacement" }; - - prob_piece_dir_constants_agent_north = { "prop_zero", "prop_displacement * 1/2", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_displacement * 1/2" }; - prob_piece_dir_constants_agent_east = { "prop_zero", "prop_displacement", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" }; - prob_piece_dir_constants_agent_south = { "prop_displacement", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" } ; - prob_piece_dir_constants_agent_west ={ "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_displacement" } ; - - - straightPosIndex = 0; // always north - straightPosIndex_east = 2; - straightPosIndex_south = 4; - straightPosIndex_west = 6; - straightPosIndex_north = 0; - specialTransition = "(y" + agentName + "'=y" + agentName + (!neighborhood.at(straightPosIndex) ? ")" : "-1)"); - break; - - case SlipperyType::East: - actionName = "\t[" + agentName + "move_on_slip_east]"; - positionGuard = "\t" + agentName + "IsOnSlipperyEast"; - // { n, ne, e, se, s, sw, w, nw } - - prob_piece_dir = { 1, 0, 0, 0, 1, 2, 0 /* <- R */, 2 }; - // TODO - prob_piece_dir_agent_north = { 0 /*n <- R */, 1, 0, 0, 0, 0, 0, 1}; - prob_piece_dir_agent_east = { 0, 2, 0 /*e <- R */, 0, 0, 0, 0, 0 }; - prob_piece_dir_agent_south = { 2, 0, 0, 0, 0 /*s <- R */, 0, 0, 0 }; - prob_piece_dir_agent_west = { 0, 0, 0, 0, 0, 0, 0 /* <- R */, 2 }; - - prob_piece_dir_constants = { "prop_displacement * 1/2", "prop_zero", "prop_zero", "prop_zero", "prop_displacement * 1/2", "prop_displacement", "prop_zero" /* <- R */, "prop_displacement" }; - - prob_piece_dir_constants_agent_north = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_displacement * 1/2", "prop_displacement * 1/2" }; - prob_piece_dir_constants_agent_east = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_displacement", "prop_zero" }; - prob_piece_dir_constants_agent_south = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_displacement * 1/2", "prop_displacement * 1/2", "prop_zero" } ; - prob_piece_dir_constants_agent_west ={ "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_displacement * 1/2", "prop_zero", "prop_displacement * 1/2" } ; - - - straightPosIndex = 6; - straightPosIndex_east = 2; - straightPosIndex_south = 4; - straightPosIndex_west = 6; - straightPosIndex_north = 0; - - specialTransition = "(x" + agentName + "'=x" + agentName + (!neighborhood.at(straightPosIndex) ? ")" : "-1)"); - break; - - case SlipperyType::West: - actionName = "\t[" + agentName + "move_on_slip_west]"; - positionGuard = "\t" + agentName + "IsOnSlipperyWest"; - prob_piece_dir = { 1, 2, 0 /* <- R */, 2, 1, 0, 0, 0 }; - // TODO - // { n, ne, e, se, s, sw, w, nw } - - prob_piece_dir_agent_north = { 0 /*n <- R */, 1, 0, 0, 0, 0, 0, 1}; - prob_piece_dir_agent_east = { 0, 2, 0 /*e <- R */, 0, 0, 0, 0, 0 }; - prob_piece_dir_agent_south = { 2, 0, 0, 0, 0 /*s <- R */, 0, 0, 0 }; - prob_piece_dir_agent_west = { 0, 0, 0, 0, 0, 0, 0 /* <- R */, 2 }; - - prob_piece_dir_constants = {"prop_displacement * 1/2", "prop_displacement", "prop_zero" /* <- R */, "prop_displacement", "prop_displacement * 1/2", "prop_zero","prop_zero", "prop_zero" }; - - prob_piece_dir_constants_agent_north = { "prop_zero", "prop_displacement * 1/2", "prop_displacement * 1/2", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" }; - prob_piece_dir_constants_agent_east = { "prop_zero", "prop_displacement * 1/2", "prop_zero", "prop_displacement * 1/2", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" }; - prob_piece_dir_constants_agent_south = { "prop_zero", "prop_zero", "prop_displacement * 1/2", "prop_displacement * 1/2", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" } ; - prob_piece_dir_constants_agent_west ={ "prop_zero", "prop_zero", "prop_displacement", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" } ; - - - straightPosIndex = 2; - straightPosIndex_east = 2; - straightPosIndex_south = 4; - straightPosIndex_west = 6; - straightPosIndex_north = 0; - specialTransition = "(x" + agentName + "'=x" + agentName + (!neighborhood.at(straightPosIndex) ? ")" : "+1)"); - break; - } - - slipperyActions.insert(actionName); - - // override probability to 0 if corresp. direction is blocked - - for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS; i++) { - if (!neighborhood.at(i)) - prob_piece_dir.at(i) = 0; - } - - // determine residual probability (R) by replacing 0 with (1 - overall sum) - if(enforceOneWays) { - prob_piece_dir = {0,0,0,0,0,0,0,0}; - prob_piece_dir_constants = {"zero","zero","zero","zero","zero","zero","zero","zero"}; - } - prob_piece_dir.at(straightPosIndex) = PROB_PIECES - std::accumulate(prob_piece_dir.begin(), prob_piece_dir.end(), 0); - prob_piece_dir_constants.at(straightPosIndex) = "prop_intended"; - prob_piece_dir_constants_agent_east.at(straightPosIndex_east) = "prop_intended"; - prob_piece_dir_constants_agent_south.at(straightPosIndex_south) = "prop_intended"; - prob_piece_dir_constants_agent_west.at(straightPosIndex_west) = "prop_intended"; - prob_piece_dir_constants_agent_north.at(straightPosIndex_north) = "prop_intended"; - // - { - assert(prob_piece_dir.at(straightPosIndex) <= 9 && prob_piece_dir.at(straightPosIndex) >= 3 && "Value not in Range!"); - assert(std::accumulate(prob_piece_dir.begin(), prob_piece_dir.end(), 0) == PROB_PIECES && "Does not sum up to 1!"); - assert(orientation != SlipperyType::North || (prob_piece_dir.at(7) == 0 && prob_piece_dir.at(0) == 0 && prob_piece_dir.at(1) == 0 && "Slippery up should be impossible!")); - assert(orientation != SlipperyType::South || (prob_piece_dir.at(3) == 0 && prob_piece_dir.at(4) == 0 && prob_piece_dir.at(5) == 0 && "Slippery down should be impossible!")); - assert(orientation != SlipperyType::East || (prob_piece_dir.at(1) == 0 && prob_piece_dir.at(2) == 0 && prob_piece_dir.at(3) == 0 && "Slippery right should be impossible!")); - assert(orientation != SlipperyType::West || (prob_piece_dir.at(5) == 0 && prob_piece_dir.at(6) == 0 && prob_piece_dir.at(7) == 0 && "Slippery left should be impossible!")); - } - // - - // special case: straight forward is blocked (then remain in same position) - - positionTransition.at(straightPosIndex) = specialTransition; + std::string PrismModulesPrinter::printSlipperyTurnUpdate(const AgentName &a, const updates &u) { + return updatesToString(u); + } - // generic output (for every view and every possible view direction) - size_t current_dir = 0; // East - os << actionName << moveGuard(agentIndex) << " x" << agentName << "=" << c.second << " & y" << agentName << "=" << c.first << " & " << agentName << "SlipperyMoveForwardAllowed " << "& " << "view" << agentName << "=" << current_dir; - - for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS; i++) { - os << (i == 0 ? " -> " : " + ") << prob_piece_dir_constants_agent_east.at(i) << " : " << positionTransition.at(i) << moveUpdate(agentIndex) << (i == ALL_POSS_DIRECTIONS - 1 ? ";\n" : "\n"); - } + void PrismModulesPrinter::printFaultyMovementModule(const AgentName &a) { + os << "\nmodule " << a << "FaultyBehaviour" << std::endl; + os << "\tpreviousAction" << a << " : [-1..2] init -1;\n"; - current_dir = 1; // South - os << actionName << moveGuard(agentIndex) << " x" << agentName << "=" << c.second << " & y" << agentName << "=" << c.first << " & " << agentName << "SlipperyMoveForwardAllowed " << "& " << "view" << agentName << "=" << current_dir; - - for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS; i++) { - os << (i == 0 ? " -> " : " + ") << prob_piece_dir_constants_agent_south.at(i) << " : " << positionTransition.at(i) << moveUpdate(agentIndex) << (i == ALL_POSS_DIRECTIONS - 1 ? ";\n" : "\n"); + for(const auto [actionId, actionName] : agentNameActionMap.at(a)) { + os << "\t" << actionName << faultyBehaviourGuard(a, actionId) << " -> " << faultyBehaviourUpdate(a, actionId) << ";\n"; } + os << "endmodule\n\n"; + } - current_dir = 2; // West + void PrismModulesPrinter::printMoveModule() { + os << "\nmodule " << "Arbiter" << std::endl; + os << "\tclock : [0.." << agentIndexMap.size() - 1 << "] init 0;\n"; - os << actionName << moveGuard(agentIndex) << " x" << agentName << "=" << c.second << " & y" << agentName << "=" << c.first << " & " << agentName << "SlipperyMoveForwardAllowed " << "& " << "view" << agentName << "=" << current_dir; - for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS; i++) { - os << (i == 0 ? " -> " : " + ") << prob_piece_dir_constants_agent_west.at(i) << " : " << positionTransition.at(i) << moveUpdate(agentIndex) << (i == ALL_POSS_DIRECTIONS - 1 ? ";\n" : "\n"); + for(const auto [agentName, actions] : agentNameActionMap) { + for(const auto [actionId, actionName] : actions) { + os << "\t" << actionName << " " << moveGuard(agentName) << " -> " << moveUpdate(agentName) << ";\n"; + } } + os << "endmodule\n\n"; + } - - current_dir = 3; // North - - os << actionName << moveGuard(agentIndex) << " x" << agentName << "=" << c.second << " & y" << agentName << "=" << c.first << " & " << agentName << "SlipperyMoveForwardAllowed " << "& " << "view" << agentName << "=" << current_dir; - for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS; i++) { - os << (i == 0 ? " -> " : " + ") << prob_piece_dir_constants_agent_north.at(i) << " : " << positionTransition.at(i) << moveUpdate(agentIndex) << (i == ALL_POSS_DIRECTIONS - 1 ? ";\n" : "\n"); + void PrismModulesPrinter::printConfiguredActions(const AgentName &agentName) { + for (auto& config : configuration) { + if (config.type_ == ConfigType::Module && !config.overwrite_ && agentName == config.module_) { + os << config.expression_ ; + } } - return os; + os << "\n"; } - std::ostream& PrismModulesPrinter::printEndmodule(std::ostream &os) { - os << "endmodule\n"; - os << "\n"; - return os; + void PrismModulesPrinter::printDoneActions(const AgentName &agentName) { + os << "\t[" << agentName << "_done]" << moveGuard(agentName) << agentName << "IsInGoal | " << agentName << "IsInLava -> (" << agentName << "Done'=true);\n"; } - std::ostream& PrismModulesPrinter::printPlayerStruct(std::ostream &os, const AgentName &agentName, const bool agentWithView, const std::vector &probabilities, const std::set &slipperyActions) { + void PrismModulesPrinter::printPlayerStruct(const AgentName &agentName) { os << "player " << agentName << "\n\t"; bool first = true; - std::list allActions = { "_move_north", "_move_east", "_move_south", "_move_west" }; - std::list movementActions = allActions; - for(auto const& probability : probabilities) { - std::string percentageString = std::to_string((int)(100 * probability)); - for(auto const& movement : movementActions) { - allActions.push_back(movement + "_" + percentageString); - } - } - if(agentWithView) { - allActions.push_back("_turn_left"); - allActions.push_back("_turn_right"); - } else { - allActions.push_back("_turns"); - } - - for(auto const& action : allActions) { - if(first) first = false; else os << ", "; - os << "[" << agentName << action << "]"; - } - for(auto const& action : slipperyActions) { - os << ", " << action; + for(const auto [actionId, actionName] : agentNameActionMap.at(agentName)) { + if(first) first = false; + else os << ", "; + os << actionName; } - - os << ", [" << agentName << "_done]"; os << "\nendplayer\n"; - return os; - } - - std::ostream& PrismModulesPrinter::printGlobalMoveVariable(std::ostream &os, const size_t &numberOfPlayer) { - os << "\nglobal move : [0.." << std::to_string(numberOfPlayer - 1) << "];\n\n"; - return os; } - std::ostream& PrismModulesPrinter::printRewards(std::ostream &os, const AgentName &agentName, const std::map &stateRewards, const cells &lava, const cells &goals, const std::map &backgroundTiles) { + void PrismModulesPrinter::printRewards(const AgentName &agentName, const std::map &stateRewards, const cells &lava, const cells &goals, const std::map &backgroundTiles) { if(lava.size() != 0) { os << "rewards \"" << agentName << "SafetyNoBFS\"\n"; os << "\t" < 0.0f; + } + + bool PrismModulesPrinter::slipperyBehaviour() const { + return !slipperyTiles.at("North").empty() || !slipperyTiles.at("East").empty() || !slipperyTiles.at("South").empty() || !slipperyTiles.at("West").empty(); } bool PrismModulesPrinter::isGame() const { return modelType == ModelType::SMG; } + + std::string PrismModulesPrinter::buildConjunction(const AgentName &a, std::vector formulae) const { + if(formulae.empty()) return "true"; + std::string conjunction = ""; + bool first = true; + for(auto const formula : formulae) { + if(first) first = false; + else conjunction += " & "; + conjunction += formula; + } + return conjunction; + } + } diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h index 9e5936c..a66d68f 100644 --- a/util/PrismModulesPrinter.h +++ b/util/PrismModulesPrinter.h @@ -1,119 +1,111 @@ #pragma once #include +#include #include #include "MinigridGrammar.h" #include "PrismPrinter.h" #include "ConfigYaml.h" + +std::string northUpdate(const AgentName &a); +std::string southUpdate(const AgentName &a); +std::string eastUpdate(const AgentName &a); +std::string westUpdate(const AgentName &a); + namespace prism { class PrismModulesPrinter { public: - PrismModulesPrinter(const ModelType &modelType, const size_t &numberOfPlayer, std::vector config ,const bool enforceOneWays = false); - - std::ostream& printRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &grid_cells, const cells& keys, const cells& doors); - std::ostream& printKeyRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &keys); - std::ostream& printDoorRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &doors); - std::ostream& printIsOnSlipperyFormula(std::ostream& os, const AgentName &agentName, const std::vector> &slipperyCollection, const cells &slipperyNorth, const cells &slipperyEast, const cells &slipperySouth, const cells &slipperyWest); - std::ostream& printGoalLabel(std::ostream& os, const AgentName&agentName, const cells &goals); - std::ostream& printCrashLabel(std::ostream &os, const std::vector agentNames); - std::ostream& printAvoidanceLabel(std::ostream &os, const std::vector agentNames, const int &distance); - std::ostream& printKeysLabels(std::ostream& os, const AgentName&agentName, const cells &keys); - std::ostream& printBackgroundLabels(std::ostream &os, const AgentName &agentName, const std::pair &backgroundTiles); - std::ostream& printIsInLavaFormula(std::ostream& os, const AgentName &agentName, const cells &lava); - std::ostream& printIsFixedFormulas(std::ostream& os, const AgentName &agentName); - std::ostream& printTurningNotAllowedFormulas(std::ostream& os, const AgentName &agentName, const cells &floor); - std::ostream& printWallFormula(std::ostream& os, const AgentName &agentName, const cells &walls); - std::ostream& printFormulas(std::ostream& os, - const AgentName&agentName, - const cells &restrictionNorth, - const cells &restrictionEast, - const cells &restrictionSouth, - const cells &restrictionWest, - const std::vector> &slipperyCollection, - const cells &lava, - const cells &walls, - const cells &noTurnFloor, - const cells &slipperyNorth, - const cells &slipperyEast, - const cells &slipperySouth, - const cells &slipperyWest, - const cells &keys, - const cells &doors); - - std::ostream& printKeyModule(std::ostream &os, const cell &key, const coordinates &boundaries, AgentName agentName); - std::ostream& printKeyActions(std::ostream &os, const cell& key ,const std::string &keyIdentifier, AgentName agentName); - - std::ostream& printDoorModule(std::ostream &os, const cell &door, const coordinates &boundaries, AgentName agentName); - std::ostream& printDoorActions(std::ostream &os, const cell &door ,const std::string &doorIdentifier, AgentName agentName); - std::ostream& printConstants(std::ostream &os, const std::vector &constants); - /* - * Representation for Slippery Tile. - * -) North: Slips from North to South - * -) East: Slips from East to West - * -) South: Slips from South to North - * -) West: Slips from West to East - */ - enum class SlipperyType { North, East, South, West }; - - /* - * Prints Slippery on move action. - * - * @param neighborhood: Information of wall-blocks in 8-neighborhood { n, nw, e, se, s, sw, w, nw }. If entry is false, then corresponding neighboorhood position is a wall. - * @param orientation: Information of slippery type (either north, south, east, west). - */ - std::ostream& printSlipperyMove(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const coordinates &c, std::set &slipperyActions, const std::array& neighborhood, SlipperyType orientation); - - /* - * Prints Slippery on turn action. - * - * @param neighborhood: Information of wall-blocks in 8-neighborhood { n, nw, e, se, s, sw, w, nw }. If entry is false, then corresponding neighboorhood position is a wall. - * @param orientation: Information of slippery type (either north, south, east, west). - */ - std::ostream& printSlipperyTurn(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const coordinates &c, std::set &slipperyActions, const std::array& neighborhood, SlipperyType orientation); - - std::ostream& printModel(std::ostream &os, const ModelType &modelType); - std::ostream& printBooleansForKeys(std::ostream &os, const AgentName &agentName, const cells &keys); - std::ostream& printActionsForKeys(std::ostream &os, const AgentName &agentName, const cells &keys); - std::ostream& printBooleansForBackground(std::ostream &os, const AgentName &agentName, const std::map &backgroundTiles); - std::ostream& printActionsForBackground(std::ostream &os, const AgentName &agentName, const std::map &backgroundTiles); - std::ostream& printInitStruct(std::ostream &os, const AgentNameAndPositionMap &agents, const KeyNameAndPositionMap &keys, const cells &lockedDoors, const cells &unlockedDoors, prism::ModelType modelType); - std::ostream& printModule(std::ostream &os, - const AgentName &agentName, - const size_t &agentIndex, - const coordinates &boundaries, - const coordinates& initialPosition, - const cells &keys, - const std::map &backgroundTiles, - const bool agentWithView, - const std::vector &probabilities = {}, - const double faultyProbability = 0); - std::ostream& printMovementActions(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const bool agentWithView, const float &probability = 1.0, const double &stickyProbability = 0.0); - std::ostream& printDoneActions(std::ostream &os, const AgentName &agentName, const size_t &agentIndex); - std::ostream& printEndmodule(std::ostream &os); - std::ostream& printPlayerStruct(std::ostream &os, const AgentName &agentName, const bool agentWithView, const std::vector &probabilities = {}, const std::set &slipperyActions = {}); - std::ostream& printGlobalMoveVariable(std::ostream &os, const size_t &numberOfPlayer); - std::ostream& printRewards(std::ostream &os, const AgentName &agentName, const std::map &stateRewards, const cells &lava, const cells &goals, const std::map &backgroundTiles); - - std::ostream& printConfiguration(std::ostream &os, const std::vector& configurations); - std::ostream& printConfiguredActions(std::ostream &os, const AgentName &agentName); - - std::string moveGuard(const size_t &agentIndex); - std::string pickupGuard(const AgentName &agentName, const std::string keyColor); - std::string dropGuard(const AgentName &agentName, const std::string keyColor, size_t view); - std::string moveUpdate(const size_t &agentIndex); - std::string unlockGuard(const AgentName &agentName, const cell& door); - std::string toggleGuard(const AgentName &agentName, const cell& door); - - std::string viewVariable(const AgentName &agentName, const size_t &agentDirection, const bool agentWithView); + PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector config, const float probIntended, const float faultyProbability); + + std::ostream& print(); + + void printModelType(const ModelType &modelType); + bool isGame() const; private: + void printPortableObjectModule(const cell &object); + void printPortableObjectActions(const std::string &agentName, const std::string &identifier); + + void printDoorModule(const cell &object, const bool &opened); + void printLockedDoorActions(const std::string &agentName, const std::string &identifier); + void printUnlockedDoorActions(const std::string &agentName, const std::string &identifier); + + void printRobotModule(const AgentName &agentName, const coordinates &initialPosition); + void printPortableObjectActionsForRobot(const std::string &agentName, const std::string &identifier); + void printUnlockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier); + void printLockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier, const std::string &key); + void printMovementActionsForRobot(const std::string &a); + void printTurnActionsForRobot(const std::string &a); + void printSlipperyMovementActionsForRobot(const AgentName &a); + void printSlipperyMovementActionsForNorth(const AgentName &a); + 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); + std::string printMovementUpdate(const AgentName &a, const update &update) const; + std::string printTurnGuard(const AgentName &a, const std::string &direction, const ActionId &actionId, const std::string &cond = ""); + 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); + 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 ActionId &actionId, const std::vector &guards, const std::string &cond); + std::string printSlipperyTurnUpdate(const AgentName &a, const updates &u); + + void printFaultyMovementModule(const AgentName &a); + void printMoveModule(); + + void printConstants(const std::vector &constants); - ModelType const& modelType; - const size_t numberOfPlayer; - bool enforceOneWays; + void printDoneActions(const AgentName &agentName); + void printPlayerStruct(const AgentName &agentName); + void printRewards(const AgentName &agentName, const std::map &stateRewards, const cells &lava, const cells &goals, const std::map &backgroundTiles); + + void printConfiguration(const std::vector& configurations); + void printConfiguredActions(const AgentName &agentName); + + bool anyPortableObject() const; + bool faultyBehaviour() const; + bool slipperyBehaviour() const; + std::string moveGuard(const AgentName &agentName) const; + std::string faultyBehaviourGuard(const AgentName &agentName, const ActionId &actionId) const; + std::string faultyBehaviourUpdate(const AgentName &agentName, const ActionId &actionId) const; + std::string moveUpdate(const AgentName &agentName) const; + std::string updatesToString(const updates &updates) const; + std::string updateToString(const update &u) const; + + std::string viewVariable(const AgentName &agentName, const size_t &agentDirection) const; + + + std::string buildConjunction(const AgentName &a, std::vector formulae) const; + + + std::ostream &os; + std::stringstream actionStream; + + ModelType const &modelType; + coordinates const &maxBoundaries; + AgentName agentName; + cells boxes; + cells balls; + cells lockedDoors; + cells unlockedDoors; + cells keys; + std::map slipperyTiles; + + AgentNameAndPositionMap agentNameAndPositionMap; + std::map agentIndexMap; + size_t numberOfPlayer; + float const faultyProbability; + float const probIntended; std::vector configuration; - std::map viewDirectionMapping; + std::vector viewDirections = {0, 1, 2, 3}; + + std::map>> agentNameActionMap; }; } diff --git a/util/PrismPrinter.cpp b/util/PrismPrinter.cpp new file mode 100644 index 0000000..4c172f1 --- /dev/null +++ b/util/PrismPrinter.cpp @@ -0,0 +1,8 @@ +#include "PrismPrinter.h" + +#include + +std::string capitalize(std::string string) { + string[0] = std::toupper(string[0]); + return string; +} diff --git a/util/PrismPrinter.h b/util/PrismPrinter.h index 55f4ada..572cb40 100644 --- a/util/PrismPrinter.h +++ b/util/PrismPrinter.h @@ -1,14 +1,22 @@ #pragma once #include +#include #include "cell.h" typedef std::string AgentName; +typedef size_t ViewDirection; typedef std::pair AgentNameAndPosition; typedef AgentNameAndPosition KeyNameAndPosition; typedef std::map AgentNameAndPositionMap; typedef std::map KeyNameAndPositionMap; +typedef std::pair CellAndCondition; +typedef std::pair update; +typedef std::vector updates; +typedef int8_t ActionId; + +std::string capitalize(std::string string); namespace prism { enum class ModelType { diff --git a/util/cell.cpp b/util/cell.cpp index 07d25f7..c6a72a1 100644 --- a/util/cell.cpp +++ b/util/cell.cpp @@ -4,10 +4,14 @@ std::ostream &operator<<(std::ostream &os, const cell &c) { os << static_cast(c.type) << static_cast(c.color); - os << " at (" << c.row << "," << c.column << ")"; + os << " at (" << c.column << "," << c.row << ")"; return os; } +coordinates cell::getCoordinates() const { + return std::make_pair(column, row); +} + cell cell::getNorth(const std::vector &grid) const { auto north = std::find_if(grid.begin(), grid.end(), [this](const cell &c) { return this->row - 1 == c.row && this->column == c.column; @@ -52,10 +56,6 @@ cell cell::getWest(const std::vector &grid) const { return *west; } -coordinates cell::getCoordinates() const { - return std::make_pair(row, column); -} - std::string cell::getColor() const { switch(color) { case Color::Red: return "red"; @@ -69,6 +69,27 @@ std::string cell::getColor() const { } } +std::string cell::getType() const { + switch(type) { + case Type::Wall: return "Wall"; + case Type::Floor: return "Floor"; + case Type::Door: return "Door"; + case Type::LockedDoor: return "LockedDoor"; + case Type::Key: return "Key"; + case Type::Ball: return "Ball"; + case Type::Box: return "Box"; + case Type::Goal: return "Goal"; + case Type::Lava: return "Lava"; + case Type::Agent: return "Agent"; + case Type::Adversary: return "Adversary"; + case Type::SlipperyNorth: return "SlipperyNorth"; + case Type::SlipperySouth: return "SlipperySouth"; + case Type::SlipperyEast: return "SlipperyEast"; + case Type::SlipperyWest: return "SlipperyWest"; + default: return ""; + } +} + std::string getColor(Color color) { switch(color) { case Color::Red: return "red"; diff --git a/util/cell.h b/util/cell.h index c369052..ca71559 100644 --- a/util/cell.h +++ b/util/cell.h @@ -40,10 +40,10 @@ std::string getColor(Color color); class cell { public: - coordinates getNorth() const { return std::make_pair(row - 1, column); } - coordinates getSouth() const { return std::make_pair(row + 1, column); } - coordinates getEast() const { return std::make_pair(row, column + 1); } - coordinates getWest() const { return std::make_pair(row, column - 1); } + coordinates getNorth() const { return std::make_pair(column, row - 1); } + coordinates getSouth() const { return std::make_pair(column, row + 1); } + coordinates getEast() const { return std::make_pair(column + 1, row); } + coordinates getWest() const { return std::make_pair(column - 1, row); } cell getNorth(const std::vector &grid) const; cell getEast(const std::vector &grid) const; @@ -54,6 +54,7 @@ class cell { coordinates getCoordinates() const; std::string getColor() const; + std::string getType() const; int row; int column;