From 85d0cbc81fe54af056f0253029bcaf3ca0604db5 Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Thu, 17 Aug 2023 11:41:16 +0200
Subject: [PATCH] initial commit
after modifications for Importance Driven Testing
---
.gitignore | 34 +
CMakeLists.txt | 22 +
main.cpp | 171 +++++
util/CMakeLists.txt | 8 +
util/Grid.cpp | 229 ++++++
util/Grid.h | 63 ++
util/MinigridGrammar.h | 102 +++
util/OptionParser.cpp | 32 +
util/OptionParser.h | 13 +
util/PrismModulesPrinter.cpp | 681 +++++++++++++++++
util/PrismModulesPrinter.h | 91 +++
util/PrismPrinter.h | 15 +
util/cell.cpp | 83 +++
util/cell.h | 62 ++
util/popl.hpp | 1331 ++++++++++++++++++++++++++++++++++
15 files changed, 2937 insertions(+)
create mode 100644 .gitignore
create mode 100644 CMakeLists.txt
create mode 100644 main.cpp
create mode 100644 util/CMakeLists.txt
create mode 100644 util/Grid.cpp
create mode 100644 util/Grid.h
create mode 100644 util/MinigridGrammar.h
create mode 100644 util/OptionParser.cpp
create mode 100644 util/OptionParser.h
create mode 100644 util/PrismModulesPrinter.cpp
create mode 100644 util/PrismModulesPrinter.h
create mode 100644 util/PrismPrinter.h
create mode 100644 util/cell.cpp
create mode 100644 util/cell.h
create mode 100644 util/popl.hpp
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