From df00224661842d46f43692679aa08ca238d38f12 Mon Sep 17 00:00:00 2001
From: Thomas Knoll <thomas.knoll@student.tugraz.at>
Date: Mon, 15 Jan 2024 22:42:10 +0100
Subject: [PATCH 01/22] 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<Module>::decode(const YAML::Node& node, Module& rhs) {
}
rhs.commands_ = node["commands"].as<std::vector<Command>>();
rhs.module_ = node["module"].as<std::string>();
+
+ if (node["module_text"]) {
+ rhs.module_text_ = node["module_text"].as<std::string>();
+ }
+ if (node["overwrite"]) {
+ rhs.overwrite_module = node["overwrite"].as<bool>();
+ }
return true;
}
@@ -96,8 +103,13 @@ bool YAML::convert<Command>::decode(const YAML::Node& node, Command& rhs) {
}
rhs.action_ = node["action"].as<std::string>();
- rhs.guard_ = node["guard"].as<std::string>();
- rhs.update_ = node["update"].as<std::string>();
+ if (node["guard"]) {
+ rhs.guard_ = node["guard"].as<std::string>();
+ }
+
+ if (node["update"]) {
+ rhs.update_ = node["update"].as<std::string>();
+ }
if (node["overwrite"]) {
rhs.overwrite_ = node["overwrite"].as<bool>();
@@ -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<int> 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<int> indexes = {0}) : expression_(expression), identifier_(identifier), type_(type), overwrite_(overwrite), module_{module}, indexes_(indexes) {}
+ , std::vector<int> 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<Command> 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 <thomas.knoll@student.tugraz.at>
Date: Mon, 15 Jan 2024 23:39:07 +0100
Subject: [PATCH 02/22] 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<Probability> configProperties, const std::string& identifier, float& prop) {
+void setProbability(const std::string& gridProperties, const std::vector<Property> 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<Probabi
prop = std::stod(value);
}
- auto yaml_config_prop = std::find_if(configProperties.begin(), configProperties.end(), [&identifier](const Probability& obj) -> 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<Configuration> configurations;
- std::vector<Probability> probabilities;
+ std::vector<Property> parsed_properties;
std::map<coordinates, float> 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<char> 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<Constant>::decode(const YAML::Node& node, Constant& rhs) {
return true;
}
-YAML::Node YAML::convert<Probability>::encode(const Probability& rhs) {
+YAML::Node YAML::convert<Property>::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<Probability>::decode(const YAML::Node& node, Probability& rhs) {
- if (!node.IsDefined() || !node["probability"] || !node["value"]) {
+bool YAML::convert<Property>::decode(const YAML::Node& node, Property& rhs) {
+ if (!node.IsDefined() || !node["property"] || !node["value"]) {
return false;
}
- rhs.probability_ = node["probability"].as<std::string>();
- rhs.value_ = node["value"].as<double>();
+ rhs.property = node["property"].as<std::string>();
+ try {
+ rhs.value_ = node["value"].as<double>();
+ }
+ catch(const std::exception& e) {
+ rhs.value_str_ = node["value"].as<std::string>();
+ }
return true;
}
@@ -227,7 +232,7 @@ const std::string Configuration::overwrite_identifier_{"; // Overwritten through
YamlConfigParseResult YamlConfigParser::parseConfiguration() {
std::vector<Configuration> configuration;
- std::vector<Probability> probabilities;
+ std::vector<Property> properties;
try {
YAML::Node config = YAML::LoadFile(file_);
@@ -250,8 +255,8 @@ YamlConfigParseResult YamlConfigParser::parseConfiguration() {
constants = config["constants"].as<std::vector<Constant>>();
}
- if (config["probabilities"]) {
- probabilities = config["probabilities"].as<std::vector<Probability>>();
+ if (config["properties"]) {
+ properties = config["properties"].as<std::vector<Property>>();
}
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<int> 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<Constant> {
};
template<>
-struct YAML::convert<Probability> {
- static YAML::Node encode(const Probability& rhs);
- static bool decode(const YAML::Node& node, Probability& rhs);
+struct YAML::convert<Property> {
+ static YAML::Node encode(const Property& rhs);
+ static bool decode(const YAML::Node& node, Property& rhs);
};
struct YamlConfigParseResult {
- YamlConfigParseResult(std::vector<Configuration> configurations, std::vector<Probability> probabilities)
- : configurations_(configurations), probabilities_(probabilities) {}
+ YamlConfigParseResult(std::vector<Configuration> configurations, std::vector<Property> probabilities)
+ : configurations_(configurations), properties_(probabilities) {}
~YamlConfigParseResult() = default;
YamlConfigParseResult(const YamlConfigParseResult&) = default;
std::vector<Configuration> configurations_;
- std::vector<Probability> probabilities_;
+ std::vector<Property> 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 <algorithm>
-Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float> &stateRewards, const float probIntended, const float faultyProbability)
+Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float> &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<coordinates, float>
}
}
- 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<Configuration>& 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<coordinates, float> &stateRewards = {}, const float probIntended = 1.0, const float faultyProbability = 0);
+ Grid(cells gridCells, cells background, const std::map<coordinates, float> &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 <thomas.knoll@student.tugraz.at>
Date: Mon, 15 Jan 2024 23:40:26 +0100
Subject: [PATCH 03/22] 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 <thomas.knoll@student.tugraz.at>
Date: Tue, 16 Jan 2024 09:17:34 +0100
Subject: [PATCH 04/22] 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 <thomas.knoll@student.tugraz.at>
Date: Tue, 16 Jan 2024 22:01:09 +0100
Subject: [PATCH 05/22] 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<Configuration>& 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<Configuration>& 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 <thomas.knoll@student.tugraz.at>
Date: Tue, 16 Jan 2024 22:06:32 +0100
Subject: [PATCH 06/22] 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 <thomas.knoll@student.tugraz.at>
Date: Tue, 16 Jan 2024 22:30:06 +0100
Subject: [PATCH 07/22] 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 <thomas.knoll@student.tugraz.at>
Date: Thu, 18 Jan 2024 21:16:31 +0100
Subject: [PATCH 08/22] 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<Module>::decode(const YAML::Node& node, Module& rhs) {
if (!node.Type() == NodeType::Map) {
return false;
}
- rhs.commands_ = node["commands"].as<std::vector<Command>>();
+
+
rhs.module_ = node["module"].as<std::string>();
+
+ if (node["commands"]) {
+ rhs.commands_ = node["commands"].as<std::vector<Command>>();
+ }
if (node["module_text"]) {
rhs.module_text_ = node["module_text"].as<std::string>();
@@ -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 <algorithm>
-Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float> &stateRewards, const float probIntended, const float faultyProbability, prism::ModelType mType)
+Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float> &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<coordinates, float>
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<Configuration>& 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<Configuration>& 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<coordinates, float> &stateRewards = {}, const float probIntended = 1.0, const float faultyProbability = 0, prism::ModelType mType = prism::ModelType::MDP);
+ Grid(cells gridCells, cells background, const std::map<coordinates, float> &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>& configuration);
void applyOverwrites(std::string& str, std::vector<Configuration>& configuration);
+ void setModelType(prism::ModelType type);
+
std::array<bool, 8> 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 <stefan.pranger@iaik.tugraz.at>
Date: Sat, 20 Jan 2024 17:02:27 +0100
Subject: [PATCH 09/22] 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 <stefan.pranger@iaik.tugraz.at>
Date: Sat, 20 Jan 2024 17:11:27 +0100
Subject: [PATCH 10/22] 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 <stefan.pranger@iaik.tugraz.at>
Date: Sat, 20 Jan 2024 17:19:39 +0100
Subject: [PATCH 11/22] 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 <stefan.pranger@iaik.tugraz.at>
Date: Wed, 24 Jan 2024 15:18:57 +0100
Subject: [PATCH 12/22] 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 <stefan.pranger@iaik.tugraz.at>
Date: Wed, 24 Jan 2024 15:19:11 +0100
Subject: [PATCH 13/22] 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 <stefan.pranger@iaik.tugraz.at>
Date: Fri, 9 Feb 2024 22:23:19 +0100
Subject: [PATCH 14/22] 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<coordinates, float>
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<Configuration>& configurat
std::map<std::string, cells> wallRestrictions = {{"North", northRestriction}, {"East", eastRestriction}, {"South", southRestriction}, {"West", westRestriction}};
- std::map<std::string, cells> slipperyTiles = {{"North", slipperyNorth}, {"East", slipperyEast}, {"South", slipperySouth}, {"West", slipperyWest}};
+ std::map<std::string, cells> slipperyTiles = {{"North", slipperyNorth}, {"East", slipperyEast}, {"South", slipperySouth}, {"West", slipperyWest}, {"NorthWest", slipperyNorthWest}, {"NorthEast", slipperyNorthEast},{"SouthWest", slipperySouthWest},{"SouthEast", slipperySouthEast}};
std::vector<AgentName> 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 <typename It>
("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 <typename It>
("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 <stefan.pranger@iaik.tugraz.at>
Date: Fri, 9 Feb 2024 22:23:36 +0100
Subject: [PATCH 15/22] 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 <string>
#include <algorithm>
+
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<std::string> allSlipperyDirections = {agentName + "IsOnSlipperyNorth", agentName + "IsOnSlipperyEast", agentName + "IsOnSlipperySouth", agentName + "IsOnSlipperyWest"};
+ std::vector<std::string> 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 <map>
#include <string>
+#include <stdexcept>
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<std::string> &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<std::string> &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<std::string> &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<std::string> &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<std::string> &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<std::string> &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 <stefan.pranger@iaik.tugraz.at>
Date: Sat, 10 Feb 2024 12:40:05 +0100
Subject: [PATCH 16/22] 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 <stefan.pranger@iaik.tugraz.at>
Date: Sat, 10 Feb 2024 13:08:33 +0100
Subject: [PATCH 17/22] 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 <stefan.pranger@iaik.tugraz.at>
Date: Tue, 16 Jul 2024 15:54:10 +0200
Subject: [PATCH 18/22] 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 <stefan.pranger@iaik.tugraz.at>
Date: Mon, 12 Aug 2024 13:03:25 +0200
Subject: [PATCH 19/22] 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
From 8c38856fafa8c5ab078cd7fec05ff8c9dd3e0f6b Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Sun, 16 Feb 2025 14:40:50 +0100
Subject: [PATCH 20/22] started to add non-directional slippery tiles
---
util/Grid.cpp | 8 +++++---
util/Grid.h | 1 +
util/MinigridGrammar.h | 1 +
util/PrismFormulaPrinter.cpp | 3 +--
util/cell.cpp | 9 +++++----
util/cell.h | 1 +
6 files changed, 14 insertions(+), 9 deletions(-)
diff --git a/util/Grid.cpp b/util/Grid.cpp
index 2e44298..c80570c 100644
--- a/util/Grid.cpp
+++ b/util/Grid.cpp
@@ -11,6 +11,7 @@ Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float>
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(walls), [](cell c) { return c.type == Type::Wall; });
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(lava), [](cell c) { return c.type == Type::Lava; });
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(floor), [](cell c) { return c.type == Type::Floor; }); // TODO CHECK IF ALL AGENTS ARE ADDED TO FLOOR
+ std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(slippery), [](cell c) { return c.type == Type::Slippery; });
std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyNorth), [](cell c) { return c.type == Type::SlipperyNorth; });
std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyEast), [](cell c) { return c.type == Type::SlipperyEast; });
std::copy_if(background.begin(), background.end(), std::back_inserter(slipperySouth), [](cell c) { return c.type == Type::SlipperySouth; });
@@ -26,6 +27,7 @@ Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float>
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(boxes), [](cell c) { return c.type == Type::Box; });
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(balls), [](cell c) { return c.type == Type::Ball; });
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(adversaries), [](cell c) { return c.type == Type::Adversary; });
+
agent = *std::find_if(gridCells.begin(), gridCells.end(), [](cell c) { return c.type == Type::Agent; });
floor.push_back(agent);
@@ -65,7 +67,7 @@ Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float>
backgroundTiles.emplace(color, cellsOfColor);
}
}
-
+
if (adversaries.empty()) {
modelType = prism::ModelType::MDP;
} else {
@@ -161,7 +163,7 @@ void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configurat
std::map<std::string, cells> wallRestrictions = {{"North", northRestriction}, {"East", eastRestriction}, {"South", southRestriction}, {"West", westRestriction}};
- std::map<std::string, cells> slipperyTiles = {{"North", slipperyNorth}, {"East", slipperyEast}, {"South", slipperySouth}, {"West", slipperyWest}, {"NorthWest", slipperyNorthWest}, {"NorthEast", slipperyNorthEast},{"SouthWest", slipperySouthWest},{"SouthEast", slipperySouthEast}};
+ std::map<std::string, cells> slipperyTiles = {{"Slippery", slippery}, {"North", slipperyNorth}, {"East", slipperyEast}, {"South", slipperySouth}, {"West", slipperyWest}, {"NorthWest", slipperyNorthWest}, {"NorthEast", slipperyNorthEast},{"SouthWest", slipperySouthWest},{"SouthEast", slipperySouthEast}};
std::vector<AgentName> agentNames;
std::transform(agentNameAndPositionMap.begin(),
@@ -197,4 +199,4 @@ void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configurat
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 f741473..74e4e9f 100644
--- a/util/Grid.h
+++ b/util/Grid.h
@@ -42,6 +42,7 @@ class Grid {
cells walls;
cells floor;
+ cells slippery;
cells slipperyNorth;
cells slipperyEast;
cells slipperySouth;
diff --git a/util/MinigridGrammar.h b/util/MinigridGrammar.h
index ea6c1cf..629f040 100644
--- a/util/MinigridGrammar.h
+++ b/util/MinigridGrammar.h
@@ -62,6 +62,7 @@ template <typename It>
("B", Type::Box)
("G", Type::Goal)
("V", Type::Lava)
+ ("S", Type::Slippery)
("n", Type::SlipperyNorth)
("e", Type::SlipperyEast)
("s", Type::SlipperySouth)
diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp
index 4115da2..ba214be 100644
--- a/util/PrismFormulaPrinter.cpp
+++ b/util/PrismFormulaPrinter.cpp
@@ -67,7 +67,6 @@ namespace prism {
for(const auto& [direction, cells] : restrictions) {
printRestrictionFormula(agentName, direction, cells);
}
-
if(slipperyBehaviour()) {
for(const auto& [direction, cells] : slipperyTiles) {
printIsOnFormula(agentName, "Slippery", cells, direction);
@@ -235,7 +234,7 @@ namespace prism {
}
bool PrismFormulaPrinter::slipperyBehaviour() const {
- return !slipperyTiles.at("North").empty() || !slipperyTiles.at("East").empty() || !slipperyTiles.at("South").empty() || !slipperyTiles.at("West").empty();
+ return !slipperyTiles.at("Slippery").empty() || !slipperyTiles.at("North").empty() || !slipperyTiles.at("East").empty() || !slipperyTiles.at("South").empty() || !slipperyTiles.at("West").empty();
}
bool PrismFormulaPrinter::anyPortableObject() const {
return !keys.empty();
diff --git a/util/cell.cpp b/util/cell.cpp
index c4812f9..40302c6 100644
--- a/util/cell.cpp
+++ b/util/cell.cpp
@@ -72,17 +72,18 @@ std::string cell::getColor() const {
std::string cell::getType() const {
switch(type) {
- case Type::Wall: return "Wall";
- case Type::Floor: return "Floor";
- case Type::Door: return "Door";
+ case Type::Wall: return "Wall";
+ case Type::Floor: return "Floor";
+ case Type::Door: return "Door";
case Type::LockedDoor: return "LockedDoor";
- case Type::Key: return "Key";
+ case Type::Key: return "Key";
case Type::Ball: return "Ball";
case Type::Box: return "Box";
case Type::Goal: return "Goal";
case Type::Lava: return "Lava";
case Type::Agent: return "Agent";
case Type::Adversary: return "Adversary";
+ case Type::Slippery: return "Slippery";
case Type::SlipperyNorth: return "SlipperyNorth";
case Type::SlipperySouth: return "SlipperySouth";
case Type::SlipperyEast: return "SlipperyEast";
diff --git a/util/cell.h b/util/cell.h
index 5e69e3b..329844e 100644
--- a/util/cell.h
+++ b/util/cell.h
@@ -20,6 +20,7 @@ enum class Type : char {
Lava = 'V',
Agent = 'X',
Adversary = 'Z',
+ Slippery = 'S',
SlipperyNorth = 'n',
SlipperySouth = 's',
SlipperyEast = 'e',
--
2.20.1
From 1d43c1d5064d0c4b5ba53ee5e6cf0414aa483b11 Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Tue, 29 Apr 2025 14:15:25 +0200
Subject: [PATCH 21/22] added slippery tiles and fixed faulty probability
passing
---
main.cpp | 5 +-
util/Grid.cpp | 8 +--
util/Grid.h | 3 +-
util/PrismModulesPrinter.cpp | 97 ++++++++++++++++++++++++++----------
util/PrismModulesPrinter.h | 5 +-
5 files changed, 85 insertions(+), 33 deletions(-)
diff --git a/main.cpp b/main.cpp
index 8228deb..fc78157 100644
--- a/main.cpp
+++ b/main.cpp
@@ -3,6 +3,7 @@
#include "util/Grid.h"
#include "util/ConfigYaml.h"
+#include <vector>
#include <iostream>
#include <fstream>
#include <filesystem>
@@ -163,7 +164,7 @@ int main(int argc, char* argv[]) {
setProbability(properties, parsed_properties, probTurnIntendedIdentifier, probTurnIntended);
}
if(ok) {
- Grid grid(contentCells, backgroundCells, stateRewards, probIntended, faultyProbability);
+ Grid grid(contentCells, backgroundCells, stateRewards, probIntended, probTurnIntended, faultyProbability);
auto modelTypeIter = std::find_if(parsed_properties.begin(), parsed_properties.end(), [](const Property& obj) -> bool {return obj.property == "modeltype";});
prism::ModelType modelType = prism::ModelType::MDP;;
@@ -176,7 +177,7 @@ int main(int argc, char* argv[]) {
grid.setModelType(modelType);
}
-
+
//grid.printToPrism(std::cout, configurations);
diff --git a/util/Grid.cpp b/util/Grid.cpp
index c80570c..d276c7b 100644
--- a/util/Grid.cpp
+++ b/util/Grid.cpp
@@ -3,15 +3,15 @@
#include <algorithm>
-Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float> &stateRewards, const float probIntended, const float faultyProbability)
- : allGridCells(gridCells), background(background), stateRewards(stateRewards), probIntended(probIntended), faultyProbability(faultyProbability)
+Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float> &stateRewards, const float probIntended, const float probTurnIntended, const float faultyProbability)
+ : allGridCells(gridCells), background(background), stateRewards(stateRewards), probIntended(probIntended), probTurnIntended(probTurnIntended), faultyProbability(faultyProbability)
{
cell max = allGridCells.at(allGridCells.size() - 1);
maxBoundaries = std::make_pair(max.column - 1, max.row - 1);
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(walls), [](cell c) { return c.type == Type::Wall; });
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(lava), [](cell c) { return c.type == Type::Lava; });
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(floor), [](cell c) { return c.type == Type::Floor; }); // TODO CHECK IF ALL AGENTS ARE ADDED TO FLOOR
- std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(slippery), [](cell c) { return c.type == Type::Slippery; });
+ std::copy_if(background.begin(), background.end(), std::back_inserter(slippery), [](cell c) { return c.type == Type::Slippery; });
std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyNorth), [](cell c) { return c.type == Type::SlipperyNorth; });
std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyEast), [](cell c) { return c.type == Type::SlipperyEast; });
std::copy_if(background.begin(), background.end(), std::back_inserter(slipperySouth), [](cell c) { return c.type == Type::SlipperySouth; });
@@ -173,7 +173,7 @@ void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configurat
std::string agentName = agentNames.at(0);
prism::PrismFormulaPrinter formulas(os, wallRestrictions, walls, lockedDoors, unlockedDoors, keys, slipperyTiles, lava, goals, agentNameAndPositionMap, faultyProbability > 0.0);
- prism::PrismModulesPrinter modules(os, modelType, maxBoundaries, lockedDoors, unlockedDoors, keys, slipperyTiles, agentNameAndPositionMap, configuration, probIntended, faultyProbability, !lava.empty(), !goals.empty());
+ prism::PrismModulesPrinter modules(os, modelType, maxBoundaries, lockedDoors, unlockedDoors, keys, slipperyTiles, agentNameAndPositionMap, configuration, probIntended, probTurnIntended, faultyProbability, !lava.empty(), !goals.empty());
modules.printModelType(modelType);
for(const auto &agentName : agentNames) {
diff --git a/util/Grid.h b/util/Grid.h
index 74e4e9f..298ec26 100644
--- a/util/Grid.h
+++ b/util/Grid.h
@@ -13,7 +13,7 @@
class Grid {
public:
- Grid(cells gridCells, cells background, const std::map<coordinates, float> &stateRewards = {}, const float probIntended = 1.0, const float faultyProbability = 0);
+ Grid(cells gridCells, cells background, const std::map<coordinates, float> &stateRewards = {}, const float probIntended = 1.0, const float probTurnIntended = 1.0, const float faultyProbability = 0);
cells getGridCells();
@@ -64,5 +64,6 @@ class Grid {
std::map<coordinates, float> stateRewards;
const float probIntended;
+ const float probTurnIntended;
const float faultyProbability;
};
diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp
index fdd8df2..a2855da 100644
--- a/util/PrismModulesPrinter.cpp
+++ b/util/PrismModulesPrinter.cpp
@@ -12,8 +12,8 @@ std::string westUpdate(const AgentName &a) { return "(col"+a+"'=col"+a+"-1)"; }
namespace prism {
- PrismModulesPrinter::PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector<Configuration> config, const float probIntended, const float faultyProbability, const bool anyLava, const bool anyGoals)
- : os(os), modelType(modelType), maxBoundaries(maxBoundaries), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), agentNameAndPositionMap(agentNameAndPositionMap), configuration(config), probIntended(probIntended), faultyProbability(faultyProbability), anyLava(anyLava), anyGoals(anyGoals) {
+ PrismModulesPrinter::PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector<Configuration> config, const float probIntended, const float probTurnIntended, const float faultyProbability, const bool anyLava, const bool anyGoals)
+ : os(os), modelType(modelType), maxBoundaries(maxBoundaries), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), agentNameAndPositionMap(agentNameAndPositionMap), configuration(config), probIntended(probIntended), probTurnIntended(probTurnIntended), faultyProbability(faultyProbability), anyLava(anyLava), anyGoals(anyGoals) {
numberOfPlayer = agentNameAndPositionMap.size();
size_t index = 0;
for(auto begin = agentNameAndPositionMap.begin(); begin != agentNameAndPositionMap.end(); begin++, index++) {
@@ -283,6 +283,10 @@ namespace prism {
}
void PrismModulesPrinter::printSlipperyMovementActionsForRobot(const AgentName &a) {
+ if(!slipperyTiles.at("Slippery").empty()) {
+ printSlipperyMovementActionsForSlippery(a);
+ printSlipperyTurnActionsForSlippery(a);
+ }
if(!slipperyTiles.at("North").empty()) {
printSlipperyMovementActionsForNorth(a);
printSlipperyTurnActionsForNorth(a);
@@ -316,10 +320,47 @@ namespace prism {
printSlipperyTurnActionsForSouthWest(a);
}
}
+ void PrismModulesPrinter::printSlipperyMovementActionsForSlippery(const AgentName &a) {
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 0, {"!"+a+"CannotSlipEast", "!"+a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {probIntended, eastUpdate(a)}, {(1 - probIntended) * 0.5, northUpdate(a)}, {(1 - probIntended) * 0.5, southUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 0, { a+"CannotSlipEast", "!"+a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {0.5 , northUpdate(a)}, {0.5 , southUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 0, {"!"+a+"CannotSlipEast", a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, eastUpdate(a)}, {(1 - probIntended) * 0.5, southUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 0, {"!"+a+"CannotSlipEast", "!"+a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, eastUpdate(a)}, {(1 - probIntended) * 0.5, northUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 0, { a+"CannotSlipEast", a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { { 1 , southUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 0, {"!"+a+"CannotSlipEast", a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {1 , eastUpdate(a)}, }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 0, { a+"CannotSlipEast", "!"+a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {1 , northUpdate(a)}, }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 0, { a+"CannotSlipEast", a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { }) << ";\n";
+
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 1, {"!"+a+"CannotSlipSouth", "!"+a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {probIntended, southUpdate(a)}, {(1 - probIntended) * 0.5, eastUpdate(a)}, {(1 - probIntended) * 0.5, westUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 1, { a+"CannotSlipSouth", "!"+a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {0.5 , eastUpdate(a)}, {0.5 , westUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 1, {"!"+a+"CannotSlipSouth", a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, southUpdate(a)}, {(1 - probIntended) * 0.5, westUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 1, {"!"+a+"CannotSlipSouth", "!"+a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, southUpdate(a)}, {(1 - probIntended) * 0.5, eastUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 1, { a+"CannotSlipSouth", a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { { 1 , westUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 1, {"!"+a+"CannotSlipSouth", a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {1 , southUpdate(a)}, }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 1, { a+"CannotSlipSouth", "!"+a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {1 , eastUpdate(a)}, }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 1, { a+"CannotSlipSouth", a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { }) << ";\n";
+
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {probIntended, westUpdate(a)}, {(1 - probIntended) * 0.5, northUpdate(a)}, {(1 - probIntended) * 0.5, southUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {0.5 , northUpdate(a)}, {0.5 , southUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, westUpdate(a)}, {(1 - probIntended) * 0.5, southUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, westUpdate(a)}, {(1 - probIntended) * 0.5, northUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 2, { a+"CannotSlipWest", a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { { 1 , southUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {1 , westUpdate(a)}, }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {1 , northUpdate(a)}, }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 2, { a+"CannotSlipWest", a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { }) << ";\n";
+
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 3, {"!"+a+"CannotSlipNorth", "!"+a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {probIntended, northUpdate(a)}, {(1 - probIntended) * 0.5, eastUpdate(a)}, {(1 - probIntended) * 0.5, westUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 3, { a+"CannotSlipNorth", "!"+a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {0.5 , eastUpdate(a)}, {0.5 , westUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 3, {"!"+a+"CannotSlipNorth", a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, northUpdate(a)}, {(1 - probIntended) * 0.5, westUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 3, {"!"+a+"CannotSlipNorth", "!"+a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, northUpdate(a)}, {(1 - probIntended) * 0.5, eastUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 3, { a+"CannotSlipNorth", a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { { 1 , westUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 3, {"!"+a+"CannotSlipNorth", a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {1 , northUpdate(a)}, }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 3, { a+"CannotSlipNorth", "!"+a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {1 , eastUpdate(a)}, }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "Slippery", 3, { a+"CannotSlipNorth", a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { }) << ";\n";
+ }
void PrismModulesPrinter::printSlipperyMovementActionsForNorth(const AgentName &a) {
- actionStream << printSlipperyMovementGuard(a, "North", 3, {"!"+a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, northUpdate(a)}, {(1 - probIntended) * 1/2, northUpdate(a)+"&"+eastUpdate(a)}, {(1 - probIntended) * 1/2, northUpdate(a)+"&"+westUpdate(a)} }) << ";\n";
- actionStream << printSlipperyMovementGuard(a, "North", 3, { a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1/2, northUpdate(a)+"&"+eastUpdate(a)}, {1/2, northUpdate(a)+"&"+westUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "North", 3, {"!"+a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, northUpdate(a)}, {(1 - probIntended) * 0.5, northUpdate(a)+"&"+eastUpdate(a)}, {(1 - probIntended) * 0.5, northUpdate(a)+"&"+westUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "North", 3, { a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {0.5, northUpdate(a)+"&"+eastUpdate(a)}, {0.5, northUpdate(a)+"&"+westUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "North", 3, {"!"+a+"CannotSlipNorth", a+"CannotSlipNorthEast", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, northUpdate(a)}, {(1 - probIntended), northUpdate(a)+"&"+westUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "North", 3, {"!"+a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast", a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, northUpdate(a)}, {(1 - probIntended), northUpdate(a)+"&"+eastUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "North", 3, { a+"CannotSlipNorth", a+"CannotSlipNorthEast", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1, northUpdate(a)+"&"+westUpdate(a) } }) << ";\n";
@@ -342,8 +383,8 @@ namespace prism {
}
void PrismModulesPrinter::printSlipperyMovementActionsForEast(const AgentName &a) {
- actionStream << printSlipperyMovementGuard(a, "East", 0, {"!"+a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a)}, {(1 - probIntended) * 1/2, eastUpdate(a)+"&"+southUpdate(a)}, {(1 - probIntended) * 1/2, eastUpdate(a)+"&"+northUpdate(a)} }) << ";\n";
- actionStream << printSlipperyMovementGuard(a, "East", 0, { a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1/2, eastUpdate(a)+"&"+southUpdate(a)}, {1/2, eastUpdate(a)+"&"+northUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "East", 0, {"!"+a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a)}, {(1 - probIntended) * 0.5, eastUpdate(a)+"&"+southUpdate(a)}, {(1 - probIntended) * 0.5, eastUpdate(a)+"&"+northUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "East", 0, { a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {0.5, eastUpdate(a)+"&"+southUpdate(a)}, {0.5, eastUpdate(a)+"&"+northUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "East", 0, {"!"+a+"CannotSlipEast", a+"CannotSlipSouthEast", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a)}, {(1 - probIntended), eastUpdate(a)+"&"+northUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "East", 0, {"!"+a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a)}, {(1 - probIntended), eastUpdate(a)+"&"+southUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "East", 0, { a+"CannotSlipEast", a+"CannotSlipSouthEast", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)+"&"+northUpdate(a) } }) << ";\n";
@@ -361,13 +402,13 @@ namespace prism {
actionStream << printSlipperyMovementGuard(a, "East", 1, {"!"+a+"CannotSlipSouth", a+"CannotSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, southUpdate(a) } }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "East", 1, { a+"CannotSlipSouth", a+"CannotSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", {}) << ";\n";
- actionStream << printSlipperyMovementGuard(a, "East", 2, {"!"+a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a) }, {1 - probIntended, "true"} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "East", 2, {"!"+a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, westUpdate(a) }, {1 - probIntended, "true"} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "East", 2, { a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {1, "true"} }) << ";\n";
}
void PrismModulesPrinter::printSlipperyMovementActionsForSouth(const AgentName &a) {
- actionStream << printSlipperyMovementGuard(a, "South", 1, {"!"+a+"CannotSlipSouth", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a)}, {(1 - probIntended) * 1/2, southUpdate(a)+"&"+eastUpdate(a)}, {(1 - probIntended) * 1/2, southUpdate(a)+"&"+westUpdate(a)} }) << ";\n";
- actionStream << printSlipperyMovementGuard(a, "South", 1, { a+"CannotSlipSouth", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1/2, southUpdate(a)+"&"+eastUpdate(a)}, {1/2, southUpdate(a)+"&"+westUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "South", 1, {"!"+a+"CannotSlipSouth", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a)}, {(1 - probIntended) * 0.5, southUpdate(a)+"&"+eastUpdate(a)}, {(1 - probIntended) * 0.5, southUpdate(a)+"&"+westUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "South", 1, { a+"CannotSlipSouth", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {0.5, southUpdate(a)+"&"+eastUpdate(a)}, {0.5, southUpdate(a)+"&"+westUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "South", 1, {"!"+a+"CannotSlipSouth", a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a)}, {(1 - probIntended), southUpdate(a)+"&"+westUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "South", 1, {"!"+a+"CannotSlipSouth", "!"+a+"CannotSlipSouthEast", a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a)}, {(1 - probIntended), southUpdate(a)+"&"+eastUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "South", 1, { a+"CannotSlipSouth", a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1, southUpdate(a)+"&"+westUpdate(a) } }) << ";\n";
@@ -390,8 +431,8 @@ namespace prism {
}
void PrismModulesPrinter::printSlipperyMovementActionsForWest(const AgentName &a) {
- actionStream << printSlipperyMovementGuard(a, "West", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipSouthWest", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a)}, {(1 - probIntended) * 1/2, westUpdate(a)+"&"+southUpdate(a)}, {(1 - probIntended) * 1/2, westUpdate(a)+"&"+northUpdate(a)} }) << ";\n";
- actionStream << printSlipperyMovementGuard(a, "West", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipSouthWest", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1/2, westUpdate(a)+"&"+southUpdate(a)}, {1/2, westUpdate(a)+"&"+northUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "West", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipSouthWest", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a)}, {(1 - probIntended) * 0.5, westUpdate(a)+"&"+southUpdate(a)}, {(1 - probIntended) * 0.5, westUpdate(a)+"&"+northUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "West", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipSouthWest", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {0.5, westUpdate(a)+"&"+southUpdate(a)}, {0.5, westUpdate(a)+"&"+northUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "West", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipSouthWest", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a)}, {(1 - probIntended), westUpdate(a)+"&"+northUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "West", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipSouthWest", a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a)}, {(1 - probIntended), westUpdate(a)+"&"+southUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "West", 2, { a+"CannotSlipWest", a+"CannotSlipSouthWest", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)+"&"+northUpdate(a) } }) << ";\n";
@@ -409,46 +450,52 @@ namespace prism {
actionStream << printSlipperyMovementGuard(a, "West", 1, {"!"+a+"CannotSlipSouth", a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, southUpdate(a) } }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "West", 1, { a+"CannotSlipSouth", a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", {}) << ";\n";
- actionStream << printSlipperyMovementGuard(a, "West", 0, {"!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a) }, {1 - probIntended, "true"} }) << ";\n";
+ actionStream << printSlipperyMovementGuard(a, "West", 0, {"!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, eastUpdate(a) }, {1 - probIntended, "true"} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "West", 0, { a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", {{1, "true"}}) << ";\n";
}
+ void PrismModulesPrinter::printSlipperyTurnActionsForSlippery(const AgentName &a) {
+ actionStream << printSlipperyTurnGuard(a, "right", "Slippery", RIGHT, {}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n";
+ actionStream << printSlipperyTurnGuard(a, "left", "Slippery", LEFT, {}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n";
+ actionStream << printSlipperyTurnGuard(a, "left", "Slippery", LEFT, {}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n";
+ }
+
void PrismModulesPrinter::printSlipperyTurnActionsForNorth(const AgentName &a) {
- actionStream << printSlipperyTurnGuard(a, "right", "North", RIGHT, {"!"+a+"CannotSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, northUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyTurnGuard(a, "right", "North", RIGHT, {"!"+a+"CannotSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probTurnIntended, northUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", "North", RIGHT, { a+"CannotSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n";
- actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, {"!"+a+"CannotSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, northUpdate(a)} }) << ";\n";
- actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, {"!"+a+"CannotSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, northUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, {"!"+a+"CannotSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probTurnIntended, northUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, {"!"+a+"CannotSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=3)"}, {1 - probTurnIntended, northUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, { a+"CannotSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, { a+"CannotSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n";
}
void PrismModulesPrinter::printSlipperyTurnActionsForEast(const AgentName &a) {
- actionStream << printSlipperyTurnGuard(a, "right", "East", RIGHT, {"!"+a+"CannotSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, eastUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyTurnGuard(a, "right", "East", RIGHT, {"!"+a+"CannotSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probTurnIntended, eastUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", "East", RIGHT, { a+"CannotSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n";
- actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, {"!"+a+"CannotSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, eastUpdate(a)} }) << ";\n";
- actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, {"!"+a+"CannotSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, eastUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, {"!"+a+"CannotSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probTurnIntended, eastUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, {"!"+a+"CannotSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=3)"}, {1 - probTurnIntended, eastUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, { a+"CannotSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, { a+"CannotSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n";
}
void PrismModulesPrinter::printSlipperyTurnActionsForSouth(const AgentName &a) {
- actionStream << printSlipperyTurnGuard(a, "right", "South", RIGHT, {"!"+a+"CannotSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, southUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyTurnGuard(a, "right", "South", RIGHT, {"!"+a+"CannotSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probTurnIntended, southUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", "South", RIGHT, { a+"CannotSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n";
- actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, {"!"+a+"CannotSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, southUpdate(a)} }) << ";\n";
- actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, {"!"+a+"CannotSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, southUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, {"!"+a+"CannotSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probTurnIntended, southUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, {"!"+a+"CannotSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=3)"}, {1 - probTurnIntended, southUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, { a+"CannotSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, { a+"CannotSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n";
}
void PrismModulesPrinter::printSlipperyTurnActionsForWest(const AgentName &a) {
- actionStream << printSlipperyTurnGuard(a, "right", "West", RIGHT, {"!"+a+"CannotSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, westUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyTurnGuard(a, "right", "West", RIGHT, {"!"+a+"CannotSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probTurnIntended, westUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", "West", RIGHT, { a+"CannotSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n";
- actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, {"!"+a+"CannotSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, westUpdate(a)} }) << ";\n";
- actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, {"!"+a+"CannotSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, westUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, {"!"+a+"CannotSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probTurnIntended, westUpdate(a)} }) << ";\n";
+ actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, {"!"+a+"CannotSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=3)"}, {1 - probTurnIntended, westUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, { a+"CannotSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, { a+"CannotSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n";
}
@@ -720,7 +767,7 @@ namespace prism {
}
bool PrismModulesPrinter::slipperyBehaviour() const {
- return !slipperyTiles.at("North").empty() || !slipperyTiles.at("East").empty() || !slipperyTiles.at("South").empty() || !slipperyTiles.at("West").empty();
+ return !slipperyTiles.at("Slippery").empty() || !slipperyTiles.at("North").empty() || !slipperyTiles.at("East").empty() || !slipperyTiles.at("South").empty() || !slipperyTiles.at("West").empty();
}
bool PrismModulesPrinter::isGame() const {
diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h
index af7601b..2178d44 100644
--- a/util/PrismModulesPrinter.h
+++ b/util/PrismModulesPrinter.h
@@ -16,7 +16,7 @@ std::string westUpdate(const AgentName &a);
namespace prism {
class PrismModulesPrinter {
public:
- PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector<Configuration> config, const float probIntended, const float faultyProbability, const bool anyLava, const bool anyGoals);
+ PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector<Configuration> config, const float probIntended, const float probTurnIntended, const float faultyProbability, const bool anyLava, const bool anyGoals);
std::ostream& print();
@@ -40,10 +40,12 @@ namespace prism {
void printTurnActionsForRobot(const std::string &a);
void printNonMovementActionsForRobot(const AgentName &agentName);
void printSlipperyMovementActionsForRobot(const AgentName &a);
+ void printSlipperyMovementActionsForSlippery(const AgentName &a);
void printSlipperyMovementActionsForNorth(const AgentName &a);
void printSlipperyMovementActionsForEast(const AgentName &a);
void printSlipperyMovementActionsForSouth(const AgentName &a);
void printSlipperyMovementActionsForWest(const AgentName &a);
+ void printSlipperyTurnActionsForSlippery(const AgentName &a);
void printSlipperyTurnActionsForNorth(const AgentName &a);
void printSlipperyTurnActionsForEast(const AgentName &a);
void printSlipperyTurnActionsForSouth(const AgentName &a);
@@ -113,6 +115,7 @@ namespace prism {
size_t numberOfPlayer;
float const faultyProbability;
float const probIntended;
+ float const probTurnIntended;
std::vector<Configuration> configuration;
std::vector<ViewDirection> viewDirections = {0, 1, 2, 3};
std::map<ViewDirection, std::string> viewDirectionToString = {{0, "East"}, {1, "South"}, {2, "West"}, {3, "North"}};
--
2.20.1
From a3413fe990500a5f273fa32dc473590fbaad512f Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Tue, 29 Apr 2025 14:17:23 +0200
Subject: [PATCH 22/22] changed behaviour when moving against wall
---
util/Grid.cpp | 5 ++---
util/PrismModulesPrinter.cpp | 10 +++++-----
2 files changed, 7 insertions(+), 8 deletions(-)
diff --git a/util/Grid.cpp b/util/Grid.cpp
index d276c7b..0c9db49 100644
--- a/util/Grid.cpp
+++ b/util/Grid.cpp
@@ -181,12 +181,11 @@ void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configurat
}
if(agentNameAndPositionMap.size() > 1) formulas.printCollisionFormula(agentName);
formulas.printInitStruct();
+ os << "const int WIDTH = " << maxBoundaries.first << ";\n";
+ os << "const int HEIGHT = " << maxBoundaries.second << ";\n";
modules.print();
-
-
-
//if(!stateRewards.empty()) {
// modules.printRewards(os, agentName, stateRewards, lava, goals, backgroundTiles);
//}
diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp
index a2855da..ffe8a7b 100644
--- a/util/PrismModulesPrinter.cpp
+++ b/util/PrismModulesPrinter.cpp
@@ -5,10 +5,10 @@
#include <stdexcept>
-std::string northUpdate(const AgentName &a) { return "(row"+a+"'=row"+a+"-1)"; }
-std::string southUpdate(const AgentName &a) { return "(row"+a+"'=row"+a+"+1)"; }
-std::string eastUpdate(const AgentName &a) { return "(col"+a+"'=col"+a+"+1)"; }
-std::string westUpdate(const AgentName &a) { return "(col"+a+"'=col"+a+"-1)"; }
+std::string northUpdate(const AgentName &a) { return "min(WIDTH, max(1, row"+a+"'=row"+a+"-1))"; }
+std::string southUpdate(const AgentName &a) { return "min(WIDTH, max(1, row"+a+"'=row"+a+"+1))"; }
+std::string eastUpdate(const AgentName &a) { return "min(HEIGHT, max(1, col"+a+"'=col"+a+"+1))"; }
+std::string westUpdate(const AgentName &a) { return "min(HEIGHT, max(1, col"+a+"'=col"+a+"-1))"; }
namespace prism {
@@ -250,7 +250,7 @@ namespace prism {
if(slipperyBehaviour()) guard += " & !" + a + "IsOnSlippery";
if(anyLava) guard += " & !" + a + "IsOnLava";
if(anyGoals && a == "Agent") guard += " & !" + a + "IsOnGoal";
- guard += " & !" + a + "CannotMove" + direction + "Wall";
+ //guard += " & !" + a + "CannotMove" + direction + "Wall";
if(anyPortableObject() || !lockedDoors.empty() || !unlockedDoors.empty()) guard += " & !" + a + "CannotMoveConditionally";
guard += " -> ";
return guard;
--
2.20.1