From df00224661842d46f43692679aa08ca238d38f12 Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Mon, 15 Jan 2024 22:42:10 +0100 Subject: [PATCH 01/19] basic overwrite guard and update --- main.cpp | 4 ++-- util/ConfigYaml.cpp | 36 +++++++++++++++++++++++++++++++----- util/ConfigYaml.h | 8 +++++++- 3 files changed, 40 insertions(+), 8 deletions(-) diff --git a/main.cpp b/main.cpp index 012f2e6..abc86a9 100644 --- a/main.cpp +++ b/main.cpp @@ -164,7 +164,7 @@ int main(int argc, char* argv[]) { } if(ok) { Grid grid(contentCells, backgroundCells, stateRewards, probIntended, faultyProbability); - + //grid.printToPrism(std::cout, configurations); std::stringstream ss; grid.printToPrism(ss, configurations); @@ -177,7 +177,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..1cfb6d2 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 { @@ -76,6 +76,13 @@ bool YAML::convert::decode(const YAML::Node& node, Module& rhs) { } rhs.commands_ = node["commands"].as>(); rhs.module_ = node["module"].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 +103,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(); @@ -249,8 +261,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_, 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::Module, true, module.module_, command.indexes_, "->", false); + } else if (!command.update_.empty() && !command.action_.empty() && command.guard_.empty()) { + config = Configuration( " " + command.update_, command.action_, ConfigType::Module, true, module.module_, command.indexes_, ";", false); + } else { + config = Configuration(command.createExpression(), command.action_, ConfigType::Module, command.overwrite_, module.module_, command.indexes_); + } + + configuration.push_back(config); } } for (auto& constant : constants) { diff --git a/util/ConfigYaml.h b/util/ConfigYaml.h index 16b34b6..53eafea 100644 --- a/util/ConfigYaml.h +++ b/util/ConfigYaml.h @@ -22,10 +22,12 @@ struct Configuration std::string module_ {}; std::string expression_{}; std::string identifier_{}; + std::string end_identifier_{}; std::vector indexes_{0}; ConfigType type_ {ConfigType::Label}; bool overwrite_ {false}; + bool include_identifier_for_overwrite_{true}; Configuration() = default; Configuration(std::string expression @@ -33,7 +35,9 @@ 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 = {";"} + , bool include_identifier_for_overwrite = true) : expression_(expression), identifier_(identifier), type_(type), overwrite_(overwrite), module_{module}, indexes_(indexes), end_identifier_{end_identifier}, include_identifier_for_overwrite_{include_identifier_for_overwrite} {} ~Configuration() = default; Configuration(const Configuration&) = default; @@ -113,6 +117,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); }; -- 2.20.1 From 88f5e2e4fd9a05c08b48c74d5bcafcdc52b306ee Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Mon, 15 Jan 2024 23:39:07 +0100 Subject: [PATCH 02/19] more overwrites --- main.cpp | 28 ++++++++++++++++++++-------- util/ConfigYaml.cpp | 31 ++++++++++++++++++------------- util/ConfigYaml.h | 31 ++++++++++++++++--------------- util/Grid.cpp | 19 ++++++++++++++++--- util/Grid.h | 2 +- 5 files changed, 71 insertions(+), 40 deletions(-) diff --git a/main.cpp b/main.cpp index abc86a9..1a74df5 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,25 @@ 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 grid(contentCells, backgroundCells, stateRewards, probIntended, faultyProbability, modelType); + + + //grid.printToPrism(std::cout, configurations); std::stringstream ss; grid.printToPrism(ss, configurations); diff --git a/util/ConfigYaml.cpp b/util/ConfigYaml.cpp index 1cfb6d2..b558d32 100644 --- a/util/ConfigYaml.cpp +++ b/util/ConfigYaml.cpp @@ -202,22 +202,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; } @@ -227,7 +232,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_); @@ -250,8 +255,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) { @@ -262,16 +267,16 @@ YamlConfigParseResult YamlConfigParser::parseConfiguration() { } for (auto& module : modules) { if (module.overwrite_module) { - Configuration config = Configuration(module.module_text_, module.module_, ConfigType::Module, true, module.module_, {0}, "endmodule"); + Configuration config = Configuration("module " + module.module_text_, "module " + module.module_, ConfigType::Module, true, module.module_, {0}, "endmodule"); configuration.push_back(config); continue; } for (auto& command : module.commands_) { Configuration config; if (!command.guard_.empty() && !command.action_.empty() && command.update_.empty()) { - config = Configuration(" " + command.guard_, command.action_, ConfigType::Module, true, module.module_, command.indexes_, "->", false); + 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::Module, true, module.module_, command.indexes_, ";", false); + 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_); } @@ -290,5 +295,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 53eafea..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' }; @@ -27,7 +29,6 @@ struct Configuration ConfigType type_ {ConfigType::Label}; bool overwrite_ {false}; - bool include_identifier_for_overwrite_{true}; Configuration() = default; Configuration(std::string expression @@ -36,8 +37,7 @@ struct Configuration , bool overwrite = false , std::string module = "" , std::vector indexes = {0} - , std::string end_identifier = {";"} - , bool include_identifier_for_overwrite = true) : expression_(expression), identifier_(identifier), type_(type), overwrite_(overwrite), module_{module}, indexes_(indexes), end_identifier_{end_identifier}, include_identifier_for_overwrite_{include_identifier_for_overwrite} {} + , 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; @@ -48,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 { @@ -156,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..8ecfa44 100644 --- a/util/Grid.cpp +++ b/util/Grid.cpp @@ -3,7 +3,7 @@ #include -Grid::Grid(cells gridCells, cells background, const std::map &stateRewards, const float probIntended, const float faultyProbability) +Grid::Grid(cells gridCells, cells background, const std::map &stateRewards, const float probIntended, const float faultyProbability, prism::ModelType mType) : allGridCells(gridCells), background(background), stateRewards(stateRewards), probIntended(probIntended), faultyProbability(faultyProbability) { cell max = allGridCells.at(allGridCells.size() - 1); @@ -62,7 +62,9 @@ Grid::Grid(cells gridCells, cells background, const std::map } } - if(adversaries.empty()) { + if(mType != prism::ModelType::MDP) { + modelType = mType; + } else if (adversaries.empty()) { modelType = prism::ModelType::MDP; } else { modelType = prism::ModelType::SMG; @@ -111,14 +113,25 @@ 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::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) { + 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_; diff --git a/util/Grid.h b/util/Grid.h index da593ba..5c2f4d9 100644 --- a/util/Grid.h +++ b/util/Grid.h @@ -13,7 +13,7 @@ class Grid { public: - Grid(cells gridCells, cells background, const std::map &stateRewards = {}, const float probIntended = 1.0, const float faultyProbability = 0); + Grid(cells gridCells, cells background, const std::map &stateRewards = {}, const float probIntended = 1.0, const float faultyProbability = 0, prism::ModelType mType = prism::ModelType::MDP); cells getGridCells(); -- 2.20.1 From 8599aab51557b2bd47914ad1982b1f3a4c3cc77c Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Mon, 15 Jan 2024 23:40:26 +0100 Subject: [PATCH 03/19] exampleconfig --- exampleConfig.yaml | 30 ++++++++++++++++++++---------- 1 file changed, 20 insertions(+), 10 deletions(-) diff --git a/exampleConfig.yaml b/exampleConfig.yaml index 8c3042b..9aafeb0 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,33 @@ 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\n\ + # " 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 -- 2.20.1 From aec701a72ee6522164381bf55f3f9d80205db29d Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Tue, 16 Jan 2024 09:17:34 +0100 Subject: [PATCH 04/19] changed example for module overwrite --- exampleConfig.yaml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/exampleConfig.yaml b/exampleConfig.yaml index 9aafeb0..0c81f90 100644 --- a/exampleConfig.yaml +++ b/exampleConfig.yaml @@ -24,8 +24,9 @@ properties: modules: - module: "Agent" # overwrite: True - # module_text: "NewModule\n\ - # " + # module_text: | + # NewModule + # True commands: - action: "[Agent_turn_left]" guard: "viewAgent=3" -- 2.20.1 From 073e1b28e5062a99bf906a9f424be0617c08e240 Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Tue, 16 Jan 2024 22:01:09 +0100 Subject: [PATCH 05/19] fixed guard overwrite --- util/Grid.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/util/Grid.cpp b/util/Grid.cpp index 8ecfa44..012b905 100644 --- a/util/Grid.cpp +++ b/util/Grid.cpp @@ -115,6 +115,8 @@ void Grid::applyOverwrites(std::string& str, std::vector& configu 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_; @@ -128,7 +130,7 @@ void Grid::applyOverwrites(std::string& str, std::vector& configu if (config.type_ == ConfigType::GuardOnly) { - start_pos += search.length(); + start_pos += search.length(); } else if (config.type_ == ConfigType::UpdateOnly) { start_pos = str.find("->", start_pos) + 2; } -- 2.20.1 From d964f557cc483183319b3b632a2db030fa7ec33b Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Tue, 16 Jan 2024 22:06:32 +0100 Subject: [PATCH 06/19] added example guards and formula --- examples/example_guards.prism | 23 +++++++++++++++++++++++ examples/example_guards.txt | 17 +++++++++++++++++ examples/example_guards.yaml | 19 +++++++++++++++++++ 3 files changed, 59 insertions(+) create mode 100644 examples/example_guards.prism create mode 100644 examples/example_guards.txt create mode 100644 examples/example_guards.yaml 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 -- 2.20.1 From 063cf9c0ee2f229672b6db82fe00235c66c6479e Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Tue, 16 Jan 2024 22:30:06 +0100 Subject: [PATCH 07/19] added example probabilities --- examples/example_probabilities.txt | 13 +++++++++++++ examples/example_probabilities.yaml | 5 +++++ 2 files changed, 18 insertions(+) create mode 100644 examples/example_probabilities.txt create mode 100644 examples/example_probabilities.yaml 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 -- 2.20.1 From acf32fbb98c9ccae82c132bd4f915810fdc5bc45 Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Thu, 18 Jan 2024 21:16:31 +0100 Subject: [PATCH 08/19] added example for module --- examples/example_module.txt | 17 +++++++++++++++++ examples/example_module.yaml | 36 ++++++++++++++++++++++++++++++++++++ main.cpp | 6 ++++-- util/ConfigYaml.cpp | 9 +++++++-- util/Grid.cpp | 16 +++++++++------- util/Grid.h | 4 +++- 6 files changed, 76 insertions(+), 12 deletions(-) create mode 100644 examples/example_module.txt create mode 100644 examples/example_module.yaml 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/main.cpp b/main.cpp index 1a74df5..8228deb 100644 --- a/main.cpp +++ b/main.cpp @@ -163,6 +163,8 @@ int main(int argc, char* argv[]) { 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()) { @@ -171,9 +173,9 @@ int main(int argc, char* argv[]) { } else { modelType = prism::ModelType::MDP; } + + grid.setModelType(modelType); } - Grid grid(contentCells, backgroundCells, stateRewards, probIntended, faultyProbability, modelType); - diff --git a/util/ConfigYaml.cpp b/util/ConfigYaml.cpp index b558d32..986d19e 100644 --- a/util/ConfigYaml.cpp +++ b/util/ConfigYaml.cpp @@ -74,8 +74,13 @@ 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(); @@ -267,7 +272,7 @@ YamlConfigParseResult YamlConfigParser::parseConfiguration() { } for (auto& module : modules) { if (module.overwrite_module) { - Configuration config = Configuration("module " + module.module_text_, "module " + module.module_, ConfigType::Module, true, module.module_, {0}, "endmodule"); + Configuration config = Configuration(module.module_text_, "module " + module.module_ + "\n", ConfigType::Module, true, module.module_, {0}, "endmodule"); configuration.push_back(config); continue; } diff --git a/util/Grid.cpp b/util/Grid.cpp index 012b905..2f294c4 100644 --- a/util/Grid.cpp +++ b/util/Grid.cpp @@ -3,7 +3,7 @@ #include -Grid::Grid(cells gridCells, cells background, const std::map &stateRewards, const float probIntended, const float faultyProbability, prism::ModelType mType) +Grid::Grid(cells gridCells, cells background, const std::map &stateRewards, const float probIntended, const float faultyProbability) : allGridCells(gridCells), background(background), stateRewards(stateRewards), probIntended(probIntended), faultyProbability(faultyProbability) { cell max = allGridCells.at(allGridCells.size() - 1); @@ -61,10 +61,8 @@ Grid::Grid(cells gridCells, cells background, const std::map backgroundTiles.emplace(color, cellsOfColor); } } - - if(mType != prism::ModelType::MDP) { - modelType = mType; - } else if (adversaries.empty()) { + + if (adversaries.empty()) { modelType = prism::ModelType::MDP; } else { modelType = prism::ModelType::SMG; @@ -128,8 +126,7 @@ void Grid::applyOverwrites(std::string& str, std::vector& configu start_pos = std::distance(str.begin(), iter.begin()); size_t end_pos = str.find(end_identifier, start_pos); - - if (config.type_ == ConfigType::GuardOnly) { + 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; @@ -192,3 +189,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 5c2f4d9..3d7f23d 100644 --- a/util/Grid.h +++ b/util/Grid.h @@ -13,7 +13,7 @@ class Grid { public: - Grid(cells gridCells, cells background, const std::map &stateRewards = {}, const float probIntended = 1.0, const float faultyProbability = 0, prism::ModelType mType = prism::ModelType::MDP); + Grid(cells gridCells, cells background, const std::map &stateRewards = {}, const float probIntended = 1.0, const float faultyProbability = 0); cells getGridCells(); @@ -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); -- 2.20.1 From 0ef98bf005febcb2df6f93b28db25fbd074b7105 Mon Sep 17 00:00:00 2001 From: sp Date: Sat, 20 Jan 2024 17:02:27 +0100 Subject: [PATCH 09/19] guard for IsCarrying formulae --- util/PrismFormulaPrinter.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp index bbb9a0c..df284f4 100644 --- a/util/PrismFormulaPrinter.cpp +++ b/util/PrismFormulaPrinter.cpp @@ -104,6 +104,8 @@ namespace prism { if(conditionalMovementRestrictions.size() > 0) { os << buildFormula(agentName + "CannotMoveConditionally", vectorToDisjunction(conditionalMovementRestrictions)); + } + if(portableObjects.size() > 0) { os << buildFormula(agentName + "IsCarrying", vectorToDisjunction(portableObjects)); } } -- 2.20.1 From 3949611e83601d970a4d4f356dddef71311d9aa0 Mon Sep 17 00:00:00 2001 From: sp Date: Sat, 20 Jan 2024 17:11:27 +0100 Subject: [PATCH 10/19] change door interaction labels to '_toggle_' --- util/PrismModulesPrinter.cpp | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index 01c8431..eecd919 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -143,21 +143,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) { @@ -209,14 +209,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"; } -- 2.20.1 From 801dc5b210f1a61e3f0b1a9c201b3833cefc9262 Mon Sep 17 00:00:00 2001 From: sp Date: Sat, 20 Jan 2024 17:19:39 +0100 Subject: [PATCH 11/19] only print goal related actions if there is one --- util/PrismModulesPrinter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index eecd919..49d0425 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -193,7 +193,7 @@ namespace prism { 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"; } @@ -502,7 +502,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"; } -- 2.20.1 From 83560bfc731796d5a22c1d4368ed7adeac2a7f3b Mon Sep 17 00:00:00 2001 From: sp Date: Wed, 24 Jan 2024 15:18:57 +0100 Subject: [PATCH 12/19] fixed conditional movement w.r.t doors --- util/PrismModulesPrinter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index 49d0425..fdbcd5c 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -250,7 +250,7 @@ namespace prism { if(anyLava) guard += " & !" + a + "IsOnLava"; if(anyGoals) 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; } -- 2.20.1 From a459232e5923102eae78fcfec7e84ff0fb0504ac Mon Sep 17 00:00:00 2001 From: sp Date: Wed, 24 Jan 2024 15:19:11 +0100 Subject: [PATCH 13/19] temporarily made all states init --- util/PrismFormulaPrinter.cpp | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp index df284f4..db44454 100644 --- a/util/PrismFormulaPrinter.cpp +++ b/util/PrismFormulaPrinter.cpp @@ -160,20 +160,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"; } -- 2.20.1 From 2e51e51320b3a15eafbb9e86cd4ea409fd4db34d Mon Sep 17 00:00:00 2001 From: sp Date: Fri, 9 Feb 2024 22:23:19 +0100 Subject: [PATCH 14/19] introduced new slippery tiles --- util/Grid.cpp | 6 +++++- util/Grid.h | 4 ++++ util/MinigridGrammar.h | 7 ++++++- util/cell.h | 7 ++++++- 4 files changed, 21 insertions(+), 3 deletions(-) diff --git a/util/Grid.cpp b/util/Grid.cpp index 2f294c4..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; }); @@ -157,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(), diff --git a/util/Grid.h b/util/Grid.h index 3d7f23d..f741473 100644 --- a/util/Grid.h +++ b/util/Grid.h @@ -46,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/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 = ' ' }; -- 2.20.1 From 44caa12fe0fb7680e494d83cc8f959690662bde4 Mon Sep 17 00:00:00 2001 From: sp Date: Fri, 9 Feb 2024 22:23:36 +0100 Subject: [PATCH 15/19] added logic for new slippery tiles --- util/PrismFormulaPrinter.cpp | 6 +- util/PrismModulesPrinter.cpp | 137 ++++++++++++++++++++++++++++------- util/PrismModulesPrinter.h | 10 ++- 3 files changed, 124 insertions(+), 29 deletions(-) diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp index db44454..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()) { diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index fdbcd5c..85604d2 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)"; } @@ -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,110 @@ 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 pd2 = (1 - probIntended) / 2; + float pd1 = 1 - probIntended; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, {"!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{probIntended, 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, "", {{probIntended, 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, "", {{probIntended, 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, "", {{probIntended, 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, "", {{probIntended, 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, "", {{probIntended, 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, "", {{probIntended, 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, "", {{probIntended, 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, "", {{probIntended, 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, "", {{probIntended, 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, "", {{probIntended, westUpdate(a)}, {pd1, northUpdate(a)+"&"+westUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipNorthWest", "!"+a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{probIntended, 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, "", {{probIntended, westUpdate(a)}, {pd1, northUpdate(a)}}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipNorthWest", a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{probIntended, 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 +529,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) { 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); -- 2.20.1 From 122ba1c5f08195660644e901656188b6e8417915 Mon Sep 17 00:00:00 2001 From: sp Date: Sat, 10 Feb 2024 12:40:05 +0100 Subject: [PATCH 16/19] do not model idle states --- util/PrismModulesPrinter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index 85604d2..9593486 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -188,7 +188,7 @@ namespace prism { printPortableObjectActionsForRobot(agentName, identifier); } - printNonMovementActionsForRobot(agentName); + //printNonMovementActionsForRobot(agentName); os << "\n" << actionStream.str(); -- 2.20.1 From 3a34e0d065d586d972dcdb889c61ac2b007a6ec6 Mon Sep 17 00:00:00 2001 From: sp Date: Sat, 10 Feb 2024 13:08:33 +0100 Subject: [PATCH 17/19] properly calculate probabilites for new slippery tiles --- util/PrismModulesPrinter.cpp | 39 +++++++++++++++++++++--------------- 1 file changed, 23 insertions(+), 16 deletions(-) diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index 9593486..97cecdc 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -469,32 +469,39 @@ namespace prism { float pd3 = (1 - probIntended) / 3; - float pd2 = (1 - probIntended) / 2; - float pd1 = 1 - probIntended; - actionStream << printSlipperyMovementGuard(a, "NorthEast", 1, {"!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", {{probIntended, southUpdate(a)}, {pd3, northUpdate(a)+"&"+eastUpdate(a)}, {pd3, eastUpdate(a)}, {pd3, southUpdate(a)+"&"+eastUpdate(a)}}) << ";\n"; + 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, "", {{probIntended, 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, "", {{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, "", {{probIntended, 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, "", {{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, "", {{probIntended, southUpdate(a)}, {pd1, northUpdate(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, "", {{probIntended, 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, "", {{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, "", {{probIntended, southUpdate(a)}, {pd1, 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, "", {{probIntended, southUpdate(a)}, {pd1, southUpdate(a)+"&"+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, "", {{probIntended, 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, "", {{probIntended, 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, "", {{probIntended, 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, "", {{probIntended, westUpdate(a)}, {pd1, northUpdate(a)+"&"+westUpdate(a)}}) << ";\n"; - actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipNorthWest", "!"+a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{probIntended, 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, "", {{probIntended, westUpdate(a)}, {pd1, northUpdate(a)}}) << ";\n"; - actionStream << printSlipperyMovementGuard(a, "NorthEast", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipNorthWest", a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "", {{probIntended, westUpdate(a)}, {pd1, northUpdate(a)+"&"+eastUpdate(a)}}) << ";\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"; -- 2.20.1 From c11e85e191d4bebebc33064bf3c95d86d47d774b Mon Sep 17 00:00:00 2001 From: sp Date: Tue, 16 Jul 2024 15:54:10 +0200 Subject: [PATCH 18/19] adversaries are allowed to move on goal --- util/PrismModulesPrinter.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index 97cecdc..fdd8df2 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -247,9 +247,9 @@ 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() || !lockedDoors.empty() || !unlockedDoors.empty()) guard += " & !" + a + "CannotMoveConditionally"; guard += " -> "; -- 2.20.1 From b816a1badb7a48181cc66e9640369d541149fb1d Mon Sep 17 00:00:00 2001 From: sp Date: Mon, 12 Aug 2024 13:03:25 +0200 Subject: [PATCH 19/19] changed CMake to assume yaml cpp is installed --- CMakeLists.txt | 37 ++++++++++++++++++------------------- 1 file changed, 18 insertions(+), 19 deletions(-) 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) + -- 2.20.1