Merge pull request 'Overhaul' (#3) from tempestpyadaption into main

Reviewed-on: #3

.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"
+  }
+}

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)

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_);

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
 )

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;
+}

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_;
+};

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);
+  //}
 }

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;
 };

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();
+  }
+}

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;
+  };
+}

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;
   };
 }

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;
+}

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 {

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";

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;