From 707d4051f045fb75209799a6de505f62987e62ef Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Mon, 27 Nov 2023 21:46:34 +0100 Subject: [PATCH] changed slippery position, added index in config --- util/ConfigYaml.cpp | 5 ++- util/ConfigYaml.h | 6 +++- util/Grid.cpp | 33 +++++++++++-------- util/PrismModulesPrinter.cpp | 63 ++++++++++++++++++++++++++++++++---- util/PrismModulesPrinter.h | 4 +-- 5 files changed, 87 insertions(+), 24 deletions(-) diff --git a/util/ConfigYaml.cpp b/util/ConfigYaml.cpp index ae3fe49..063face 100644 --- a/util/ConfigYaml.cpp +++ b/util/ConfigYaml.cpp @@ -89,6 +89,9 @@ bool YAML::convert::decode(const YAML::Node& node, Action& rhs) { if (node["overwrite"]) { rhs.overwrite_ = node["overwrite"].as(); } + if (node["index"]) { + rhs.index_ = node["index"].as(); + } return true; } @@ -172,7 +175,7 @@ const std::string Configuration::overwrite_identifier_{"; // Overwritten through } for (auto& module : modules) { for (auto& action : module.actions_) { - configuration.push_back({action.createExpression(), action.action_, ConfigType::Module, action.overwrite_, module.module_}); + configuration.push_back({action.createExpression(), action.action_, ConfigType::Module, action.overwrite_, module.module_, action.index_}); } } diff --git a/util/ConfigYaml.h b/util/ConfigYaml.h index 0e1b46e..9eed26f 100644 --- a/util/ConfigYaml.h +++ b/util/ConfigYaml.h @@ -20,6 +20,8 @@ struct Configuration std::string module_ {}; std::string expression_{}; std::string identifier_{}; + int index_{}; + ConfigType type_ {ConfigType::Label}; bool overwrite_ {false}; @@ -28,7 +30,8 @@ struct Configuration , std::string identifier , ConfigType type , bool overwrite = false - , std::string module = "") : expression_(expression), identifier_(identifier), type_(type), overwrite_(overwrite), module_{module} {} + , std::string module = "" + , int index = 0) : expression_(expression), identifier_(identifier), type_(type), overwrite_(overwrite), module_{module}, index_(index) {} ~Configuration() = default; Configuration(const Configuration&) = default; @@ -72,6 +75,7 @@ struct Action { std::string action_; std::string guard_; std::string update_; + int index_{0}; bool overwrite_ {false}; std::string createExpression() const; diff --git a/util/Grid.cpp b/util/Grid.cpp index fa17d6c..f5bc5d6 100644 --- a/util/Grid.cpp +++ b/util/Grid.cpp @@ -1,4 +1,5 @@ #include "Grid.h" +#include #include @@ -162,7 +163,8 @@ void Grid::applyOverwrites(std::string& str, std::vector& configu } else if (config.type_ == ConfigType::Label) { start_pos = str.find("label " + config.identifier_); } else if (config.type_ == ConfigType::Module) { - start_pos = str.find(config.identifier_); + auto iter = boost::find_nth(str, config.identifier_, config.index_); + start_pos = std::distance(str.begin(), iter.begin()); } size_t end_pos = str.find(';', start_pos) + 1; @@ -260,22 +262,25 @@ void Grid::printToPrism(std::ostream& os, std::vector& configurat 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); - 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); - + if (!slipperyNorth.empty()) { + auto c = slipperyNorth.at(0); + printer.printSlipperyMove(os, agentName, agentIndex, slipperyActions, getWalkableDirOf8Neighborhood(c), prism::PrismModulesPrinter::SlipperyType::North); + if(!gridOptions.enforceOneWays) printer.printSlipperyTurn(os, agentName, agentIndex, 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); + if (!slipperyEast.empty()) { + auto c = slipperyEast.at(0); + printer.printSlipperyMove(os, agentName, agentIndex, slipperyActions, getWalkableDirOf8Neighborhood(c), prism::PrismModulesPrinter::SlipperyType::East); + if(!gridOptions.enforceOneWays) printer.printSlipperyTurn(os, agentName, agentIndex, 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); + if (!slipperySouth.empty()) { + auto c = slipperySouth.at(0); + printer.printSlipperyMove(os, agentName, agentIndex, slipperyActions, getWalkableDirOf8Neighborhood(c), prism::PrismModulesPrinter::SlipperyType::South); + if(!gridOptions.enforceOneWays) printer.printSlipperyTurn(os, agentName, agentIndex, 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); + if (!slipperyWest.empty()) { + auto c = slipperyWest.at(0); + printer.printSlipperyMove(os, agentName, agentIndex, slipperyActions, getWalkableDirOf8Neighborhood(c), prism::PrismModulesPrinter::SlipperyType::West); + if(!gridOptions.enforceOneWays) printer.printSlipperyTurn(os, agentName, agentIndex, slipperyActions, getWalkableDirOf8Neighborhood(c), prism::PrismModulesPrinter::SlipperyType::West); } printer.printEndmodule(os); diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index 757683b..09b30d6 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -127,8 +127,49 @@ namespace prism { 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"; + } + + 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 (!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 << ")"; + } + 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 << ")"; + } + os << ";\n"; + } + + first = true; os << "formula " << agentName << "IsOnSlippery = "; for (const auto& slippery: slipperyCollection) { @@ -640,7 +681,7 @@ namespace prism { return os; } - 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) { + std::ostream& PrismModulesPrinter::printSlipperyTurn(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, std::set &slipperyActions, const std::array& neighborhood, SlipperyType orientation) { constexpr std::size_t PROB_PIECES = 9, ALL_POSS_DIRECTIONS = 9; std::array positionTransition = { @@ -668,6 +709,7 @@ namespace prism { // direction specifics std::string actionName; + std::string positionGuard; std::size_t remainPosIndex = 8; std::array prob_piece_dir; // { n, ne, w, se, s, sw, w, nw, CURRENT POS } @@ -675,21 +717,25 @@ namespace prism { { case SlipperyType::North: actionName = "\t[" + agentName + "turn_at_slip_north"; + positionGuard = "\t" + agentName + "IsOnSlipperyNorth"; prob_piece_dir = { 0, 0, 0, 1, 1, 1, 0, 0, 0 /* <- R */ }; break; case SlipperyType::South: actionName = "\t[" + agentName + "turn_at_slip_south"; + positionGuard = "\t" + agentName + "IsOnSlipperySouth"; prob_piece_dir = { 1, 1, 0, 0, 0, 0, 0, 1, 0 /* <- R */ }; break; case SlipperyType::East: actionName = "\t[" + agentName + "turn_at_slip_east"; + positionGuard = "\t" + agentName + "IsOnSlipperyEast"; prob_piece_dir = { 0, 0, 0, 0, 0, 1, 1, 1, 0 /* <- R */ }; break; case SlipperyType::West: actionName = "\t[" + agentName + "turn_at_slip_west"; + positionGuard = "\t" + agentName + "IsOnSlipperyWest"; prob_piece_dir = { 0, 1, 1, 1, 0, 0, 0, 0, 0 /* <- R */ }; break; } @@ -715,11 +761,11 @@ namespace prism { } // - // 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) << positionGuard << std::get<0>(viewTransition.at(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)); + // 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++) { os << (i == 0 ? " -> " : " + ") << prob_piece_dir.at(i) << "/" << PROB_PIECES << " : " << positionTransition.at(i) << std::get<1>(viewTransition.at(v)) << moveUpdate(agentIndex) << (i == ALL_POSS_DIRECTIONS - 1 ? ";\n" : "\n"); } @@ -728,7 +774,7 @@ namespace prism { return os; } - 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) { + std::ostream& PrismModulesPrinter::printSlipperyMove(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, std::set &slipperyActions, const std::array& neighborhood, SlipperyType orientation) { constexpr std::size_t PROB_PIECES = 9, ALL_POSS_DIRECTIONS = 8; std::array positionTransition = { @@ -746,12 +792,14 @@ namespace prism { std::size_t straightPosIndex; std::string actionName, specialTransition; // if straight ahead is blocked + std::string positionGuard; std::array prob_piece_dir; // { n, ne, w, se, s, sw, w, nw } 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 }; straightPosIndex = 4; specialTransition = "(y" + agentName + "'=y" + agentName + (!neighborhood.at(straightPosIndex) ? ")" : "+1)"); @@ -759,6 +807,7 @@ namespace prism { 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 }; straightPosIndex = 0; // always north specialTransition = "(y" + agentName + "'=y" + agentName + (!neighborhood.at(straightPosIndex) ? ")" : "-1)"); @@ -766,6 +815,7 @@ namespace prism { case SlipperyType::East: actionName = "\t[" + agentName + "move_on_slip_east]"; + positionGuard = "\t" + agentName + "IsOnSlipperyEast"; prob_piece_dir = { 1, 0, 0, 0, 1, 2, 0 /* <- R */, 2 }; straightPosIndex = 6; specialTransition = "(x" + agentName + "'=x" + agentName + (!neighborhood.at(straightPosIndex) ? ")" : "-1)"); @@ -773,6 +823,7 @@ namespace prism { 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 }; straightPosIndex = 2; specialTransition = "(x" + agentName + "'=x" + agentName + (!neighborhood.at(straightPosIndex) ? ")" : "+1)"); @@ -811,7 +862,7 @@ namespace prism { // generic output (for every view and every possible view direction) - os << actionName << moveGuard(agentIndex) << " x" << agentName << "=" << c.second << " & y" << agentName << "=" << c.first << " & " << agentName << "SlipperyMoveForwardAllowed "; + os << actionName << moveGuard(agentIndex) << positionGuard << " & " << agentName << "SlipperyMoveForwardAllowed "; for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS; i++) { os << (i == 0 ? " -> " : " + ") << prob_piece_dir.at(i) << "/" << PROB_PIECES << " : " << positionTransition.at(i) << moveUpdate(agentIndex) << (i == ALL_POSS_DIRECTIONS - 1 ? ";\n" : "\n"); diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h index 07f67bd..7d31b45 100644 --- a/util/PrismModulesPrinter.h +++ b/util/PrismModulesPrinter.h @@ -62,7 +62,7 @@ namespace prism { * @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); + std::ostream& printSlipperyMove(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, std::set &slipperyActions, const std::array& neighborhood, SlipperyType orientation); /* * Prints Slippery on turn action. @@ -70,7 +70,7 @@ namespace prism { * @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& printSlipperyTurn(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, 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);