diff --git a/.vscode/settings.json b/.vscode/settings.json
new file mode 100644
index 0000000..5232ae8
--- /dev/null
+++ b/.vscode/settings.json
@@ -0,0 +1,72 @@
+{
+ "files.associations": {
+ "sstream": "cpp",
+ "cctype": "cpp",
+ "clocale": "cpp",
+ "cmath": "cpp",
+ "cstdarg": "cpp",
+ "cstddef": "cpp",
+ "cstdio": "cpp",
+ "cstdlib": "cpp",
+ "cstring": "cpp",
+ "ctime": "cpp",
+ "cwchar": "cpp",
+ "cwctype": "cpp",
+ "array": "cpp",
+ "atomic": "cpp",
+ "bit": "cpp",
+ "*.tcc": "cpp",
+ "bitset": "cpp",
+ "chrono": "cpp",
+ "codecvt": "cpp",
+ "compare": "cpp",
+ "complex": "cpp",
+ "concepts": "cpp",
+ "condition_variable": "cpp",
+ "cstdint": "cpp",
+ "deque": "cpp",
+ "list": "cpp",
+ "map": "cpp",
+ "set": "cpp",
+ "string": "cpp",
+ "unordered_map": "cpp",
+ "vector": "cpp",
+ "exception": "cpp",
+ "algorithm": "cpp",
+ "functional": "cpp",
+ "iterator": "cpp",
+ "memory": "cpp",
+ "memory_resource": "cpp",
+ "numeric": "cpp",
+ "optional": "cpp",
+ "random": "cpp",
+ "ratio": "cpp",
+ "string_view": "cpp",
+ "system_error": "cpp",
+ "tuple": "cpp",
+ "type_traits": "cpp",
+ "utility": "cpp",
+ "fstream": "cpp",
+ "initializer_list": "cpp",
+ "iomanip": "cpp",
+ "iosfwd": "cpp",
+ "iostream": "cpp",
+ "istream": "cpp",
+ "limits": "cpp",
+ "mutex": "cpp",
+ "new": "cpp",
+ "numbers": "cpp",
+ "ostream": "cpp",
+ "semaphore": "cpp",
+ "stdexcept": "cpp",
+ "stop_token": "cpp",
+ "streambuf": "cpp",
+ "thread": "cpp",
+ "cfenv": "cpp",
+ "cinttypes": "cpp",
+ "typeindex": "cpp",
+ "typeinfo": "cpp",
+ "valarray": "cpp",
+ "variant": "cpp"
+ }
+}
\ No newline at end of file
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 1ca1571..0392819 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -1,22 +1,26 @@
-include(util/CMakeLists.txt)
-
-set(CMAKE_CXX_STANDARD 20)
-
-set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D__FILENAME__='\"$(subst ${CMAKE_SOURCE_DIR}/,,$(abspath $<))\"'")
-add_definitions(-DLOG_DEBUG)
-
cmake_minimum_required(VERSION 3.0...3.22)
-
-set(CMAKE_BUILD_TYPE Debug)
-
project(
Minigrid2PRISM
VERSION 0.1
LANGUAGES CXX)
+set(CMAKE_CXX_STANDARD 20)
+
+include(util/CMakeLists.txt)
+include(FetchContent)
-add_executable(main
- ${SRCS}
- main.cpp
- )
+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)
-target_link_libraries(main pthread)
+add_executable(main ${SRCS} main.cpp)
+target_link_libraries(main pthread yaml-cpp::yaml-cpp)
diff --git a/main.cpp b/main.cpp
index 58de07f..be33399 100644
--- a/main.cpp
+++ b/main.cpp
@@ -1,12 +1,14 @@
#include "util/OptionParser.h"
#include "util/MinigridGrammar.h"
#include "util/Grid.h"
+#include "util/ConfigYaml.h"
#include <iostream>
#include <fstream>
#include <filesystem>
#include <sstream>
+
std::vector<std::string> parseCommaSeparatedString(std::string const& str) {
std::vector<std::string> result;
std::stringstream stream(str);
@@ -19,6 +21,7 @@ std::vector<std::string> parseCommaSeparatedString(std::string const& str) {
return result;
}
+
struct printer {
typedef boost::spirit::utf8_string string;
@@ -54,6 +57,9 @@ int main(int argc, char* argv[]) {
auto enforceOneWays = optionParser.add<popl::Switch>("f", "force-oneways", "Enforce encoding of oneways. This entails that slippery tiles do not allow turning and have prob 1 to shift the agent by one and makes turning impossible if in a one tile wide section of the grid.");
+ auto configFilename = optionParser.add<popl::Value<std::string>, popl::Attribute::optional>("c", "config-file", "Filename of the predicate configuration file.");
+
+
try {
optionParser.parse(argc, argv);
@@ -100,32 +106,36 @@ int main(int argc, char* argv[]) {
std::fstream file {outputFilename->value(0), file.trunc | file.out};
std::fstream infile {inputFilename->value(0), infile.in};
- std::string line, content, background, rewards;
+ std::string line, content, background, rewards, properties;
std::cout << "\n";
bool parsingBackground = false;
bool parsingStateRewards = false;
+ bool parsingEnvironmentProperties = false;
while (std::getline(infile, line) && !line.empty()) {
if(line.at(0) == '-' && line.at(line.size() - 1) == '-' && parsingBackground) {
parsingStateRewards = true;
parsingBackground = false;
continue;
+ } else if (line.at(0) == '-' && line.at(line.size() - 1 ) == '-' && parsingStateRewards) {
+ parsingStateRewards = false;
+ parsingEnvironmentProperties = true;
+ continue;
} else if(line.at(0) == '-' && line.at(line.size() - 1) == '-') {
parsingBackground = true;
continue;
}
- if(!parsingBackground && !parsingStateRewards) {
- std::cout << "Reading :\t" << line << "\n";
+ if(!parsingBackground && !parsingStateRewards && !parsingEnvironmentProperties) {
content += line + "\n";
} else if (parsingBackground) {
- std::cout << "Background:\t" << line << "\n";
background += line + "\n";
} else if(parsingStateRewards) {
rewards += line + "\n";
+ } else if (parsingEnvironmentProperties) {
+ properties += line + "\n";
}
}
std::cout << "\n";
-
pos_iterator_t contentFirst(content.begin());
pos_iterator_t contentIter = contentFirst;
pos_iterator_t contentLast(content.end());
@@ -137,12 +147,20 @@ int main(int argc, char* argv[]) {
cells contentCells;
cells backgroundCells;
+ std::vector<Configuration> configurations;
std::map<coordinates, float> stateRewards;
+ float faultyProbability = 0.0;
+ float probIntended = 0.9;
+
try {
bool ok = phrase_parse(contentIter, contentLast, contentParser, qi::space, contentCells);
// TODO if(background is not empty) {
ok &= phrase_parse(backgroundIter, backgroundLast, backgroundParser, qi::space, backgroundCells);
// TODO }
+ if (configFilename->is_set()) {
+ YamlConfigParser parser(configFilename->value(0));
+ configurations = parser.parseConfiguration();
+ }
boost::escaped_list_separator<char> seps('\\', ';', '\n');
Tokenizer csvParser(rewards, seps);
@@ -152,10 +170,27 @@ int main(int argc, char* argv[]) {
float reward = std::stof(*(++iter));
stateRewards[std::make_pair(x,y)] = reward;
}
+ if (!properties.empty()) {
+ auto faultProbabilityIdentifier = std::string("FaultProbability:");
+ auto start_pos = properties.find(faultProbabilityIdentifier);
+
+
+ if (start_pos != std::string::npos) {
+ auto end_pos = properties.find('\n', start_pos);
+ auto value = properties.substr(start_pos + faultProbabilityIdentifier.length(), end_pos - start_pos - faultProbabilityIdentifier.length());
+ faultyProbability = std::stod(value);
+ }
+ }
if(ok) {
- Grid grid(contentCells, backgroundCells, gridOptions, stateRewards);
- //grid.printToPrism(std::cout, prism::ModelType::MDP);
- grid.printToPrism(file, prism::ModelType::MDP);
+ Grid grid(contentCells, backgroundCells, gridOptions, stateRewards, probIntended, faultyProbability);
+
+ grid.printToPrism(std::cout, configurations , gridOptions.getModelType());
+ std::stringstream ss;
+ // grid.printToPrism(file, configurations ,prism::ModelType::MDP);
+ grid.printToPrism(ss, configurations , gridOptions.getModelType());
+ std::string str = ss.str();
+ grid.applyOverwrites(str, configurations);
+ file << str;
}
} catch(qi::expectation_failure<pos_iterator_t> const& e) {
std::cout << "expected: "; print_info(e.what_);
diff --git a/util/CMakeLists.txt b/util/CMakeLists.txt
index f5884fe..2325d92 100644
--- a/util/CMakeLists.txt
+++ b/util/CMakeLists.txt
@@ -2,7 +2,10 @@ list(APPEND SRCS
${CMAKE_CURRENT_LIST_DIR}/cell.cpp
${CMAKE_CURRENT_LIST_DIR}/MinigridGrammar.h
${CMAKE_CURRENT_LIST_DIR}/Grid.cpp
+ ${CMAKE_CURRENT_LIST_DIR}/PrismPrinter.cpp
${CMAKE_CURRENT_LIST_DIR}/PrismModulesPrinter.cpp
+ ${CMAKE_CURRENT_LIST_DIR}/PrismFormulaPrinter.cpp
${CMAKE_CURRENT_LIST_DIR}/popl.hpp
${CMAKE_CURRENT_LIST_DIR}/OptionParser.cpp
+ ${CMAKE_CURRENT_LIST_DIR}/ConfigYaml.cpp
)
diff --git a/util/ConfigYaml.cpp b/util/ConfigYaml.cpp
new file mode 100644
index 0000000..07c2b8e
--- /dev/null
+++ b/util/ConfigYaml.cpp
@@ -0,0 +1,238 @@
+#include "ConfigYaml.h"
+#include <iostream>
+
+std::ostream& operator <<(std::ostream &os, const Label& label) {
+ os << "\"" << label.label_ << "\"" << "=" << label.text_;
+ return os;
+}
+
+std::ostream& operator << (std::ostream &os, const Formula& formula) {
+ os << formula.formula_ << "=" << formula.content_;
+ return os;
+}
+
+std::ostream& operator << (std::ostream& os, const Action& action) {
+ os << action.action_;
+ return os;
+}
+
+std::ostream& operator << (std::ostream& os, const Constant& constant) {
+ os << "const " << constant.type_ << " " << constant.constant_ << " = " << constant.value_;
+ return os;
+}
+
+std::ostream& operator << (std::ostream& os, const Module& module) {
+ os << "Module: " << module.module_ << std::endl;
+ for (auto& action : module.actions_) {
+ os << action << std::endl;
+ }
+ return os;
+}
+
+std::string Label::createExpression() const {
+ if (overwrite_) {
+ return "label \"" + label_ + "\" = " + text_ + Configuration::overwrite_identifier_;
+ }
+
+ return "label \"" + label_ + "\" = " + text_ + Configuration::configuration_identifier_;
+}
+
+std::string Formula::createExpression() const {
+ if (overwrite_) {
+ return "formula " + formula_ + " = " + content_ + Configuration::overwrite_identifier_;
+ }
+
+ return "formula " + formula_ + " = " + content_ + Configuration::configuration_identifier_;
+}
+
+std::string Action::createExpression() const {
+ if (overwrite_) {
+ return action_ + "\t" + guard_ + "-> " + update_ + Configuration::overwrite_identifier_;
+ }
+
+ return "\t" + action_ + "\t" + guard_ + "-> " + update_+ Configuration::configuration_identifier_;
+}
+
+std::string Constant::createExpression() const {
+ if (overwrite_) {
+ return "const " + type_ + " " + constant_ + " = " + value_ + Configuration::overwrite_identifier_;
+ }
+
+ return "const " + type_ + " " + constant_ + " = " + value_ + Configuration::configuration_identifier_;
+}
+
+YAML::Node YAML::convert<Module>::encode(const Module& rhs) {
+ YAML::Node node;
+
+ node.push_back(rhs.module_);
+ node.push_back(rhs.actions_);
+
+ return node;
+}
+
+bool YAML::convert<Module>::decode(const YAML::Node& node, Module& rhs) {
+ if (!node.Type() == NodeType::Map) {
+ return false;
+ }
+ rhs.actions_ = node["actions"].as<std::vector<Action>>();
+ rhs.module_ = node["module"].as<std::string>();
+ return true;
+}
+
+YAML::Node YAML::convert<Action>::encode(const Action& rhs) {
+ YAML::Node node;
+
+ node.push_back(rhs.action_);
+ node.push_back(rhs.guard_);
+ node.push_back(rhs.overwrite_);
+ node.push_back(rhs.update_);
+
+ return node;
+}
+
+bool YAML::convert<Action>::decode(const YAML::Node& node, Action& rhs) {
+ if (!node.Type() == NodeType::Map) {
+ return false;
+ }
+
+ rhs.action_ = node["action"].as<std::string>();
+ rhs.guard_ = node["guard"].as<std::string>();
+ rhs.update_ = node["update"].as<std::string>();
+
+ if (node["overwrite"]) {
+ rhs.overwrite_ = node["overwrite"].as<bool>();
+ }
+ if (node["index"]) {
+ rhs.index_ = node["index"].as<int>();
+ }
+
+ return true;
+}
+
+
+YAML::Node YAML::convert<Label>::encode(const Label& rhs) {
+ YAML::Node node;
+
+ node.push_back(rhs.label_);
+ node.push_back(rhs.text_);
+
+ return node;
+}
+
+bool YAML::convert<Label>::decode(const YAML::Node& node, Label& rhs) {
+ if (!node.Type() == NodeType::Map || !node["label"] || !node["text"]) {
+ return false;
+ }
+ rhs.label_ = node["label"].as<std::string>();
+ rhs.text_ = node["text"].as<std::string>();
+
+ if (node["overwrite"]) {
+ rhs.overwrite_ = node["overwrite"].as<bool>();
+ }
+
+ return true;
+}
+
+YAML::Node YAML::convert<Formula>::encode(const Formula& rhs) {
+ YAML::Node node;
+
+ node.push_back(rhs.content_);
+ node.push_back(rhs.formula_);
+ node.push_back(rhs.overwrite_);
+
+ return node;
+}
+
+bool YAML::convert<Formula>::decode(const YAML::Node& node, Formula& rhs) {
+ if (!node.IsDefined() || !node.Type() == NodeType::Map || !node["formula"] || !node["content"]) {
+ return false;
+ }
+
+ rhs.formula_ = node["formula"].as<std::string>();
+ rhs.content_ = node["content"].as<std::string>();
+
+ if(node["overwrite"]) {
+ rhs.overwrite_ = node["overwrite"].as<bool>();
+ }
+
+ return true;
+}
+
+YAML::Node YAML::convert<Constant>::encode(const Constant& rhs) {
+ YAML::Node node;
+
+ node.push_back(rhs.constant_);
+ node.push_back(rhs.value_);
+ node.push_back(rhs.type_);
+ node.push_back(rhs.overwrite_);
+
+ return node;
+}
+
+bool YAML::convert<Constant>::decode(const YAML::Node& node, Constant& rhs) {
+ if (!node.IsDefined() || !node.Type() == NodeType::Map || !node["constant"] || !node["type"] || !node["value"]) {
+ return false;
+ }
+
+ rhs.constant_ = node["constant"].as<std::string>();
+ rhs.type_ = node["type"].as<std::string>();
+ rhs.value_ = node["value"].as<std::string>();
+
+ if(node["overwrite"]) {
+ rhs.overwrite_ = node["overwrite"].as<bool>();
+ }
+
+ return true;
+}
+
+const std::string Configuration::configuration_identifier_ { "; // created through configuration"};
+const std::string Configuration::overwrite_identifier_{"; // Overwritten through configuration"};
+
+ std::vector<Configuration> YamlConfigParser::parseConfiguration() {
+ std::vector<Configuration> configuration;
+
+ try {
+ YAML::Node config = YAML::LoadFile(file_);
+ std::vector<Label> labels;
+ std::vector<Formula> formulas;
+ std::vector<Module> modules;
+ std::vector<Constant> constants;
+
+ if (config["labels"]) {
+ labels = config["labels"].as<std::vector<Label>>();
+ }
+ if (config["formulas"]) {
+ formulas = config["formulas"].as<std::vector<Formula>>();
+ }
+ if (config["modules"]) {
+ modules = config["modules"].as<std::vector<Module>>();
+ }
+
+ if (config["constants"]) {
+ constants = config["constants"].as<std::vector<Constant>>();
+ }
+
+ for (auto& label : labels) {
+ configuration.push_back({label.createExpression(), label.label_ , ConfigType::Label, label.overwrite_});
+ }
+ for (auto& formula : formulas) {
+ configuration.push_back({formula.createExpression(), formula.formula_ ,ConfigType::Formula, formula.overwrite_});
+ }
+ for (auto& module : modules) {
+ for (auto& action : module.actions_) {
+ configuration.push_back({action.createExpression(), action.action_, ConfigType::Module, action.overwrite_, module.module_, action.index_});
+ }
+ }
+ for (auto& constant : constants) {
+ // std::cout << constant.constant_ << std::endl;
+ configuration.push_back({constant.createExpression(), "const " + constant.type_ + " " + constant.constant_, ConfigType::Constant, constant.overwrite_});
+ }
+ }
+ catch(const std::exception& e) {
+ std::cout << "Exception '" << typeid(e).name() << "' caught:" << std::endl;
+ std::cout << "\t" << e.what() << std::endl;
+ std::cout << "while parsing configuration " << file_ << std::endl;
+ }
+
+ return configuration;
+}
\ No newline at end of file
diff --git a/util/ConfigYaml.h b/util/ConfigYaml.h
new file mode 100644
index 0000000..6b4e93a
--- /dev/null
+++ b/util/ConfigYaml.h
@@ -0,0 +1,151 @@
+#pragma once
+
+#include <vector>
+#include <ostream>
+
+#include "yaml-cpp/yaml.h"
+
+
+enum class ConfigType : char {
+ Label = 'L',
+ Formula = 'F',
+ Module = 'M',
+ Constant = 'C'
+};
+
+struct Configuration
+{
+ static const std::string overwrite_identifier_;
+ static const std::string configuration_identifier_;
+
+ std::string module_ {};
+ std::string expression_{};
+ std::string identifier_{};
+ int index_{};
+
+ ConfigType type_ {ConfigType::Label};
+ bool overwrite_ {false};
+
+ Configuration() = default;
+ Configuration(std::string expression
+ , std::string identifier
+ , ConfigType type
+ , bool overwrite = false
+ , std::string module = ""
+ , int index = 0) : expression_(expression), identifier_(identifier), type_(type), overwrite_(overwrite), module_{module}, index_(index) {}
+
+ ~Configuration() = default;
+ Configuration(const Configuration&) = default;
+
+ friend std::ostream& operator << (std::ostream& os, const Configuration& config) {
+ os << "Configuration with Type: " << static_cast<char>(config.type_) << std::endl;
+ return os << "\tExpression=" << config.expression_ << std::endl;
+ }
+};
+
+struct Constant {
+ private:
+
+ public:
+ std::string constant_;
+ std::string type_;
+ std::string value_;
+ bool overwrite_{false};
+
+ std::string createExpression() const;
+
+ friend std::ostream& operator <<(std::ostream &os, const Constant& constant);
+};
+
+struct Label {
+ private:
+
+ public:
+ std::string text_;
+ std::string label_;
+ bool overwrite_{false};
+
+ std::string createExpression() const;
+
+ friend std::ostream& operator <<(std::ostream &os, const Label& label);
+};
+
+struct Formula {
+ private:
+
+ public:
+ std::string formula_;
+ std::string content_;
+ bool overwrite_ {false};
+
+ std::string createExpression() const;
+
+ friend std::ostream& operator << (std::ostream &os, const Formula& formula);
+};
+
+struct Action {
+ public:
+ std::string action_;
+ std::string guard_;
+ std::string update_;
+ int index_{0};
+ bool overwrite_ {false};
+
+ std::string createExpression() const;
+
+ friend std::ostream& operator << (std::ostream& os, const Action& action);
+};
+
+struct Module {
+ public:
+
+ std::vector<Action> actions_;
+ std::string module_;
+
+ friend std::ostream& operator << (std::ostream& os, const Module& module);
+};
+
+
+template<>
+struct YAML::convert<Module> {
+ static YAML::Node encode(const Module& rhs);
+ static bool decode(const YAML::Node& node, Module& rhs);
+};
+
+template<>
+struct YAML::convert<Action> {
+ static YAML::Node encode(const Action& rhs);
+ static bool decode(const YAML::Node& node, Action& rhs);
+};
+
+
+template<>
+struct YAML::convert<Label> {
+ static YAML::Node encode(const Label& rhs);
+ static bool decode(const YAML::Node& node, Label& rhs);
+};
+
+template<>
+struct YAML::convert<Formula> {
+ static YAML::Node encode(const Formula& rhs);
+ static bool decode(const YAML::Node& node, Formula& rhs);
+};
+
+template<>
+struct YAML::convert<Constant> {
+ static YAML::Node encode(const Constant& rhs);
+ static bool decode(const YAML::Node& node, Constant& rhs);
+};
+
+
+struct YamlConfigParser {
+ public:
+ YamlConfigParser(std::string file) : file_(file) {}
+ YamlConfigParser(const YamlConfigParser&) = delete;
+ ~YamlConfigParser() = default;
+
+ std::vector<Configuration> parseConfiguration();
+ private:
+
+ std::string file_;
+};
\ No newline at end of file
diff --git a/util/Grid.cpp b/util/Grid.cpp
index 1184e1e..294ddd1 100644
--- a/util/Grid.cpp
+++ b/util/Grid.cpp
@@ -1,51 +1,38 @@
#include "Grid.h"
+#include <boost/algorithm/string/find.hpp>
#include <algorithm>
-Grid::Grid(cells gridCells, cells background, const GridOptions &gridOptions, const std::map<coordinates, float> &stateRewards)
- : allGridCells(gridCells), background(background), gridOptions(gridOptions), stateRewards(stateRewards)
+prism::ModelType GridOptions::getModelType() const
+{
+ if (agentsWithView.size() > 1) {
+ return prism::ModelType::SMG;
+ }
+ return prism::ModelType::MDP;
+}
+
+Grid::Grid(cells gridCells, cells background, const GridOptions &gridOptions, const std::map<coordinates, float> &stateRewards, const float probIntended, const float faultyProbability)
+ : allGridCells(gridCells), background(background), gridOptions(gridOptions), stateRewards(stateRewards), probIntended(probIntended), faultyProbability(faultyProbability)
{
cell max = allGridCells.at(allGridCells.size() - 1);
maxBoundaries = std::make_pair(max.row - 1, max.column - 1);
- std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(walls), [](cell c) {
- return c.type == Type::Wall;
- });
- std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(lava), [](cell c) {
- return c.type == Type::Lava;
- });
- std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(floor), [](cell c) {
- return c.type == Type::Floor;
- });
- std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyNorth), [](cell c) {
- return c.type == Type::SlipperyNorth;
- });
- std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyEast), [](cell c) {
- return c.type == Type::SlipperyEast;
- });
- std::copy_if(background.begin(), background.end(), std::back_inserter(slipperySouth), [](cell c) {
- return c.type == Type::SlipperySouth;
- });
- std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyWest), [](cell c) {
- return c.type == Type::SlipperyWest;
- });
- std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(lockedDoors), [](cell c) {
- return c.type == Type::LockedDoor;
- });
- std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(goals), [](cell c) {
- return c.type == Type::Goal;
- });
- std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(keys), [](cell c) {
- return c.type == Type::Key;
- });
- std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(boxes), [](cell c) {
- return c.type == Type::Box;
- });
- agent = *std::find_if(gridCells.begin(), gridCells.end(), [](cell c) {
- return c.type == Type::Agent;
- });
- std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(adversaries), [](cell c) {
- return c.type == Type::Adversary;
- });
+ std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(walls), [](cell c) { return c.type == Type::Wall; });
+ std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(lava), [](cell c) { return c.type == Type::Lava; });
+ std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(floor), [](cell c) { return c.type == Type::Floor; }); // TODO CHECK IF ALL AGENTS ARE ADDED TO FLOOR
+ std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyNorth), [](cell c) { return c.type == Type::SlipperyNorth; });
+ std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyEast), [](cell c) { return c.type == Type::SlipperyEast; });
+ std::copy_if(background.begin(), background.end(), std::back_inserter(slipperySouth), [](cell c) { return c.type == Type::SlipperySouth; });
+ std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyWest), [](cell c) { return c.type == Type::SlipperyWest; });
+ std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(lockedDoors), [](cell c) { return c.type == Type::LockedDoor; });
+ std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(unlockedDoors), [](cell c) { return c.type == Type::Door; });
+ std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(goals), [](cell c) { return c.type == Type::Goal; });
+ std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(keys), [](cell c) { return c.type == Type::Key; });
+ std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(boxes), [](cell c) { return c.type == Type::Box; });
+ std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(balls), [](cell c) { return c.type == Type::Ball; });
+ std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(adversaries), [](cell c) { return c.type == Type::Adversary; });
+ agent = *std::find_if(gridCells.begin(), gridCells.end(), [](cell c) { return c.type == Type::Agent; });
+ floor.push_back(agent);
+
agentNameAndPositionMap.insert({ "Agent", agent.getCoordinates() });
for(auto const& adversary : adversaries) {
std::string color = adversary.getColor();
@@ -53,6 +40,7 @@ Grid::Grid(cells gridCells, cells background, const GridOptions &gridOptions, co
try {
if(gridOptions.agentsToBeConsidered.size() != 0 && std::find(gridOptions.agentsToBeConsidered.begin(), gridOptions.agentsToBeConsidered.end(), color) == gridOptions.agentsToBeConsidered.end()) continue;
auto success = agentNameAndPositionMap.insert({ color, adversary.getCoordinates() });
+ floor.push_back(adversary);
if(!success.second) {
throw std::logic_error("Agent with " + color + " already present\n");
}
@@ -61,6 +49,18 @@ Grid::Grid(cells gridCells, cells background, const GridOptions &gridOptions, co
throw;
}
}
+ for(auto const& key : keys) {
+ std::string color = key.getColor();
+ try {
+ auto success = keyNameAndPositionMap.insert({color, key.getCoordinates() });
+ if (!success.second) {
+ throw std::logic_error("Multiple keys with same color not supported " + color + "\n");
+ }
+ } catch(const std::logic_error& e) {
+ std::cerr << "Expected key colors to be different. Key with color : '" << color << "' already present." << std::endl;
+ throw;
+ }
+ }
for(auto const& color : allColors) {
cells cellsOfColor;
std::copy_if(background.begin(), background.end(), std::back_inserter(cellsOfColor), [&color](cell c) {
@@ -88,142 +88,101 @@ cells Grid::getGridCells() {
}
bool Grid::isBlocked(coordinates p) {
- return isWall(p) || isLockedDoor(p) || isKey(p);
+ return isWall(p);
}
bool Grid::isWall(coordinates p) {
return std::find_if(walls.begin(), walls.end(),
[p](cell cell) {
- return cell.row == p.first && cell.column == p.second;
+ return cell.row == p.second && cell.column == p.first;
}) != walls.end();
}
-bool Grid::isLockedDoor(coordinates p) {
- return std::find_if(lockedDoors.begin(), lockedDoors.end(),
- [p](cell cell) {
- return cell.row == p.first && cell.column == p.second;
- }) != lockedDoors.end();
-}
-bool Grid::isKey(coordinates p) {
- return std::find_if(keys.begin(), keys.end(),
- [p](cell cell) {
- return cell.row == p.first && cell.column == p.second;
- }) != keys.end();
-}
+void Grid::applyOverwrites(std::string& str, std::vector<Configuration>& configuration) {
+ for (auto& config : configuration) {
+ if (!config.overwrite_) {
+ continue;
+ }
+ size_t start_pos;
+
+ if (config.type_ == ConfigType::Formula) {
+ start_pos = str.find("formula " + config.identifier_);
+ } else if (config.type_ == ConfigType::Label) {
+ start_pos = str.find("label " + config.identifier_);
+ } else if (config.type_ == ConfigType::Module) {
+ auto iter = boost::find_nth(str, config.identifier_, config.index_);
+ start_pos = std::distance(str.begin(), iter.begin());
+ }
+ else if (config.type_ == ConfigType::Constant) {
+ start_pos = str.find(config.identifier_);
-bool Grid::isBox(coordinates p) {
- return std::find_if(boxes.begin(), boxes.end(),
- [p](cell cell) {
- return cell.row == p.first && cell.column == p.second;
- }) != boxes.end();
+ if (start_pos == std::string::npos) {
+ std::cout << "Couldn't find overwrite:" << config.expression_ << std::endl;
+ }
+ }
+
+ size_t end_pos = str.find(';', start_pos) + 1;
+
+ std::string expression = config.expression_;
+
+ str.replace(start_pos, end_pos - start_pos , expression);
+ }
}
+void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configuration ,const prism::ModelType& modelType) {
+ cells northRestriction, eastRestriction, southRestriction, westRestriction;
-void Grid::printToPrism(std::ostream& os, const prism::ModelType& modelType) {
- cells northRestriction;
- cells eastRestriction;
- cells southRestriction;
- cells westRestriction;
cells walkable = floor;
walkable.insert(walkable.end(), goals.begin(), goals.end());
walkable.insert(walkable.end(), boxes.begin(), boxes.end());
- walkable.push_back(agent);
- walkable.insert(walkable.end(), adversaries.begin(), adversaries.end());
walkable.insert(walkable.end(), lava.begin(), lava.end());
+ walkable.insert(walkable.end(), keys.begin(), keys.end());
+ walkable.insert(walkable.end(), balls.begin(), balls.end());
+
for(auto const& c : walkable) {
- if(isBlocked(c.getNorth())) northRestriction.push_back(c);
- if(isBlocked(c.getEast())) eastRestriction.push_back(c);
- if(isBlocked(c.getSouth())) southRestriction.push_back(c);
- if(isBlocked(c.getWest())) westRestriction.push_back(c);
+ if(isWall(c.getNorth())) northRestriction.push_back(c);
+ if(isWall(c.getEast())) eastRestriction.push_back(c);
+ if(isWall(c.getSouth())) southRestriction.push_back(c);
+ if(isWall(c.getWest())) westRestriction.push_back(c);
}
- prism::PrismModulesPrinter printer(modelType, agentNameAndPositionMap.size(), gridOptions.enforceOneWays);
- printer.printModel(os, modelType);
- if(modelType == prism::ModelType::SMG) {
- printer.printGlobalMoveVariable(os, agentNameAndPositionMap.size());
- }
- for(auto const &backgroundTilesOfColor : backgroundTiles) {
- for(auto agentNameAndPosition = agentNameAndPositionMap.begin(); agentNameAndPosition != agentNameAndPositionMap.end(); ++agentNameAndPosition) {
- printer.printBackgroundLabels(os, agentNameAndPosition->first, backgroundTilesOfColor);
- }
- }
- cells noTurnFloor;
- if(gridOptions.enforceOneWays) {
- for(auto const& c : floor) {
- cell east = c.getEast(allGridCells);
- cell south = c.getSouth(allGridCells);
- cell west = c.getWest(allGridCells);
- cell north = c.getNorth(allGridCells);
- if( (east.type == Type::Wall && west.type == Type::Wall) or
- (north.type == Type::Wall && south.type == Type::Wall) ) {
- noTurnFloor.push_back(c);
- }
- }
- }
- for(auto agentNameAndPosition = agentNameAndPositionMap.begin(); agentNameAndPosition != agentNameAndPositionMap.end(); ++agentNameAndPosition) {
- printer.printFormulas(os, agentNameAndPosition->first, northRestriction, eastRestriction, southRestriction, westRestriction, { slipperyNorth, slipperyEast, slipperySouth, slipperyWest }, lava, walls, noTurnFloor, slipperyNorth, slipperyEast, slipperySouth, slipperyWest);
- printer.printGoalLabel(os, agentNameAndPosition->first, goals);
- printer.printKeysLabels(os, agentNameAndPosition->first, keys);
- }
+ 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::vector<AgentName> agentNames;
std::transform(agentNameAndPositionMap.begin(),
agentNameAndPositionMap.end(),
std::back_inserter(agentNames),
[](const std::map<AgentNameAndPosition::first_type,AgentNameAndPosition::second_type>::value_type &pair){return pair.first;});
- if(modelType == prism::ModelType::SMG) {
- printer.printCrashLabel(os, agentNames);
- }
- size_t agentIndex = 0;
- for(auto agentNameAndPosition = agentNameAndPositionMap.begin(); agentNameAndPosition != agentNameAndPositionMap.end(); ++agentNameAndPosition, agentIndex++) {
- AgentName agentName = agentNameAndPosition->first;
- bool agentWithView = std::find(gridOptions.agentsWithView.begin(), gridOptions.agentsWithView.end(), agentName) != gridOptions.agentsWithView.end();
- bool agentWithProbabilisticBehaviour = std::find(gridOptions.agentsWithProbabilisticBehaviour.begin(), gridOptions.agentsWithProbabilisticBehaviour.end(), agentName) != gridOptions.agentsWithProbabilisticBehaviour.end();
- std::set<std::string> slipperyActions;
- printer.printInitStruct(os, agentName);
- if(agentWithProbabilisticBehaviour) printer.printModule(os, agentName, agentIndex, maxBoundaries, agentNameAndPosition->second, keys, backgroundTiles, agentWithView, gridOptions.probabilitiesForActions);
- else printer.printModule(os, agentName, agentIndex, maxBoundaries, agentNameAndPosition->second, keys, backgroundTiles, agentWithView);
- for(auto const& c : slipperyNorth) {
- printer.printSlipperyMove(os, agentName, agentIndex, c.getCoordinates(), slipperyActions, getWalkableDirOf8Neighborhood(c), prism::PrismModulesPrinter::SlipperyType::North);
- if(!gridOptions.enforceOneWays) printer.printSlipperyTurn(os, agentName, agentIndex, c.getCoordinates(), slipperyActions, getWalkableDirOf8Neighborhood(c), prism::PrismModulesPrinter::SlipperyType::North);
+ std::string agentName = agentNames.at(0);
- }
- for(auto const& c : slipperyEast) {
- printer.printSlipperyMove(os, agentName, agentIndex, c.getCoordinates(), slipperyActions, getWalkableDirOf8Neighborhood(c), prism::PrismModulesPrinter::SlipperyType::East);
- if(!gridOptions.enforceOneWays) printer.printSlipperyTurn(os, agentName, agentIndex, c.getCoordinates(), slipperyActions, getWalkableDirOf8Neighborhood(c), prism::PrismModulesPrinter::SlipperyType::East);
- }
- for(auto const& c : slipperySouth) {
- printer.printSlipperyMove(os, agentName, agentIndex, c.getCoordinates(), slipperyActions, getWalkableDirOf8Neighborhood(c), prism::PrismModulesPrinter::SlipperyType::South);
- if(!gridOptions.enforceOneWays) printer.printSlipperyTurn(os, agentName, agentIndex, c.getCoordinates(), slipperyActions, getWalkableDirOf8Neighborhood(c), prism::PrismModulesPrinter::SlipperyType::South);
- }
- for(auto const& c : slipperyWest) {
- printer.printSlipperyMove(os, agentName, agentIndex, c.getCoordinates(), slipperyActions, getWalkableDirOf8Neighborhood(c), prism::PrismModulesPrinter::SlipperyType::West);
- if(!gridOptions.enforceOneWays) printer.printSlipperyTurn(os, agentName, agentIndex, c.getCoordinates(), slipperyActions, getWalkableDirOf8Neighborhood(c), prism::PrismModulesPrinter::SlipperyType::West);
- }
+ prism::PrismFormulaPrinter formulas(os, wallRestrictions, walls, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, lava, goals);
+ prism::PrismModulesPrinter modules(os, modelType, maxBoundaries, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, agentNameAndPositionMap, configuration, probIntended, faultyProbability);
- printer.printEndmodule(os);
- if(modelType == prism::ModelType::SMG) {
- if(agentWithProbabilisticBehaviour) printer.printPlayerStruct(os, agentNameAndPosition->first, agentWithView, gridOptions.probabilitiesForActions, slipperyActions);
- else printer.printPlayerStruct(os, agentNameAndPosition->first, agentWithView, {}, slipperyActions);
- }
- //if(!stateRewards.empty()) {
- printer.printRewards(os, agentName, stateRewards, lava, goals, backgroundTiles);
- //}
+ modules.printModelType(modelType);
+ for(const auto &agentName : agentNames) {
+ formulas.print(agentName);
}
-}
+ //std::vector<std::string> constants {"const double prop_zero = 0/9;",
+ // "const double prop_intended = 6/9;",
+ // "const double prop_turn_intended = 6/9;",
+ // "const double prop_displacement = 3/9;",
+ // "const double prop_turn_displacement = 3/9;",
+ // "const int width = " + std::to_string(maxBoundaries.first) + ";",
+ // "const int height = " + std::to_string(maxBoundaries.second) + ";"
+ // };
+ //modules.printConstants(os, constants);
+ modules.print();
+
+
+
+ //if(!stateRewards.empty()) {
+ // modules.printRewards(os, agentName, stateRewards, lava, goals, backgroundTiles);
+ //}
-std::array<bool, 8> Grid::getWalkableDirOf8Neighborhood(cell c) /* const */ {
- return (std::array<bool, 8>)
- {
- !isBlocked(c.getNorth()),
- !isBlocked(c.getNorth(allGridCells).getEast()),
- !isBlocked(c.getEast()),
- !isBlocked(c.getSouth(allGridCells).getEast()),
- !isBlocked(c.getSouth()),
- !isBlocked(c.getSouth(allGridCells).getWest()),
- !isBlocked(c.getWest()),
- !isBlocked(c.getNorth(allGridCells).getWest())
- };
+ //if (!configuration.empty()) {
+ // modules.printConfiguration(os, configuration);
+ //}
}
diff --git a/util/Grid.h b/util/Grid.h
index 84c2eb2..eb95437 100644
--- a/util/Grid.h
+++ b/util/Grid.h
@@ -7,6 +7,8 @@
#include "MinigridGrammar.h"
#include "PrismModulesPrinter.h"
+#include "PrismFormulaPrinter.h"
+#include "ConfigYaml.h"
struct GridOptions {
std::vector<AgentName> agentsToBeConsidered;
@@ -14,20 +16,20 @@ struct GridOptions {
std::vector<AgentName> agentsWithProbabilisticBehaviour;
std::vector<float> probabilitiesForActions;
bool enforceOneWays;
+
+ prism::ModelType getModelType() const;
};
class Grid {
public:
- Grid(cells gridCells, cells background, const GridOptions &gridOptions, const std::map<coordinates, float> &stateRewards = {});
+ Grid(cells gridCells, cells background, const GridOptions &gridOptions, const std::map<coordinates, float> &stateRewards = {}, const float probIntended = 1.0, const float faultyProbability = 0);
cells getGridCells();
bool isBlocked(coordinates p);
bool isWall(coordinates p);
- bool isLockedDoor(coordinates p);
- bool isKey(coordinates p);
- bool isBox(coordinates p);
- void printToPrism(std::ostream &os, const prism::ModelType& modelType);
+ void printToPrism(std::ostream &os, std::vector<Configuration>& configuration, const prism::ModelType& modelType);
+ void applyOverwrites(std::string& str, std::vector<Configuration>& configuration);
std::array<bool, 8> getWalkableDirOf8Neighborhood(cell c);
@@ -43,6 +45,7 @@ class Grid {
cell agent;
cells adversaries;
AgentNameAndPositionMap agentNameAndPositionMap;
+ KeyNameAndPositionMap keyNameAndPositionMap;
cells walls;
cells floor;
@@ -51,7 +54,9 @@ class Grid {
cells slipperySouth;
cells slipperyWest;
cells lockedDoors;
+ cells unlockedDoors;
cells boxes;
+ cells balls;
cells lava;
cells goals;
@@ -60,4 +65,6 @@ class Grid {
std::map<Color, cells> backgroundTiles;
std::map<coordinates, float> stateRewards;
+ const float probIntended;
+ const float faultyProbability;
};
diff --git a/util/MinigridGrammar.h b/util/MinigridGrammar.h
index 79684a5..e2cfddc 100644
--- a/util/MinigridGrammar.h
+++ b/util/MinigridGrammar.h
@@ -75,7 +75,7 @@ template <typename It>
("P", Color::Purple)
("Y", Color::Yellow)
(" ", Color::None);
-
+
cell_ = type_ > color_;
row_ = (cell_ % -qi::char_("\n"));
diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp
new file mode 100644
index 0000000..ef2f5a5
--- /dev/null
+++ b/util/PrismFormulaPrinter.cpp
@@ -0,0 +1,222 @@
+#include "PrismFormulaPrinter.h"
+
+#include <map>
+#include <string>
+#include <algorithm>
+
+std::string oneOffToString(const int &offset) {
+ return offset != 0 ? ( offset == 1 ? "+1" : "-1" ) : "";
+}
+
+std::string vectorToDisjunction(const std::vector<std::string> &formulae) {
+ bool first = true;
+ std::string disjunction = "";
+ for(const auto &formula : formulae) {
+ if(first) first = false;
+ else disjunction += " | ";
+ disjunction += formula;
+ }
+ return disjunction;
+}
+
+std::string cellToConjunction(const AgentName &agentName, const cell &c) {
+ return "x" + agentName + "=" + std::to_string(c.column) + "&y" + agentName + "=" + std::to_string(c.row);
+}
+
+std::string cellToConjunctionWithOffset(const AgentName &agentName, const cell &c, const std::string &xOffset, const std::string &yOffset){
+ return "x" + agentName + xOffset + "=" + std::to_string(c.column) + "&y" + agentName + yOffset + "=" + std::to_string(c.row);
+}
+
+std::string coordinatesToConjunction(const AgentName &agentName, const coordinates &c, const ViewDirection viewDirection) {
+ return "x" + agentName + "=" + std::to_string(c.first) + "&y" + agentName + "=" + std::to_string(c.second) + "&view" + agentName + "=" + std::to_string(viewDirection);
+}
+
+std::string objectPositionToConjunction(const AgentName &agentName, const std::string &identifier, const std::pair<int, int> &relativePosition) {
+ std::string xOffset = oneOffToString(relativePosition.first);
+ std::string yOffset = oneOffToString(relativePosition.second);
+ return "x" + agentName + xOffset + "=x" + identifier + "&y" + agentName + yOffset + "=y" + identifier;
+}
+std::string objectPositionToConjunction(const AgentName &agentName, const std::string &identifier, const std::pair<int, int> &relativePosition, const ViewDirection viewDirection) {
+ std::string xOffset = oneOffToString(relativePosition.first);
+ std::string yOffset = oneOffToString(relativePosition.second);
+ return "x" + agentName + xOffset + "=x" + identifier + "&y" + agentName + yOffset + "=y" + identifier + "&view" + agentName + "=" + std::to_string(viewDirection);
+}
+
+std::map<ViewDirection, coordinates> getAdjacentCells(const cell &c) {
+ return {{1, c.getNorth()}, {2, c.getEast()}, {3, c.getSouth()}, {0, c.getWest()}};
+}
+
+std::map<ViewDirection, std::pair<int, int>> getRelativeAdjacentCells() {
+ return { {1, {0,+1}}, {2, {-1,0}}, {3, {0,-1}}, {0, {+1,0}} };
+}
+
+std::map<std::string, std::pair<int, int>> getRelativeSurroundingCells() {
+ return { {"NorthWest", {-1,-1}}, {"North", { 0,-1}}, {"NorthEast", {+1,-1}},
+ {"West", {-1, 0}}, {"East", {+1, 0}},
+ {"SouthWest", {-1,+1}}, {"South", { 0,+1}}, {"SouthEast", {+1,+1}} };
+}
+
+namespace prism {
+ PrismFormulaPrinter::PrismFormulaPrinter(std::ostream &os, const std::map<std::string, cells> &restrictions, const cells &walls, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const cells &lava, const cells &goals)
+ : os(os), restrictions(restrictions), walls(walls), boxes(boxes), balls(balls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), lava(lava), goals(goals)
+ { }
+
+ void PrismFormulaPrinter::print(const AgentName &agentName) {
+ for(const auto& [direction, cells] : restrictions) {
+ printRestrictionFormula(agentName, direction, cells);
+ }
+
+ if(slipperyBehaviour()) {
+ for(const auto& [direction, cells] : slipperyTiles) {
+ printIsOnFormula(agentName, "Slippery", cells, direction);
+ }
+ std::vector<std::string> allSlipperyDirections = {agentName + "IsOnSlipperyNorth", agentName + "IsOnSlipperyEast", agentName + "IsOnSlipperySouth", agentName + "IsOnSlipperyWest"};
+ os << buildFormula(agentName + "IsOnSlippery", vectorToDisjunction(allSlipperyDirections));
+
+ for(const auto& [direction, relativePosition] : getRelativeSurroundingCells()) {
+ printSlipRestrictionFormula(agentName, direction);
+ }
+ } else {
+ os << buildFormula(agentName + "IsOnSlippery", "false");
+ }
+ printIsOnFormula(agentName, "Lava", lava);
+ printIsOnFormula(agentName, "Goal", goals);
+
+ for(const auto& ball : balls) {
+ std::string identifier = capitalize(ball.getColor()) + ball.getType();
+ printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp");
+ portableObjects.push_back(agentName + "Carrying" + identifier);
+ }
+
+ for(const auto& box : boxes) {
+ std::string identifier = capitalize(box.getColor()) + box.getType();
+ printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp");
+ portableObjects.push_back(agentName + "Carrying" + identifier);
+ }
+
+ for(const auto& key : keys) {
+ std::string identifier = capitalize(key.getColor()) + key.getType();
+ printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp");
+ portableObjects.push_back(agentName + "Carrying" + identifier);
+ }
+
+ for(const auto& door : unlockedDoors) {
+ std::string identifier = capitalize(door.getColor()) + door.getType();
+ printRestrictionFormulaWithCondition(agentName, identifier, getAdjacentCells(door), "!" + identifier + "Open");
+ printIsNextToFormula(agentName, identifier, getAdjacentCells(door));
+ }
+
+ for(const auto& door : lockedDoors) {
+ std::string identifier = capitalize(door.getColor()) + door.getType();
+ printRestrictionFormulaWithCondition(agentName, identifier, getAdjacentCells(door), "!" + identifier + "Open");
+ printIsNextToFormula(agentName, identifier, getAdjacentCells(door));
+ }
+
+ if(conditionalMovementRestrictions.size() > 0) {
+ os << buildFormula(agentName + "CannotMoveConditionally", vectorToDisjunction(conditionalMovementRestrictions));
+ os << buildFormula(agentName + "IsCarrying", vectorToDisjunction(portableObjects));
+ } else {
+ os << buildFormula(agentName + "CannotMoveConditionally", "false");
+ }
+ }
+
+ void PrismFormulaPrinter::printRestrictionFormula(const AgentName &agentName, const std::string &direction, const cells &grid_cells) {
+ os << buildFormula(agentName + "CannotMove" + direction + "Wall", buildDisjunction(agentName, grid_cells));
+ }
+
+ void PrismFormulaPrinter::printIsOnFormula(const AgentName &agentName, const std::string &type, const cells &grid_cells, const std::string &direction) {
+ os << buildFormula(agentName + "IsOn" + type + direction, buildDisjunction(agentName, grid_cells));
+ }
+
+ void PrismFormulaPrinter::printIsNextToFormula(const AgentName &agentName, const std::string &type, const std::map<ViewDirection, coordinates> &coordinates) {
+ os << buildFormula(agentName + "IsNextTo" + type, buildDisjunction(agentName, coordinates));
+ }
+
+ void PrismFormulaPrinter::printRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::map<ViewDirection, coordinates> &coordinates, const std::string &condition) {
+ os << buildFormula(agentName + "CannotMove" + reason, "(" + buildDisjunction(agentName, coordinates) + ") & " + condition);
+ conditionalMovementRestrictions.push_back(agentName + "CannotMove" + reason);
+ }
+
+ void PrismFormulaPrinter::printRelativeRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::string &condition) {
+ os << buildFormula(agentName + "CannotMove" + reason, "(" + buildDisjunction(agentName, reason) + ") & " + condition);
+ conditionalMovementRestrictions.push_back(agentName + "CannotMove" + reason);
+ }
+
+ void PrismFormulaPrinter::printSlipRestrictionFormula(const AgentName &agentName, const std::string &direction) {
+ std::pair<int, int> slipCell = getRelativeSurroundingCells().at(direction);
+ bool semicolon = anyPortableObject() ? false : true;
+ os << buildFormula(agentName + "CannotSlip" + direction, buildDisjunction(agentName, walls, slipCell), semicolon);
+ for(auto const key : keys) {
+ std::string identifier = capitalize(key.getColor()) + key.getType();
+ os << " | " << objectPositionToConjunction(agentName, identifier, slipCell);
+ }
+ for(auto const ball : balls) {
+ std::string identifier = capitalize(ball.getColor()) + ball.getType();
+ os << " | " << objectPositionToConjunction(agentName, identifier, slipCell);
+ }
+ for(auto const box : boxes) {
+ std::string identifier = capitalize(box.getColor()) + box.getType();
+ os << " | " << objectPositionToConjunction(agentName, identifier, slipCell);
+ }
+ os << ";\n";
+ }
+
+ std::string PrismFormulaPrinter::buildFormula(const std::string &formulaName, const std::string &formula, const bool semicolon) {
+ return "formula " + formulaName + " = " + formula + (semicolon ? ";\n": "");
+ }
+
+ std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const std::map<ViewDirection, coordinates> &cells) {
+ if(cells.size() == 0) return "false";
+ bool first = true;
+ std::string disjunction = "";
+ for(const auto [viewDirection, coordinates] : cells) {
+ if(first) first = false;
+ else disjunction += " | ";
+ disjunction += "(" + coordinatesToConjunction(agentName, coordinates, viewDirection) + ")";
+ }
+ return disjunction;
+ }
+
+ std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const cells &cells) {
+ if(cells.size() == 0) return "false";
+ bool first = true;
+ std::string disjunction = "";
+ for(auto const cell : cells) {
+ if(first) first = false;
+ else disjunction += " | ";
+ disjunction += "(" + cellToConjunction(agentName, cell) + ")";
+ }
+ return disjunction;
+ }
+
+ std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const std::string &reason) {
+ std::string disjunction = "";
+ bool first = true;
+ for(auto const [viewDirection, relativePosition] : getRelativeAdjacentCells()) {
+ if(first) first = false;
+ else disjunction += " | ";
+ disjunction += "(" + objectPositionToConjunction(agentName, reason, relativePosition, viewDirection) + ")";
+ }
+ return disjunction;
+ }
+
+ std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const cells &cells, const std::pair<int, int> &offset) {
+ std::string disjunction = "";
+ bool first = true;
+ std::string xOffset = oneOffToString(offset.first);
+ std::string yOffset = oneOffToString(offset.second);
+ for(auto const cell : cells) {
+ if(first) first = false;
+ else disjunction += " | ";
+ disjunction += "(" + cellToConjunctionWithOffset(agentName, cell, xOffset, yOffset) + ")";
+ }
+ return disjunction;
+ }
+
+ bool PrismFormulaPrinter::slipperyBehaviour() const {
+ return !slipperyTiles.at("North").empty() || !slipperyTiles.at("East").empty() || !slipperyTiles.at("South").empty() || !slipperyTiles.at("West").empty();
+ }
+ bool PrismFormulaPrinter::anyPortableObject() const {
+ return !keys.empty() || !boxes.empty() || !balls.empty();
+ }
+}
diff --git a/util/PrismFormulaPrinter.h b/util/PrismFormulaPrinter.h
new file mode 100644
index 0000000..f1def2d
--- /dev/null
+++ b/util/PrismFormulaPrinter.h
@@ -0,0 +1,61 @@
+#pragma once
+
+#include <iostream>
+#include <functional>
+#include "MinigridGrammar.h"
+#include "PrismPrinter.h"
+#include "ConfigYaml.h"
+
+
+std::string oneOffToString(const int &offset);
+std::string vectorToDisjunction(const std::vector<std::string> &formulae);
+std::string cellToConjunction(const AgentName &agentName, const cell &c);
+std::string cellToConjunctionWithOffset(const AgentName &agentName, const cell &c, const std::string &xOffset, const std::string &yOffset);
+std::string coordinatesToConjunction(const AgentName &agentName, const coordinates &c, const ViewDirection viewDirection);
+std::string objectPositionToConjunction(const AgentName &agentName, const std::string &identifier, const std::pair<int, int> &relativePosition);
+std::string objectPositionToConjunction(const AgentName &agentName, const std::string &identifier, const std::pair<int, int> &relativePosition, const ViewDirection viewDirection);
+std::map<ViewDirection, coordinates> getAdjacentCells(const cell &c);
+std::map<ViewDirection, std::pair<int, int>> getRelativeAdjacentCells();
+std::map<std::string, std::pair<int, int>> getRelativeSurroundingCells();
+
+namespace prism {
+ class PrismFormulaPrinter {
+ public:
+ PrismFormulaPrinter(std::ostream &os, const std::map<std::string, cells> &restrictions, const cells &walls, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const cells &lava, const cells &goals);
+
+ void print(const AgentName &agentName);
+
+ void printRestrictionFormula(const AgentName &agentName, const std::string &direction, const cells &grid_cells);
+ void printIsOnFormula(const AgentName &agentName, const std::string &type, const cells &grid_cells, const std::string &direction = "");
+ void printIsNextToFormula(const AgentName &agentName, const std::string &type, const std::map<ViewDirection, coordinates> &coordinates);
+ void printRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::map<ViewDirection, coordinates> &coordinates, const std::string &condition);
+ void printRelativeRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::string &condition);
+ void printSlipRestrictionFormula(const AgentName &agentName, const std::string &direction);
+ private:
+ std::string buildFormula(const std::string &formulaName, const std::string &formula, const bool semicolon = true);
+ std::string buildLabel(const std::string &labelName, const std::string &label);
+ std::string buildDisjunction(const AgentName &agentName, const std::map<ViewDirection, coordinates> &cells);
+ std::string buildDisjunction(const AgentName &agentName, const cells &cells);
+ std::string buildDisjunction(const AgentName &agentName, const std::string &reason);
+ std::string buildDisjunction(const AgentName &agentName, const cells &cells, const std::pair<int, int> &offset);
+
+ bool slipperyBehaviour() const;
+ bool anyPortableObject() const;
+
+
+ std::ostream &os;
+ std::map<std::string, cells> restrictions;
+ cells walls;
+ cells boxes;
+ cells balls;
+ cells lockedDoors;
+ cells unlockedDoors;
+ cells keys;
+ std::map<std::string, cells> slipperyTiles;
+ cells lava;
+ cells goals;
+
+ std::vector<std::string> conditionalMovementRestrictions;
+ std::vector<std::string> portableObjects;
+ };
+}
diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp
index f6aca04..430dd3c 100644
--- a/util/PrismModulesPrinter.cpp
+++ b/util/PrismModulesPrinter.cpp
@@ -3,13 +3,29 @@
#include <map>
#include <string>
+#define NOFAULT -1
+#define LEFT 0
+#define RIGHT 1
+#define FORWARD 2
+
+
+std::string northUpdate(const AgentName &a) { return "(y"+a+"'=y"+a+"-1)"; }
+std::string southUpdate(const AgentName &a) { return "(y"+a+"'=y"+a+"+1)"; }
+std::string eastUpdate(const AgentName &a) { return "(x"+a+"'=x"+a+"+1)"; }
+std::string westUpdate(const AgentName &a) { return "(x"+a+"'=x"+a+"-1)"; }
+
namespace prism {
- PrismModulesPrinter::PrismModulesPrinter(const ModelType &modelType, const size_t &numberOfPlayer, const bool enforceOneWays)
- : modelType(modelType), numberOfPlayer(numberOfPlayer), enforceOneWays(enforceOneWays) {
+ PrismModulesPrinter::PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector<Configuration> config, const float probIntended, const float faultyProbability)
+ : os(os), modelType(modelType), maxBoundaries(maxBoundaries), boxes(boxes), balls(balls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), agentNameAndPositionMap(agentNameAndPositionMap), configuration(config), probIntended(probIntended), faultyProbability(faultyProbability) {
+ numberOfPlayer = agentNameAndPositionMap.size();
+ size_t index = 0;
+ for(auto begin = agentNameAndPositionMap.begin(); begin != agentNameAndPositionMap.end(); begin++, index++) {
+ agentIndexMap[begin->first] = index;
+ }
}
- std::ostream& PrismModulesPrinter::printModel(std::ostream &os, const ModelType &modelType) {
+ void PrismModulesPrinter::printModelType(const ModelType &modelType) {
switch(modelType) {
case(ModelType::MDP):
os << "mdp";
@@ -19,610 +35,503 @@ namespace prism {
break;
}
os << "\n\n";
- return os;
- }
-
- std::ostream& PrismModulesPrinter::printBackgroundLabels(std::ostream &os, const AgentName &agentName, const std::pair<Color, cells> &backgroundTiles) {
- if(backgroundTiles.second.size() == 0) return os;
-
- bool first = true;
- std::string color = getColor(backgroundTiles.first);
- color.at(0) = std::toupper(color.at(0));
- os << "formula " << agentName << "On" << color << " = ";
- for(auto const& cell : backgroundTiles.second) {
- if(first) first = false; else os << " | ";
- os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
- }
- os << ";\n";
- os << "label \"" << agentName << "On" << color << "\" = " << agentName << "On" << color << ";\n";
- return os;
}
- std::ostream& PrismModulesPrinter::printRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &cells) {
- bool first = true;
- os << "formula " << agentName << "CannotMove" << direction << " = " ;
- for(auto const& cell : cells) {
- if(first) first = false;
- else os << " | ";
- os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
+ std::ostream& PrismModulesPrinter::print() {
+ for(const auto [agentName, initialPosition] : agentNameAndPositionMap) {
+ agentNameActionMap[agentName] = {};
}
- os << ";\n";
- return os;
- }
- std::ostream& PrismModulesPrinter::printIsOnSlipperyFormula(std::ostream& os, const AgentName &agentName, const std::vector<std::reference_wrapper<cells>> &slipperyCollection, const cells &slipperyNorth, const cells &slipperyEast, const cells &slipperySouth, const cells &slipperyWest) {
- if(std::find_if(slipperyCollection.cbegin(), slipperyCollection.cend(), [=](const std::reference_wrapper<cells>& c) { return !c.get().empty(); }) == slipperyCollection.cend()) {
- os << "formula " << agentName << "IsOnSlippery = false;\n";
- return os;
+ for(const auto &key : keys) {
+ printPortableObjectModule(key);
+ }
+ for(const auto &ball : balls) {
+ printPortableObjectModule(ball);
+ }
+ for(const auto &box : boxes) {
+ printPortableObjectModule(box);
+ }
+ for(const auto &door : unlockedDoors) {
+ printDoorModule(door, true);
+ }
+ for(const auto &door : lockedDoors) {
+ printDoorModule(door, false);
}
- bool first = true;
- os << "formula " << agentName << "IsOnSlippery = ";
-
- for (const auto& slippery: slipperyCollection) {
- for(const auto& cell : slippery.get()) {
- if(first) first = false; else os << " | ";
- os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
- }
+ for(const auto [agentName, initialPosition] : agentNameAndPositionMap) {
+ printRobotModule(agentName, initialPosition);
}
- os << ";\n";
- if(enforceOneWays) {
- first = true;
- os << "formula " << agentName << "IsOnSlipperyNorth = ";
- for (const auto& cell: slipperyNorth) {
- if(first) first = false; else os << " | ";
- os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
- }
- os << ";\n";
- first = true;
- os << "formula " << agentName << "IsOnSlipperyEast = ";
+ if(agentNameAndPositionMap.size() > 1) {
+ printMoveModule();
+ }
- for (const auto& cell: slipperyEast) {
- if(first) first = false; else os << " | ";
- os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
+ if(faultyBehaviour()) {
+ for(const auto [agentName, initialPosition] : agentNameAndPositionMap) {
+ printFaultyMovementModule(agentName);
}
- os << ";\n";
- first = true;
- os << "formula " << agentName << "IsOnSlipperySouth = ";
+ }
- for (const auto& cell: slipperySouth) {
- if(first) first = false; else os << " | ";
- os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
- }
- os << ";\n";
- first = true;
- os << "formula " << agentName << "IsOnSlipperyWest = ";
- for (const auto& cell: slipperyWest) {
- if(first) first = false; else os << " | ";
- os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
+ if(agentNameAndPositionMap.size() > 1) {
+ for(const auto [agentName, index] : agentIndexMap) {
+ printPlayerStruct(agentName);
}
- os << ";\n";
}
- return os;
- }
- std::ostream& PrismModulesPrinter::printIsInLavaFormula(std::ostream& os, const AgentName &agentName, const cells &lava) {
- if(lava.size() == 0) {
- os << "formula " << agentName << "IsInLava = false;\n";
- return os;
- }
- bool first = true;
- os << "formula " << agentName << "IsInLava = ";
- for(auto const& cell : lava) {
- if(first) first = false; else os << " | ";
- os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
- }
- os << ";\n";
- os << "formula " << agentName << "IsInLavaAndNotDone = " << agentName << "IsInLava & !" << agentName << "Done;\n";
- os << "label \"" << agentName << "IsInLavaAndNotDone\" = " << agentName << "IsInLava & !" << agentName << "Done;\n";
return os;
}
- std::ostream& PrismModulesPrinter::printTurningNotAllowedFormulas(std::ostream& os, const AgentName &agentName, const cells &noTurnFloor) {
- if( (!enforceOneWays or noTurnFloor.size() == 0) or (noTurnFloor.size() == 0) ) {
- os << "formula " << agentName << "CannotTurn = false;\n";
- return os;
- }
- bool first = true;
- os << "formula " << agentName << "CannotTurn = ";
- for(auto const& cell : noTurnFloor) {
- if(first) first = false; else os << " | ";
- os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
- }
- os << " | " << agentName << "IsOnSlippery;\n";
- return os;
- }
- std::ostream& PrismModulesPrinter::printIsFixedFormulas(std::ostream& os, const AgentName &agentName) {
- os << "formula " << agentName << "IsFixed = false;\n";
- os << "formula " << agentName << "SlipperyTurnLeftAllowed = true;\n";
- os << "formula " << agentName << "SlipperyTurnRightAllowed = true;\n";
- os << "formula " << agentName << "SlipperyMoveForwardAllowed = true;\n";
- os << "label \"FixedStates\" = " << agentName << "IsFixed | !" << agentName << "SlipperyTurnRightAllowed | !" << agentName << "SlipperyTurnLeftAllowed | !" << agentName << "SlipperyMoveForwardAllowed | " << agentName << "IsInGoal | " << agentName << "IsInLava";
- if(enforceOneWays) {
- os << " | " << agentName << "CannotTurn";
+ void PrismModulesPrinter::printConfiguration(const std::vector<Configuration>& configurations) {
+ for (auto& configuration : configurations) {
+ if (configuration.overwrite_ || configuration.type_ == ConfigType::Module) {
+ continue;
+ }
+ os << configuration.expression_ << std::endl;
}
- os << ";\n";
- //os << "label \"FixedStates\" = " << agentName << "IsFixed | " << agentName << "IsOnSlippery | " << agentName << "IsInGoal | " << agentName << "IsInLava;\n";
-
- return os;
}
-
- std::ostream& PrismModulesPrinter::printWallFormula(std::ostream& os, const AgentName &agentName, const cells &walls) {
- os << "formula " << agentName << "IsOnWall = ";
- bool first = true;
- for(auto const& cell : walls) {
- if(first) first = false; else os << " | ";
- os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
+ void PrismModulesPrinter::printConstants(const std::vector<std::string> &constants) {
+ for (auto& constant : constants) {
+ os << constant << std::endl;
}
- os << ";\n";
- return os;
}
- std::ostream& PrismModulesPrinter::printFormulas(std::ostream& os,
- const AgentName &agentName,
- const cells &restrictionNorth,
- const cells &restrictionEast,
- const cells &restrictionSouth,
- const cells &restrictionWest,
- const std::vector<std::reference_wrapper<cells>> &slipperyCollection,
- const cells &lava,
- const cells &walls,
- const cells &noTurnFloor,
- const cells &slipperyNorth,
- const cells &slipperyEast,
- const cells &slipperySouth,
- const cells &slipperyWest) {
- printRestrictionFormula(os, agentName, "North", restrictionNorth);
- printRestrictionFormula(os, agentName, "East ", restrictionEast);
- printRestrictionFormula(os, agentName, "South", restrictionSouth);
- printRestrictionFormula(os, agentName, "West ", restrictionWest);
- printIsOnSlipperyFormula(os, agentName, slipperyCollection, slipperyNorth, slipperyEast, slipperySouth, slipperyWest);
- printIsInLavaFormula(os, agentName, lava);
- printWallFormula(os, agentName, walls);
- printTurningNotAllowedFormulas(os, agentName, noTurnFloor);
- printIsFixedFormulas(os, agentName);
+ void PrismModulesPrinter::printPortableObjectModule(const cell &object) {
+ std::string identifier = capitalize(object.getColor()) + object.getType();
+ os << "\nmodule " << identifier << std::endl;
+ os << "\tx" << identifier << " : [-1.." << maxBoundaries.second << "] init " << object.column << ";\n";
+ os << "\ty" << identifier << " : [-1.." << maxBoundaries.first << "] init " << object.row << ";\n";
+ os << "\t" << identifier << "PickedUp : bool;\n";
+ os << "\n";
+
+ for(const auto [name, position] : agentNameAndPositionMap) {
+ printPortableObjectActions(name, identifier);
+ }
+ os << "endmodule\n\n";
+ }
+
+ void PrismModulesPrinter::printPortableObjectActions(const std::string &agentName, const std::string &identifier) {
+ std::string actionName = "[" + agentName + "_pickup_" + identifier + "]";
+ agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
+ os << "\t" << actionName << " true -> (x" << identifier << "'=-1) & (y" << identifier << "'=-1) & (" << identifier << "PickedUp'=true);\n";
+ actionName = "[" + agentName + "_drop_" + identifier + "_north]";
+ agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
+ os << "\t" << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << ") & (y" << identifier << "'=y" << agentName << "-1) & (" << identifier << "PickedUp'=false);\n";
+ actionName = "[" + agentName + "_drop_" + identifier + "_west]";
+ agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
+ os << "\t" << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << "-1) & (y" << identifier << "'=y" << agentName << ") & (" << identifier << "PickedUp'=false);\n";
+ actionName = "[" + agentName + "_drop_" + identifier + "_south]";
+ agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
+ os << "\t" << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << ") & (y" << identifier << "'=y" << agentName << "+1) & (" << identifier << "PickedUp'=false);\n";
+ actionName = "[" + agentName + "_drop_" + identifier + "_east]";
+ agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
+ os << "\t" << actionName << " " << " ttrue -> (x" << identifier << "'=x" << agentName << "+1) & (y" << identifier << "'=y" << agentName << ") & (" << identifier << "PickedUp'=false);\n";
+ }
+
+ void PrismModulesPrinter::printDoorModule(const cell &door, const bool &opened) {
+ std::string identifier = capitalize(door.getColor()) + door.getType();
+ os << "\nmodule " << identifier << std::endl;
+ os << "\t" << identifier << "Open : bool init false;\n";
os << "\n";
- return os;
- }
- std::ostream& PrismModulesPrinter::printGoalLabel(std::ostream& os, const AgentName &agentName, const cells &goals) {
- if(goals.size() == 0) {
- os << "formula " << agentName << "IsInGoal = false;\n";
- return os;
+ if(opened) {
+ for(const auto [name, position] : agentNameAndPositionMap) {
+ printUnlockedDoorActions(name, identifier);
+ }
+ } else {
+ for(const auto [name, position] : agentNameAndPositionMap) {
+ printLockedDoorActions(name, identifier);
+ }
}
+ os << "endmodule\n\n";
+ }
- bool first = true;
- os << "formula " << agentName << "IsInGoal = ";
- for(auto const& cell : goals) {
- if(first) first = false; else os << " | ";
- os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
- }
- os << ";\n";
- os << "formula " << agentName << "IsInGoalAndNotDone = " << agentName << "IsInGoal & !" << agentName << "Done;\n";
- os << "label \"" << agentName << "IsInGoalAndNotDone\" = " << agentName << "IsInGoal & !" << agentName << "Done;\n";
- return os;
+ void PrismModulesPrinter::printLockedDoorActions(const std::string &agentName, const std::string &identifier) {
+ std::string actionName = "[" + agentName + "_unlock_" + identifier + "]";
+ agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
+ os << "\t" << actionName << " !" << identifier << "Open -> (" << identifier << "Open'=true);\n";
+ actionName = "[" + agentName + "_close_" + identifier + "]";
+ agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
+ os << "\t" << actionName << " " << identifier << "Open -> (" << identifier << "Open'=false);\n";
}
- std::ostream& PrismModulesPrinter::printCrashLabel(std::ostream &os, const std::vector<AgentName> agentNames) {
- os << "label crash = ";
- bool first = true;
- for(auto const& agentName : agentNames) {
- if(agentName == "Agent") continue;
- if(first) first = false; else os << " | ";
- os << "(xAgent=x" << agentName << ")&(yAgent=y" << agentName << ")";
- }
- os << ";\n\n";
- return os;
+ void PrismModulesPrinter::printUnlockedDoorActions(const std::string &agentName, const std::string &identifier) {
+ std::string actionName = "[" + agentName + "_open_" + identifier + "]";
+ agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
+ os << "\t !" << identifier << "Open -> (" << identifier << "Open'=true);\n";
+ actionName = "[" + agentName + "_close_" + identifier + "]";
+ agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
+ os << "\t" << agentName << " " << identifier << "Open -> (" << identifier << "Open'=false);\n";
}
- std::ostream& PrismModulesPrinter::printAvoidanceLabel(std::ostream &os, const std::vector<AgentName> agentNames, const int &distance) {
- os << "label avoidance = ";
- bool first = true;
- for(auto const& agentName : agentNames) {
- if(agentName == "Agent") continue;
- if(first) first = false; else os << " | ";
- os << "max(xAgent-x" << agentName << ",x" << agentName << "-xAgent)+";
- os << "max(yAgent-y" << agentName << ",y" << agentName << "-yAgent) ";
+ void PrismModulesPrinter::printRobotModule(const AgentName &agentName, const coordinates &initialPosition) {
+ os << "\nmodule " << agentName << std::endl;
+ os << "\tx" << agentName << " : [0.." << maxBoundaries.second << "] init " << initialPosition.second << ";\n";
+ os << "\ty" << agentName << " : [0.." << maxBoundaries.first << "] init " << initialPosition.first << ";\n";
+ os << "\tview" << agentName << " : [0..3] init 1;\n";
+
+ printTurnActionsForRobot(agentName);
+ printMovementActionsForRobot(agentName);
+ if(slipperyBehaviour()) printSlipperyMovementActionsForRobot(agentName);
+
+ for(const auto &door : unlockedDoors) {
+ std::string identifier = capitalize(door.getColor()) + door.getType();
+ printUnlockedDoorActionsForRobot(agentName, identifier);
}
- os << ";\n\n";
- return os;
- }
- // TODO this does not account for multiple agents yet, i.e. key can be picked up multiple times
- std::ostream& PrismModulesPrinter::printKeysLabels(std::ostream& os, const AgentName &agentName, const cells &keys) {
- if(keys.size() == 0) return os;
+ for(const auto &door : lockedDoors) {
+ std::string identifier = capitalize(door.getColor()) + door.getType();
+ std::string key = capitalize(door.getColor()) + "Key";
+ printLockedDoorActionsForRobot(agentName, identifier, key);
+ }
- for(auto const& key : keys) {
- int xKey = key.getCoordinates().first;
- int yKey = key.getCoordinates().second;
- std::string keyColor = key.getColor();
- os << "label \"" << agentName << "PickedUp" << keyColor << "Key\" = " << agentName << "_has_" << keyColor << "_key = true;\n";
- os << "formula " << agentName << "CanPickUp" << keyColor << "Key = ";
- os << "((x" << agentName << "-1 = " << xKey << "&y" << agentName << " = " << yKey << "&view" << agentName << " = 1) |";
- os << " (x" << agentName << "+1 = " << xKey << "&y" << agentName << " = " << yKey << "&view" << agentName << " = 3) |";
- os << " (x" << agentName << " = " << xKey << "&y" << agentName << "-1 = " << yKey << "&view" << agentName << " = 0) |";
- os << " (x" << agentName << " = " << xKey << "&y" << agentName << "+1 = " << yKey << "&view" << agentName << " = 2) ) &";
- os << "!" << agentName << "_has_" << keyColor << "_key;";
+ for(const auto &key : keys) {
+ std::string identifier = capitalize(key.getColor()) + key.getType();
+ os << "\t" << agentName << "Carrying" << identifier << " : bool init false;\n";
+ printPortableObjectActionsForRobot(agentName, identifier);
}
- os << "\n";
- return os;
- }
- std::ostream& PrismModulesPrinter::printBooleansForKeys(std::ostream &os, const AgentName &agentName, const cells &keys) {
- for(auto const& key : keys) {
- os << "\t" << agentName << "_has_"<< key.getColor() << "_key : bool init false;\n";
+ for(const auto &ball : balls) {
+ std::string identifier = capitalize(ball.getColor()) + ball.getType();
+ os << "\t" << agentName << "Carrying" << identifier << " : bool init false;\n";
+ printPortableObjectActionsForRobot(agentName, identifier);
}
- os << "\n";
- return os;
- }
- std::ostream& PrismModulesPrinter::printBooleansForBackground(std::ostream &os, const AgentName &agentName, const std::map<Color, cells> &backgroundTiles) {
- for(auto const& [color, cells] : backgroundTiles) {
- if(cells.size() == 0) continue;
- std::string c = getColor(color);
- c.at(0) = std::toupper(c.at(0));
- os << "\t" << agentName << "_picked_up_" << c << " : bool init false;\n";
+ for(const auto &box : boxes) {
+ std::string identifier = capitalize(box.getColor()) + box.getType();
+ os << "\t" << agentName << "Carrying" << identifier << " : bool init false;\n";
+ printPortableObjectActionsForRobot(agentName, identifier);
}
- os << "\n";
- return os;
+
+ os << "\n" << actionStream.str();
+ actionStream.str(std::string());
+ os << "endmodule\n\n";
}
- std::ostream& PrismModulesPrinter::printActionsForKeys(std::ostream &os, const AgentName &agentName, const cells &keys) {
- for(auto const& key : keys) {
- std::string keyColor = key.getColor();
- os << "\t[pickup_" << keyColor << "_key] " << agentName << "CanPickUp" << keyColor << "Key -> ";
- os << "(" << agentName << "_has_" << keyColor << "_key'=true);";
- }
- os << "\n";
- return os;
+ void PrismModulesPrinter::printPortableObjectActionsForRobot(const std::string &a, const std::string &i) {
+ actionStream << "\t[" << a << "_pickup_" << i << "] " << " !" << a << "IsCarrying & " << a << "CannotMove" << i << " -> (" << a << "Carrying" << i << "'=true);\n";
+ actionStream << "\t[" << a << "_drop_" << i << "_north]\t" << a << "Carrying" << i << " & view" << a << "=3 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveNorthWall -> (" << a << "Carrying" << i << "'=false);\n";
+ actionStream << "\t[" << a << "_drop_" << i << "_west] \t" << a << "Carrying" << i << " & view" << a << "=2 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveWestWall -> (" << a << "Carrying" << i << "'=false);\n";
+ actionStream << "\t[" << a << "_drop_" << i << "_south]\t" << a << "Carrying" << i << " & view" << a << "=1 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveSouthWall -> (" << a << "Carrying" << i << "'=false);\n";
+ actionStream << "\t[" << a << "_drop_" << i << "_east] \t" << a << "Carrying" << i << " & view" << a << "=0 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveEastWall -> (" << a << "Carrying" << i << "'=false);\n";
+ actionStream << "\n";
}
- std::ostream& PrismModulesPrinter::printActionsForBackground(std::ostream &os, const AgentName &agentName, const std::map<Color, cells> &backgroundTiles) {
- for(auto const& [color, cells] : backgroundTiles) {
- if(cells.size() == 0) continue;
- std::string c = getColor(color);
- c.at(0) = std::toupper(c.at(0));
- os << "\t[" << agentName << "_pickup_" << c << "] " << agentName << "On" << c << " & !" << agentName << "_picked_up_" << c << " -> ";
- os << "(" << agentName << "_picked_up_" << c << "'=true);\n";
- }
- os << "\n";
- return os;
+ void PrismModulesPrinter::printUnlockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier) {
+ actionStream << "\t[" << agentName << "_open_" << identifier << "] " << agentName << "CannotMove" << identifier << " -> true;\n";
+ actionStream << "\t[" << agentName << "_close_" << identifier << "] " << agentName << "IsNextTo" << identifier << " -> true;\n";
+ actionStream << "\n";
}
- std::ostream& PrismModulesPrinter::printInitStruct(std::ostream &os, const AgentName &agentName) {
- os << "init\n";
- os << "\t(!AgentIsInGoal & !AgentIsInLava & !AgentDone & !AgentIsOnWall)";
- if(enforceOneWays) {
- os << " & ( !AgentCannotTurn ) ";
- } else {
- os << " & ( !AgentIsOnSlippery ) ";
- }
- os << "\nendinit\n\n";
+ void PrismModulesPrinter::printLockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier, const std::string &key) {
+ actionStream << "\t[" << agentName << "_unlock_" << identifier << "] " << agentName << "CannotMove" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n";
+ actionStream << "\t[" << agentName << "_close_" << identifier << "] " << agentName << "IsNextTo" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n";
+ actionStream << "\n";
+ }
- return os;
+ void PrismModulesPrinter::printTurnActionsForRobot(const AgentName &a) {
+ actionStream << printTurnGuard(a, "right", RIGHT, "true") << printTurnUpdate(a, {1.0, "(view"+a+"'=mod(view"+a+"+1,4))"}, RIGHT);
+ actionStream << printTurnGuard(a, "left", LEFT, "view"+a+">0") << printTurnUpdate(a, {1.0, "(view"+a+"'=view"+a+"-1)"}, LEFT);
+ actionStream << printTurnGuard(a, "left", LEFT, "view"+a+"=0") << printTurnUpdate(a, {1.0, "(view"+a+"'=3)"}, LEFT);
}
- std::ostream& PrismModulesPrinter::printModule(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const coordinates &boundaries, const coordinates& initialPosition, const cells &keys, const std::map<Color, cells> &backgroundTiles, const bool agentWithView, const std::vector<float> &probabilities) {
- os << "module " << agentName << "\n";
- os << "\tx" << agentName << " : [1.." << boundaries.second << "];\n";
- os << "\ty" << agentName << " : [1.." << boundaries.first << "];\n";
- printBooleansForKeys(os, agentName, keys);
- printBooleansForBackground(os, agentName, backgroundTiles);
- os << "\t" << agentName << "Done : bool;\n";
- if(agentWithView) {
- os << "\tview" << agentName << " : [0..3];\n";
- os << "\n";
- os << "\t[" << agentName << "_turn_right] " << moveGuard(agentIndex) << " !" << agentName << "CannotTurn & " << " !" << agentName << "IsFixed & " << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & !" << agentName << "IsOnSlippery -> (view" << agentName << "'=mod(view" << agentName << " + 1, 4)) " << moveUpdate(agentIndex) << ";\n";
- os << "\t[" << agentName << "_turn_left] " << moveGuard(agentIndex) << " !" << agentName << "CannotTurn & " << " !" << agentName << "IsFixed & " << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & !" << agentName << "IsOnSlippery & view" << agentName << ">0 -> (view" << agentName << "'=view" << agentName << " - 1) " << moveUpdate(agentIndex) << ";\n";
- os << "\t[" << agentName << "_turn_left] " << moveGuard(agentIndex) << " !" << agentName << "CannotTurn & " << " !" << agentName << "IsFixed & " << " !" << agentName << "IsInGoal & !" << agentName << "IsInLava & !" << agentName << "IsOnSlippery & view" << agentName << "=0 -> (view" << agentName << "'=3) " << moveUpdate(agentIndex) << ";\n";
- if(enforceOneWays) {
- os << "\t[" << agentName << "_stuck] !" << agentName << "IsFixed & " << agentName << "CannotTurn & view" << agentName << " = 0 & " << agentName << "CannotMoveEast -> true;\n";
- os << "\t[" << agentName << "_stuck] !" << agentName << "IsFixed & " << agentName << "CannotTurn & view" << agentName << " = 1 & " << agentName << "CannotMoveSouth -> true;\n";
- os << "\t[" << agentName << "_stuck] !" << agentName << "IsFixed & " << agentName << "CannotTurn & view" << agentName << " = 2 & " << agentName << "CannotMoveWest -> true;\n";
- os << "\t[" << agentName << "_stuck] !" << agentName << "IsFixed & " << agentName << "CannotTurn & view" << agentName << " = 3 & " << agentName << "CannotMoveNorth -> true;\n";
- }
- } else {
- os << "\t[" << agentName << "_turns] " << " !" << agentName << "CannotTurn & " << " !" << agentName << "IsFixed & " << moveGuard(agentIndex) << " true -> (x" << agentName << "'=x" << agentName << ")" << moveUpdate(agentIndex) << ";\n";
+ void PrismModulesPrinter::printMovementActionsForRobot(const AgentName &a) {
+ actionStream << printMovementGuard(a, "North", 3) << printMovementUpdate(a, {1.0, northUpdate(a)});
+ actionStream << printMovementGuard(a, "East", 0) << printMovementUpdate(a, {1.0, eastUpdate(a)});
+ actionStream << printMovementGuard(a, "South", 1) << printMovementUpdate(a, {1.0, southUpdate(a)});
+ actionStream << printMovementGuard(a, "West", 2) << printMovementUpdate(a, {1.0, westUpdate(a)});
+ if(faultyBehaviour()) {
+ std::string actionName = "[" + a + "_stuck]";
+ agentNameActionMap.at(a).insert({FORWARD, actionName});
+ actionStream << "\t" << actionName << " " << "previousAction" << a << "=" << std::to_string(FORWARD);
+ actionStream << " & ((view" << a << "=0 & " << a << "CannotMoveEastWall) |";
+ actionStream << " (view" << a << "=1 & " << a << "CannotMoveSouthWall) |";
+ actionStream << " (view" << a << "=2 & " << a << "CannotMoveWestWall) |";
+ actionStream << " (view" << a << "=3 & " << a << "CannotMoveNorthWall) ) -> true;\n";
}
- printActionsForKeys(os, agentName, keys);
- printActionsForBackground(os, agentName, backgroundTiles);
- os << "\n";
- printMovementActions(os, agentName, agentIndex, agentWithView);
- for(auto const& probability : probabilities) {
- printMovementActions(os, agentName, agentIndex, agentWithView, probability);
- }
- printDoneActions(os, agentName, agentIndex);
- os << "\n";
- return os;
}
- std::ostream& PrismModulesPrinter::printMovementActions(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const bool agentWithView, const float &probability) {
- if(probability >= 1) {
- os << "\t[" << agentName << "_move_north]" << moveGuard(agentIndex) << viewVariable(agentName, 3, agentWithView) << " !" << agentName << "IsFixed & " << " !" << agentName << "IsOnSlippery & !" << agentName << "IsInLava &!" << agentName << "IsInGoal & !" << agentName << "CannotMoveNorth -> (y" << agentName << "'=y" << agentName << "-1)" << moveUpdate(agentIndex) << ";\n";
- os << "\t[" << agentName << "_move_east] " << moveGuard(agentIndex) << viewVariable(agentName, 0, agentWithView) << " !" << agentName << "IsFixed & " << " !" << agentName << "IsOnSlippery & !" << agentName << "IsInLava &!" << agentName << "IsInGoal & !" << agentName << "CannotMoveEast -> (x" << agentName << "'=x" << agentName << "+1)" << moveUpdate(agentIndex) << ";\n";
- os << "\t[" << agentName << "_move_south]" << moveGuard(agentIndex) << viewVariable(agentName, 1, agentWithView) << " !" << agentName << "IsFixed & " << " !" << agentName << "IsOnSlippery & !" << agentName << "IsInLava &!" << agentName << "IsInGoal & !" << agentName << "CannotMoveSouth -> (y" << agentName << "'=y" << agentName << "+1)" << moveUpdate(agentIndex) << ";\n";
- os << "\t[" << agentName << "_move_west] " << moveGuard(agentIndex) << viewVariable(agentName, 2, agentWithView) << " !" << agentName << "IsFixed & " << " !" << agentName << "IsOnSlippery & !" << agentName << "IsInLava &!" << agentName << "IsInGoal & !" << agentName << "CannotMoveWest -> (x" << agentName << "'=x" << agentName << "-1)" << moveUpdate(agentIndex) << ";\n";
- } else {
- std::string probabilityString = std::to_string(probability);
- std::string percentageString = std::to_string((int)(100 * probability));
- std::string complementProbabilityString = std::to_string(1 - probability);
- os << "\t[" << agentName << "_move_north_" << percentageString << "] ";
- os << moveGuard(agentIndex) << viewVariable(agentName, 3, agentWithView) << " !" << agentName << "IsFixed & " << " !" << agentName << "IsOnSlippery & !" << agentName << "IsInLava & !" << agentName << "CannotMoveNorth -> ";
- os << probabilityString << ": (y" << agentName << "'=y" << agentName << "-1)" << moveUpdate(agentIndex) << " + ";
- os << complementProbabilityString << ": (y" << agentName << "'=y" << agentName << ") " << moveUpdate(agentIndex) << ";\n";
-
- os << "\t[" << agentName << "_move_east_" << percentageString << "] ";
- os << moveGuard(agentIndex) << viewVariable(agentName, 0, agentWithView) << " !" << agentName << "IsFixed & " << " !" << agentName << "IsOnSlippery & !" << agentName << "IsInLava & !" << agentName << "CannotMoveEast -> ";
- os << probabilityString << ": (x" << agentName << "'=x" << agentName << "+1)" << moveUpdate(agentIndex) << " + ";
- os << complementProbabilityString << ": (x" << agentName << "'=x" << agentName << ") " << moveUpdate(agentIndex) << ";\n";
-
- os << "\t[" << agentName << "_move_south_" << percentageString << "] ";
- os << moveGuard(agentIndex) << viewVariable(agentName, 1, agentWithView) << " !" << agentName << "IsFixed & " << " !" << agentName << "IsOnSlippery & !" << agentName << "IsInLava & !" << agentName << "CannotMoveSouth -> ";
- os << probabilityString << ": (y" << agentName << "'=y" << agentName << "+1)" << moveUpdate(agentIndex) << " + ";
- os << complementProbabilityString << ": (y" << agentName << "'=y" << agentName << ") " << moveUpdate(agentIndex) << ";\n";
-
- os << "\t[" << agentName << "_move_west_" << percentageString << "] ";
- os << moveGuard(agentIndex) << viewVariable(agentName, 2, agentWithView) << " !" << agentName << "IsFixed & " << " !" << agentName << "IsOnSlippery & !" << agentName << "IsInLava & !" << agentName << "CannotMoveWest -> ";
- os << probabilityString << ": (x" << agentName << "'=x" << agentName << "-1)" << moveUpdate(agentIndex) << " + ";
- os << complementProbabilityString << ": (x" << agentName << "'=x" << agentName << ") " << moveUpdate(agentIndex) << ";\n";
- }
- return os;
+ std::string PrismModulesPrinter::printMovementGuard(const AgentName &a, const std::string &direction, const size_t &viewDirection) {
+ std::string actionName = "[" + a + "_move_" + direction + "]";
+ agentNameActionMap.at(a).insert({FORWARD, actionName});
+ return "\t" + actionName + " " + viewVariable(a, viewDirection) + " !" + a + "IsOnSlippery & !" + a + "IsOnLava & !" + a + "IsOnGoal & !" + a + "CannotMove" + direction + "Wall &!" + a + "CannotMoveConditionally -> ";
}
- std::ostream& PrismModulesPrinter::printDoneActions(std::ostream &os, const AgentName &agentName, const size_t &agentIndex) {
- os << "\t[" << agentName << "_done]" << moveGuard(agentIndex) << agentName << "IsInGoal | " << agentName << "IsInLava -> (" << agentName << "Done'=true);\n";
- return os;
+ std::string PrismModulesPrinter::printMovementUpdate(const AgentName &a, const update &u) const {
+ return updateToString(u) + ";\n";
}
- std::ostream& PrismModulesPrinter::printSlipperyTurn(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const coordinates &c, std::set<std::string> &slipperyActions, const std::array<bool, 8>& neighborhood, SlipperyType orientation) {
- constexpr std::size_t PROB_PIECES = 9, ALL_POSS_DIRECTIONS = 9;
+ std::string PrismModulesPrinter::printTurnGuard(const AgentName &a, const std::string &direction, const ActionId &actionId, const std::string &cond) {
+ std::string actionName = "[" + a + "_turn_" + direction + "]";
+ agentNameActionMap.at(a).insert({actionId, actionName});
+ return "\t" + actionName + " " + cond + " -> ";
+ }
- std::array<std::string, ALL_POSS_DIRECTIONS> positionTransition = {
- /* north */ "(y" + agentName + "'=y" + agentName + "-1)",
- /* north east */ "(x" + agentName + "'=x" + agentName + "+1) & (y" + agentName + "'=y" + agentName + "-1)",
- /* east */ "(x" + agentName + "'=x" + agentName + "+1)",
- /* east south */ "(x" + agentName + "'=x" + agentName + "+1) & (y" + agentName + "'=y" + agentName + "+1)",
- /* south */ "(y" + agentName + "'=y" + agentName + "+1)",
- /* south west */ "(x" + agentName + "'=x" + agentName + "-1) & (y" + agentName + "'=y" + agentName + "+1)",
- /* west */ "(x" + agentName + "'=x" + agentName + "-1)",
- /* north west */ "(x" + agentName + "'=x" + agentName + "-1) & (y" + agentName + "'=y" + agentName + "-1)",
- /* own position */ "(x" + agentName + "'=x" + agentName + ") & (y" + agentName + "'=y" + agentName + ")"
- };
+ std::string PrismModulesPrinter::printTurnUpdate(const AgentName &a, const update &u, const ActionId &actionId) const {
+ return updateToString(u) + ";\n";
+ }
- // view transition appdx in form (guard, update part)
- // IMPORTANT: No mod() usage for turn left due to bug in mod() function for decrement
+ void PrismModulesPrinter::printSlipperyMovementActionsForRobot(const AgentName &a) {
+ if(!slipperyTiles.at("North").empty()) {
+ printSlipperyMovementActionsForNorth(a);
+ printSlipperyTurnActionsForNorth(a);
+ }
+ if(!slipperyTiles.at("East").empty()) {
+ printSlipperyMovementActionsForEast(a) ;
+ printSlipperyTurnActionsForEast(a);
+ }
+ if(!slipperyTiles.at("South").empty()) {
+ printSlipperyMovementActionsForSouth(a);
+ printSlipperyTurnActionsForSouth(a);
+ }
+ if(!slipperyTiles.at("West").empty()) {
+ printSlipperyMovementActionsForWest(a) ;
+ printSlipperyTurnActionsForWest(a);
+ }
+ }
- std::array<std::pair<std::string, std::string>, 3> viewTransition = {
- /* turn to right */ std::make_pair(" & " + agentName + "SlipperyTurnRightAllowed ", " & (view" + agentName + "'=mod(view" + agentName + " + 1, 4))"),
- /* turn to left */ std::make_pair(" & " + agentName + "SlipperyTurnLeftAllowed & view" + agentName + ">0", " & (view" + agentName + "'=view" + agentName + " - 1)"),
- /* turn to left */ std::make_pair(" & " + agentName + "SlipperyTurnLeftAllowed & view" + agentName + "=0", " & (view" + agentName + "'=3)")
- };
+ void PrismModulesPrinter::printSlipperyMovementActionsForNorth(const AgentName &a) {
+ actionStream << printSlipperyMovementGuard(a, "North", 3, { "CanSlipNorth", "CanSlipNorthEast", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, northUpdate(a)}, {(1 - probIntended) * 1/2, northUpdate(a)+"&"+eastUpdate(a)}, {(1 - probIntended) * 1/2, northUpdate(a)+"&"+westUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "North", 3, {"!CanSlipNorth", "CanSlipNorthEast", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1/2, northUpdate(a)+"&"+eastUpdate(a)}, {1/2, northUpdate(a)+"&"+westUpdate(a)} });
+ actionStream << printSlipperyMovementGuard(a, "North", 3, { "CanSlipNorth", "!CanSlipNorthEast", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, northUpdate(a)}, {(1 - probIntended), northUpdate(a)+"&"+westUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "North", 3, { "CanSlipNorth", "CanSlipNorthEast", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, northUpdate(a)}, {(1 - probIntended), northUpdate(a)+"&"+eastUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "North", 3, {"!CanSlipNorth", "!CanSlipNorthEast", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1, northUpdate(a)+"&"+westUpdate(a) } }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "North", 3, { "CanSlipNorth", "!CanSlipNorthEast", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1, northUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "North", 3, {"!CanSlipNorth", "CanSlipNorthEast", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1, northUpdate(a)+"&"+eastUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "North", 3, {"!CanSlipNorth", "!CanSlipNorthEast", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", {}) << "\n";
- // direction specifics
+ actionStream << printSlipperyMovementGuard(a, "North", 2, { "CanSlipWest", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, westUpdate(a) }, {1 - probIntended, westUpdate(a)+"&"+northUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "North", 2, {"!CanSlipWest", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1, westUpdate(a)+"&"+northUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "North", 2, { "CanSlipWest", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1, westUpdate(a) } }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "North", 2, {"!CanSlipWest", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", {}) << "\n";
- std::string actionName;
- std::size_t remainPosIndex = 8;
- std::array<std::size_t, ALL_POSS_DIRECTIONS> prob_piece_dir; // { n, ne, w, se, s, sw, w, nw, CURRENT POS }
+ actionStream << printSlipperyMovementGuard(a, "North", 0, { "CanSlipEast", "CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, eastUpdate(a) }, {1 - probIntended, eastUpdate(a)+"&"+northUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "North", 0, {"!CanSlipEast", "CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "North", { {1, eastUpdate(a)+"&"+northUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "North", 0, { "CanSlipEast", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "North", { {1, eastUpdate(a) } }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "North", 0, {"!CanSlipEast", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "North", {}) << "\n";
+
+ actionStream << printSlipperyMovementGuard(a, "North", 1, { "CanSlipSouth", "CanSlipNorth"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, southUpdate(a) }, {1 - probIntended, northUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "North", 1, {"!CanSlipSouth", "CanSlipNorth"}) << printSlipperyMovementUpdate(a, "North", { {1, northUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "North", 1, { "CanSlipSouth", "!CanSlipNorth"}) << printSlipperyMovementUpdate(a, "North", { {1, southUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "North", 1, {"!CanSlipSouth", "!CanSlipNorth"}) << printSlipperyMovementUpdate(a, "North", {}) << "\n";
+ }
- switch (orientation)
- {
- case SlipperyType::North:
- actionName = "\t[" + agentName + "turn_at_slip_north]";
- prob_piece_dir = { 0, 0, 0, 1, 1, 1, 0, 0, 0 /* <- R */ };
- break;
+ void PrismModulesPrinter::printSlipperyMovementActionsForEast(const AgentName &a) {
+ actionStream << printSlipperyMovementGuard(a, "East", 0, { "CanSlipEast", "CanSlipSouthEast", "CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a)}, {(1 - probIntended) * 1/2, eastUpdate(a)+"&"+southUpdate(a)}, {(1 - probIntended) * 1/2, eastUpdate(a)+"&"+northUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "East", 0, {"!CanSlipEast", "CanSlipSouthEast", "CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1/2, eastUpdate(a)+"&"+southUpdate(a)}, {1/2, eastUpdate(a)+"&"+northUpdate(a)} });
+ actionStream << printSlipperyMovementGuard(a, "East", 0, { "CanSlipEast", "!CanSlipSouthEast", "CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a)}, {(1 - probIntended), eastUpdate(a)+"&"+northUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "East", 0, { "CanSlipEast", "CanSlipSouthEast", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a)}, {(1 - probIntended), eastUpdate(a)+"&"+southUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "East", 0, {"!CanSlipEast", "!CanSlipSouthEast", "CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)+"&"+northUpdate(a) } }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "East", 0, { "CanSlipEast", "!CanSlipSouthEast", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "East", 0, {"!CanSlipEast", "CanSlipSouthEast", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)+"&"+southUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "East", 0, {"!CanSlipEast", "!CanSlipSouthEast", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", {}) << "\n";
- case SlipperyType::South:
- actionName = "\t[" + agentName + "turn_at_slip_south]";
- prob_piece_dir = { 1, 1, 0, 0, 0, 0, 0, 1, 0 /* <- R */ };
- break;
+ actionStream << printSlipperyMovementGuard(a, "East", 3, { "CanSlipNorth", "CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, northUpdate(a) }, {1 - probIntended, eastUpdate(a)+"&"+northUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "East", 3, {"!CanSlipNorth", "CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)+"&"+northUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "East", 3, { "CanSlipNorth", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, northUpdate(a) } }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "East", 3, {"!CanSlipNorth", "!CanSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", {}) << "\n";
+
+ actionStream << printSlipperyMovementGuard(a, "East", 1, { "CanSlipSouth", "CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, southUpdate(a) }, {1 - probIntended, eastUpdate(a)+"&"+southUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "East", 1, {"!CanSlipSouth", "CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)+"&"+southUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "East", 1, { "CanSlipSouth", "!CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, southUpdate(a) } }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "East", 1, {"!CanSlipSouth", "!CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", {}) << "\n";
+
+ actionStream << printSlipperyMovementGuard(a, "East", 2, { "CanSlipWest", "CanSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a) }, {1 - probIntended, westUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "East", 2, {"!CanSlipWest", "CanSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "East", 2, { "CanSlipWest", "!CanSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {1, westUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "East", 2, {"!CanSlipWest", "!CanSlipEast"}) << printSlipperyMovementUpdate(a, "East", {}) << "\n";
+ }
- case SlipperyType::East:
- actionName = "\t[" + agentName + "turn_at_slip_east]";
- prob_piece_dir = { 0, 0, 0, 0, 0, 1, 1, 1, 0 /* <- R */ };
- break;
+ void PrismModulesPrinter::printSlipperyMovementActionsForSouth(const AgentName &a) {
+ actionStream << printSlipperyMovementGuard(a, "South", 1, { "CanSlipSouth", "CanSlipSouthEast", "CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a)}, {(1 - probIntended) * 1/2, southUpdate(a)+"&"+eastUpdate(a)}, {(1 - probIntended) * 1/2, southUpdate(a)+"&"+westUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "South", 1, {"!CanSlipSouth", "CanSlipSouthEast", "CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1/2, southUpdate(a)+"&"+eastUpdate(a)}, {1/2, southUpdate(a)+"&"+westUpdate(a)} });
+ actionStream << printSlipperyMovementGuard(a, "South", 1, { "CanSlipSouth", "!CanSlipSouthEast", "CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a)}, {(1 - probIntended), southUpdate(a)+"&"+westUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "South", 1, { "CanSlipSouth", "CanSlipSouthEast", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a)}, {(1 - probIntended), southUpdate(a)+"&"+eastUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "South", 1, {"!CanSlipSouth", "!CanSlipSouthEast", "CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1, southUpdate(a)+"&"+westUpdate(a) } }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "South", 1, { "CanSlipSouth", "!CanSlipSouthEast", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1, southUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "South", 1, {"!CanSlipSouth", "CanSlipSouthEast", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1, southUpdate(a)+"&"+eastUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "South", 1, {"!CanSlipSouth", "!CanSlipSouthEast", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", {}) << "\n";
- case SlipperyType::West:
- actionName = "\t[" + agentName + "turn_at_slip_west]";
- prob_piece_dir = { 0, 1, 1, 1, 0, 0, 0, 0, 0 /* <- R */ };
- break;
- }
+ actionStream << printSlipperyMovementGuard(a, "South", 2, { "CanSlipWest", "CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, westUpdate(a) }, {1 - probIntended, westUpdate(a)+"&"+southUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "South", 2, {"!CanSlipWest", "CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1, westUpdate(a)+"&"+southUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "South", 2, { "CanSlipWest", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1, westUpdate(a) } }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "South", 2, {"!CanSlipWest", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", {}) << "\n";
- slipperyActions.insert(actionName);
+ actionStream << printSlipperyMovementGuard(a, "South", 0, { "CanSlipEast", "CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, eastUpdate(a) }, {1 - probIntended, eastUpdate(a)+"&"+southUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "South", 0, {"!CanSlipEast", "CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "South", { {1, eastUpdate(a)+"&"+southUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "South", 0, { "CanSlipEast", "!CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "South", { {1, eastUpdate(a) } }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "South", 0, {"!CanSlipEast", "!CanSlipSouthEast"}) << printSlipperyMovementUpdate(a, "South", {}) << "\n";
- // override probability to 0 if corresp. direction is blocked
+ actionStream << printSlipperyMovementGuard(a, "South", 3, { "CanSlipSouth", "CanSlipNorth"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a) }, {1 - probIntended, northUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "South", 3, {"!CanSlipSouth", "CanSlipNorth"}) << printSlipperyMovementUpdate(a, "South", { {1, northUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "South", 3, { "CanSlipSouth", "!CanSlipNorth"}) << printSlipperyMovementUpdate(a, "South", { {1, southUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "South", 3, {"!CanSlipSouth", "!CanSlipNorth"}) << printSlipperyMovementUpdate(a, "South", {}) << "\n";
+ }
- for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS - 1; i++) {
- if (!neighborhood.at(i))
- prob_piece_dir.at(i) = 0;
- }
+ void PrismModulesPrinter::printSlipperyMovementActionsForWest(const AgentName &a) {
+ actionStream << printSlipperyMovementGuard(a, "West", 2, { "CanSlipWest", "CanSlipSouthWest", "CanSlipNorthWest"}) << 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, {"!CanSlipWest", "CanSlipSouthWest", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1/2, westUpdate(a)+"&"+southUpdate(a)}, {1/2, westUpdate(a)+"&"+northUpdate(a)} });
+ actionStream << printSlipperyMovementGuard(a, "West", 2, { "CanSlipWest", "!CanSlipSouthWest", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a)}, {(1 - probIntended), westUpdate(a)+"&"+northUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "West", 2, { "CanSlipWest", "CanSlipSouthWest", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a)}, {(1 - probIntended), westUpdate(a)+"&"+southUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "West", 2, {"!CanSlipWest", "!CanSlipSouthWest", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)+"&"+northUpdate(a) } }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "West", 2, { "CanSlipWest", "!CanSlipSouthWest", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "West", 2, {"!CanSlipWest", "CanSlipSouthWest", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)+"&"+southUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "West", 2, {"!CanSlipWest", "!CanSlipSouthWest", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", {}) << "\n";
- // determine residual probability (R) by replacing 0 with (1 - overall sum)
+ actionStream << printSlipperyMovementGuard(a, "West", 3, { "CanSlipNorth", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, northUpdate(a) }, {1 - probIntended, westUpdate(a)+"&"+northUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "West", 3, {"!CanSlipNorth", "CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)+"&"+northUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "West", 3, { "CanSlipNorth", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a) } }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "West", 3, {"!CanSlipNorth", "!CanSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", {}) << "\n";
- prob_piece_dir.at(remainPosIndex) = PROB_PIECES - std::accumulate(prob_piece_dir.begin(), prob_piece_dir.end(), 0);
+ actionStream << printSlipperyMovementGuard(a, "West", 1, { "CanSlipSouth", "CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, southUpdate(a) }, {1 - probIntended, westUpdate(a)+"&"+southUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "West", 1, {"!CanSlipSouth", "CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)+"&"+southUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "West", 1, { "CanSlipSouth", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, southUpdate(a) } }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "West", 1, {"!CanSlipSouth", "!CanSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", {}) << "\n";
- // <DEBUG_AREA>
- {
- assert(prob_piece_dir.at(remainPosIndex) <= 9 && prob_piece_dir.at(remainPosIndex) >= 6 && "Value not in Range!");
- assert(std::accumulate(prob_piece_dir.begin(), prob_piece_dir.end(), 0) == PROB_PIECES && "Does not sum up to 1!");
- }
- // </DEBUG_AREA>
+ actionStream << printSlipperyMovementGuard(a, "West", 0, { "CanSlipEast", "CanSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a) }, {1 - probIntended, eastUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "West", 0, {"!CanSlipEast", "CanSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "West", 0, { "CanSlipEast", "!CanSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {1, eastUpdate(a)} }) << "\n";
+ actionStream << printSlipperyMovementGuard(a, "West", 0, {"!CanSlipEast", "!CanSlipWest"}) << printSlipperyMovementUpdate(a, "West", {}) << "\n";
+ }
+ void PrismModulesPrinter::printSlipperyTurnActionsForNorth(const AgentName &a) {
+ actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { "CanSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, northUpdate(a)} }) << "\n";
+ actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!CanSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n";
- // generic output (for every view transition)
- for (std::size_t v = 0; v < viewTransition.size(); v++) {
+ actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"-1)"}, {1 - probIntended, northUpdate(a)} }) << "\n";
+ actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"=3)"}, {1 - probIntended, northUpdate(a)} }) << "\n";
+ actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n";
+ actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"=3)"} }) << "\n";
+ }
- os << actionName << moveGuard(agentIndex) << " x" << agentName << "=" << c.second << " & y" << agentName << "=" << c.first << viewTransition.at(v).first;
- for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS; i++) {
- os << (i == 0 ? " -> " : " + ") << prob_piece_dir.at(i) << "/" << PROB_PIECES << " : " << positionTransition.at(i) << viewTransition.at(v).second << moveUpdate(agentIndex) << (i == ALL_POSS_DIRECTIONS - 1 ? ";\n" : "\n");
- }
- }
+ void PrismModulesPrinter::printSlipperyTurnActionsForEast(const AgentName &a) {
+ actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { "CanSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, eastUpdate(a)} }) << "\n";
+ actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!CanSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n";
- return os;
+ actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"-1)"}, {1 - probIntended, eastUpdate(a)} }) << "\n";
+ actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"=3)"}, {1 - probIntended, eastUpdate(a)} }) << "\n";
+ actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n";
+ actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"=3)"} }) << "\n";
}
- std::ostream& PrismModulesPrinter::printSlipperyMove(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const coordinates &c, std::set<std::string> &slipperyActions, const std::array<bool, 8>& neighborhood, SlipperyType orientation) {
- constexpr std::size_t PROB_PIECES = 9, ALL_POSS_DIRECTIONS = 8;
-
- std::array<std::string, ALL_POSS_DIRECTIONS> positionTransition = {
- /* north */ "(y" + agentName + "'=y" + agentName + "-1)",
- /* north east */ "(x" + agentName + "'=x" + agentName + "+1) & (y" + agentName + "'=y" + agentName + "-1)",
- /* east */ "(x" + agentName + "'=x" + agentName + "+1)",
- /* east south */ "(x" + agentName + "'=x" + agentName + "+1) & (y" + agentName + "'=y" + agentName + "+1)",
- /* south */ "(y" + agentName + "'=y" + agentName + "+1)",
- /* south west */ "(x" + agentName + "'=x" + agentName + "-1) & (y" + agentName + "'=y" + agentName + "+1)",
- /* west */ "(x" + agentName + "'=x" + agentName + "-1)",
- /* north west */ "(x" + agentName + "'=x" + agentName + "-1) & (y" + agentName + "'=y" + agentName + "-1)"
- };
+ void PrismModulesPrinter::printSlipperyTurnActionsForSouth(const AgentName &a) {
+ actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { "CanSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, southUpdate(a)} }) << "\n";
+ actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!CanSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n";
- // direction specifics
+ actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"-1)"}, {1 - probIntended, southUpdate(a)} }) << "\n";
+ actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"=3)"}, {1 - probIntended, southUpdate(a)} }) << "\n";
+ actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n";
+ actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"=3)"} }) << "\n";
+ }
- std::size_t straightPosIndex;
- std::string actionName, specialTransition; // if straight ahead is blocked
- std::array<std::size_t, ALL_POSS_DIRECTIONS> prob_piece_dir; // { n, ne, w, se, s, sw, w, nw }
+ void PrismModulesPrinter::printSlipperyTurnActionsForWest(const AgentName &a) {
+ actionStream << printSlipperyTurnGuard(a, "right", RIGHT, { "CanSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, westUpdate(a)} }) << "\n";
+ actionStream << printSlipperyTurnGuard(a, "right", RIGHT, {"!CanSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n";
- switch (orientation)
- {
- case SlipperyType::North:
- actionName = "\t[" + agentName + "move_on_slip_north]";
- prob_piece_dir = { 0, 0, 1, 2, 0 /* <- R */, 2, 1, 0 };
- straightPosIndex = 4;
- specialTransition = "(y" + agentName + "'=y" + agentName + (!neighborhood.at(straightPosIndex) ? ")" : "+1)");
- break;
+ actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"-1)"}, {1 - probIntended, westUpdate(a)} }) << "\n";
+ actionStream << printSlipperyTurnGuard(a, "left", LEFT, { "CanSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"=3)"}, {1 - probIntended, westUpdate(a)} }) << "\n";
+ actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << "\n";
+ actionStream << printSlipperyTurnGuard(a, "left", LEFT, {"!CanSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"=3)"} }) << "\n";
+ }
- case SlipperyType::South:
- actionName = "\t[" + agentName + "move_on_slip_south]";
- prob_piece_dir = { 0 /* <- R */, 2, 1, 0, 0, 0, 1, 2 };
- straightPosIndex = 0; // always north
- specialTransition = "(y" + agentName + "'=y" + agentName + (!neighborhood.at(straightPosIndex) ? ")" : "-1)");
- break;
+ 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_" + direction + "]";
+ agentNameActionMap.at(a).insert({FORWARD, actionName});
+ return "\t" + actionName + " " + viewVariable(a, viewDirection) + a + "IsOnSlippery" + direction + " & " + buildConjunction(a, guards) + " -> ";
+ }
- case SlipperyType::East:
- actionName = "\t[" + agentName + "move_on_slip_east]";
- prob_piece_dir = { 1, 0, 0, 0, 1, 2, 0 /* <- R */, 2 };
- straightPosIndex = 6;
- specialTransition = "(x" + agentName + "'=x" + agentName + (!neighborhood.at(straightPosIndex) ? ")" : "-1)");
- break;
+ std::string PrismModulesPrinter::printSlipperyMovementUpdate(const AgentName &a, const std::string &direction, const updates &u) const {
+ return updatesToString(u);
+ }
- case SlipperyType::West:
- actionName = "\t[" + agentName + "move_on_slip_west]";
- prob_piece_dir = { 1, 2, 0 /* <- R */, 2, 1, 0, 0, 0 };
- straightPosIndex = 2;
- specialTransition = "(x" + agentName + "'=x" + agentName + (!neighborhood.at(straightPosIndex) ? ")" : "+1)");
- break;
- }
+ 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 actionName = "[" + a + "_turn_" + direction + "]";
+ agentNameActionMap.at(a).insert({actionId, actionName});
+ return "\t" + actionName + " " + buildConjunction(a, guards) + " & " + cond + " -> ";
+ }
- slipperyActions.insert(actionName);
+ std::string PrismModulesPrinter::printSlipperyTurnUpdate(const AgentName &a, const updates &u) {
+ return updatesToString(u);
+ }
- // override probability to 0 if corresp. direction is blocked
+ void PrismModulesPrinter::printFaultyMovementModule(const AgentName &a) {
+ os << "\nmodule " << a << "FaultyBehaviour" << std::endl;
+ os << "\tpreviousAction" << a << " : [-1..2] init -1;\n";
- for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS; i++) {
- if (!neighborhood.at(i))
- prob_piece_dir.at(i) = 0;
+ for(const auto [actionId, actionName] : agentNameActionMap.at(a)) {
+ os << "\t" << actionName << faultyBehaviourGuard(a, actionId) << " -> " << faultyBehaviourUpdate(a, actionId) << ";\n";
}
+ os << "endmodule\n\n";
+ }
- // determine residual probability (R) by replacing 0 with (1 - overall sum)
- if(enforceOneWays) {
- prob_piece_dir = {0,0,0,0,0,0,0,0};
- }
- prob_piece_dir.at(straightPosIndex) = PROB_PIECES - std::accumulate(prob_piece_dir.begin(), prob_piece_dir.end(), 0);
+ void PrismModulesPrinter::printMoveModule() {
+ os << "\nmodule " << "Arbiter" << std::endl;
+ os << "\tclock : [0.." << agentIndexMap.size() - 1 << "] init 0;\n";
- // <DEBUG_AREA>
- {
- assert(prob_piece_dir.at(straightPosIndex) <= 9 && prob_piece_dir.at(straightPosIndex) >= 3 && "Value not in Range!");
- assert(std::accumulate(prob_piece_dir.begin(), prob_piece_dir.end(), 0) == PROB_PIECES && "Does not sum up to 1!");
- assert(orientation != SlipperyType::North || (prob_piece_dir.at(7) == 0 && prob_piece_dir.at(0) == 0 && prob_piece_dir.at(1) == 0 && "Slippery up should be impossible!"));
- assert(orientation != SlipperyType::South || (prob_piece_dir.at(3) == 0 && prob_piece_dir.at(4) == 0 && prob_piece_dir.at(5) == 0 && "Slippery down should be impossible!"));
- assert(orientation != SlipperyType::East || (prob_piece_dir.at(1) == 0 && prob_piece_dir.at(2) == 0 && prob_piece_dir.at(3) == 0 && "Slippery right should be impossible!"));
- assert(orientation != SlipperyType::West || (prob_piece_dir.at(5) == 0 && prob_piece_dir.at(6) == 0 && prob_piece_dir.at(7) == 0 && "Slippery left should be impossible!"));
+ for(const auto [agentName, actions] : agentNameActionMap) {
+ for(const auto [actionId, actionName] : actions) {
+ os << "\t" << actionName << " " << moveGuard(agentName) << " -> " << moveUpdate(agentName) << ";\n";
+ }
}
- // </DEBUG_AREA>
-
- // special case: straight forward is blocked (then remain in same position)
-
- positionTransition.at(straightPosIndex) = specialTransition;
-
- // generic output (for every view and every possible view direction)
-
- os << actionName << moveGuard(agentIndex) << " x" << agentName << "=" << c.second << " & y" << agentName << "=" << c.first << " & " << agentName << "SlipperyMoveForwardAllowed ";
+ os << "endmodule\n\n";
+ }
- for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS; i++) {
- os << (i == 0 ? " -> " : " + ") << prob_piece_dir.at(i) << "/" << PROB_PIECES << " : " << positionTransition.at(i) << moveUpdate(agentIndex) << (i == ALL_POSS_DIRECTIONS - 1 ? ";\n" : "\n");
+ void PrismModulesPrinter::printConfiguredActions(const AgentName &agentName) {
+ for (auto& config : configuration) {
+ if (config.type_ == ConfigType::Module && !config.overwrite_ && agentName == config.module_) {
+ os << config.expression_ ;
+ }
}
- return os;
+ os << "\n";
}
- std::ostream& PrismModulesPrinter::printEndmodule(std::ostream &os) {
- os << "endmodule\n";
- os << "\n";
- return os;
+ void PrismModulesPrinter::printDoneActions(const AgentName &agentName) {
+ os << "\t[" << agentName << "_done]" << moveGuard(agentName) << agentName << "IsInGoal | " << agentName << "IsInLava -> (" << agentName << "Done'=true);\n";
}
- std::ostream& PrismModulesPrinter::printPlayerStruct(std::ostream &os, const AgentName &agentName, const bool agentWithView, const std::vector<float> &probabilities, const std::set<std::string> &slipperyActions) {
+ void PrismModulesPrinter::printPlayerStruct(const AgentName &agentName) {
os << "player " << agentName << "\n\t";
bool first = true;
- std::list<std::string> allActions = { "_move_north", "_move_east", "_move_south", "_move_west" };
- std::list<std::string> movementActions = allActions;
- for(auto const& probability : probabilities) {
- std::string percentageString = std::to_string((int)(100 * probability));
- for(auto const& movement : movementActions) {
- allActions.push_back(movement + "_" + percentageString);
- }
- }
- if(agentWithView) {
- allActions.push_back("_turn_left");
- allActions.push_back("_turn_right");
- } else {
- allActions.push_back("_turns");
- }
-
- for(auto const& action : allActions) {
- if(first) first = false; else os << ", ";
- os << "[" << agentName << action << "]";
- }
- for(auto const& action : slipperyActions) {
- os << ", " << action;
+ for(const auto [actionId, actionName] : agentNameActionMap.at(agentName)) {
+ if(first) first = false;
+ else os << ", ";
+ os << actionName;
}
os << "\nendplayer\n";
- return os;
- }
-
- std::ostream& PrismModulesPrinter::printGlobalMoveVariable(std::ostream &os, const size_t &numberOfPlayer) {
- os << "\nglobal move : [0.." << std::to_string(numberOfPlayer - 1) << "] init 0;\n\n";
- return os;
}
- std::ostream& PrismModulesPrinter::printRewards(std::ostream &os, const AgentName &agentName, const std::map<coordinates, float> &stateRewards, const cells &lava, const cells &goals, const std::map<Color, cells> &backgroundTiles) {
+ void PrismModulesPrinter::printRewards(const AgentName &agentName, const std::map<coordinates, float> &stateRewards, const cells &lava, const cells &goals, const std::map<Color, cells> &backgroundTiles) {
if(lava.size() != 0) {
- os << "rewards \"SafetyNoBFS\"\n";
- os << "\tAgentIsInLavaAndNotDone: -100;\n";
+ os << "rewards \"" << agentName << "SafetyNoBFS\"\n";
+ os << "\t" <<agentName << "IsInLavaAndNotDone: -100;\n";
os << "endrewards\n";
}
- os << "rewards \"SafetyNoBFSAndGoal\"\n";
- if(goals.size() != 0) os << "\tAgentIsInGoalAndNotDone: 100;\n";
- if(lava.size() != 0) os << "\tAgentIsInLavaAndNotDone: -100;\n";
- os << "endrewards\n";
+ if (!goals.empty() || !lava.empty()) {
+ os << "rewards \"" << agentName << "SafetyNoBFSAndGoal\"\n";
+ if(goals.size() != 0) os << "\t" << agentName << "IsInGoalAndNotDone: 100;\n";
+ if(lava.size() != 0) os << "\t" << agentName << "IsInLavaAndNotDone: -100;\n";
+ os << "endrewards\n";
+ }
- os << "rewards \"Time\"\n";
- os << "\t!AgentIsInGoal : -1;\n";
- if(goals.size() != 0) os << "\tAgentIsInGoalAndNotDone: 100;\n";
- if(lava.size() != 0) os << "\tAgentIsInLavaAndNotDone: -100;\n";
+ os << "rewards \"" << agentName << "Time\"\n";
+ os << "\t!" << agentName << "IsInGoal : -1;\n";
+ if(goals.size() != 0) os << "\t" << agentName << "IsInGoalAndNotDone: 100;\n";
+ if(lava.size() != 0) os << "\t" << agentName << "IsInLavaAndNotDone: -100;\n";
os << "endrewards\n";
if(stateRewards.size() > 0) {
- os << "rewards \"SafetyWithBFS\"\n";
- if(lava.size() != 0) os << "\tAgentIsInLavaAndNotDone: -100;\n";
+ os << "rewards \"" << agentName << "SafetyWithBFS\"\n";
+ if(lava.size() != 0) os << "\t" << agentName << "IsInLavaAndNotDone: -100;\n";
for(auto const [coordinates, reward] : stateRewards) {
os << "\txAgent=" << coordinates.first << "&yAgent=" << coordinates.second << " : " << reward << ";\n";
}
os << "endrewards\n";
}
if(stateRewards.size() > 0) {
- os << "rewards \"SafetyWithBFSAndGoal\"\n";
+ os << "rewards \"" << agentName << "SafetyWithBFSAndGoal\"\n";
if(goals.size() != 0) os << "\tAgentIsInGoalAndNotDone: 100;\n";
if(lava.size() != 0) os << "\tAgentIsInLavaAndNotDone: -100;\n";
for(auto const [coordinates, reward] : stateRewards) {
@@ -656,26 +565,84 @@ namespace prism {
if(goals.size() != 0) os << "\tAgentIsInGoalAndNotDone & !(" << allPassengersPickedUp << ") : -100;\n";
os << "endrewards";
}
- return os;
}
- std::string PrismModulesPrinter::moveGuard(const size_t &agentIndex) {
- return isGame() ? " move=" + std::to_string(agentIndex) + " & " : " ";
+ std::string PrismModulesPrinter::faultyBehaviourGuard(const AgentName &agentName, const ActionId &actionId) const {
+ if(faultyBehaviour()) {
+ if(actionId == NOFAULT) {
+ return "(previousAction" + agentName + "=" + std::to_string(NOFAULT) + ") ";
+ } else {
+ return "(previousAction" + agentName + "=" + std::to_string(NOFAULT) + " | previousAction" + agentName + "=" + std::to_string(actionId) + ") ";
+ }
+ } else {
+ return "";
+ }
+ }
+
+ std::string PrismModulesPrinter::faultyBehaviourUpdate(const AgentName &agentName, const ActionId &actionId) const {
+ if(actionId != NOFAULT) {
+ return updatesToString({ {1 - faultyProbability, "(previousAction" + agentName + "'=" + std::to_string(NOFAULT) + ")"}, {faultyProbability, "(previousAction" + agentName + "'=" + std::to_string(actionId) + ")" } });
+ } else {
+ return "true";
+ }
+ }
+
+ std::string PrismModulesPrinter::moveGuard(const AgentName &agentName) const {
+ return "clock=" + std::to_string(agentIndexMap.at(agentName));
+ }
+
+ std::string PrismModulesPrinter::moveUpdate(const AgentName &agentName) const {
+ size_t agentIndex = agentIndexMap.at(agentName);
+ return (agentIndex == numberOfPlayer - 1) ? "(clock'=0) " : "(clock'=" + std::to_string(agentIndex + 1) + ") ";
+
+ }
+
+ std::string PrismModulesPrinter::updatesToString(const updates &updates) const {
+ if(updates.empty()) return "true";
+ std::string updatesString = "";
+ bool first = true;
+ for(auto const update : updates) {
+ if(first) first = false;
+ else updatesString += " + ";
+ updatesString += updateToString(update);
+ }
+ return updatesString;
}
- std::string PrismModulesPrinter::moveUpdate(const size_t &agentIndex) {
- return isGame() ?
- (agentIndex == numberOfPlayer - 1) ?
- " & (move'=0) " :
- " & (move'=" + std::to_string(agentIndex + 1) + ") " :
- "";
+ std::string PrismModulesPrinter::updateToString(const update &u) const {
+ return std::to_string(u.first) + ": " + u.second;
}
- std::string PrismModulesPrinter::viewVariable(const AgentName &agentName, const size_t &agentDirection, const bool agentWithView) {
- return agentWithView ? " view" + agentName + "=" + std::to_string(agentDirection) + " & " : " ";
+ std::string PrismModulesPrinter::viewVariable(const AgentName &agentName, const size_t &agentDirection) const {
+ return "view" + agentName + "=" + std::to_string(agentDirection) + " & ";
+ }
+
+ bool PrismModulesPrinter::anyPortableObject() const {
+ return !keys.empty() || !boxes.empty() || !balls.empty();
+ }
+
+ bool PrismModulesPrinter::faultyBehaviour() const {
+ return faultyProbability > 0.0f;
+ }
+
+ bool PrismModulesPrinter::slipperyBehaviour() const {
+ return !slipperyTiles.at("North").empty() || !slipperyTiles.at("East").empty() || !slipperyTiles.at("South").empty() || !slipperyTiles.at("West").empty();
}
bool PrismModulesPrinter::isGame() const {
return modelType == ModelType::SMG;
}
+
+ std::string PrismModulesPrinter::buildConjunction(const AgentName &a, std::vector<std::string> formulae) const {
+ if(formulae.empty()) return "true";
+ std::string conjunction = "";
+ bool first = true;
+ for(auto const formula : formulae) {
+ if(first) first = false;
+ else conjunction += " & ";
+ conjunction += formula;
+ }
+ return conjunction;
+ }
+
}
diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h
index 7a196fc..a66d68f 100644
--- a/util/PrismModulesPrinter.h
+++ b/util/PrismModulesPrinter.h
@@ -1,91 +1,111 @@
#pragma once
#include <iostream>
+#include <set>
#include <functional>
#include "MinigridGrammar.h"
#include "PrismPrinter.h"
+#include "ConfigYaml.h"
+
+
+std::string northUpdate(const AgentName &a);
+std::string southUpdate(const AgentName &a);
+std::string eastUpdate(const AgentName &a);
+std::string westUpdate(const AgentName &a);
namespace prism {
class PrismModulesPrinter {
public:
- PrismModulesPrinter(const ModelType &modelType, const size_t &numberOfPlayer, const bool enforceOneWays = false);
-
- std::ostream& printRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &cells);
- std::ostream& printIsOnSlipperyFormula(std::ostream& os, const AgentName &agentName, const std::vector<std::reference_wrapper<cells>> &slipperyCollection, const cells &slipperyNorth, const cells &slipperyEast, const cells &slipperySouth, const cells &slipperyWest);
- std::ostream& printGoalLabel(std::ostream& os, const AgentName&agentName, const cells &goals);
- std::ostream& printCrashLabel(std::ostream &os, const std::vector<AgentName> agentNames);
- std::ostream& printAvoidanceLabel(std::ostream &os, const std::vector<AgentName> agentNames, const int &distance);
- std::ostream& printKeysLabels(std::ostream& os, const AgentName&agentName, const cells &keys);
- std::ostream& printBackgroundLabels(std::ostream &os, const AgentName &agentName, const std::pair<Color, cells> &backgroundTiles);
- std::ostream& printIsInLavaFormula(std::ostream& os, const AgentName &agentName, const cells &lava);
- std::ostream& printIsFixedFormulas(std::ostream& os, const AgentName &agentName);
- std::ostream& printTurningNotAllowedFormulas(std::ostream& os, const AgentName &agentName, const cells &floor);
- std::ostream& printWallFormula(std::ostream& os, const AgentName &agentName, const cells &walls);
- std::ostream& printFormulas(std::ostream& os,
- const AgentName&agentName,
- const cells &restrictionNorth,
- const cells &restrictionEast,
- const cells &restrictionSouth,
- const cells &restrictionWest,
- const std::vector<std::reference_wrapper<cells>> &slipperyCollection,
- const cells &lava,
- const cells &walls,
- const cells &noTurnFloor,
- const cells &slipperyNorth,
- const cells &slipperyEast,
- const cells &slipperySouth,
- const cells &slipperyWest);
-
- /*
- * Representation for Slippery Tile.
- * -) North: Slips from North to South
- * -) East: Slips from East to West
- * -) South: Slips from South to North
- * -) West: Slips from West to East
- */
- enum class SlipperyType { North, East, South, West };
-
- /*
- * Prints Slippery on move action.
- *
- * @param neighborhood: Information of wall-blocks in 8-neighborhood { n, nw, e, se, s, sw, w, nw }. If entry is false, then corresponding neighboorhood position is a wall.
- * @param orientation: Information of slippery type (either north, south, east, west).
- */
- std::ostream& printSlipperyMove(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const coordinates &c, std::set<std::string> &slipperyActions, const std::array<bool, 8>& neighborhood, SlipperyType orientation);
-
- /*
- * Prints Slippery on turn action.
- *
- * @param neighborhood: Information of wall-blocks in 8-neighborhood { n, nw, e, se, s, sw, w, nw }. If entry is false, then corresponding neighboorhood position is a wall.
- * @param orientation: Information of slippery type (either north, south, east, west).
- */
- std::ostream& printSlipperyTurn(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const coordinates &c, std::set<std::string> &slipperyActions, const std::array<bool, 8>& neighborhood, SlipperyType orientation);
-
- std::ostream& printModel(std::ostream &os, const ModelType &modelType);
- std::ostream& printBooleansForKeys(std::ostream &os, const AgentName &agentName, const cells &keys);
- std::ostream& printActionsForKeys(std::ostream &os, const AgentName &agentName, const cells &keys);
- std::ostream& printBooleansForBackground(std::ostream &os, const AgentName &agentName, const std::map<Color, cells> &backgroundTiles);
- std::ostream& printActionsForBackground(std::ostream &os, const AgentName &agentName, const std::map<Color, cells> &backgroundTiles);
- std::ostream& printInitStruct(std::ostream &os, const AgentName &agentName);
- std::ostream& printModule(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const coordinates &boundaries, const coordinates& initialPosition, const cells &keys, const std::map<Color, cells> &backgroundTiles, const bool agentWithView, const std::vector<float> &probabilities = {});
- std::ostream& printMovementActions(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const bool agentWithView, const float &probability = 1.0);
- std::ostream& printDoneActions(std::ostream &os, const AgentName &agentName, const size_t &agentIndex);
- std::ostream& printEndmodule(std::ostream &os);
- std::ostream& printPlayerStruct(std::ostream &os, const AgentName &agentName, const bool agentWithView, const std::vector<float> &probabilities = {}, const std::set<std::string> &slipperyActions = {});
- std::ostream& printGlobalMoveVariable(std::ostream &os, const size_t &numberOfPlayer);
-
- std::ostream& printRewards(std::ostream &os, const AgentName &agentName, const std::map<coordinates, float> &stateRewards, const cells &lava, const cells &goals, const std::map<Color, cells> &backgroundTiles);
-
- std::string moveGuard(const size_t &agentIndex);
- std::string moveUpdate(const size_t &agentIndex);
-
- std::string viewVariable(const AgentName &agentName, const size_t &agentDirection, const bool agentWithView);
+ PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector<Configuration> config, const float probIntended, const float faultyProbability);
+
+ std::ostream& print();
+
+ void printModelType(const ModelType &modelType);
+
bool isGame() const;
private:
+ void printPortableObjectModule(const cell &object);
+ void printPortableObjectActions(const std::string &agentName, const std::string &identifier);
+
+ void printDoorModule(const cell &object, const bool &opened);
+ void printLockedDoorActions(const std::string &agentName, const std::string &identifier);
+ void printUnlockedDoorActions(const std::string &agentName, const std::string &identifier);
+
+ void printRobotModule(const AgentName &agentName, const coordinates &initialPosition);
+ void printPortableObjectActionsForRobot(const std::string &agentName, const std::string &identifier);
+ void printUnlockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier);
+ void printLockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier, const std::string &key);
+ void printMovementActionsForRobot(const std::string &a);
+ void printTurnActionsForRobot(const std::string &a);
+ void printSlipperyMovementActionsForRobot(const AgentName &a);
+ void printSlipperyMovementActionsForNorth(const AgentName &a);
+ void printSlipperyMovementActionsForEast(const AgentName &a);
+ void printSlipperyMovementActionsForSouth(const AgentName &a);
+ void printSlipperyMovementActionsForWest(const AgentName &a);
+ void printSlipperyTurnActionsForNorth(const AgentName &a);
+ void printSlipperyTurnActionsForEast(const AgentName &a);
+ void printSlipperyTurnActionsForSouth(const AgentName &a);
+ void printSlipperyTurnActionsForWest(const AgentName &a);
+
+ std::string printMovementGuard(const AgentName &a, const std::string &direction, const size_t &viewDirection);
+ std::string printMovementUpdate(const AgentName &a, const update &update) const;
+ std::string printTurnGuard(const AgentName &a, const std::string &direction, const ActionId &actionId, const std::string &cond = "");
+ std::string printTurnUpdate(const AgentName &a, const update &u, const ActionId &actionId) const;
+ std::string printSlipperyMovementGuard(const AgentName &a, const std::string &direction, const ViewDirection &viewDirection, const std::vector<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 printSlipperyTurnUpdate(const AgentName &a, const updates &u);
+
+ void printFaultyMovementModule(const AgentName &a);
+ void printMoveModule();
+
+ void printConstants(const std::vector<std::string> &constants);
+
+ void printDoneActions(const AgentName &agentName);
+ void printPlayerStruct(const AgentName &agentName);
+ void printRewards(const AgentName &agentName, const std::map<coordinates, float> &stateRewards, const cells &lava, const cells &goals, const std::map<Color, cells> &backgroundTiles);
+
+ void printConfiguration(const std::vector<Configuration>& configurations);
+ void printConfiguredActions(const AgentName &agentName);
+
+ bool anyPortableObject() const;
+ bool faultyBehaviour() const;
+ bool slipperyBehaviour() const;
+ std::string moveGuard(const AgentName &agentName) const;
+ std::string faultyBehaviourGuard(const AgentName &agentName, const ActionId &actionId) const;
+ std::string faultyBehaviourUpdate(const AgentName &agentName, const ActionId &actionId) const;
+ std::string moveUpdate(const AgentName &agentName) const;
+ std::string updatesToString(const updates &updates) const;
+ std::string updateToString(const update &u) const;
+
+ std::string viewVariable(const AgentName &agentName, const size_t &agentDirection) const;
+
+
+ std::string buildConjunction(const AgentName &a, std::vector<std::string> formulae) const;
+
+
+ std::ostream &os;
+ std::stringstream actionStream;
+
+ ModelType const &modelType;
+ coordinates const &maxBoundaries;
+ AgentName agentName;
+ cells boxes;
+ cells balls;
+ cells lockedDoors;
+ cells unlockedDoors;
+ cells keys;
+ std::map<std::string, cells> slipperyTiles;
+
+ AgentNameAndPositionMap agentNameAndPositionMap;
+ std::map<AgentName, size_t> agentIndexMap;
+ size_t numberOfPlayer;
+ float const faultyProbability;
+ float const probIntended;
+ std::vector<Configuration> configuration;
+ std::vector<ViewDirection> viewDirections = {0, 1, 2, 3};
- ModelType const& modelType;
- const size_t numberOfPlayer;
- bool enforceOneWays;
+ std::map<AgentName, std::set<std::pair<ActionId, std::string>>> agentNameActionMap;
};
}
diff --git a/util/PrismPrinter.cpp b/util/PrismPrinter.cpp
new file mode 100644
index 0000000..4c172f1
--- /dev/null
+++ b/util/PrismPrinter.cpp
@@ -0,0 +1,8 @@
+#include "PrismPrinter.h"
+
+#include <algorithm>
+
+std::string capitalize(std::string string) {
+ string[0] = std::toupper(string[0]);
+ return string;
+}
diff --git a/util/PrismPrinter.h b/util/PrismPrinter.h
index ed12126..572cb40 100644
--- a/util/PrismPrinter.h
+++ b/util/PrismPrinter.h
@@ -1,12 +1,22 @@
#pragma once
#include <string>
+#include <map>
#include "cell.h"
typedef std::string AgentName;
+typedef size_t ViewDirection;
typedef std::pair<std::string, coordinates> AgentNameAndPosition;
+typedef AgentNameAndPosition KeyNameAndPosition;
typedef std::map<AgentNameAndPosition::first_type, AgentNameAndPosition::second_type> AgentNameAndPositionMap;
+typedef std::map<KeyNameAndPosition::first_type, KeyNameAndPosition::second_type> KeyNameAndPositionMap;
+typedef std::pair<cell, std::string> CellAndCondition;
+typedef std::pair<float, std::string> update;
+typedef std::vector<update> updates;
+typedef int8_t ActionId;
+
+std::string capitalize(std::string string);
namespace prism {
enum class ModelType {
diff --git a/util/cell.cpp b/util/cell.cpp
index 07d25f7..c6a72a1 100644
--- a/util/cell.cpp
+++ b/util/cell.cpp
@@ -4,10 +4,14 @@
std::ostream &operator<<(std::ostream &os, const cell &c) {
os << static_cast<char>(c.type) << static_cast<char>(c.color);
- os << " at (" << c.row << "," << c.column << ")";
+ os << " at (" << c.column << "," << c.row << ")";
return os;
}
+coordinates cell::getCoordinates() const {
+ return std::make_pair(column, row);
+}
+
cell cell::getNorth(const std::vector<cell> &grid) const {
auto north = std::find_if(grid.begin(), grid.end(), [this](const cell &c) {
return this->row - 1 == c.row && this->column == c.column;
@@ -52,10 +56,6 @@ cell cell::getWest(const std::vector<cell> &grid) const {
return *west;
}
-coordinates cell::getCoordinates() const {
- return std::make_pair(row, column);
-}
-
std::string cell::getColor() const {
switch(color) {
case Color::Red: return "red";
@@ -69,6 +69,27 @@ std::string cell::getColor() const {
}
}
+std::string cell::getType() const {
+ switch(type) {
+ case Type::Wall: return "Wall";
+ case Type::Floor: return "Floor";
+ case Type::Door: return "Door";
+ case Type::LockedDoor: return "LockedDoor";
+ case Type::Key: return "Key";
+ case Type::Ball: return "Ball";
+ case Type::Box: return "Box";
+ case Type::Goal: return "Goal";
+ case Type::Lava: return "Lava";
+ case Type::Agent: return "Agent";
+ case Type::Adversary: return "Adversary";
+ case Type::SlipperyNorth: return "SlipperyNorth";
+ case Type::SlipperySouth: return "SlipperySouth";
+ case Type::SlipperyEast: return "SlipperyEast";
+ case Type::SlipperyWest: return "SlipperyWest";
+ default: return "";
+ }
+}
+
std::string getColor(Color color) {
switch(color) {
case Color::Red: return "red";
diff --git a/util/cell.h b/util/cell.h
index c369052..ca71559 100644
--- a/util/cell.h
+++ b/util/cell.h
@@ -40,10 +40,10 @@ std::string getColor(Color color);
class cell {
public:
- coordinates getNorth() const { return std::make_pair(row - 1, column); }
- coordinates getSouth() const { return std::make_pair(row + 1, column); }
- coordinates getEast() const { return std::make_pair(row, column + 1); }
- coordinates getWest() const { return std::make_pair(row, column - 1); }
+ coordinates getNorth() const { return std::make_pair(column, row - 1); }
+ coordinates getSouth() const { return std::make_pair(column, row + 1); }
+ coordinates getEast() const { return std::make_pair(column + 1, row); }
+ coordinates getWest() const { return std::make_pair(column - 1, row); }
cell getNorth(const std::vector<cell> &grid) const;
cell getEast(const std::vector<cell> &grid) const;
@@ -54,6 +54,7 @@ class cell {
coordinates getCoordinates() const;
std::string getColor() const;
+ std::string getType() const;
int row;
int column;