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;