commit 85d0cbc81fe54af056f0253029bcaf3ca0604db5
Author: sp <stefan.pranger@iaik.tugraz.at>
Date:   Thu Aug 17 11:41:16 2023 +0200

    initial commit
    
    after modifications for Importance Driven Testing

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..ce34176
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,34 @@
+# Prerequisites
+*.d
+
+# Compiled Object files
+*.slo
+*.lo
+*.o
+*.obj
+
+# Precompiled Headers
+*.gch
+*.pch
+
+# Compiled Dynamic libraries
+*.so
+*.dylib
+*.dll
+
+# Fortran module files
+*.mod
+*.smod
+
+# Compiled Static libraries
+*.lai
+*.la
+*.a
+*.lib
+
+# Executables
+*.exe
+*.out
+*.app
+
+build/*
diff --git a/CMakeLists.txt b/CMakeLists.txt
new file mode 100644
index 0000000..1ca1571
--- /dev/null
+++ b/CMakeLists.txt
@@ -0,0 +1,22 @@
+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)
+
+add_executable(main
+               ${SRCS}
+               main.cpp
+               )
+
+target_link_libraries(main pthread)
diff --git a/main.cpp b/main.cpp
new file mode 100644
index 0000000..58de07f
--- /dev/null
+++ b/main.cpp
@@ -0,0 +1,171 @@
+#include "util/OptionParser.h"
+#include "util/MinigridGrammar.h"
+#include "util/Grid.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);
+  while(stream.good()) {
+    std::string substr;
+    getline(stream, substr, ',');
+    substr.at(0) = std::toupper(substr.at(0));
+    result.push_back(substr);
+  }
+  return result;
+}
+
+struct printer {
+    typedef boost::spirit::utf8_string string;
+
+    void element(string const& tag, string const& value, int depth) const {
+        for (int i = 0; i < (depth*4); ++i) std::cout << ' ';
+
+        std::cout << "tag: " << tag;
+        if (value != "") std::cout << ", value: " << value;
+        std::cout << std::endl;
+    }
+};
+
+void print_info(boost::spirit::info const& what) {
+  using boost::spirit::basic_info_walker;
+
+  printer pr;
+  basic_info_walker<printer> walker(pr, what.tag, 0);
+  boost::apply_visitor(walker, what.value);
+}
+
+int main(int argc, char* argv[]) {
+  popl::OptionParser optionParser("Allowed options");
+
+  auto helpOption = optionParser.add<popl::Switch>("h", "help", "Print this help message.");
+  auto inputFilename = optionParser.add<popl::Value<std::string>>("i", "input-file", "Filename of the input file.");
+  auto outputFilename = optionParser.add<popl::Value<std::string>>("o", "output-file", "Filename for the output file.");
+
+  auto agentsToBeConsidered = optionParser.add<popl::Value<std::string>, popl::Attribute::optional>("a", "agents", "Which parsed agents should be considered in the output. WIP.");
+  auto viewForAgents = optionParser.add<popl::Value<std::string>, popl::Attribute::optional>("v", "view", "Agents for which the 'view'('direction') variable should be included. WIP.");
+
+  auto probabilisticBehaviourAgents = optionParser.add<popl::Value<std::string>, popl::Attribute::optional>("p", "prob-beh", "Agents for which we want to include probabilistic actions");
+  auto probabilities = optionParser.add<popl::Value<std::string>, popl::Attribute::optional>("q", "probs", "The probabilities for which probabilistic actions should be added. WIP");
+
+  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.");
+
+  try {
+    optionParser.parse(argc, argv);
+
+    if(helpOption->count() > 0) {
+      std::cout << optionParser << std::endl;
+      return EXIT_SUCCESS;
+    }
+  } catch (const popl::invalid_option &e) {
+    return io::printPoplException(e);
+  } catch (const std::exception &e) {
+		std::cerr << "Exception: " << e.what() << "\n";
+		return EXIT_FAILURE;
+	}
+
+  GridOptions gridOptions = { {}, {} };
+  if(agentsToBeConsidered->is_set()) {
+    gridOptions.agentsToBeConsidered = parseCommaSeparatedString(agentsToBeConsidered->value(0));
+  }
+  if(viewForAgents->is_set()) {
+    gridOptions.agentsWithView = parseCommaSeparatedString(viewForAgents->value(0));
+  }
+  if(enforceOneWays->is_set()) {
+    gridOptions.enforceOneWays = true;
+  }
+  if(probabilisticBehaviourAgents->is_set()) {
+    gridOptions.agentsWithProbabilisticBehaviour = parseCommaSeparatedString(probabilisticBehaviourAgents->value(0));
+    for(auto const& a : gridOptions.agentsWithProbabilisticBehaviour) {
+      std::cout << a << std::endl;
+    }
+    if(probabilities->is_set()) {
+      std::vector<std::string> parsedStrings = parseCommaSeparatedString(probabilities->value(0));
+
+      std::transform(parsedStrings.begin(), parsedStrings.end(), std::back_inserter(gridOptions.probabilitiesForActions), [](const std::string& string) {
+        return std::stof(string);
+      });
+      for(auto const& a : gridOptions.probabilitiesForActions) {
+        std::cout << a << std::endl;
+      }
+    } else {
+      throw std::logic_error{ "When adding agents with probabilistic behaviour, you also need to specify a list of probabilities via --probs." };
+    }
+  }
+
+
+  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::cout << "\n";
+  bool parsingBackground = false;
+  bool parsingStateRewards = 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) == '-') {
+      parsingBackground = true;
+      continue;
+    }
+    if(!parsingBackground && !parsingStateRewards) {
+      std::cout << "Reading   :\t" << line << "\n";
+      content += line + "\n";
+    } else if (parsingBackground) {
+      std::cout << "Background:\t" << line << "\n";
+      background += line + "\n";
+    } else if(parsingStateRewards) {
+      rewards += line + "\n";
+    }
+  }
+  std::cout << "\n";
+
+
+  pos_iterator_t contentFirst(content.begin());
+  pos_iterator_t contentIter = contentFirst;
+  pos_iterator_t contentLast(content.end());
+  MinigridParser<pos_iterator_t> contentParser(contentFirst);
+  pos_iterator_t backgroundFirst(background.begin());
+  pos_iterator_t backgroundIter = backgroundFirst;
+  pos_iterator_t backgroundLast(background.end());
+  MinigridParser<pos_iterator_t> backgroundParser(backgroundFirst);
+
+  cells contentCells;
+  cells backgroundCells;
+  std::map<coordinates, float> stateRewards;
+  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 }
+
+    boost::escaped_list_separator<char> seps('\\', ';', '\n');
+    Tokenizer csvParser(rewards, seps);
+    for(auto iter = csvParser.begin(); iter != csvParser.end(); ++iter) {
+      int x = std::stoi(*iter);
+      int y = std::stoi(*(++iter));
+      float reward = std::stof(*(++iter));
+      stateRewards[std::make_pair(x,y)] = reward;
+    }
+    if(ok) {
+      Grid grid(contentCells, backgroundCells, gridOptions, stateRewards);
+      //grid.printToPrism(std::cout, prism::ModelType::MDP);
+      grid.printToPrism(file, prism::ModelType::MDP);
+    }
+  } catch(qi::expectation_failure<pos_iterator_t> const& e) {
+    std::cout << "expected: "; print_info(e.what_);
+    std::cout << "got: \"" << std::string(e.first, e.last) << '"' << std::endl;
+    std::cout << "Expectation failure: " << e.what() << " at '" << std::string(e.first,e.last) << "'\n";
+  } catch(const std::exception& e) {
+    std::cerr << "Exception '" << typeid(e).name() << "' caught:" << std::endl;
+    std::cerr << "\t" << e.what() << std::endl;
+    std::exit(EXIT_FAILURE);
+  }
+
+  return 0;
+}
diff --git a/util/CMakeLists.txt b/util/CMakeLists.txt
new file mode 100644
index 0000000..f5884fe
--- /dev/null
+++ b/util/CMakeLists.txt
@@ -0,0 +1,8 @@
+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}/PrismModulesPrinter.cpp
+  ${CMAKE_CURRENT_LIST_DIR}/popl.hpp
+  ${CMAKE_CURRENT_LIST_DIR}/OptionParser.cpp
+)
diff --git a/util/Grid.cpp b/util/Grid.cpp
new file mode 100644
index 0000000..1184e1e
--- /dev/null
+++ b/util/Grid.cpp
@@ -0,0 +1,229 @@
+#include "Grid.h"
+
+#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)
+{
+  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;
+  });
+  agentNameAndPositionMap.insert({ "Agent", agent.getCoordinates() });
+  for(auto const& adversary : adversaries) {
+    std::string color = adversary.getColor();
+    color.at(0) = std::toupper(color.at(0));
+    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() });
+      if(!success.second) {
+        throw std::logic_error("Agent with " + color + " already present\n");
+      }
+    } catch(const std::logic_error& e) {
+      std::cerr << "Expected agents colors to be different. Agent 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) {
+        return c.type == Type::Floor && c.color == color;
+    });
+    if(cellsOfColor.size() > 0) {
+      backgroundTiles.emplace(color, cellsOfColor);
+    }
+  }
+}
+
+std::ostream& operator<<(std::ostream& os, const Grid& grid) {
+  int lastRow = 1;
+  for(auto const& cell : grid.allGridCells) {
+    if(lastRow != cell.row)
+      os << std::endl;
+    os << static_cast<char>(cell.type) << static_cast<char>(cell.color);
+    lastRow = cell.row;
+  }
+  return os;
+}
+
+cells Grid::getGridCells() {
+  return allGridCells;
+}
+
+bool Grid::isBlocked(coordinates p) {
+  return isWall(p) || isLockedDoor(p) || isKey(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;
+      }) != 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();
+}
+
+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();
+}
+
+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());
+  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);
+  }
+
+  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::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);
+
+    }
+    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);
+    }
+
+    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);
+    //}
+  }
+}
+
+
+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())
+         };
+}
diff --git a/util/Grid.h b/util/Grid.h
new file mode 100644
index 0000000..84c2eb2
--- /dev/null
+++ b/util/Grid.h
@@ -0,0 +1,63 @@
+#pragma once
+
+#include <iostream>
+#include <fstream>
+#include <map>
+#include <utility>
+
+#include "MinigridGrammar.h"
+#include "PrismModulesPrinter.h"
+
+struct GridOptions {
+  std::vector<AgentName> agentsToBeConsidered;
+  std::vector<AgentName> agentsWithView;
+  std::vector<AgentName> agentsWithProbabilisticBehaviour;
+  std::vector<float>     probabilitiesForActions;
+  bool                   enforceOneWays;
+};
+
+class Grid {
+  public:
+    Grid(cells gridCells, cells background, const GridOptions &gridOptions, const std::map<coordinates, float> &stateRewards = {});
+
+    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);
+
+    std::array<bool, 8> getWalkableDirOf8Neighborhood(cell c);
+
+    friend std::ostream& operator<<(std::ostream& os, const Grid &grid);
+
+  private:
+    GridOptions gridOptions;
+
+    cells allGridCells;
+    cells background;
+    coordinates maxBoundaries;
+
+    cell agent;
+    cells adversaries;
+    AgentNameAndPositionMap agentNameAndPositionMap;
+
+    cells walls;
+    cells floor;
+    cells slipperyNorth;
+    cells slipperyEast;
+    cells slipperySouth;
+    cells slipperyWest;
+    cells lockedDoors;
+    cells boxes;
+    cells lava;
+
+    cells goals;
+    cells keys;
+
+    std::map<Color, cells> backgroundTiles;
+
+    std::map<coordinates, float> stateRewards;
+};
diff --git a/util/MinigridGrammar.h b/util/MinigridGrammar.h
new file mode 100644
index 0000000..79684a5
--- /dev/null
+++ b/util/MinigridGrammar.h
@@ -0,0 +1,102 @@
+#pragma once
+
+#include "cell.h"
+
+#include <vector>
+
+#include <boost/tokenizer.hpp>
+#include <boost/fusion/adapted/struct.hpp>
+#include <boost/spirit/include/qi.hpp>
+#include <boost/spirit/include/phoenix.hpp>
+#include <boost/spirit/include/phoenix_operator.hpp>
+#include <boost/variant/recursive_wrapper.hpp>
+#include <boost/spirit/include/support_line_pos_iterator.hpp>
+
+namespace qi      = boost::spirit::qi;
+namespace phoenix = boost::phoenix;
+
+typedef boost::spirit::line_pos_iterator<std::string::const_iterator> pos_iterator_t;
+
+typedef std::vector<cell> row;
+typedef std::vector<cell> cells;
+
+BOOST_FUSION_ADAPT_STRUCT(
+    cell,
+    (Type, type)
+    (Color, color)
+)
+
+template<typename It>
+struct annotation_f {
+    typedef void result_type;
+
+    annotation_f(It first) : first(first) {}
+    It const first;
+
+    template<typename Val, typename First, typename Last>
+    void operator()(Val& v, First f, Last l) const {
+        do_annotate(v, f, l, first);
+    }
+
+  private:
+    void static do_annotate(cell& c, It f, It l, It first) {
+        c.row    = get_line(f) - 1;
+        c.column = get_column(first, f) / 2;
+    }
+    static void do_annotate(...) { std::cerr << "(not having LocationInfo)\n"; }
+};
+
+template <typename It>
+    struct MinigridParser : qi::grammar<It, row()>
+{
+  MinigridParser(It first) : MinigridParser::base_type(row_), annotate(first)
+  {
+    using namespace qi;
+    type_.add
+      ("W", Type::Wall)
+      (" ", Type::Floor)
+      ("D", Type::Door)
+      ("L", Type::LockedDoor)
+      ("K", Type::Key)
+      ("A", Type::Ball)
+      ("B", Type::Box)
+      ("G", Type::Goal)
+      ("V", Type::Lava)
+      ("n", Type::SlipperyNorth)
+      ("e", Type::SlipperyEast)
+      ("s", Type::SlipperySouth)
+      ("w", Type::SlipperyWest)
+      ("X", Type::Agent)
+      ("Z", Type::Adversary);
+    color_.add
+      ("R", Color::Red)
+      ("G", Color::Green)
+      ("B", Color::Blue)
+      ("P", Color::Purple)
+      ("Y", Color::Yellow)
+      (" ", Color::None);
+
+    cell_ = type_ > color_;
+
+    row_ = (cell_ % -qi::char_("\n"));
+
+    auto set_location_info = annotate(_val, _1, _3);
+    on_success(cell_, set_location_info);
+
+    BOOST_SPIRIT_DEBUG_NODE(type_);
+    BOOST_SPIRIT_DEBUG_NODE(color_);
+    BOOST_SPIRIT_DEBUG_NODE(cell_);
+  }
+
+  private:
+    phoenix::function<annotation_f<It>> annotate;
+
+    qi::symbols<char, Type>  type_;
+    qi::symbols<char, Color> color_;
+
+    qi::rule<It, cell()> cell_;
+    qi::rule<It, row()>  row_;
+};
+
+typedef boost::tokenizer< boost::escaped_list_separator<char> , std::string::const_iterator, std::string> Tokenizer;
+//std::ostream& operator<<(std::ostream& os, const row& r);
diff --git a/util/OptionParser.cpp b/util/OptionParser.cpp
new file mode 100644
index 0000000..715c8c4
--- /dev/null
+++ b/util/OptionParser.cpp
@@ -0,0 +1,32 @@
+#include <iostream>
+
+#include "popl.hpp"
+#include "OptionParser.h"
+
+namespace io {
+  int printPoplException(const popl::invalid_option &e) {
+    std::cerr << "Invalid Option Exception: " << e.what() << "\n";
+		std::cerr << "error:  ";
+		if (e.error() == popl::invalid_option::Error::missing_argument) {
+			std::cerr << "missing_argument\n";
+    } else if (e.error() == popl::invalid_option::Error::invalid_argument) {
+			std::cerr << "invalid_argument\n";
+    } else if (e.error() == popl::invalid_option::Error::too_many_arguments) {
+			std::cerr << "too_many_arguments\n";
+    } else if (e.error() == popl::invalid_option::Error::missing_option) {
+			std::cerr << "missing_option\n";
+    }
+
+		if (e.error() == popl::invalid_option::Error::missing_option) {
+      std::string option_name(e.option()->name(popl::OptionName::short_name, true));
+			if (option_name.empty())
+				option_name = e.option()->name(popl::OptionName::long_name, true);
+			std::cerr << "option: " << option_name << "\n";
+		}
+		else {
+			std::cerr << "option: " << e.option()->name(e.what_name()) << "\n";
+			std::cerr << "value:  " << e.value() << "\n";
+		}
+		return EXIT_FAILURE;
+  }
+}
diff --git a/util/OptionParser.h b/util/OptionParser.h
new file mode 100644
index 0000000..68af918
--- /dev/null
+++ b/util/OptionParser.h
@@ -0,0 +1,13 @@
+#pragma once
+
+#include <iostream>
+
+#include "popl.hpp"
+
+#define INPUT_ERROR 1
+#define INPUT_OK 0
+
+namespace io {
+  int printPoplException(const popl::invalid_option &e);
+
+}
diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp
new file mode 100644
index 0000000..f6aca04
--- /dev/null
+++ b/util/PrismModulesPrinter.cpp
@@ -0,0 +1,681 @@
+#include "PrismModulesPrinter.h"
+
+#include <map>
+#include <string>
+
+namespace prism {
+
+  PrismModulesPrinter::PrismModulesPrinter(const ModelType &modelType, const size_t &numberOfPlayer, const bool enforceOneWays)
+    : modelType(modelType), numberOfPlayer(numberOfPlayer), enforceOneWays(enforceOneWays) {
+  }
+
+  std::ostream& PrismModulesPrinter::printModel(std::ostream &os, const ModelType &modelType) {
+    switch(modelType) {
+      case(ModelType::MDP):
+        os << "mdp";
+        break;
+      case(ModelType::SMG):
+        os << "smg";
+        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 << ")";
+    }
+    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;
+    }
+
+    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 << ")";
+      }
+    }
+    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 = ";
+
+      for (const auto& cell: slipperyEast) {
+        if(first) first = false; else os << " | ";
+        os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
+      }
+      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 << ")";
+      }
+      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";
+    }
+    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 << ")";
+    }
+    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);
+    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;
+    }
+
+    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;
+  }
+
+  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;
+  }
+
+  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) ";
+    }
+    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(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;";
+    }
+    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";
+    }
+    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";
+    }
+    os << "\n";
+    return os;
+  }
+
+  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;
+  }
+
+  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;
+  }
+
+  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";
+
+    return os;
+  }
+
+  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";
+    }
+    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::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::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::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 + ")"
+    };
+
+    // view transition appdx in form (guard, update part)
+    // IMPORTANT: No mod() usage for turn left due to bug in mod() function for decrement
+
+    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)")
+    };
+
+    // direction specifics
+
+    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 }
+
+    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;
+
+      case SlipperyType::South:
+        actionName = "\t[" + agentName + "turn_at_slip_south]";
+        prob_piece_dir = { 1, 1, 0, 0, 0, 0, 0, 1, 0 /* <- R */ };
+        break;
+
+      case SlipperyType::East:
+        actionName = "\t[" + agentName + "turn_at_slip_east]";
+        prob_piece_dir = { 0, 0, 0, 0, 0, 1, 1, 1, 0 /* <- R */ };
+        break;
+
+      case SlipperyType::West:
+        actionName = "\t[" + agentName + "turn_at_slip_west]";
+        prob_piece_dir = { 0, 1, 1, 1, 0, 0, 0, 0, 0 /* <- R */ };
+        break;
+    }
+
+    slipperyActions.insert(actionName);
+
+    // override probability to 0 if corresp. direction is blocked
+
+    for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS - 1; i++) {
+      if (!neighborhood.at(i))
+        prob_piece_dir.at(i) = 0;
+    }
+
+    // determine residual probability (R) by replacing 0 with (1 - overall sum)
+
+    prob_piece_dir.at(remainPosIndex) = PROB_PIECES - std::accumulate(prob_piece_dir.begin(), prob_piece_dir.end(), 0);
+
+    // <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>
+
+
+    // generic output (for every view transition)
+    for (std::size_t v = 0; v < viewTransition.size(); v++) {
+
+        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");
+        }
+    }
+
+    return os;
+  }
+
+  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)"
+    };
+
+    // direction specifics
+
+    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 }
+
+    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;
+
+      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;
+
+      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;
+
+      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;
+    }
+
+    slipperyActions.insert(actionName);
+
+    // override probability to 0 if corresp. direction is blocked
+
+    for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS; i++) {
+      if (!neighborhood.at(i))
+        prob_piece_dir.at(i) = 0;
+    }
+
+    // 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);
+
+    // <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!"));
+    }
+    // </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 ";
+
+    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");
+    }
+
+    return os;
+  }
+
+  std::ostream& PrismModulesPrinter::printEndmodule(std::ostream &os) {
+    os << "endmodule\n";
+    os << "\n";
+    return os;
+  }
+
+  std::ostream& PrismModulesPrinter::printPlayerStruct(std::ostream &os, const AgentName &agentName, const bool agentWithView, const std::vector<float> &probabilities, const std::set<std::string> &slipperyActions) {
+    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;
+    }
+    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) {
+    if(lava.size() != 0) {
+      os << "rewards \"SafetyNoBFS\"\n";
+      os << "\tAgentIsInLavaAndNotDone: -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";
+
+    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 << "endrewards\n";
+
+    if(stateRewards.size() > 0) {
+      os << "rewards \"SafetyWithBFS\"\n";
+      if(lava.size() != 0) os << "\tAgentIsInLavaAndNotDone: -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";
+      if(goals.size() != 0) os << "\tAgentIsInGoalAndNotDone:  100;\n";
+      if(lava.size() != 0) os << "\tAgentIsInLavaAndNotDone: -100;\n";
+      for(auto const [coordinates, reward] : stateRewards) {
+        os << "\txAgent=" << coordinates.first << "&yAgent=" << coordinates.second << " : " << reward << ";\n";
+      }
+      os << "endrewards\n";
+    }
+
+    for(auto const entry : backgroundTiles)
+    {
+      std::cout << getColor(entry.first) << " ";
+      for(auto const cell : entry.second){
+        std::cout << cell.getCoordinates().first << " " << cell.getCoordinates().second << std::endl;
+      }
+    }
+    if(backgroundTiles.size() > 0) {
+      os << "rewards \"TaxiReward\"\n";
+      os << "\t!AgentIsInGoal : -1;\n";
+      std::string allPassengersPickedUp = "";
+      bool first = true;
+      for(auto const [color, cells] : backgroundTiles) {
+        if(cells.size() == 0) continue;
+        if(first) first = false; else allPassengersPickedUp += "&";
+        std::string c = getColor(color);
+        c.at(0) = std::toupper(c.at(0));
+        std::string visitedLabel = agentName + "_picked_up_" + c;
+        allPassengersPickedUp += visitedLabel;
+        os << "[" << agentName << "_pickup_" << c << "] true : 100;\n";
+      }
+      if(goals.size() != 0) os << "\tAgentIsInGoalAndNotDone & " << allPassengersPickedUp << " :  100;\n";
+      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::moveUpdate(const size_t &agentIndex) {
+    return isGame() ?
+             (agentIndex == numberOfPlayer - 1) ?
+               " & (move'=0) " :
+               " & (move'=" + std::to_string(agentIndex + 1) + ") " :
+               "";
+  }
+
+  std::string PrismModulesPrinter::viewVariable(const AgentName &agentName, const size_t &agentDirection, const bool agentWithView) {
+    return agentWithView ? " view" + agentName + "=" + std::to_string(agentDirection) + " & " : " ";
+  }
+
+  bool PrismModulesPrinter::isGame() const {
+    return modelType == ModelType::SMG;
+  }
+}
diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h
new file mode 100644
index 0000000..7a196fc
--- /dev/null
+++ b/util/PrismModulesPrinter.h
@@ -0,0 +1,91 @@
+#pragma once
+
+#include <iostream>
+#include <functional>
+#include "MinigridGrammar.h"
+#include "PrismPrinter.h"
+
+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);
+
+      bool isGame() const;
+    private:
+
+      ModelType const& modelType;
+      const size_t numberOfPlayer;
+      bool enforceOneWays;
+  };
+}
diff --git a/util/PrismPrinter.h b/util/PrismPrinter.h
new file mode 100644
index 0000000..ed12126
--- /dev/null
+++ b/util/PrismPrinter.h
@@ -0,0 +1,15 @@
+#pragma once
+
+#include <string>
+
+#include "cell.h"
+
+typedef std::string AgentName;
+typedef std::pair<std::string, coordinates> AgentNameAndPosition;
+typedef std::map<AgentNameAndPosition::first_type, AgentNameAndPosition::second_type> AgentNameAndPositionMap;
+
+namespace prism {
+  enum class ModelType {
+    MDP, SMG
+  };
+}
diff --git a/util/cell.cpp b/util/cell.cpp
new file mode 100644
index 0000000..07d25f7
--- /dev/null
+++ b/util/cell.cpp
@@ -0,0 +1,83 @@
+#include "cell.h"
+
+#include <stdexcept>
+
+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 << ")";
+  return os;
+}
+
+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;
+      });
+  if(north == grid.end()) {
+    throw std::logic_error{ "Cannot get cell north of (" + std::to_string(row) + "," + std::to_string(column) + ")"};
+    std::exit(EXIT_FAILURE);
+  }
+  return *north;
+}
+
+cell cell::getEast(const std::vector<cell> &grid) const {
+  auto east = std::find_if(grid.begin(), grid.end(), [this](const cell &c) {
+        return this->row == c.row && this->column + 1 == c.column;
+      });
+  if(east == grid.end()) {
+    throw std::logic_error{ "Cannot get cell east of (" + std::to_string(row) + "," + std::to_string(column) + ")"};
+    std::exit(EXIT_FAILURE);
+  }
+  return *east;
+}
+
+cell cell::getSouth(const std::vector<cell> &grid) const {
+  auto south = std::find_if(grid.begin(), grid.end(), [this](const cell &c) {
+        return this->row + 1 == c.row && this->column == c.column;
+      });
+  if(south == grid.end()) {
+    throw std::logic_error{ "Cannot get cell south of (" + std::to_string(row) + "," + std::to_string(column) + ")"};
+    std::exit(EXIT_FAILURE);
+  }
+  return *south;
+}
+
+cell cell::getWest(const std::vector<cell> &grid) const {
+  auto west = std::find_if(grid.begin(), grid.end(), [this](const cell &c) {
+        return this->row == c.row && this->column - 1 == c.column;
+      });
+  if(west == grid.end()) {
+    throw std::logic_error{ "Cannot get cell west of (" + std::to_string(row) + "," + std::to_string(column) + ")"};
+    std::exit(EXIT_FAILURE);
+  }
+  return *west;
+}
+
+coordinates cell::getCoordinates() const {
+  return std::make_pair(row, column);
+}
+
+std::string cell::getColor() const {
+  switch(color) {
+    case Color::Red:    return "red";
+    case Color::Green:  return "green";
+    case Color::Blue:   return "blue";
+    case Color::Purple: return "purple";
+    case Color::Yellow: return "yellow";
+    case Color::None:   return "transparent";
+    default: return "";
+    //case Color::Grey   = 'G',
+  }
+}
+
+std::string getColor(Color color) {
+  switch(color) {
+    case Color::Red:    return "red";
+    case Color::Green:  return "green";
+    case Color::Blue:   return "blue";
+    case Color::Purple: return "purple";
+    case Color::Yellow: return "yellow";
+    case Color::None:   return "transparent";
+    default: return "";
+    //case Color::Grey   = 'G',
+  }
+}
diff --git a/util/cell.h b/util/cell.h
new file mode 100644
index 0000000..c369052
--- /dev/null
+++ b/util/cell.h
@@ -0,0 +1,62 @@
+#pragma once
+
+#include <iostream>
+#include <utility>
+#include <vector>
+
+typedef std::pair<int, int> coordinates;
+
+class Grid;
+
+enum class Type : char {
+  Wall       = 'W',
+  Floor      = ' ',
+  Door       = 'D',
+  LockedDoor = 'L',
+  Key        = 'K',
+  Ball       = 'A',
+  Box        = 'B',
+  Goal       = 'G',
+  Lava       = 'V',
+  Agent      = 'X',
+  Adversary  = 'Z',
+  SlipperyNorth = 'n',
+  SlipperySouth = 's',
+  SlipperyEast  = 'e',
+  SlipperyWest  = 'w'
+};
+enum class Color : char {
+  Red    = 'R',
+  Green  = 'G',
+  Blue   = 'B',
+  Purple = 'P',
+  Yellow = 'Y',
+  //Grey   = 'G',
+  None   = ' '
+};
+
+constexpr std::initializer_list<Color> allColors = {Color::Red, Color::Green, Color::Blue, Color::Purple, Color::Yellow};
+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); }
+
+    cell getNorth(const std::vector<cell> &grid) const;
+    cell getEast(const std::vector<cell> &grid) const;
+    cell getSouth(const std::vector<cell> &grid) const;
+    cell getWest(const std::vector<cell> &grid) const;
+
+    friend std::ostream& operator<<(std::ostream& os, const cell& cell);
+
+    coordinates getCoordinates() const;
+    std::string getColor() const;
+
+    int row;
+    int column;
+    Type type;
+    Color color;
+};
diff --git a/util/popl.hpp b/util/popl.hpp
new file mode 100644
index 0000000..8fd668b
--- /dev/null
+++ b/util/popl.hpp
@@ -0,0 +1,1331 @@
+/***
+     ____   __  ____  __
+    (  _ \ /  \(  _ \(  )
+     ) __/(  O )) __// (_/\
+    (__)   \__/(__)  \____/
+    version 1.3.0
+    https://github.com/badaix/popl
+
+    This file is part of popl (program options parser lib)
+    Copyright (C) 2015-2021 Johannes Pohl
+
+    This software may be modified and distributed under the terms
+    of the MIT license.  See the LICENSE file for details.
+***/
+
+/// checked with clang-tidy:
+/// run-clang-tidy-3.8.py -header-filter='.*'
+/// -checks='*,-misc-definitions-in-headers,-google-readability-braces-around-statements,-readability-braces-around-statements,-cppcoreguidelines-pro-bounds-pointer-arithmetic,-google-build-using-namespace,-google-build-using-namespace'
+
+#ifndef POPL_HPP
+#define POPL_HPP
+
+#ifndef NOMINMAX
+#define NOMINMAX
+#endif // NOMINMAX
+
+#include <algorithm>
+#include <cstdio>
+#include <cstring>
+#include <fstream>
+#include <iostream>
+#include <memory>
+#include <sstream>
+#include <stdexcept>
+#include <vector>
+#ifdef WINDOWS
+#include <cctype>
+#endif
+
+
+namespace popl
+{
+
+#define POPL_VERSION "1.3.0"
+
+
+/// Option's argument type
+/**
+ * Switch has "no" argument
+ * Value has "required" argument
+ * Implicit has "optional" argument
+ */
+enum class Argument
+{
+    no = 0,   // option never takes an argument
+    required, // option always requires an argument
+    optional  // option may take an argument
+};
+
+
+/// Option's attribute
+/**
+ * inactive: Option is not set and will not be parsed
+ * hidden:   Option is active, but will not show up in the help message
+ * required: Option must be set on the command line. Otherwise an exception will be thrown
+ * optional: Option must not be set. Default attribute.
+ * advanced: Option is advanced and will only show up in the advanced help message
+ * expoert:  Option is expert and will only show up in the expert help message
+ */
+enum class Attribute
+{
+    inactive = 0,
+    hidden = 1,
+    required = 2,
+    optional = 3,
+    advanced = 4,
+    expert = 5
+};
+
+
+/// Option name type. Used in invalid_option exception.
+/**
+ * unspecified: not specified
+ * short_name:  The option's short name
+ * long_name:   The option's long name
+ */
+enum class OptionName
+{
+    unspecified,
+    short_name,
+    long_name
+};
+
+
+/// Abstract Base class for Options
+/**
+ * Base class for Options
+ * holds just configuration data, no runtime data.
+ * Option is not bound to a special type "T"
+ */
+class Option
+{
+    friend class OptionParser;
+
+public:
+    /// Construct an Option
+    /// @param short_name the options's short name. Must be empty or one character.
+    /// @param long_name the option's long name. Can be empty.
+    /// @param description the Option's description that will be shown in the help message
+    Option(const std::string& short_name, const std::string& long_name, std::string description);
+
+    /// Destructor
+    virtual ~Option() = default;
+
+    /// default copy constructor
+    Option(const Option&) = default;
+
+    /// default move constructor
+    Option(Option&&) = default;
+
+    /// default assignement operator
+    Option& operator=(const Option&) = default;
+
+    /// default move assignement operator
+    Option& operator=(Option&&) = default;
+
+    /// Get the Option's short name
+    /// @return character of the options's short name or 0 if no short name is defined
+    char short_name() const;
+
+    /// Get the Option's long name
+    /// @return the long name of the Option. Empty string if no long name is defined
+    std::string long_name() const;
+
+    /// Get the Option's long or short name
+    /// @param what_name the option's name to return
+    /// @param what_hyphen preced the returned name with (double-)hypen
+    /// @return the requested name of the Option. Empty string if not defined.
+    std::string name(OptionName what_name, bool with_hypen = false) const;
+
+    /// Get the Option's description
+    /// @return the description
+    std::string description() const;
+
+    /// Get the Option's default value
+    /// @param out stream to write the default value to
+    /// @return true if a default value is available, false if not
+    virtual bool get_default(std::ostream& out) const = 0;
+
+    /// Set the Option's attribute
+    /// @param attribute
+    void set_attribute(const Attribute& attribute);
+
+    /// Get the Option's attribute
+    /// @return the Options's attribute
+    Attribute attribute() const;
+
+    /// Get the Option's argument type
+    /// @return argument type (no, required, optional)
+    virtual Argument argument_type() const = 0;
+
+    /// Check how often the Option is set on command line
+    /// @return the Option's count on command line
+    virtual size_t count() const = 0;
+
+    /// Check if the Option is set
+    /// @return true if set at least once
+    virtual bool is_set() const = 0;
+
+
+protected:
+    /// Parse the command line option and fill the internal data structure
+    /// @param what_name short or long option name
+    /// @param value the value as given on command line
+    virtual void parse(OptionName what_name, const char* value) = 0;
+
+    /// Clear the internal data structure
+    virtual void clear() = 0;
+
+    std::string short_name_;
+    std::string long_name_;
+    std::string description_;
+    Attribute attribute_;
+};
+
+
+
+/// Value option with optional default value
+/**
+ * Value option with optional default value
+ * If set, it requires an argument
+ */
+template <class T>
+class Value : public Option
+{
+public:
+    /// Construct an Value Option
+    /// @param short_name the option's short name. Must be empty or one character.
+    /// @param long_name the option's long name. Can be empty.
+    /// @param description the Option's description that will be shown in the help message
+    Value(const std::string& short_name, const std::string& long_name, const std::string& description);
+
+    /// Construct an Value Option
+    /// @param short_name the option's short name. Must be empty or one character.
+    /// @param long_name the option's long name. Can be empty.
+    /// @param description the Option's description that will be shown in the help message
+    /// @param default_val the Option's default value
+    /// @param assign_to pointer to a variable to assign the parsed command line value to
+    Value(const std::string& short_name, const std::string& long_name, const std::string& description, const T& default_val, T* assign_to = nullptr);
+
+    size_t count() const override;
+    bool is_set() const override;
+
+    /// Assign the last parsed command line value to "var"
+    /// @param var pointer to the variable where is value is written to
+    void assign_to(T* var);
+
+    /// Manually set the Option's value. Deletes current value(s)
+    /// @param value the new value of the option
+    void set_value(const T& value);
+
+    /// Get the Option's value. Will throw if option at index idx is not available
+    /// @param idx the zero based index of the value (if set multiple times)
+    /// @return the Option's value at index "idx"
+    T value(size_t idx = 0) const;
+
+    /// Get the Option's value, return default_value if not set.
+    /// @param default_value return value if value is not set
+    /// @param idx the zero based index of the value (if set multiple times)
+    /// @return the Option's value at index "idx" or the default value or default_value
+    T value_or(const T& default_value, size_t idx = 0) const;
+
+    /// Set the Option's default value
+    /// @param value the default value if not specified on command line
+    void set_default(const T& value);
+
+    /// Check if the Option has a default value
+    /// @return true if the Option has a default value
+    bool has_default() const;
+
+    /// Get the Option's default value. Will throw if no default is set.
+    /// @return the Option's default value
+    T get_default() const;
+    bool get_default(std::ostream& out) const override;
+
+    Argument argument_type() const override;
+
+protected:
+    void parse(OptionName what_name, const char* value) override;
+    std::unique_ptr<T> default_;
+
+    virtual void update_reference();
+    virtual void add_value(const T& value);
+    void clear() override;
+
+    T* assign_to_;
+    std::vector<T> values_;
+};
+
+
+
+/// Value option with implicit default value
+/**
+ * Value option with implicit default value
+ * If set, an argument is optional
+ * -without argument it carries the implicit default value
+ * -with argument it carries the explicit value
+ */
+template <class T>
+class Implicit : public Value<T>
+{
+public:
+    Implicit(const std::string& short_name, const std::string& long_name, const std::string& description, const T& implicit_val, T* assign_to = nullptr);
+
+    Argument argument_type() const override;
+
+protected:
+    void parse(OptionName what_name, const char* value) override;
+};
+
+
+
+/// Value option without value
+/**
+ * Value option without value
+ * Does not require an argument
+ * Can be either set or not set
+ */
+class Switch : public Value<bool>
+{
+public:
+    Switch(const std::string& short_name, const std::string& long_name, const std::string& description, bool* assign_to = nullptr);
+
+    void set_default(const bool& value) = delete;
+    Argument argument_type() const override;
+
+protected:
+    void parse(OptionName what_name, const char* value) override;
+};
+
+
+
+using Option_ptr = std::shared_ptr<Option>;
+
+/// OptionParser manages all Options
+/**
+ * OptionParser manages all Options
+ * Add Options (Option_Type = Value<T>, Implicit<T> or Switch) with "add<Option_Type>(option params)"
+ * Call "parse(argc, argv)" to trigger parsing of the options and to
+ * fill "non_option_args" and "unknown_options"
+ */
+class OptionParser
+{
+public:
+    /// Construct the OptionParser
+    /// @param description used for the help message
+    explicit OptionParser(std::string description = "");
+
+    /// Destructor
+    virtual ~OptionParser() = default;
+
+    /// Add an Option e.g. 'add<Value<int>>("i", "int", "description for the -i option")'
+    /// @param T the option type (Value, Switch, Implicit)
+    /// @param attribute the Option's attribute (inactive, hidden, required, optional, ...)
+    /// @param Ts the Option's parameter
+    template <typename T, Attribute attribute, typename... Ts>
+    std::shared_ptr<T> add(Ts&&... params);
+
+    /// Add an Option e.g. 'add<Value<int>>("i", "int", "description for the -i option")'
+    /// @param T the option type (Value, Switch, Implicit)
+    /// @param Ts the Option's parameter
+    template <typename T, typename... Ts>
+    std::shared_ptr<T> add(Ts&&... params);
+
+    /// Parse an ini file into the added Options
+    /// @param ini_filename full path of the ini file
+    void parse(const std::string& ini_filename);
+
+    /// Parse the command line into the added Options
+    /// @param argc command line argument count
+    /// @param argv command line arguments
+    void parse(int argc, const char* const argv[]);
+
+    /// Delete all parsed options
+    void reset();
+
+    /// Produce a help message
+    /// @param max_attribute show options up to this level (optional, advanced, expert)
+    /// @return the help message
+    std::string help(const Attribute& max_attribute = Attribute::optional) const;
+
+    /// Get the OptionParser's description
+    /// @return the description as given during construction
+    std::string description() const;
+
+    /// Get all options that where added with "add"
+    /// @return a vector of the contained Options
+    const std::vector<Option_ptr>& options() const;
+
+    /// Get command line arguments without option
+    /// e.g. "-i 5 hello" => hello
+    /// e.g. "-i 5 -- from here non option args" => "from", "here", "non", "option", "args"
+    /// @return vector to "stand-alone" command line arguments
+    const std::vector<std::string>& non_option_args() const;
+
+    /// Get unknown command options
+    /// e.g. '--some_unknown_option="hello"'
+    /// @return vector to "stand-alone" command line arguments
+    const std::vector<std::string>& unknown_options() const;
+
+    /// Get an Option by it's long name
+    /// @param the Option's long name
+    /// @return a pointer of type "Value, Switch, Implicit" to the Option or nullptr
+    template <typename T>
+    std::shared_ptr<T> get_option(const std::string& long_name) const;
+
+    /// Get an Option by it's short name
+    /// @param the Option's short name
+    /// @return a pointer of type "Value, Switch, Implicit" to the Option or nullptr
+    template <typename T>
+    std::shared_ptr<T> get_option(char short_name) const;
+
+protected:
+    std::vector<Option_ptr> options_;
+    std::string description_;
+    std::vector<std::string> non_option_args_;
+    std::vector<std::string> unknown_options_;
+
+    Option_ptr find_option(const std::string& long_name) const;
+    Option_ptr find_option(char short_name) const;
+};
+
+
+
+class invalid_option : public std::invalid_argument
+{
+public:
+    enum class Error
+    {
+        missing_argument,
+        invalid_argument,
+        too_many_arguments,
+        missing_option
+    };
+
+    invalid_option(const Option* option, invalid_option::Error error, OptionName what_name, std::string value, const std::string& text)
+        : std::invalid_argument(text.c_str()), option_(option), error_(error), what_name_(what_name), value_(std::move(value))
+    {
+    }
+
+    invalid_option(const Option* option, invalid_option::Error error, const std::string& text)
+        : invalid_option(option, error, OptionName::unspecified, "", text)
+    {
+    }
+
+    const Option* option() const
+    {
+        return option_;
+    }
+
+    Error error() const
+    {
+        return error_;
+    }
+
+    OptionName what_name() const
+    {
+        return what_name_;
+    }
+
+    std::string value() const
+    {
+        return value_;
+    }
+
+private:
+    const Option* option_;
+    Error error_;
+    OptionName what_name_;
+    std::string value_;
+};
+
+
+
+/// Base class for an OptionPrinter
+/**
+ * OptionPrinter creates a help message for a given OptionParser
+ */
+class OptionPrinter
+{
+public:
+    /// Constructor
+    /// @param option_parser the OptionParser to create the help message from
+    explicit OptionPrinter(const OptionParser* option_parser) : option_parser_(option_parser)
+    {
+    }
+
+    /// Destructor
+    virtual ~OptionPrinter() = default;
+
+    /// Create a help message
+    /// @param max_attribute show options up to this level (optional, advanced, expert)
+    /// @return the help message
+    virtual std::string print(const Attribute& max_attribute = Attribute::optional) const = 0;
+
+protected:
+    const OptionParser* option_parser_;
+};
+
+
+
+/// Option printer for the console
+/**
+ * Standard console option printer
+ * Creates a human readable help message
+ */
+class ConsoleOptionPrinter : public OptionPrinter
+{
+public:
+    explicit ConsoleOptionPrinter(const OptionParser* option_parser);
+    ~ConsoleOptionPrinter() override = default;
+
+    std::string print(const Attribute& max_attribute = Attribute::optional) const override;
+
+private:
+    std::string to_string(Option_ptr option) const;
+};
+
+
+
+/// Option printer for man pages
+/**
+ * Creates help messages in groff format that can be used in man pages
+ */
+class GroffOptionPrinter : public OptionPrinter
+{
+public:
+    explicit GroffOptionPrinter(const OptionParser* option_parser);
+    ~GroffOptionPrinter() override = default;
+
+    std::string print(const Attribute& max_attribute = Attribute::optional) const override;
+
+private:
+    std::string to_string(Option_ptr option) const;
+};
+
+
+
+/// Option printer for bash completion
+/**
+ * Creates a script with all options (short and long) that can be used for bash completion
+ */
+class BashCompletionOptionPrinter : public OptionPrinter
+{
+public:
+    BashCompletionOptionPrinter(const OptionParser* option_parser, std::string program_name);
+    ~BashCompletionOptionPrinter() override = default;
+
+    std::string print(const Attribute& max_attribute = Attribute::optional) const override;
+
+private:
+    std::string program_name_;
+};
+
+
+
+/// Option implementation /////////////////////////////////
+
+inline Option::Option(const std::string& short_name, const std::string& long_name, std::string description)
+    : short_name_(short_name), long_name_(long_name), description_(std::move(description)), attribute_(Attribute::optional)
+{
+    if (short_name.size() > 1)
+        throw std::invalid_argument("length of short name must be <= 1: '" + short_name + "'");
+
+    if (short_name.empty() && long_name.empty())
+        throw std::invalid_argument("short and long name are empty");
+}
+
+
+inline char Option::short_name() const
+{
+    if (!short_name_.empty())
+        return short_name_[0];
+    return 0;
+}
+
+
+inline std::string Option::long_name() const
+{
+    return long_name_;
+}
+
+
+inline std::string Option::name(OptionName what_name, bool with_hypen) const
+{
+    if (what_name == OptionName::short_name)
+        return short_name_.empty() ? "" : ((with_hypen ? "-" : "") + short_name_);
+    if (what_name == OptionName::long_name)
+        return long_name_.empty() ? "" : ((with_hypen ? "--" : "") + long_name_);
+    return "";
+}
+
+
+inline std::string Option::description() const
+{
+    return description_;
+}
+
+
+inline void Option::set_attribute(const Attribute& attribute)
+{
+    attribute_ = attribute;
+}
+
+
+inline Attribute Option::attribute() const
+{
+    return attribute_;
+}
+
+
+
+/// Value implementation /////////////////////////////////
+
+template <class T>
+inline Value<T>::Value(const std::string& short_name, const std::string& long_name, const std::string& description)
+    : Option(short_name, long_name, description), assign_to_(nullptr)
+{
+}
+
+
+template <class T>
+inline Value<T>::Value(const std::string& short_name, const std::string& long_name, const std::string& description, const T& default_val, T* assign_to)
+    : Value<T>(short_name, long_name, description)
+{
+    assign_to_ = assign_to;
+    set_default(default_val);
+}
+
+
+template <class T>
+inline size_t Value<T>::count() const
+{
+    return values_.size();
+}
+
+
+template <class T>
+inline bool Value<T>::is_set() const
+{
+    return !values_.empty();
+}
+
+
+template <class T>
+inline void Value<T>::assign_to(T* var)
+{
+    assign_to_ = var;
+    update_reference();
+}
+
+
+template <class T>
+inline void Value<T>::set_value(const T& value)
+{
+    clear();
+    add_value(value);
+}
+
+template <class T>
+inline T Value<T>::value_or(const T& default_value, size_t idx) const
+{
+    if (idx < values_.size())
+        return values_[idx];
+    else if (default_)
+        return *default_;
+    else
+        return default_value;
+}
+
+template <class T>
+inline T Value<T>::value(size_t idx) const
+{
+    if (!this->is_set() && default_)
+        return *default_;
+
+    if (!is_set() || (idx >= count()))
+    {
+        std::stringstream optionStr;
+        if (!is_set())
+            optionStr << "option not set: \"";
+        else
+            optionStr << "index out of range (" << idx << ") for \"";
+
+        if (short_name() != 0)
+            optionStr << "-" << short_name();
+        else
+            optionStr << "--" << long_name();
+
+        optionStr << "\"";
+        throw std::out_of_range(optionStr.str());
+    }
+
+    return values_[idx];
+}
+
+
+
+template <class T>
+inline void Value<T>::set_default(const T& value)
+{
+    this->default_.reset(new T);
+    *this->default_ = value;
+    update_reference();
+}
+
+
+template <class T>
+inline bool Value<T>::has_default() const
+{
+    return (this->default_ != nullptr);
+}
+
+
+template <class T>
+inline T Value<T>::get_default() const
+{
+    if (!has_default())
+        throw std::runtime_error("no default value set");
+    return *this->default_;
+}
+
+
+template <class T>
+inline bool Value<T>::get_default(std::ostream& out) const
+{
+    if (!has_default())
+        return false;
+    out << *this->default_;
+    return true;
+}
+
+
+template <class T>
+inline Argument Value<T>::argument_type() const
+{
+    return Argument::required;
+}
+
+
+template <>
+inline void Value<std::string>::parse(OptionName what_name, const char* value)
+{
+    if (strlen(value) == 0)
+        throw invalid_option(this, invalid_option::Error::missing_argument, what_name, value, "missing argument for " + name(what_name, true));
+
+    add_value(value);
+}
+
+
+template <>
+inline void Value<bool>::parse(OptionName /*what_name*/, const char* value)
+{
+    bool val =
+        ((value != nullptr) && ((strcmp(value, "1") == 0) || (strcmp(value, "true") == 0) || (strcmp(value, "True") == 0) || (strcmp(value, "TRUE") == 0)));
+    add_value(val);
+}
+
+
+template <class T>
+inline void Value<T>::parse(OptionName what_name, const char* value)
+{
+    T parsed_value;
+    std::string strValue;
+    if (value != nullptr)
+        strValue = value;
+
+    std::istringstream is(strValue);
+    int valuesRead = 0;
+    while (is.good())
+    {
+        if (is.peek() != EOF)
+            is >> parsed_value;
+        else
+            break;
+
+        valuesRead++;
+    }
+
+    if (is.fail())
+        throw invalid_option(this, invalid_option::Error::invalid_argument, what_name, value,
+                             "invalid argument for " + name(what_name, true) + ": '" + strValue + "'");
+
+    if (valuesRead > 1)
+        throw invalid_option(this, invalid_option::Error::too_many_arguments, what_name, value,
+                             "too many arguments for " + name(what_name, true) + ": '" + strValue + "'");
+
+    if (strValue.empty())
+        throw invalid_option(this, invalid_option::Error::missing_argument, what_name, "", "missing argument for " + name(what_name, true));
+
+    this->add_value(parsed_value);
+}
+
+
+template <class T>
+inline void Value<T>::update_reference()
+{
+    if (this->assign_to_)
+    {
+        if (!this->is_set() && default_)
+            *this->assign_to_ = *default_;
+        else if (this->is_set())
+            *this->assign_to_ = values_.back();
+    }
+}
+
+
+template <class T>
+inline void Value<T>::add_value(const T& value)
+{
+    values_.push_back(value);
+    update_reference();
+}
+
+
+template <class T>
+inline void Value<T>::clear()
+{
+    values_.clear();
+    update_reference();
+}
+
+
+
+/// Implicit implementation /////////////////////////////////
+
+template <class T>
+inline Implicit<T>::Implicit(const std::string& short_name, const std::string& long_name, const std::string& description, const T& implicit_val, T* assign_to)
+    : Value<T>(short_name, long_name, description, implicit_val, assign_to)
+{
+}
+
+
+template <class T>
+inline Argument Implicit<T>::argument_type() const
+{
+    return Argument::optional;
+}
+
+
+template <class T>
+inline void Implicit<T>::parse(OptionName what_name, const char* value)
+{
+    if ((value != nullptr) && (strlen(value) > 0))
+        Value<T>::parse(what_name, value);
+    else
+        this->add_value(*this->default_);
+}
+
+
+
+/// Switch implementation /////////////////////////////////
+
+inline Switch::Switch(const std::string& short_name, const std::string& long_name, const std::string& description, bool* assign_to)
+    : Value<bool>(short_name, long_name, description, false, assign_to)
+{
+}
+
+
+inline void Switch::parse(OptionName /*what_name*/, const char* /*value*/)
+{
+    add_value(true);
+}
+
+
+inline Argument Switch::argument_type() const
+{
+    return Argument::no;
+}
+
+
+
+/// OptionParser implementation /////////////////////////////////
+
+inline OptionParser::OptionParser(std::string description) : description_(std::move(description))
+{
+}
+
+
+template <typename T, typename... Ts>
+inline std::shared_ptr<T> OptionParser::add(Ts&&... params)
+{
+    return add<T, Attribute::optional>(std::forward<Ts>(params)...);
+}
+
+
+template <typename T, Attribute attribute, typename... Ts>
+inline std::shared_ptr<T> OptionParser::add(Ts&&... params)
+{
+    static_assert(std::is_base_of<Option, typename std::decay<T>::type>::value, "type T must be Switch, Value or Implicit");
+    std::shared_ptr<T> option = std::make_shared<T>(std::forward<Ts>(params)...);
+
+    for (const auto& o : options_)
+    {
+        if ((option->short_name() != 0) && (option->short_name() == o->short_name()))
+            throw std::invalid_argument("duplicate short option name '-" + std::string(1, option->short_name()) + "'");
+        if (!option->long_name().empty() && (option->long_name() == (o->long_name())))
+            throw std::invalid_argument("duplicate long option name '--" + option->long_name() + "'");
+    }
+    option->set_attribute(attribute);
+    options_.push_back(option);
+    return option;
+}
+
+
+inline std::string OptionParser::description() const
+{
+    return description_;
+}
+
+
+inline const std::vector<Option_ptr>& OptionParser::options() const
+{
+    return options_;
+}
+
+
+inline const std::vector<std::string>& OptionParser::non_option_args() const
+{
+    return non_option_args_;
+}
+
+
+inline const std::vector<std::string>& OptionParser::unknown_options() const
+{
+    return unknown_options_;
+}
+
+
+inline Option_ptr OptionParser::find_option(const std::string& long_name) const
+{
+    for (const auto& option : options_)
+        if (option->long_name() == long_name)
+            return option;
+    return nullptr;
+}
+
+
+inline Option_ptr OptionParser::find_option(char short_name) const
+{
+    for (const auto& option : options_)
+        if (option->short_name() == short_name)
+            return option;
+    return nullptr;
+}
+
+
+template <typename T>
+inline std::shared_ptr<T> OptionParser::get_option(const std::string& long_name) const
+{
+    Option_ptr option = find_option(long_name);
+    if (!option)
+        throw std::invalid_argument("option not found: " + long_name);
+    auto result = std::dynamic_pointer_cast<T>(option);
+    if (!result)
+        throw std::invalid_argument("cannot cast option to T: " + long_name);
+    return result;
+}
+
+
+template <typename T>
+inline std::shared_ptr<T> OptionParser::get_option(char short_name) const
+{
+    Option_ptr option = find_option(short_name);
+    if (!option)
+        throw std::invalid_argument("option not found: " + std::string(1, short_name));
+    auto result = std::dynamic_pointer_cast<T>(option);
+    if (!result)
+        throw std::invalid_argument("cannot cast option to T: " + std::string(1, short_name));
+    return result;
+}
+
+inline void OptionParser::parse(const std::string& ini_filename)
+{
+    std::ifstream file(ini_filename.c_str());
+    std::string line;
+
+    auto trim = [](std::string& s) {
+        s.erase(s.begin(), std::find_if(s.begin(), s.end(), [](int ch) { return !std::isspace(ch); }));
+        s.erase(std::find_if(s.rbegin(), s.rend(), [](int ch) { return !std::isspace(ch); }).base(), s.end());
+        return s;
+    };
+
+    auto trim_copy = [trim](const std::string& s) {
+        std::string copy(s);
+        return trim(copy);
+    };
+
+    auto split = [trim_copy](const std::string& s) -> std::pair<std::string, std::string> {
+        size_t pos = s.find('=');
+        if (pos == std::string::npos)
+            return {"", ""};
+        return {trim_copy(s.substr(0, pos)), trim_copy(s.substr(pos + 1, std::string::npos))};
+    };
+
+    std::string section;
+    while (std::getline(file, line))
+    {
+        trim(line);
+        if (line.empty())
+            continue;
+        if (line.front() == '#')
+            continue;
+
+        if ((line.front() == '[') && (line.back() == ']'))
+        {
+            section = trim_copy(line.substr(1, line.size() - 2));
+            continue;
+        }
+        auto key_value = split(line);
+        if (key_value.first.empty())
+            continue;
+
+        std::string key = section.empty() ? key_value.first : section + "." + key_value.first;
+        Option_ptr option = find_option(key);
+        if (option && (option->attribute() == Attribute::inactive))
+            option = nullptr;
+
+        if (option)
+            option->parse(OptionName::long_name, key_value.second.c_str());
+        else
+            unknown_options_.push_back(key);
+    }
+}
+
+inline void OptionParser::parse(int argc, const char* const argv[])
+{
+    for (int n = 1; n < argc; ++n)
+    {
+        const std::string arg(argv[n]);
+        if (arg == "--")
+        {
+            /// from here on only non opt args
+            for (int m = n + 1; m < argc; ++m)
+                non_option_args_.emplace_back(argv[m]);
+        }
+        else if (arg.find("--") == 0)
+        {
+            /// long option arg
+            std::string opt = arg.substr(2);
+            std::string optarg;
+            size_t equalIdx = opt.find('=');
+            if (equalIdx != std::string::npos)
+            {
+                optarg = opt.substr(equalIdx + 1);
+                opt.resize(equalIdx);
+            }
+
+            Option_ptr option = find_option(opt);
+            if (option && (option->attribute() == Attribute::inactive))
+                option = nullptr;
+            if (option)
+            {
+                if (option->argument_type() == Argument::no)
+                {
+                    if (!optarg.empty())
+                        option = nullptr;
+                }
+                else if (option->argument_type() == Argument::required)
+                {
+                    if (optarg.empty() && n < argc - 1)
+                        optarg = argv[++n];
+                }
+            }
+
+            if (option)
+                option->parse(OptionName::long_name, optarg.c_str());
+            else
+                unknown_options_.push_back(arg);
+        }
+        else if (arg.find('-') == 0)
+        {
+            /// short option arg
+            std::string opt = arg.substr(1);
+            bool unknown = false;
+            for (size_t m = 0; m < opt.size(); ++m)
+            {
+                char c = opt[m];
+                std::string optarg;
+
+                Option_ptr option = find_option(c);
+                if (option && (option->attribute() == Attribute::inactive))
+                    option = nullptr;
+                if (option)
+                {
+                    if (option->argument_type() == Argument::required)
+                    {
+                        /// use the rest of the current argument as optarg
+                        optarg = opt.substr(m + 1);
+                        /// or the next arg
+                        if (optarg.empty() && n < argc - 1)
+                            optarg = argv[++n];
+                        m = opt.size();
+                    }
+                    else if (option->argument_type() == Argument::optional)
+                    {
+                        /// use the rest of the current argument as optarg
+                        optarg = opt.substr(m + 1);
+                        m = opt.size();
+                    }
+                }
+
+                if (option)
+                    option->parse(OptionName::short_name, optarg.c_str());
+                else
+                    unknown = true;
+            }
+            if (unknown)
+                unknown_options_.push_back(arg);
+        }
+        else
+        {
+            non_option_args_.push_back(arg);
+        }
+    }
+
+    for (auto& opt : options_)
+    {
+        if ((opt->attribute() == Attribute::required) && !opt->is_set())
+        {
+            std::string option = opt->long_name().empty() ? std::string(1, opt->short_name()) : opt->long_name();
+            throw invalid_option(opt.get(), invalid_option::Error::missing_option, "option \"" + option + "\" is required");
+        }
+    }
+}
+
+
+inline void OptionParser::reset()
+{
+    unknown_options_.clear();
+    non_option_args_.clear();
+    for (auto& opt : options_)
+        opt->clear();
+}
+
+
+inline std::string OptionParser::help(const Attribute& max_attribute) const
+{
+    ConsoleOptionPrinter option_printer(this);
+    return option_printer.print(max_attribute);
+}
+
+
+
+/// ConsoleOptionPrinter implementation /////////////////////////////////
+
+inline ConsoleOptionPrinter::ConsoleOptionPrinter(const OptionParser* option_parser) : OptionPrinter(option_parser)
+{
+}
+
+
+inline std::string ConsoleOptionPrinter::to_string(Option_ptr option) const
+{
+    std::stringstream line;
+    if (option->short_name() != 0)
+    {
+        line << "  -" << option->short_name();
+        if (!option->long_name().empty())
+            line << ", ";
+    }
+    else
+        line << "  ";
+    if (!option->long_name().empty())
+        line << "--" << option->long_name();
+
+    if (option->argument_type() == Argument::required)
+    {
+        line << " arg";
+        std::stringstream defaultStr;
+        if (option->get_default(defaultStr))
+        {
+            if (!defaultStr.str().empty())
+                line << " (=" << defaultStr.str() << ")";
+        }
+    }
+    else if (option->argument_type() == Argument::optional)
+    {
+        std::stringstream defaultStr;
+        if (option->get_default(defaultStr))
+            line << " [=arg(=" << defaultStr.str() << ")]";
+    }
+
+    return line.str();
+}
+
+
+inline std::string ConsoleOptionPrinter::print(const Attribute& max_attribute) const
+{
+    if (option_parser_ == nullptr)
+        return "";
+
+    if (max_attribute < Attribute::optional)
+        throw std::invalid_argument("attribute must be 'optional', 'advanced', or 'default'");
+
+    std::stringstream s;
+    if (!option_parser_->description().empty())
+        s << option_parser_->description() << ":\n";
+
+    size_t optionRightMargin(20);
+    const size_t maxDescriptionLeftMargin(40);
+    //	const size_t descriptionRightMargin(80);
+
+    for (const auto& option : option_parser_->options())
+        optionRightMargin = std::max(optionRightMargin, to_string(option).size() + 2);
+    optionRightMargin = std::min(maxDescriptionLeftMargin - 2, optionRightMargin);
+
+    for (const auto& option : option_parser_->options())
+    {
+        if ((option->attribute() <= Attribute::hidden) || (option->attribute() > max_attribute))
+            continue;
+        std::string optionStr = to_string(option);
+        if (optionStr.size() < optionRightMargin)
+            optionStr.resize(optionRightMargin, ' ');
+        else
+            optionStr += "\n" + std::string(optionRightMargin, ' ');
+        s << optionStr;
+
+        std::string line;
+        std::vector<std::string> lines;
+        std::stringstream description(option->description());
+        while (std::getline(description, line, '\n'))
+            lines.push_back(line);
+
+        std::string empty(optionRightMargin, ' ');
+        for (size_t n = 0; n < lines.size(); ++n)
+        {
+            if (n > 0)
+                s << "\n" << empty;
+            s << lines[n];
+        }
+        s << "\n";
+    }
+
+    return s.str();
+}
+
+
+
+/// GroffOptionPrinter implementation /////////////////////////////////
+
+inline GroffOptionPrinter::GroffOptionPrinter(const OptionParser* option_parser) : OptionPrinter(option_parser)
+{
+}
+
+
+inline std::string GroffOptionPrinter::to_string(Option_ptr option) const
+{
+    std::stringstream line;
+    if (option->short_name() != 0)
+    {
+        line << "-" << option->short_name();
+        if (!option->long_name().empty())
+            line << ", ";
+    }
+    if (!option->long_name().empty())
+        line << "--" << option->long_name();
+
+    if (option->argument_type() == Argument::required)
+    {
+        line << " arg";
+        std::stringstream defaultStr;
+        if (option->get_default(defaultStr))
+        {
+            if (!defaultStr.str().empty())
+                line << " (=" << defaultStr.str() << ")";
+        }
+    }
+    else if (option->argument_type() == Argument::optional)
+    {
+        std::stringstream defaultStr;
+        if (option->get_default(defaultStr))
+            line << " [=arg(=" << defaultStr.str() << ")]";
+    }
+
+    return line.str();
+}
+
+
+inline std::string GroffOptionPrinter::print(const Attribute& max_attribute) const
+{
+    if (option_parser_ == nullptr)
+        return "";
+
+    if (max_attribute < Attribute::optional)
+        throw std::invalid_argument("attribute must be 'optional', 'advanced', or 'default'");
+
+    std::stringstream s;
+    if (!option_parser_->description().empty())
+        s << ".SS " << option_parser_->description() << ":\n";
+
+    for (const auto& option : option_parser_->options())
+    {
+        if ((option->attribute() <= Attribute::hidden) || (option->attribute() > max_attribute))
+            continue;
+        s << ".TP\n\\fB" << to_string(option) << "\\fR\n";
+        if (!option->description().empty())
+            s << option->description() << "\n";
+    }
+
+    return s.str();
+}
+
+
+
+/// BashCompletionOptionPrinter implementation /////////////////////////////////
+
+inline BashCompletionOptionPrinter::BashCompletionOptionPrinter(const OptionParser* option_parser, std::string program_name)
+    : OptionPrinter(option_parser), program_name_(std::move(program_name))
+{
+}
+
+
+inline std::string BashCompletionOptionPrinter::print(const Attribute& /*max_attribute*/) const
+{
+    if (option_parser_ == nullptr)
+        return "";
+
+    std::stringstream s;
+    s << "_" << program_name_ << "()\n";
+    s << R"({
+	local cur prev opts
+	COMPREPLY=()
+	cur="${COMP_WORDS[COMP_CWORD]}"
+	prev="${COMP_WORDS[COMP_CWORD-1]}"
+	opts=")";
+
+    for (const auto& option : option_parser_->options())
+    {
+        if (option->attribute() > Attribute::hidden)
+        {
+            if (option->short_name() != 0)
+                s << "-" << option->short_name() << " ";
+            if (!option->long_name().empty())
+                s << "--" << option->long_name() << " ";
+        }
+    }
+
+    s << R"("
+	if [[ ${cur} == -* ]] ; then
+		COMPREPLY=( $(compgen -W "${opts}" -- ${cur}) )
+		return 0
+	fi
+}
+complete -F )";
+    s << "_" << program_name_ << " " << program_name_ << "\n";
+
+    return s.str();
+}
+
+
+
+static inline std::ostream& operator<<(std::ostream& out, const OptionParser& op)
+{
+    return out << op.help();
+}
+
+
+} // namespace popl
+
+
+#endif // POPL_HPP