diff --git a/CMakeLists.txt b/CMakeLists.txt index 0392819..28e6f07 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,26 +1,25 @@ +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) -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) +find_package(yaml-cpp) + +add_executable(main + ${SRCS} + main.cpp + ) + target_link_libraries(main pthread yaml-cpp::yaml-cpp) + diff --git a/exampleConfig.yaml b/exampleConfig.yaml index 8c3042b..0c81f90 100644 --- a/exampleConfig.yaml +++ b/exampleConfig.yaml @@ -1,7 +1,9 @@ --- -labels: - - label: "AgentIsInGoal" - text: "AgentIsInGoal" +# labels: +# - label: "AgentIsInGoal" +# text: "AgentIsInGoal" +# - label: "Hallo" +# text: "AgentIsInGoal" # constants: # - constant: "prop_slippery_turn" @@ -9,25 +11,34 @@ labels: # value: "9/9" # overwrite: True -probabilities: - - probability: "FaultProbability" +properties: + - property: "FaultProbability" value: 0.2 - - probability: "ProbForwardIntended" + - property: "ProbForwardIntended" value: 0.1 - - probability: "ProbTurnIntended" + - property: "ProbTurnIntended" value: 0.1 + # - property: "modeltype" + # value: "smg" modules: - module: "Agent" + # overwrite: True + # module_text: | + # NewModule + # True commands: - action: "[Agent_turn_left]" - guard: "AgentIsOnSlippery" - update: "True" + guard: "viewAgent=3" + overwrite: True + index: 1 + - action: "[Agent_turn_left]" + update: "(viewAgent'=3)" overwrite: True index: 3 - action: "[Agent_turn_right]" guard: "AgentIsOnSlippery" - update: "True" + update: "(viewAgent'=3)" overwrite: True index: [0,1] ... \ No newline at end of file diff --git a/examples/example_guards.prism b/examples/example_guards.prism new file mode 100644 index 0000000..5c2ce10 --- /dev/null +++ b/examples/example_guards.prism @@ -0,0 +1,23 @@ +mdp + +formula AgentCannotMoveEastWall = (colAgent=1&rowAgent=2) | (colAgent=4&rowAgent=2) | (colAgent=4&rowAgent=3) | (colAgent=4&rowAgent=4) | (colAgent=4&rowAgent=1); +formula AgentCannotMoveNorthWall = (colAgent=1&rowAgent=1) | (colAgent=2&rowAgent=1) | (colAgent=3&rowAgent=1) | (colAgent=2&rowAgent=3) | (colAgent=3&rowAgent=3) | (colAgent=4&rowAgent=1); +formula AgentCannotMoveSouthWall = (colAgent=2&rowAgent=1) | (colAgent=3&rowAgent=1) | (colAgent=1&rowAgent=4) | (colAgent=2&rowAgent=4) | (colAgent=3&rowAgent=4) | (colAgent=4&rowAgent=4); +formula AgentCannotMoveWestWall = (colAgent=1&rowAgent=1) | (colAgent=1&rowAgent=2) | (colAgent=4&rowAgent=2) | (colAgent=1&rowAgent=3) | (colAgent=1&rowAgent=4); +formula AgentIsOnSlippery = false; + +module Agent + colAgent : [1..4] init 4; + rowAgent : [1..4] init 1; + viewAgent : [0..3] init 1; + + [Agent_turn_right] !AgentIsOnOneWay-> 1.000000: (viewAgent'=mod(viewAgent+1,4)); + [Agent_turn_left] !AgentIsOnOneWay-> 1.000000: (viewAgent'=viewAgent-1); + [Agent_turn_left] !AgentIsOnOneWay-> 1.000000: (viewAgent'=3); + [Agent_move_North] viewAgent=3 & !AgentCannotMoveNorthWall -> 1.000000: (rowAgent'=rowAgent-1); + [Agent_move_East] colAgent != 1 & rowAgent != 1-> 1.000000: (colAgent'=colAgent+1); + [Agent_move_South] viewAgent=1 & !AgentCannotMoveSouthWall -> 1.000000: (rowAgent'=rowAgent+1); + [Agent_move_West] viewAgent=2 & !AgentCannotMoveWestWall -> 1.000000: (colAgent'=colAgent-1); +endmodule + +formula AgentIsOnOneWay = (colAgent=2&rowAgent=1) | (colAgent=3&rowAgent=1); // created through configuration diff --git a/examples/example_guards.txt b/examples/example_guards.txt new file mode 100644 index 0000000..33e9289 --- /dev/null +++ b/examples/example_guards.txt @@ -0,0 +1,17 @@ +WGWGWGWGWGWG +WG XRWG +WG WGWG WG +WG WG +WG WG +WGWGWGWGWGWG +------------ +WGWGWGWGWGWG +WG WG +WG WGWG WG +WG WG +WG WG +WGWGWGWGWGWG +------------ +------------ +ProbTurnIntended:0.85 +ProbForwardIntended:0.25 \ No newline at end of file diff --git a/examples/example_guards.yaml b/examples/example_guards.yaml new file mode 100644 index 0000000..9624b19 --- /dev/null +++ b/examples/example_guards.yaml @@ -0,0 +1,19 @@ +--- +formulas: + - formula: "AgentIsOnOneWay" + content: "(colAgent=2&rowAgent=1) | (colAgent=3&rowAgent=1)" + +modules: + - module: "Agent" + commands: + - action: "[Agent_move_East]" + guard: "colAgent != 1 & rowAgent != 1" + overwrite: True + - action: "[Agent_turn_right]" + guard: "!AgentIsOnOneWay" + overwrite: True + - action: "[Agent_turn_left]" + guard: "!AgentIsOnOneWay" + overwrite: True + index: [0,1] +... \ No newline at end of file diff --git a/examples/example_module.txt b/examples/example_module.txt new file mode 100644 index 0000000..8d0e2d7 --- /dev/null +++ b/examples/example_module.txt @@ -0,0 +1,17 @@ +WGWGWGWGWGWGWG +WGZY XRWG +WG WG +WG WG +WG WGWGWGWGWG +WG AYGGWG +WGWGWGWGWGWGWG +-------------- +WGWGWGWGWGWGWG +WG WG +WG WG +WG WG +WG WGWGWGWGWG +WG WG +WGWGWGWGWGWGWG +-------------- +-------------- \ No newline at end of file diff --git a/examples/example_module.yaml b/examples/example_module.yaml new file mode 100644 index 0000000..9005c10 --- /dev/null +++ b/examples/example_module.yaml @@ -0,0 +1,36 @@ +--- + +properties: + - property: "modeltype" + value: "mdp" + +formulas: + - formula: "YellowMovesNorth" + content: "(rowYellow=2 | rowYellow=3 | rowYellow=4) & colYellow=1 & viewYellow=3" + - formula: "YellowMovesSouth" + content: "(rowYellow=2 | rowYellow=3 | rowYellow=4) & colYellow=1 & viewYellow=1" + +modules: + - module: "Yellow" + overwrite: True + module_text: | + colYellow : [1..5] init 1; + rowYellow : [1..5] init 1; + viewYellow : [0..3] init 1; + YellowCarryingYellowBall : bool init false; + + [Yellow_turn_right] (!YellowMovesSouth & !YellowMovesNorth) -> 1.000000: (viewYellow'=mod(viewYellow+1,4)); + [Yellow_turn_left] (!YellowMovesSouth & !YellowMovesNorth) -> 1.000000: (viewYellow'=viewYellow-1); + [Yellow_turn_left] (!YellowMovesSouth & !YellowMovesNorth) -> 1.000000: (viewYellow'=3); + [Yellow_move_North] !YellowMovesSouth & viewYellow=3 & !YellowIsOnGoal & !YellowCannotMoveNorthWall & !YellowCannotMoveConditionally -> 1.000000: (rowYellow'=rowYellow-1); + [Yellow_move_East] !(YellowMovesNorth|YellowMovesSouth) & viewYellow=0 & !YellowIsOnGoal & !YellowCannotMoveEastWall & !YellowCannotMoveConditionally -> 1.000000: (colYellow'=colYellow+1); + [Yellow_move_South] !YellowMovesNorth & viewYellow=1 & !YellowIsOnGoal & !YellowCannotMoveSouthWall & !YellowCannotMoveConditionally -> 1.000000: (rowYellow'=rowYellow+1); + [Yellow_move_West] !(YellowMovesNorth|YellowMovesSouth) & viewYellow=2 & !YellowIsOnGoal & !YellowCannotMoveWestWall & !YellowCannotMoveConditionally -> 1.000000: (colYellow'=colYellow-1); + [Yellow_pickup_YellowBall] !YellowIsCarrying & YellowCannotMoveYellowBall -> (YellowCarryingYellowBall'=true); + [Yellow_drop_YellowBall_north] YellowCarryingYellowBall & viewYellow=3 & !YellowCannotMoveConditionally & !YellowCannotMoveNorthWall -> (YellowCarryingYellowBall'=false); + [Yellow_drop_YellowBall_west] YellowCarryingYellowBall & viewYellow=2 & !YellowCannotMoveConditionally & !YellowCannotMoveWestWall -> (YellowCarryingYellowBall'=false); + [Yellow_drop_YellowBall_south] YellowCarryingYellowBall & viewYellow=1 & !YellowCannotMoveConditionally & !YellowCannotMoveSouthWall -> (YellowCarryingYellowBall'=false); + [Yellow_drop_YellowBall_east] YellowCarryingYellowBall & viewYellow=0 & !YellowCannotMoveConditionally & !YellowCannotMoveEastWall -> (YellowCarryingYellowBall'=false); + + +... \ No newline at end of file diff --git a/examples/example_probabilities.txt b/examples/example_probabilities.txt new file mode 100644 index 0000000..56bd60b --- /dev/null +++ b/examples/example_probabilities.txt @@ -0,0 +1,13 @@ +WGWGWGWG +WGVRXRWG +WGnB WG +WGWGWGWG +-------- +WGWGWGWG +WG WG +WGnB WG +WGWGWGWG +-------- +-------- +ProbTurnIntended:0.85 +ProbForwardIntended:0.25 \ No newline at end of file diff --git a/examples/example_probabilities.yaml b/examples/example_probabilities.yaml new file mode 100644 index 0000000..f77c598 --- /dev/null +++ b/examples/example_probabilities.yaml @@ -0,0 +1,5 @@ +--- +properties: + - property: "ProbForwardIntended" + value: 0.98 +... \ No newline at end of file diff --git a/main.cpp b/main.cpp index 012f2e6..8228deb 100644 --- a/main.cpp +++ b/main.cpp @@ -42,7 +42,7 @@ void print_info(boost::spirit::info const& what) { boost::apply_visitor(walker, what.value); } -void setProbability(const std::string& gridProperties, const std::vector configProperties, const std::string& identifier, float& prop) { +void setProbability(const std::string& gridProperties, const std::vector configProperties, const std::string& identifier, float& prop) { auto start_pos = gridProperties.find(identifier); std::string seperator = ";"; @@ -52,7 +52,7 @@ void setProbability(const std::string& gridProperties, const std::vector bool {return obj.probability_ == identifier;} ); + auto yaml_config_prop = std::find_if(configProperties.begin(), configProperties.end(), [&identifier](const Property& obj) -> bool {return obj.property == identifier;} ); if (yaml_config_prop != configProperties.end()) { prop = (*yaml_config_prop).value_; @@ -127,7 +127,7 @@ int main(int argc, char* argv[]) { cells contentCells; cells backgroundCells; std::vector configurations; - std::vector probabilities; + std::vector parsed_properties; std::map stateRewards; float faultyProbability = 0.0; float probIntended = 1.0; @@ -142,7 +142,7 @@ int main(int argc, char* argv[]) { YamlConfigParser parser(configFilename->value(0)); auto parseResult = parser.parseConfiguration(); configurations = parseResult.configurations_; - probabilities = parseResult.probabilities_; + parsed_properties = parseResult.properties_; } boost::escaped_list_separator seps('\\', ';', '\n'); @@ -158,13 +158,27 @@ int main(int argc, char* argv[]) { auto probForwardIntendedIdentifier = std::string("ProbForwardIntended"); auto probTurnIntendedIdentifier = std::string("ProbTurnIntended"); - setProbability(properties, probabilities, faultProbabilityIdentifier, faultyProbability); - setProbability(properties, probabilities, probForwardIntendedIdentifier, probIntended); - setProbability(properties, probabilities, probTurnIntendedIdentifier, probTurnIntended); + setProbability(properties, parsed_properties, faultProbabilityIdentifier, faultyProbability); + setProbability(properties, parsed_properties, probForwardIntendedIdentifier, probIntended); + setProbability(properties, parsed_properties, probTurnIntendedIdentifier, probTurnIntended); } if(ok) { Grid grid(contentCells, backgroundCells, stateRewards, probIntended, faultyProbability); + auto modelTypeIter = std::find_if(parsed_properties.begin(), parsed_properties.end(), [](const Property& obj) -> bool {return obj.property == "modeltype";}); + prism::ModelType modelType = prism::ModelType::MDP;; + if (modelTypeIter != parsed_properties.end()) { + if ((*modelTypeIter).value_str_ == "smg") { + modelType = prism::ModelType::SMG; + } else { + modelType = prism::ModelType::MDP; + } + + grid.setModelType(modelType); + } + + + //grid.printToPrism(std::cout, configurations); std::stringstream ss; grid.printToPrism(ss, configurations); @@ -177,7 +191,7 @@ int main(int argc, char* argv[]) { std::cout << "got: \"" << std::string(e.first, e.last) << '"' << std::endl; std::cout << "Expectation failure: " << e.what() << " at '" << std::string(e.first,e.last) << "'\n"; } catch(const std::exception& e) { - std::cerr << "Exception '" << typeid(e).name() << "' caught:" << std::endl; + std::cerr << "Exception '" << typeid(e).name() << "' caught:" << e.what() << std::endl; std::cerr << "\t" << e.what() << std::endl; std::exit(EXIT_FAILURE); } diff --git a/util/ConfigYaml.cpp b/util/ConfigYaml.cpp index ecb5337..986d19e 100644 --- a/util/ConfigYaml.cpp +++ b/util/ConfigYaml.cpp @@ -47,10 +47,10 @@ std::string Formula::createExpression() const { std::string Command::createExpression() const { if (overwrite_) { - return action_ + "\t" + guard_ + "-> " + update_ + Configuration::overwrite_identifier_; + return action_ + "\t" + guard_ + " -> " + update_ + Configuration::overwrite_identifier_; } - return "\t" + action_ + "\t" + guard_ + "-> " + update_+ Configuration::configuration_identifier_; + return "\t" + action_ + "\t" + guard_ + " -> " + update_+ Configuration::configuration_identifier_; } std::string Constant::createExpression() const { @@ -74,8 +74,20 @@ bool YAML::convert::decode(const YAML::Node& node, Module& rhs) { if (!node.Type() == NodeType::Map) { return false; } - rhs.commands_ = node["commands"].as>(); + + rhs.module_ = node["module"].as(); + + if (node["commands"]) { + rhs.commands_ = node["commands"].as>(); + } + + if (node["module_text"]) { + rhs.module_text_ = node["module_text"].as(); + } + if (node["overwrite"]) { + rhs.overwrite_module = node["overwrite"].as(); + } return true; } @@ -96,8 +108,13 @@ bool YAML::convert::decode(const YAML::Node& node, Command& rhs) { } rhs.action_ = node["action"].as(); - rhs.guard_ = node["guard"].as(); - rhs.update_ = node["update"].as(); + if (node["guard"]) { + rhs.guard_ = node["guard"].as(); + } + + if (node["update"]) { + rhs.update_ = node["update"].as(); + } if (node["overwrite"]) { rhs.overwrite_ = node["overwrite"].as(); @@ -190,22 +207,27 @@ bool YAML::convert::decode(const YAML::Node& node, Constant& rhs) { return true; } -YAML::Node YAML::convert::encode(const Probability& rhs) { +YAML::Node YAML::convert::encode(const Property& rhs) { YAML::Node node; - node.push_back(rhs.probability_); + node.push_back(rhs.property); node.push_back(rhs.value_); return node; } -bool YAML::convert::decode(const YAML::Node& node, Probability& rhs) { - if (!node.IsDefined() || !node["probability"] || !node["value"]) { +bool YAML::convert::decode(const YAML::Node& node, Property& rhs) { + if (!node.IsDefined() || !node["property"] || !node["value"]) { return false; } - rhs.probability_ = node["probability"].as(); - rhs.value_ = node["value"].as(); + rhs.property = node["property"].as(); + try { + rhs.value_ = node["value"].as(); + } + catch(const std::exception& e) { + rhs.value_str_ = node["value"].as(); + } return true; } @@ -215,7 +237,7 @@ const std::string Configuration::overwrite_identifier_{"; // Overwritten through YamlConfigParseResult YamlConfigParser::parseConfiguration() { std::vector configuration; - std::vector probabilities; + std::vector properties; try { YAML::Node config = YAML::LoadFile(file_); @@ -238,8 +260,8 @@ YamlConfigParseResult YamlConfigParser::parseConfiguration() { constants = config["constants"].as>(); } - if (config["probabilities"]) { - probabilities = config["probabilities"].as>(); + if (config["properties"]) { + properties = config["properties"].as>(); } for (auto& label : labels) { @@ -249,8 +271,22 @@ YamlConfigParseResult YamlConfigParser::parseConfiguration() { configuration.push_back({formula.createExpression(), formula.formula_ ,ConfigType::Formula, formula.overwrite_}); } for (auto& module : modules) { + if (module.overwrite_module) { + Configuration config = Configuration(module.module_text_, "module " + module.module_ + "\n", ConfigType::Module, true, module.module_, {0}, "endmodule"); + configuration.push_back(config); + continue; + } for (auto& command : module.commands_) { - configuration.push_back({command.createExpression(), command.action_, ConfigType::Module, command.overwrite_, module.module_, command.indexes_}); + Configuration config; + if (!command.guard_.empty() && !command.action_.empty() && command.update_.empty()) { + config = Configuration(" " + command.guard_, command.action_, ConfigType::GuardOnly, true, module.module_, command.indexes_, "->"); + } else if (!command.update_.empty() && !command.action_.empty() && command.guard_.empty()) { + config = Configuration( " " + command.update_, command.action_, ConfigType::UpdateOnly, true, module.module_, command.indexes_, ";"); + } else { + config = Configuration(command.createExpression(), command.action_, ConfigType::Module, command.overwrite_, module.module_, command.indexes_); + } + + configuration.push_back(config); } } for (auto& constant : constants) { @@ -264,5 +300,5 @@ YamlConfigParseResult YamlConfigParser::parseConfiguration() { std::cout << "while parsing configuration " << file_ << std::endl; } - return YamlConfigParseResult(configuration, probabilities); + return YamlConfigParseResult(configuration, properties); } \ No newline at end of file diff --git a/util/ConfigYaml.h b/util/ConfigYaml.h index 16b34b6..80fe5c1 100644 --- a/util/ConfigYaml.h +++ b/util/ConfigYaml.h @@ -11,6 +11,8 @@ enum class ConfigType : char { Label = 'L', Formula = 'F', Module = 'M', + UpdateOnly = 'U', + GuardOnly = 'G', Constant = 'C' }; @@ -22,6 +24,7 @@ struct Configuration std::string module_ {}; std::string expression_{}; std::string identifier_{}; + std::string end_identifier_{}; std::vector indexes_{0}; ConfigType type_ {ConfigType::Label}; @@ -33,7 +36,8 @@ struct Configuration , ConfigType type , bool overwrite = false , std::string module = "" - , std::vector indexes = {0}) : expression_(expression), identifier_(identifier), type_(type), overwrite_(overwrite), module_{module}, indexes_(indexes) {} + , std::vector indexes = {0} + , std::string end_identifier = {";"}) : expression_(expression), identifier_(identifier), type_(type), overwrite_(overwrite), module_{module}, indexes_(indexes), end_identifier_{end_identifier} {} ~Configuration() = default; Configuration(const Configuration&) = default; @@ -44,15 +48,16 @@ struct Configuration } }; -struct Probability { - Probability() = default; - Probability(const Probability&) = default; - ~Probability() = default; +struct Property { + Property() = default; + Property(const Property&) = default; + ~Property() = default; - std::string probability_; + std::string property; double value_; + std::string value_str_; - friend std::ostream& operator <<(std::ostream& os, const Probability& property); + friend std::ostream& operator <<(std::ostream& os, const Property& property); }; struct Constant { @@ -113,6 +118,8 @@ struct Module { std::vector commands_; std::string module_; + std::string module_text_; + bool overwrite_module{false}; friend std::ostream& operator << (std::ostream& os, const Module& module); }; @@ -150,20 +157,20 @@ struct YAML::convert { }; template<> -struct YAML::convert { - static YAML::Node encode(const Probability& rhs); - static bool decode(const YAML::Node& node, Probability& rhs); +struct YAML::convert { + static YAML::Node encode(const Property& rhs); + static bool decode(const YAML::Node& node, Property& rhs); }; struct YamlConfigParseResult { - YamlConfigParseResult(std::vector configurations, std::vector probabilities) - : configurations_(configurations), probabilities_(probabilities) {} + YamlConfigParseResult(std::vector configurations, std::vector probabilities) + : configurations_(configurations), properties_(probabilities) {} ~YamlConfigParseResult() = default; YamlConfigParseResult(const YamlConfigParseResult&) = default; std::vector configurations_; - std::vector probabilities_; + std::vector properties_; }; struct YamlConfigParser { diff --git a/util/Grid.cpp b/util/Grid.cpp index 8f83703..2e44298 100644 --- a/util/Grid.cpp +++ b/util/Grid.cpp @@ -15,6 +15,10 @@ Grid::Grid(cells gridCells, cells background, const std::map 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(background.begin(), background.end(), std::back_inserter(slipperyNorthWest), [](cell c) { return c.type == Type::SlipperyNorthWest; }); + std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyNorthEast), [](cell c) { return c.type == Type::SlipperyNorthEast; }); + std::copy_if(background.begin(), background.end(), std::back_inserter(slipperySouthWest), [](cell c) { return c.type == Type::SlipperySouthWest; }); + std::copy_if(background.begin(), background.end(), std::back_inserter(slipperySouthEast), [](cell c) { return c.type == Type::SlipperySouthEast; }); 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; }); @@ -61,8 +65,8 @@ Grid::Grid(cells gridCells, cells background, const std::map backgroundTiles.emplace(color, cellsOfColor); } } - - if(adversaries.empty()) { + + if (adversaries.empty()) { modelType = prism::ModelType::MDP; } else { modelType = prism::ModelType::SMG; @@ -111,14 +115,26 @@ void Grid::applyOverwrites(std::string& str, std::vector& configu search = "label " + config.identifier_; } else if (config.type_ == ConfigType::Module) { search = config.identifier_; + } else if (config.type_ == ConfigType::UpdateOnly) { + search = config.identifier_; + } else if (config.type_ == ConfigType::GuardOnly) { + search = config.identifier_; } else if (config.type_ == ConfigType::Constant) { search = config.identifier_; } auto iter = boost::find_nth(str, search, index); + auto end_identifier = config.end_identifier_; + start_pos = std::distance(str.begin(), iter.begin()); - size_t end_pos = str.find(';', start_pos) + 1; + size_t end_pos = str.find(end_identifier, start_pos); + + if (config.type_ == ConfigType::GuardOnly || config.type_ == ConfigType::Module) { + start_pos += search.length(); + } else if (config.type_ == ConfigType::UpdateOnly) { + start_pos = str.find("->", start_pos) + 2; + } if (end_pos != std::string::npos && end_pos != 0) { std::string expression = config.expression_; @@ -145,7 +161,7 @@ void Grid::printToPrism(std::ostream& os, std::vector& configurat std::map wallRestrictions = {{"North", northRestriction}, {"East", eastRestriction}, {"South", southRestriction}, {"West", westRestriction}}; - std::map slipperyTiles = {{"North", slipperyNorth}, {"East", slipperyEast}, {"South", slipperySouth}, {"West", slipperyWest}}; + std::map slipperyTiles = {{"North", slipperyNorth}, {"East", slipperyEast}, {"South", slipperySouth}, {"West", slipperyWest}, {"NorthWest", slipperyNorthWest}, {"NorthEast", slipperyNorthEast},{"SouthWest", slipperySouthWest},{"SouthEast", slipperySouthEast}}; std::vector agentNames; std::transform(agentNameAndPositionMap.begin(), @@ -177,3 +193,8 @@ void Grid::printToPrism(std::ostream& os, std::vector& configurat // modules.printConfiguration(os, configuration); //} } + +void Grid::setModelType(prism::ModelType type) +{ + modelType = type; +} \ No newline at end of file diff --git a/util/Grid.h b/util/Grid.h index da593ba..f741473 100644 --- a/util/Grid.h +++ b/util/Grid.h @@ -22,6 +22,8 @@ class Grid { void printToPrism(std::ostream &os, std::vector& configuration); void applyOverwrites(std::string& str, std::vector& configuration); + void setModelType(prism::ModelType type); + std::array getWalkableDirOf8Neighborhood(cell c); friend std::ostream& operator<<(std::ostream& os, const Grid &grid); @@ -44,6 +46,10 @@ class Grid { cells slipperyEast; cells slipperySouth; cells slipperyWest; + cells slipperyNorthWest; + cells slipperyNorthEast; + cells slipperySouthWest; + cells slipperySouthEast; cells lockedDoors; cells unlockedDoors; cells boxes; diff --git a/util/MinigridGrammar.h b/util/MinigridGrammar.h index e2cfddc..ea6c1cf 100644 --- a/util/MinigridGrammar.h +++ b/util/MinigridGrammar.h @@ -66,6 +66,10 @@ template ("e", Type::SlipperyEast) ("s", Type::SlipperySouth) ("w", Type::SlipperyWest) + ("a", Type::SlipperyNorthWest) + ("b", Type::SlipperyNorthEast) + ("c", Type::SlipperySouthWest) + ("d", Type::SlipperySouthEast) ("X", Type::Agent) ("Z", Type::Adversary); color_.add @@ -74,8 +78,9 @@ template ("B", Color::Blue) ("P", Color::Purple) ("Y", Color::Yellow) + ("W", Color::White) (" ", Color::None); - + cell_ = type_ > color_; row_ = (cell_ % -qi::char_("\n")); diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp index bbb9a0c..4115da2 100644 --- a/util/PrismFormulaPrinter.cpp +++ b/util/PrismFormulaPrinter.cpp @@ -4,6 +4,7 @@ #include #include + std::string oneOffToString(const int &offset) { return offset != 0 ? ( offset == 1 ? "+1" : "-1" ) : ""; } @@ -71,7 +72,10 @@ namespace prism { for(const auto& [direction, cells] : slipperyTiles) { printIsOnFormula(agentName, "Slippery", cells, direction); } - std::vector allSlipperyDirections = {agentName + "IsOnSlipperyNorth", agentName + "IsOnSlipperyEast", agentName + "IsOnSlipperySouth", agentName + "IsOnSlipperyWest"}; + std::vector allSlipperyDirections; + for(const auto &[slipperyType, _] : slipperyTiles) { + allSlipperyDirections.push_back(agentName + "IsOnSlippery" + slipperyType); + } os << buildFormula(agentName + "IsOnSlippery", vectorToDisjunction(allSlipperyDirections)); for(const auto& [direction, relativePosition] : getRelativeSurroundingCells()) { @@ -104,6 +108,8 @@ namespace prism { if(conditionalMovementRestrictions.size() > 0) { os << buildFormula(agentName + "CannotMoveConditionally", vectorToDisjunction(conditionalMovementRestrictions)); + } + if(portableObjects.size() > 0) { os << buildFormula(agentName + "IsCarrying", vectorToDisjunction(portableObjects)); } } @@ -158,20 +164,20 @@ namespace prism { } void PrismFormulaPrinter::printInitStruct() { - os << "init\n"; - bool first = true; - for(auto const [a, coordinates] : agentNameAndPositionMap) { - if(first) first = false; - else os << " & "; - os << "(col"+a+"="+std::to_string(coordinates.first)+"&row"+a+"="+std::to_string(coordinates.second)+" & "; - os << "(view"+a+"=0|view"+a+"=1|view"+a+"=2|view"+a+"=3) "; - if(faulty) os << " & previousAction"+a+"="+std::to_string(NOFAULT); - os << ")"; - } - for(auto const key : keys) { - std::string identifier = capitalize(key.getColor()) + key.getType(); - os << " & (col"+identifier+"="+std::to_string(key.column)+"&row"+identifier+"="+std::to_string(key.row)+"&"+identifier+"PickedUp=false) "; - } + os << "init\n true\n"; + //bool first = true; + //for(auto const [a, coordinates] : agentNameAndPositionMap) { + // if(first) first = false; + // else os << " & "; + // os << "(col"+a+"="+std::to_string(coordinates.first)+"&row"+a+"="+std::to_string(coordinates.second)+" & "; + // os << "(view"+a+"=0|view"+a+"=1|view"+a+"=2|view"+a+"=3) "; + // if(faulty) os << " & previousAction"+a+"="+std::to_string(NOFAULT); + // os << ")"; + //} + //for(auto const key : keys) { + // std::string identifier = capitalize(key.getColor()) + key.getType(); + // os << " & (col"+identifier+"="+std::to_string(key.column)+"&row"+identifier+"="+std::to_string(key.row)+"&"+identifier+"PickedUp=false) "; + //} os << "endinit\n\n"; } diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index 01c8431..fdd8df2 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -2,6 +2,7 @@ #include #include +#include std::string northUpdate(const AgentName &a) { return "(row"+a+"'=row"+a+"-1)"; } @@ -143,21 +144,21 @@ namespace prism { } void PrismModulesPrinter::printLockedDoorActions(const std::string &agentName, const std::string &identifier) { - std::string actionName = "[" + agentName + "_unlock_" + identifier + "]"; + std::string actionName = "[" + agentName + "_toggle_" + identifier + "]"; agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); os << " " << actionName << " !" << identifier << "Open -> (" << identifier << "Open'=true);\n"; - actionName = "[" + agentName + "_close_" + identifier + "]"; + actionName = "[" + agentName + "_toggle_" + identifier + "]"; agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); os << " " << actionName << " " << identifier << "Open -> (" << identifier << "Open'=false);\n"; } void PrismModulesPrinter::printUnlockedDoorActions(const std::string &agentName, const std::string &identifier) { - std::string actionName = "[" + agentName + "_open_" + identifier + "]"; + std::string actionName = "[" + agentName + "_toggle_" + identifier + "]"; agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); - os << " !" << identifier << "Open -> (" << identifier << "Open'=true);\n"; - actionName = "[" + agentName + "_close_" + identifier + "]"; + os << " " << actionName << " !" << identifier << "Open -> (" << identifier << "Open'=true);\n"; + actionName = "[" + agentName + "_toggle_" + identifier + "]"; agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); - os << " " << agentName << " " << identifier << "Open -> (" << identifier << "Open'=false);\n"; + os << " " << actionName << " " << identifier << "Open -> (" << identifier << "Open'=false);\n"; } void PrismModulesPrinter::printRobotModule(const AgentName &agentName, const coordinates &initialPosition) { @@ -187,13 +188,13 @@ namespace prism { printPortableObjectActionsForRobot(agentName, identifier); } - printNonMovementActionsForRobot(agentName); + //printNonMovementActionsForRobot(agentName); os << "\n" << actionStream.str(); actionStream.str(std::string()); - if(agentNameAndPositionMap.size() > 1 && agentName == "Agent") printDoneActions(agentName); + if(agentNameAndPositionMap.size() > 1 && agentName == "Agent" && anyGoals) printDoneActions(agentName); os << "endmodule\n\n"; } @@ -209,14 +210,14 @@ namespace prism { } void PrismModulesPrinter::printUnlockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier) { - actionStream << " [" << agentName << "_open_" << identifier << "] " << agentName << "CannotMove" << identifier << " -> true;\n"; - actionStream << " [" << agentName << "_close_" << identifier << "] " << agentName << "IsNextTo" << identifier << " -> true;\n"; + actionStream << " [" << agentName << "_toggle_" << identifier << "] " << agentName << "CannotMove" << identifier << " -> true;\n"; + actionStream << " [" << agentName << "_toggle_" << identifier << "] " << agentName << "IsNextTo" << identifier << " -> true;\n"; actionStream << "\n"; } void PrismModulesPrinter::printLockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier, const std::string &key) { - actionStream << " [" << agentName << "_unlock_" << identifier << "] " << agentName << "CannotMove" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n"; - actionStream << " [" << agentName << "_close_" << identifier << "] " << agentName << "IsNextTo" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n"; + actionStream << " [" << agentName << "_toggle_" << identifier << "] " << agentName << "CannotMove" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n"; + actionStream << " [" << agentName << "_toggle_" << identifier << "] " << agentName << "IsNextTo" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n"; actionStream << "\n"; } @@ -246,11 +247,11 @@ namespace prism { std::string actionName = "[" + a + "_move_" + direction + "]"; agentNameActionMap.at(a).insert({FORWARD, actionName}); std::string guard = " " + actionName + " " + viewVariable(a, viewDirection); - if(slipperyBehaviour()) guard += " & !" + a + "IsOnSlippery"; - if(anyLava) guard += " & !" + a + "IsOnLava"; - if(anyGoals) guard += " & !" + a + "IsOnGoal"; + if(slipperyBehaviour()) guard += " & !" + a + "IsOnSlippery"; + if(anyLava) guard += " & !" + a + "IsOnLava"; + if(anyGoals && a == "Agent") guard += " & !" + a + "IsOnGoal"; guard += " & !" + a + "CannotMove" + direction + "Wall"; - if(anyPortableObject()) guard += " & !" + a + "CannotMoveConditionally"; + if(anyPortableObject() || !lockedDoors.empty() || !unlockedDoors.empty()) guard += " & !" + a + "CannotMoveConditionally"; guard += " -> "; return guard; } @@ -298,6 +299,22 @@ namespace prism { printSlipperyMovementActionsForWest(a) ; printSlipperyTurnActionsForWest(a); } + if(!slipperyTiles.at("NorthWest").empty()) { + printSlipperyMovementActionsForNorthWest(a); + printSlipperyTurnActionsForNorthWest(a); + } + if(!slipperyTiles.at("NorthEast").empty()) { + printSlipperyMovementActionsForNorthEast(a); + printSlipperyTurnActionsForNorthEast(a); + } + if(!slipperyTiles.at("SouthWest").empty()) { + printSlipperyMovementActionsForSouthWest(a); + printSlipperyTurnActionsForSouthWest(a); + } + if(!slipperyTiles.at("SouthWest").empty()) { + printSlipperyMovementActionsForSouthWest(a); + printSlipperyTurnActionsForSouthWest(a); + } } void PrismModulesPrinter::printSlipperyMovementActionsForNorth(const AgentName &a) { @@ -397,44 +414,117 @@ namespace prism { } void PrismModulesPrinter::printSlipperyTurnActionsForNorth(const AgentName &a) { - actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!"+a+"CannotSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, northUpdate(a)} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { a+"CannotSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "right", "North", RIGHT, {"!"+a+"CannotSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "right", "North", RIGHT, { a+"CannotSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, northUpdate(a)} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, northUpdate(a)} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, {"!"+a+"CannotSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, {"!"+a+"CannotSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, northUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, { a+"CannotSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, { a+"CannotSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n"; } void PrismModulesPrinter::printSlipperyTurnActionsForEast(const AgentName &a) { - actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!"+a+"CannotSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, eastUpdate(a)} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { a+"CannotSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "right", "East", RIGHT, {"!"+a+"CannotSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, eastUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "right", "East", RIGHT, { a+"CannotSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, eastUpdate(a)} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, eastUpdate(a)} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, {"!"+a+"CannotSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, eastUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, {"!"+a+"CannotSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, eastUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, { a+"CannotSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, { a+"CannotSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n"; } void PrismModulesPrinter::printSlipperyTurnActionsForSouth(const AgentName &a) { - actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!"+a+"CannotSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, southUpdate(a)} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { a+"CannotSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "right", "South", RIGHT, {"!"+a+"CannotSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "right", "South", RIGHT, { a+"CannotSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, southUpdate(a)} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, southUpdate(a)} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, {"!"+a+"CannotSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, {"!"+a+"CannotSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, southUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, { a+"CannotSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, { a+"CannotSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n"; } void PrismModulesPrinter::printSlipperyTurnActionsForWest(const AgentName &a) { - actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!"+a+"CannotSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, westUpdate(a)} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { a+"CannotSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "right", "West", RIGHT, {"!"+a+"CannotSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "right", "West", RIGHT, { a+"CannotSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n"; + + actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, {"!"+a+"CannotSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, {"!"+a+"CannotSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, westUpdate(a)} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, { a+"CannotSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, { a+"CannotSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n"; + } + + void PrismModulesPrinter::printSlipperyMovementActionsForNorthWest(const AgentName &a) { throw std::logic_error("The logic for SlipperyNorthWest tiles is not yet implemented."); } + void PrismModulesPrinter::printSlipperyTurnActionsForNorthWest(const AgentName &a){ throw std::logic_error("The logic for SlipperyNorthWest tiles is not yet implemented."); } + + void PrismModulesPrinter::printSlipperyMovementActionsForNorthEast(const AgentName &a) { + actionStream << printSlipperyMovementGuard(a, "NorthEast", 0, {"!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "", {{probIntended, eastUpdate(a)}, {1-probIntended, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 0, {"!"+a+"CannotSlipNorthEast", a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "", {{1, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 0, { a+"CannotSlipNorthEast", "!"+a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "", {{1, eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 0, { a+"CannotSlipNorthEast", a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "", {{1, "true"}}) << ";\n"; + + actionStream << printSlipperyMovementGuard(a, "NorthEast", 3, {"!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "", {{probIntended, northUpdate(a)}, {1-probIntended, eastUpdate(a)+"&"+northUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 3, {"!"+a+"CannotSlipNorthEast", a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "", {{1, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 3, { a+"CannotSlipNorthEast", "!"+a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "", {{1, northUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 3, { a+"CannotSlipNorthEast", a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "", {{1, "true"}}) << ";\n"; + + + float pd3 = (1 - probIntended) / 3; + float pi3 = probIntended; + + float sum2 = probIntended + 2 * (1 - probIntended)/3; + float pd2 = (1 - probIntended) / sum2; + float pi2 = probIntended / sum2; + + float sum1 = probIntended + (1 - probIntended)/3; + float pd1 = (1 - probIntended) / sum1; + float pi1 = probIntended / sum1; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, {"!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{pi3, southUpdate(a)}, {pd3, northUpdate(a)+"&"+eastUpdate(a)}, {pd3, eastUpdate(a)}, {pd3, southUpdate(a)+"&"+eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, {"!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{1/3.f, northUpdate(a)+"&"+eastUpdate(a)}, {1/3.f, eastUpdate(a)}, {1/3.f, southUpdate(a)+"&"+eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, {"!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipEast", a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{pi1, southUpdate(a)}, {pd2, northUpdate(a)+"&"+eastUpdate(a)}, {pd2, eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, {"!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipEast", a+"CannotSlipSouthEast", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{1/2.f, northUpdate(a)+"&"+eastUpdate(a)}, {1/2.f, eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, {"!"+a+"CannotSlipNorthEast", a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{pi1, southUpdate(a)}, {pd2, northUpdate(a)+"&"+eastUpdate(a)}, {pd2, southUpdate(a)+"&"+eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, {"!"+a+"CannotSlipNorthEast", a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{1/2.f, northUpdate(a)+"&"+eastUpdate(a)}, {1/2.f, southUpdate(a)+"&"+eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, {"!"+a+"CannotSlipNorthEast", a+"CannotSlipEast", a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{pi1, southUpdate(a)}, {pd1, northUpdate(a)+"&"+eastUpdate(a) }}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, {"!"+a+"CannotSlipNorthEast", a+"CannotSlipEast", a+"CannotSlipSouthEast", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{1, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, { a+"CannotSlipNorthEast", "!"+a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{pi1, southUpdate(a)}, {pd2, eastUpdate(a)}, {pd2, southUpdate(a)+"&"+eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, { a+"CannotSlipNorthEast", "!"+a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{1/2.f, eastUpdate(a)}, {1/2.f, southUpdate(a)+"&"+eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, { a+"CannotSlipNorthEast", "!"+a+"CannotSlipEast", a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{pi1, southUpdate(a)}, {pd1, eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, { a+"CannotSlipNorthEast", "!"+a+"CannotSlipEast", a+"CannotSlipSouthEast", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{1, eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, { a+"CannotSlipNorthEast", a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{pi1, southUpdate(a)}, {pd1, southUpdate(a)+"&"+eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, { a+"CannotSlipNorthEast", a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{1, southUpdate(a)+"&"+eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, { a+"CannotSlipNorthEast", a+"CannotSlipEast", a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{1, southUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, { a+"CannotSlipNorthEast", a+"CannotSlipEast", a+"CannotSlipSouthEast", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{1, "true"}}) << ";\n"; + + actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipNorthWest", "!"+a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{pi3, westUpdate(a)}, {pd3, northUpdate(a)+"&"+westUpdate(a)}, {pd3, northUpdate(a)}, {pd3, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipNorthWest", "!"+a+"CannotSlipNorth", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{pi2, westUpdate(a)}, {pd2, northUpdate(a)+"&"+westUpdate(a)}, {pd2, northUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipNorthWest", a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{pi2, westUpdate(a)}, {pd2, northUpdate(a)+"&"+westUpdate(a)}, {pd2, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipNorthWest", a+"CannotSlipNorth", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{pi1, westUpdate(a)}, {pd1, northUpdate(a)+"&"+westUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipNorthWest", "!"+a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{pi2, westUpdate(a)}, {pd2, northUpdate(a)}, {pd2, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipNorthWest", "!"+a+"CannotSlipNorth", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{pi1, westUpdate(a)}, {pd1, northUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipNorthWest", a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{pi1, westUpdate(a)}, {pd1, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipNorthWest", a+"CannotSlipNorth", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{1, westUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipNorthWest", "!"+a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{1/3.f, northUpdate(a)+"&"+westUpdate(a)}, {1/3.f, northUpdate(a)}, {1/3.f, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipNorthWest", "!"+a+"CannotSlipNorth", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{1/2.f, northUpdate(a)+"&"+westUpdate(a)}, {1/2.f, northUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipNorthWest", a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{1/2.f, northUpdate(a)+"&"+westUpdate(a)}, {1/2.f, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipNorthWest", a+"CannotSlipNorth", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{1, northUpdate(a)+"&"+westUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, { a+"CannotSlipWest", a+"CannotSlipNorthWest", "!"+a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{1/2.f, northUpdate(a)}, {1/2.f, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, { a+"CannotSlipWest", a+"CannotSlipNorthWest", "!"+a+"CannotSlipNorth", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{1, northUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, { a+"CannotSlipWest", a+"CannotSlipNorthWest", a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{1, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, { a+"CannotSlipWest", a+"CannotSlipNorthWest", a+"CannotSlipNorth", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{1, "true"}}) << ";\n"; + } + + void PrismModulesPrinter::printSlipperyTurnActionsForNorthEast(const AgentName &a) { + actionStream << printSlipperyTurnGuard(a, "right", "NorthEast", RIGHT, {}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "NorthEast", LEFT, {}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n"; + actionStream << printSlipperyTurnGuard(a, "left", "NorthEast", LEFT, {}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n"; + + } + + void PrismModulesPrinter::printSlipperyMovementActionsForSouthWest(const AgentName &a){ throw std::logic_error("The logic for SlipperySouthWest tiles is not yet implemented."); } + void PrismModulesPrinter::printSlipperyTurnActionsForSouthWest(const AgentName &a){ throw std::logic_error("The logic for SlipperySouthWest tiles is not yet implemented."); } + void PrismModulesPrinter::printSlipperyMovementActionsForSouthEast(const AgentName &a){ throw std::logic_error("The logic for SlipperySouthEast tiles is not yet implemented."); } + void PrismModulesPrinter::printSlipperyTurnActionsForSouthEast(const AgentName &a){ throw std::logic_error("The logic for SlipperySouthEast tiles is not yet implemented."); } - actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, westUpdate(a)} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!"+a+"CannotSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, westUpdate(a)} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n"; - actionStream << printSlipperyTurnGuard(a, "left", LEFT, { a+"CannotSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n"; - } std::string PrismModulesPrinter::printSlipperyMovementGuard(const AgentName &a, const std::string &direction, const ViewDirection &viewDirection, const std::vector &guards) { std::string actionName = "[" + a + "_move_" + viewDirectionToString.at(viewDirection) + "]"; @@ -446,10 +536,10 @@ namespace prism { return updatesToString(u); } - std::string PrismModulesPrinter::printSlipperyTurnGuard(const AgentName &a, const std::string &direction, const ActionId &actionId, const std::vector &guards, const std::string &cond) { + std::string PrismModulesPrinter::printSlipperyTurnGuard(const AgentName &a, const std::string &direction, const std::string &tiltDirection, const ActionId &actionId, const std::vector &guards, const std::string &cond) { std::string actionName = "[" + a + "_turn_" + direction + "]"; agentNameActionMap.at(a).insert({actionId, actionName}); - return " " + actionName + " " + a + "IsOnSlippery & " + buildConjunction(a, guards) + " & " + cond + " -> "; + return " " + actionName + " " + a + "IsOnSlippery" + tiltDirection + " & " + buildConjunction(a, guards) + " & " + cond + " -> "; } std::string PrismModulesPrinter::printSlipperyTurnUpdate(const AgentName &a, const updates &u) { @@ -502,7 +592,7 @@ namespace prism { else os << ", "; os << actionName; } - if(agentName == "Agent") os << ", [Agent_on_goal]"; + if(agentName == "Agent" && anyGoals) os << ", [Agent_on_goal]"; os << "\nendplayer\n"; } diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h index 618833a..af7601b 100644 --- a/util/PrismModulesPrinter.h +++ b/util/PrismModulesPrinter.h @@ -48,6 +48,14 @@ namespace prism { void printSlipperyTurnActionsForEast(const AgentName &a); void printSlipperyTurnActionsForSouth(const AgentName &a); void printSlipperyTurnActionsForWest(const AgentName &a); + void printSlipperyMovementActionsForNorthWest(const AgentName &a); + void printSlipperyTurnActionsForNorthWest(const AgentName &a); + void printSlipperyMovementActionsForNorthEast(const AgentName &a); + void printSlipperyTurnActionsForNorthEast(const AgentName &a); + void printSlipperyMovementActionsForSouthWest(const AgentName &a); + void printSlipperyTurnActionsForSouthWest(const AgentName &a); + void printSlipperyMovementActionsForSouthEast(const AgentName &a); + void printSlipperyTurnActionsForSouthEast(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; @@ -55,7 +63,7 @@ namespace prism { std::string printTurnUpdate(const AgentName &a, const update &u, const ActionId &actionId) const; std::string printSlipperyMovementGuard(const AgentName &a, const std::string &direction, const ViewDirection &viewDirection, const std::vector &guards); 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 printSlipperyTurnGuard(const AgentName &a, const std::string &direction, const std::string &tiltDirection, 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); diff --git a/util/cell.h b/util/cell.h index ca71559..5e69e3b 100644 --- a/util/cell.h +++ b/util/cell.h @@ -23,7 +23,11 @@ enum class Type : char { SlipperyNorth = 'n', SlipperySouth = 's', SlipperyEast = 'e', - SlipperyWest = 'w' + SlipperyWest = 'w', + SlipperyNorthWest = 'a', + SlipperyNorthEast = 'b', + SlipperySouthWest = 'c', + SlipperySouthEast = 'd' }; enum class Color : char { Red = 'R', @@ -31,6 +35,7 @@ enum class Color : char { Blue = 'B', Purple = 'P', Yellow = 'Y', + White = 'W', //Grey = 'G', None = ' ' };