sp
/
Minigrid2PRISM
1
0
Fork 0
Code Issues 5 Pull Requests 1 Projects Releases Wiki Activity
Labels Milestones
New Pull Request

Refactoring of Prism Output #1

Merged
sp merged 38 commits from adversaries_and_refactoring into tempestpyadaption 6 months ago
Conversation 0 Commits 38 Files Changed 13
13 changed files with 944 additions and 1282 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 38
      CMakeLists.txt
  2. 12
      main.cpp
  3. 2
      util/CMakeLists.txt
  4. 272
      util/Grid.cpp
  5. 11
      util/Grid.h
  6. 222
      util/PrismFormulaPrinter.cpp
  7. 61
      util/PrismFormulaPrinter.h
  8. 1358
      util/PrismModulesPrinter.cpp
  9. 194
      util/PrismModulesPrinter.h
  10. 8
      util/PrismPrinter.cpp
  11. 8
      util/PrismPrinter.h
  12. 31
      util/cell.cpp
  13. 9
      util/cell.h

38
CMakeLists.txt
View File

@ -1,24 +1,26 @@
include(util/CMakeLists.txt)
set(CMAKE_CXX_STANDARD 20)
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D__FILENAME__='\"$(subst ${CMAKE_SOURCE_DIR}/,,$(abspath $<))\"'")
add_definitions(-DLOG_DEBUG)
cmake_minimum_required(VERSION 3.0...3.22)
set(CMAKE_BUILD_TYPE Debug)
project(
Minigrid2PRISM
VERSION 0.1
LANGUAGES CXX)
set(CMAKE_CXX_STANDARD 20)
find_package(yaml-cpp)
add_executable(main
${SRCS}
main.cpp
)
target_link_libraries(main pthread yaml-cpp)
include(util/CMakeLists.txt)
include(FetchContent)
FetchContent_Declare(
yaml-cpp
GIT_REPOSITORY https://github.com/jbeder/yaml-cpp.git
GIT_TAG master
OVERRIDE_FIND_PACKAGE
)
FetchContent_GetProperties(yaml-cpp)
if(NOT yaml-cpp_POPULATED)
message(STATUS "Fetching yaml-cpp...")
FetchContent_Populate(yaml-cpp)
add_subdirectory(${yaml-cpp_SOURCE_DIR} ${yaml-cpp_BINARY_DIR})
endif()
FetchContent_MakeAvailable(yaml-cpp)
add_executable(main ${SRCS} main.cpp)
target_link_libraries(main pthread yaml-cpp::yaml-cpp)

12
main.cpp
View File

@ -144,12 +144,13 @@ int main(int argc, char* argv[]) {
pos_iterator_t backgroundIter = backgroundFirst;
pos_iterator_t backgroundLast(background.end());
MinigridParser<pos_iterator_t> backgroundParser(backgroundFirst);
cells contentCells;
cells backgroundCells;
std::vector<Configuration> configurations;
std::map<coordinates, float> stateRewards;
double faultyProbability;
float faultyProbability = 0.0;
float probIntended = 0.9;
try {
bool ok = phrase_parse(contentIter, contentLast, contentParser, qi::space, contentCells);
@ -157,7 +158,7 @@ int main(int argc, char* argv[]) {
ok &= phrase_parse(backgroundIter, backgroundLast, backgroundParser, qi::space, backgroundCells);
// TODO }
if (configFilename->is_set()) {
YamlConfigParser parser(configFilename->value(0));
YamlConfigParser parser(configFilename->value(0));
configurations = parser.parseConfiguration();
}
@ -181,8 +182,9 @@ int main(int argc, char* argv[]) {
}
}
if(ok) {
Grid grid(contentCells, backgroundCells, gridOptions, stateRewards, faultyProbability);
//grid.printToPrism(std::cout, prism::ModelType::MDP);
Grid grid(contentCells, backgroundCells, gridOptions, stateRewards, probIntended, faultyProbability);
grid.printToPrism(std::cout, configurations , gridOptions.getModelType());
std::stringstream ss;
// grid.printToPrism(file, configurations ,prism::ModelType::MDP);
grid.printToPrism(ss, configurations , gridOptions.getModelType());

2
util/CMakeLists.txt
View File

@ -2,7 +2,9 @@ list(APPEND SRCS
${CMAKE_CURRENT_LIST_DIR}/cell.cpp
${CMAKE_CURRENT_LIST_DIR}/MinigridGrammar.h
${CMAKE_CURRENT_LIST_DIR}/Grid.cpp
${CMAKE_CURRENT_LIST_DIR}/PrismPrinter.cpp
${CMAKE_CURRENT_LIST_DIR}/PrismModulesPrinter.cpp
${CMAKE_CURRENT_LIST_DIR}/PrismFormulaPrinter.cpp
${CMAKE_CURRENT_LIST_DIR}/popl.hpp
${CMAKE_CURRENT_LIST_DIR}/OptionParser.cpp
${CMAKE_CURRENT_LIST_DIR}/ConfigYaml.cpp

272
util/Grid.cpp
View File

@ -3,62 +3,36 @@
#include <algorithm>
prism::ModelType GridOptions::getModelType() const
prism::ModelType GridOptions::getModelType() const
{
if (agentsWithView.size() > 1) {
return prism::ModelType::SMG;
}
}
return prism::ModelType::MDP;
}
Grid::Grid(cells gridCells, cells background, const GridOptions &gridOptions, const std::map<coordinates, float> &stateRewards, const double faultyProbability)
: allGridCells(gridCells), background(background), gridOptions(gridOptions), stateRewards(stateRewards), faultyProbability(faultyProbability)
Grid::Grid(cells gridCells, cells background, const GridOptions &gridOptions, const std::map<coordinates, float> &stateRewards, const float probIntended, const float faultyProbability)
: allGridCells(gridCells), background(background), gridOptions(gridOptions), stateRewards(stateRewards), probIntended(probIntended), faultyProbability(faultyProbability)
{
cell max = allGridCells.at(allGridCells.size() - 1);
maxBoundaries = std::make_pair(max.row - 1, max.column - 1);
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(walls), [](cell c) {
return c.type == Type::Wall;
});
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(lava), [](cell c) {
return c.type == Type::Lava;
});
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(floor), [](cell c) {
return c.type == Type::Floor;
});
std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyNorth), [](cell c) {
return c.type == Type::SlipperyNorth;
});
std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyEast), [](cell c) {
return c.type == Type::SlipperyEast;
});
std::copy_if(background.begin(), background.end(), std::back_inserter(slipperySouth), [](cell c) {
return c.type == Type::SlipperySouth;
});
std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyWest), [](cell c) {
return c.type == Type::SlipperyWest;
});
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(lockedDoors), [](cell c) {
return c.type == Type::LockedDoor;
});
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(unlockedDoors), [](cell c) {
return c.type == Type::Door;
});
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(goals), [](cell c) {
return c.type == Type::Goal;
});
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(keys), [this](cell c) {
return c.type == Type::Key;
});
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(boxes), [](cell c) {
return c.type == Type::Box;
});
agent = *std::find_if(gridCells.begin(), gridCells.end(), [](cell c) {
return c.type == Type::Agent;
});
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(adversaries), [](cell c) {
return c.type == Type::Adversary;
});
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(walls), [](cell c) { return c.type == Type::Wall; });
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(lava), [](cell c) { return c.type == Type::Lava; });
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(floor), [](cell c) { return c.type == Type::Floor; }); // TODO CHECK IF ALL AGENTS ARE ADDED TO FLOOR
std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyNorth), [](cell c) { return c.type == Type::SlipperyNorth; });
std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyEast), [](cell c) { return c.type == Type::SlipperyEast; });
std::copy_if(background.begin(), background.end(), std::back_inserter(slipperySouth), [](cell c) { return c.type == Type::SlipperySouth; });
std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyWest), [](cell c) { return c.type == Type::SlipperyWest; });
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(lockedDoors), [](cell c) { return c.type == Type::LockedDoor; });
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(unlockedDoors), [](cell c) { return c.type == Type::Door; });
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(goals), [](cell c) { return c.type == Type::Goal; });
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(keys), [](cell c) { return c.type == Type::Key; });
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(boxes), [](cell c) { return c.type == Type::Box; });
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(balls), [](cell c) { return c.type == Type::Ball; });
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(adversaries), [](cell c) { return c.type == Type::Adversary; });
agent = *std::find_if(gridCells.begin(), gridCells.end(), [](cell c) { return c.type == Type::Agent; });
floor.push_back(agent);
agentNameAndPositionMap.insert({ "Agent", agent.getCoordinates() });
for(auto const& adversary : adversaries) {
std::string color = adversary.getColor();
@ -66,6 +40,7 @@ Grid::Grid(cells gridCells, cells background, const GridOptions &gridOptions, co
try {
if(gridOptions.agentsToBeConsidered.size() != 0 && std::find(gridOptions.agentsToBeConsidered.begin(), gridOptions.agentsToBeConsidered.end(), color) == gridOptions.agentsToBeConsidered.end()) continue;
auto success = agentNameAndPositionMap.insert({ color, adversary.getCoordinates() });
floor.push_back(adversary);
if(!success.second) {
throw std::logic_error("Agent with " + color + " already present\n");
}
@ -113,43 +88,16 @@ cells Grid::getGridCells() {
}
bool Grid::isBlocked(coordinates p) {
return isWall(p); //|| isLockedDoor(p) || isKey(p);
return isWall(p);
}
bool Grid::isWall(coordinates p) {
return std::find_if(walls.begin(), walls.end(),
[p](cell cell) {
return cell.row == p.first && cell.column == p.second;
return cell.row == p.second && cell.column == p.first;
}) != walls.end();
}
bool Grid::isLockedDoor(coordinates p) {
return std::find_if(lockedDoors.begin(), lockedDoors.end(),
[p](cell cell) {
return cell.row == p.first && cell.column == p.second;
}) != lockedDoors.end();
}
bool Grid::isUnlockedDoor(coordinates p) {
return std::find_if(unlockedDoors.begin(), unlockedDoors.end(),
[p](cell cell) {
return cell.row == p.first && cell.column == p.second;
}) != unlockedDoors.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::applyOverwrites(std::string& str, std::vector<Configuration>& configuration) {
for (auto& config : configuration) {
@ -157,7 +105,7 @@ void Grid::applyOverwrites(std::string& str, std::vector<Configuration>& configu
continue;
}
size_t start_pos;
if (config.type_ == ConfigType::Formula) {
start_pos = str.find("formula " + config.identifier_);
} else if (config.type_ == ConfigType::Label) {
@ -177,168 +125,64 @@ void Grid::applyOverwrites(std::string& str, std::vector<Configuration>& configu
size_t end_pos = str.find(';', start_pos) + 1;
std::string expression = config.expression_;
str.replace(start_pos, end_pos - start_pos , expression);
}
}
void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configuration ,const prism::ModelType& modelType) {
cells northRestriction;
cells eastRestriction;
cells southRestriction;
cells westRestriction;
cells walkable = floor;
cells conditionallyWalkable;
cells northRestriction, eastRestriction, southRestriction, 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());
conditionallyWalkable.insert(conditionallyWalkable.end(), keys.begin(), keys.end());
conditionallyWalkable.insert(conditionallyWalkable.end(), lockedDoors.begin(), lockedDoors.end());
conditionallyWalkable.insert(conditionallyWalkable.end(), unlockedDoors.begin(), unlockedDoors.end());
walkable.insert(walkable.end(), keys.begin(), keys.end());
walkable.insert(walkable.end(), balls.begin(), balls.end());
for(auto const& c : walkable) {
if(isBlocked(c.getNorth())) northRestriction.push_back(c);
if(isBlocked(c.getEast())) eastRestriction.push_back(c);
if(isBlocked(c.getSouth())) southRestriction.push_back(c);
if(isBlocked(c.getWest())) westRestriction.push_back(c);
}
// TODO Add doors here (list of doors keys etc)
// walkable.insert(walkable.end(), lockedDoors.begin(), lockedDoors.end());
// walkable.insert(walkable.end(), unlockedDoors.begin(), unlockedDoors.end());
for(auto const& c : conditionallyWalkable) {
if(isBlocked(c.getNorth())) northRestriction.push_back(c);
if(isBlocked(c.getEast())) eastRestriction.push_back(c);
if(isBlocked(c.getSouth())) southRestriction.push_back(c);
if(isBlocked(c.getWest())) westRestriction.push_back(c);
if(isWall(c.getNorth())) northRestriction.push_back(c);
if(isWall(c.getEast())) eastRestriction.push_back(c);
if(isWall(c.getSouth())) southRestriction.push_back(c);
if(isWall(c.getWest())) westRestriction.push_back(c);
}
prism::PrismModulesPrinter printer(modelType, agentNameAndPositionMap.size(), configuration, 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);
}
}
}
cells doors;
doors.insert(doors.end(), lockedDoors.begin(), lockedDoors.end());
doors.insert(doors.end(), unlockedDoors.begin(), unlockedDoors.end());
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, keys, doors);
printer.printGoalLabel(os, agentNameAndPosition->first, goals);
printer.printKeysLabels(os, agentNameAndPosition->first, keys);
}
std::vector<std::string> constants {"const double prop_zero = 0/9;",
"const double prop_intended = 6/9;",
"const double prop_turn_intended = 6/9;",
"const double prop_displacement = 3/9;",
"const double prop_turn_displacement = 3/9;",
"const int width = " + std::to_string(maxBoundaries.first) + ";",
"const int height = " + std::to_string(maxBoundaries.second) + ";"
};
printer.printConstants(os, constants);
std::map<std::string, cells> wallRestrictions = {{"North", northRestriction}, {"East", eastRestriction}, {"South", southRestriction}, {"West", westRestriction}};
std::map<std::string, cells> slipperyTiles = {{"North", slipperyNorth}, {"East", slipperyEast}, {"South", slipperySouth}, {"West", slipperyWest}};
std::vector<AgentName> agentNames;
std::transform(agentNameAndPositionMap.begin(),
agentNameAndPositionMap.end(),
std::back_inserter(agentNames),
[](const std::map<AgentNameAndPosition::first_type,AgentNameAndPosition::second_type>::value_type &pair){return pair.first;});
if(modelType == prism::ModelType::SMG) {
printer.printCrashLabel(os, agentNames);
}
size_t agentIndex = 0;
printer.printInitStruct(os, agentNameAndPositionMap, keyNameAndPositionMap, lockedDoors, unlockedDoors, modelType);
for(auto agentNameAndPosition = agentNameAndPositionMap.begin(); agentNameAndPosition != agentNameAndPositionMap.end(); ++agentNameAndPosition, agentIndex++) {
AgentName agentName = agentNameAndPosition->first;
//std::cout << "Agent Name: " << agentName << std::endl;
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; // TODO AGENT POSITION INITIALIZATIN
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, {} ,faultyProbability);
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);
std::string agentName = agentNames.at(0);
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);
//}
prism::PrismFormulaPrinter formulas(os, wallRestrictions, walls, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, lava, goals);
prism::PrismModulesPrinter modules(os, modelType, maxBoundaries, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, agentNameAndPositionMap, configuration, probIntended, faultyProbability);
modules.printModelType(modelType);
for(const auto &agentName : agentNames) {
formulas.print(agentName);
}
//std::vector<std::string> constants {"const double prop_zero = 0/9;",
// "const double prop_intended = 6/9;",
// "const double prop_turn_intended = 6/9;",
// "const double prop_displacement = 3/9;",
// "const double prop_turn_displacement = 3/9;",
// "const int width = " + std::to_string(maxBoundaries.first) + ";",
// "const int height = " + std::to_string(maxBoundaries.second) + ";"
// };
//modules.printConstants(os, constants);
modules.print();
if (!configuration.empty()) {
printer.printConfiguration(os, configuration);
}
// TODO CHANGE HANDLING
std::string agentName = agentNames.at(0);
for (auto const & key : keys) {
os << "\n";
printer.printKeyModule(os, key, maxBoundaries, agentName);
printer.printEndmodule(os);
}
for (auto const& door : lockedDoors) {
os << "\n";
printer.printDoorModule(os, door, maxBoundaries, agentName);
printer.printEndmodule(os);
}
}
//if(!stateRewards.empty()) {
// modules.printRewards(os, agentName, stateRewards, lava, goals, backgroundTiles);
//}
std::array<bool, 8> Grid::getWalkableDirOf8Neighborhood(cell c) /* const */ {
return (std::array<bool, 8>)
{
!isBlocked(c.getNorth()),
!isBlocked(c.getNorth(allGridCells).getEast()),
!isBlocked(c.getEast()),
!isBlocked(c.getSouth(allGridCells).getEast()),
!isBlocked(c.getSouth()),
!isBlocked(c.getSouth(allGridCells).getWest()),
!isBlocked(c.getWest()),
!isBlocked(c.getNorth(allGridCells).getWest())
};
//if (!configuration.empty()) {
// modules.printConfiguration(os, configuration);
//}
}

11
util/Grid.h
View File

@ -7,6 +7,7 @@
#include "MinigridGrammar.h"
#include "PrismModulesPrinter.h"
#include "PrismFormulaPrinter.h"
#include "ConfigYaml.h"
struct GridOptions {
@ -21,16 +22,12 @@ struct GridOptions {
class Grid {
public:
Grid(cells gridCells, cells background, const GridOptions &gridOptions, const std::map<coordinates, float> &stateRewards = {}, const double faultyProbability = 0);
Grid(cells gridCells, cells background, const GridOptions &gridOptions, const std::map<coordinates, float> &stateRewards = {}, const float probIntended = 1.0, const float faultyProbability = 0);
cells getGridCells();
bool isBlocked(coordinates p);
bool isWall(coordinates p);
bool isLockedDoor(coordinates p);
bool isUnlockedDoor(coordinates p);
bool isKey(coordinates p);
bool isBox(coordinates p);
void printToPrism(std::ostream &os, std::vector<Configuration>& configuration, const prism::ModelType& modelType);
void applyOverwrites(std::string& str, std::vector<Configuration>& configuration);
@ -59,6 +56,7 @@ class Grid {
cells lockedDoors;
cells unlockedDoors;
cells boxes;
cells balls;
cells lava;
cells goals;
@ -67,5 +65,6 @@ class Grid {
std::map<Color, cells> backgroundTiles;
std::map<coordinates, float> stateRewards;
double faultyProbability;
const float probIntended;
const float faultyProbability;
};

222
util/PrismFormulaPrinter.cpp
View File

@ -0,0 +1,222 @@
#include "PrismFormulaPrinter.h"
#include <map>
#include <string>
#include <algorithm>
std::string oneOffToString(const int &offset) {
return offset != 0 ? ( offset == 1 ? "+1" : "-1" ) : "";
}
std::string vectorToDisjunction(const std::vector<std::string> &formulae) {
bool first = true;
std::string disjunction = "";
for(const auto &formula : formulae) {
if(first) first = false;
else disjunction += " | ";
disjunction += formula;
}
return disjunction;
}
std::string cellToConjunction(const AgentName &agentName, const cell &c) {
return "x" + agentName + "=" + std::to_string(c.column) + "&y" + agentName + "=" + std::to_string(c.row);
}
std::string cellToConjunctionWithOffset(const AgentName &agentName, const cell &c, const std::string &xOffset, const std::string &yOffset){
return "x" + agentName + xOffset + "=" + std::to_string(c.column) + "&y" + agentName + yOffset + "=" + std::to_string(c.row);
}
std::string coordinatesToConjunction(const AgentName &agentName, const coordinates &c, const ViewDirection viewDirection) {
return "x" + agentName + "=" + std::to_string(c.first) + "&y" + agentName + "=" + std::to_string(c.second) + "&view" + agentName + "=" + std::to_string(viewDirection);
}
std::string objectPositionToConjunction(const AgentName &agentName, const std::string &identifier, const std::pair<int, int> &relativePosition) {
std::string xOffset = oneOffToString(relativePosition.first);
std::string yOffset = oneOffToString(relativePosition.second);
return "x" + agentName + xOffset + "=x" + identifier + "&y" + agentName + yOffset + "=y" + identifier;
}
std::string objectPositionToConjunction(const AgentName &agentName, const std::string &identifier, const std::pair<int, int> &relativePosition, const ViewDirection viewDirection) {
std::string xOffset = oneOffToString(relativePosition.first);
std::string yOffset = oneOffToString(relativePosition.second);
return "x" + agentName + xOffset + "=x" + identifier + "&y" + agentName + yOffset + "=y" + identifier + "&view" + agentName + "=" + std::to_string(viewDirection);
}
std::map<ViewDirection, coordinates> getAdjacentCells(const cell &c) {
return {{1, c.getNorth()}, {2, c.getEast()}, {3, c.getSouth()}, {0, c.getWest()}};
}
std::map<ViewDirection, std::pair<int, int>> getRelativeAdjacentCells() {
return { {1, {0,+1}}, {2, {-1,0}}, {3, {0,-1}}, {0, {+1,0}} };
}
std::map<std::string, std::pair<int, int>> getRelativeSurroundingCells() {
return { {"NorthWest", {-1,-1}}, {"North", { 0,-1}}, {"NorthEast", {+1,-1}},
{"West", {-1, 0}}, {"East", {+1, 0}},
{"SouthWest", {-1,+1}}, {"South", { 0,+1}}, {"SouthEast", {+1,+1}} };
}
namespace prism {
PrismFormulaPrinter::PrismFormulaPrinter(std::ostream &os, const std::map<std::string, cells> &restrictions, const cells &walls, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const cells &lava, const cells &goals)
: os(os), restrictions(restrictions), walls(walls), boxes(boxes), balls(balls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), lava(lava), goals(goals)
{ }
void PrismFormulaPrinter::print(const AgentName &agentName) {
for(const auto& [direction, cells] : restrictions) {
printRestrictionFormula(agentName, direction, cells);
}
if(slipperyBehaviour()) {
for(const auto& [direction, cells] : slipperyTiles) {
printIsOnFormula(agentName, "Slippery", cells, direction);
}
std::vector<std::string> allSlipperyDirections = {agentName + "IsOnSlipperyNorth", agentName + "IsOnSlipperyEast", agentName + "IsOnSlipperySouth", agentName + "IsOnSlipperyWest"};
os << buildFormula(agentName + "IsOnSlippery", vectorToDisjunction(allSlipperyDirections));
for(const auto& [direction, relativePosition] : getRelativeSurroundingCells()) {
printSlipRestrictionFormula(agentName, direction);
}
} else {
os << buildFormula(agentName + "IsOnSlippery", "false");
}
printIsOnFormula(agentName, "Lava", lava);
printIsOnFormula(agentName, "Goal", goals);
for(const auto& ball : balls) {
std::string identifier = capitalize(ball.getColor()) + ball.getType();
printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp");
portableObjects.push_back(agentName + "Carrying" + identifier);
}
for(const auto& box : boxes) {
std::string identifier = capitalize(box.getColor()) + box.getType();
printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp");
portableObjects.push_back(agentName + "Carrying" + identifier);
}
for(const auto& key : keys) {
std::string identifier = capitalize(key.getColor()) + key.getType();
printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp");
portableObjects.push_back(agentName + "Carrying" + identifier);
}
for(const auto& door : unlockedDoors) {
std::string identifier = capitalize(door.getColor()) + door.getType();
printRestrictionFormulaWithCondition(agentName, identifier, getAdjacentCells(door), "!" + identifier + "Open");
printIsNextToFormula(agentName, identifier, getAdjacentCells(door));
}
for(const auto& door : lockedDoors) {
std::string identifier = capitalize(door.getColor()) + door.getType();
printRestrictionFormulaWithCondition(agentName, identifier, getAdjacentCells(door), "!" + identifier + "Open");
printIsNextToFormula(agentName, identifier, getAdjacentCells(door));
}
if(conditionalMovementRestrictions.size() > 0) {
os << buildFormula(agentName + "CannotMoveConditionally", vectorToDisjunction(conditionalMovementRestrictions));
os << buildFormula(agentName + "IsCarrying", vectorToDisjunction(portableObjects));
} else {
os << buildFormula(agentName + "CannotMoveConditionally", "false");
}
}
void PrismFormulaPrinter::printRestrictionFormula(const AgentName &agentName, const std::string &direction, const cells &grid_cells) {
os << buildFormula(agentName + "CannotMove" + direction + "Wall", buildDisjunction(agentName, grid_cells));
}
void PrismFormulaPrinter::printIsOnFormula(const AgentName &agentName, const std::string &type, const cells &grid_cells, const std::string &direction) {
os << buildFormula(agentName + "IsOn" + type + direction, buildDisjunction(agentName, grid_cells));
}
void PrismFormulaPrinter::printIsNextToFormula(const AgentName &agentName, const std::string &type, const std::map<ViewDirection, coordinates> &coordinates) {
os << buildFormula(agentName + "IsNextTo" + type, buildDisjunction(agentName, coordinates));
}
void PrismFormulaPrinter::printRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::map<ViewDirection, coordinates> &coordinates, const std::string &condition) {
os << buildFormula(agentName + "CannotMove" + reason, "(" + buildDisjunction(agentName, coordinates) + ") & " + condition);
conditionalMovementRestrictions.push_back(agentName + "CannotMove" + reason);
}
void PrismFormulaPrinter::printRelativeRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::string &condition) {
os << buildFormula(agentName + "CannotMove" + reason, "(" + buildDisjunction(agentName, reason) + ") & " + condition);
conditionalMovementRestrictions.push_back(agentName + "CannotMove" + reason);
}
void PrismFormulaPrinter::printSlipRestrictionFormula(const AgentName &agentName, const std::string &direction) {
std::pair<int, int> slipCell = getRelativeSurroundingCells().at(direction);
bool semicolon = anyPortableObject() ? false : true;
os << buildFormula(agentName + "CannotSlip" + direction, buildDisjunction(agentName, walls, slipCell), semicolon);
for(auto const key : keys) {
std::string identifier = capitalize(key.getColor()) + key.getType();
os << " | " << objectPositionToConjunction(agentName, identifier, slipCell);
}
for(auto const ball : balls) {
std::string identifier = capitalize(ball.getColor()) + ball.getType();
os << " | " << objectPositionToConjunction(agentName, identifier, slipCell);
}
for(auto const box : boxes) {
std::string identifier = capitalize(box.getColor()) + box.getType();
os << " | " << objectPositionToConjunction(agentName, identifier, slipCell);
}
os << ";\n";
}
std::string PrismFormulaPrinter::buildFormula(const std::string &formulaName, const std::string &formula, const bool semicolon) {
return "formula " + formulaName + " = " + formula + (semicolon ? ";\n": "");
}
std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const std::map<ViewDirection, coordinates> &cells) {
if(cells.size() == 0) return "false";
bool first = true;
std::string disjunction = "";
for(const auto [viewDirection, coordinates] : cells) {
if(first) first = false;
else disjunction += " | ";
disjunction += "(" + coordinatesToConjunction(agentName, coordinates, viewDirection) + ")";
}
return disjunction;
}
std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const cells &cells) {
if(cells.size() == 0) return "false";
bool first = true;
std::string disjunction = "";
for(auto const cell : cells) {
if(first) first = false;
else disjunction += " | ";
disjunction += "(" + cellToConjunction(agentName, cell) + ")";
}
return disjunction;
}
std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const std::string &reason) {
std::string disjunction = "";
bool first = true;
for(auto const [viewDirection, relativePosition] : getRelativeAdjacentCells()) {
if(first) first = false;
else disjunction += " | ";
disjunction += "(" + objectPositionToConjunction(agentName, reason, relativePosition, viewDirection) + ")";
}
return disjunction;
}
std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const cells &cells, const std::pair<int, int> &offset) {
std::string disjunction = "";
bool first = true;
std::string xOffset = oneOffToString(offset.first);
std::string yOffset = oneOffToString(offset.second);
for(auto const cell : cells) {
if(first) first = false;
else disjunction += " | ";
disjunction += "(" + cellToConjunctionWithOffset(agentName, cell, xOffset, yOffset) + ")";
}
return disjunction;
}
bool PrismFormulaPrinter::slipperyBehaviour() const {
return !slipperyTiles.at("North").empty() || !slipperyTiles.at("East").empty() || !slipperyTiles.at("South").empty() || !slipperyTiles.at("West").empty();
}
bool PrismFormulaPrinter::anyPortableObject() const {
return !keys.empty() || !boxes.empty() || !balls.empty();
}
}

61
util/PrismFormulaPrinter.h
View File

@ -0,0 +1,61 @@
#pragma once
#include <iostream>
#include <functional>
#include "MinigridGrammar.h"
#include "PrismPrinter.h"
#include "ConfigYaml.h"
std::string oneOffToString(const int &offset);
std::string vectorToDisjunction(const std::vector<std::string> &formulae);
std::string cellToConjunction(const AgentName &agentName, const cell &c);
std::string cellToConjunctionWithOffset(const AgentName &agentName, const cell &c, const std::string &xOffset, const std::string &yOffset);
std::string coordinatesToConjunction(const AgentName &agentName, const coordinates &c, const ViewDirection viewDirection);
std::string objectPositionToConjunction(const AgentName &agentName, const std::string &identifier, const std::pair<int, int> &relativePosition);
std::string objectPositionToConjunction(const AgentName &agentName, const std::string &identifier, const std::pair<int, int> &relativePosition, const ViewDirection viewDirection);
std::map<ViewDirection, coordinates> getAdjacentCells(const cell &c);
std::map<ViewDirection, std::pair<int, int>> getRelativeAdjacentCells();
std::map<std::string, std::pair<int, int>> getRelativeSurroundingCells();
namespace prism {
class PrismFormulaPrinter {
public:
PrismFormulaPrinter(std::ostream &os, const std::map<std::string, cells> &restrictions, const cells &walls, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const cells &lava, const cells &goals);
void print(const AgentName &agentName);
void printRestrictionFormula(const AgentName &agentName, const std::string &direction, const cells &grid_cells);
void printIsOnFormula(const AgentName &agentName, const std::string &type, const cells &grid_cells, const std::string &direction = "");
void printIsNextToFormula(const AgentName &agentName, const std::string &type, const std::map<ViewDirection, coordinates> &coordinates);
void printRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::map<ViewDirection, coordinates> &coordinates, const std::string &condition);
void printRelativeRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::string &condition);
void printSlipRestrictionFormula(const AgentName &agentName, const std::string &direction);
private:
std::string buildFormula(const std::string &formulaName, const std::string &formula, const bool semicolon = true);
std::string buildLabel(const std::string &labelName, const std::string &label);
std::string buildDisjunction(const AgentName &agentName, const std::map<ViewDirection, coordinates> &cells);
std::string buildDisjunction(const AgentName &agentName, const cells &cells);
std::string buildDisjunction(const AgentName &agentName, const std::string &reason);
std::string buildDisjunction(const AgentName &agentName, const cells &cells, const std::pair<int, int> &offset);
bool slipperyBehaviour() const;
bool anyPortableObject() const;
std::ostream &os;
std::map<std::string, cells> restrictions;
cells walls;
cells boxes;
cells balls;
cells lockedDoors;
cells unlockedDoors;
cells keys;
std::map<std::string, cells> slipperyTiles;
cells lava;
cells goals;
std::vector<std::string> conditionalMovementRestrictions;
std::vector<std::string> portableObjects;
};
}

1358
util/PrismModulesPrinter.cpp
File diff suppressed because it is too large
View File

194
util/PrismModulesPrinter.h
View File

@ -1,119 +1,111 @@
#pragma once
#include <iostream>
#include <set>
#include <functional>
#include "MinigridGrammar.h"
#include "PrismPrinter.h"
#include "ConfigYaml.h"
std::string northUpdate(const AgentName &a);
std::string southUpdate(const AgentName &a);
std::string eastUpdate(const AgentName &a);
std::string westUpdate(const AgentName &a);
namespace prism {
class PrismModulesPrinter {
public:
PrismModulesPrinter(const ModelType &modelType, const size_t &numberOfPlayer, std::vector<Configuration> config ,const bool enforceOneWays = false);
std::ostream& printRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &grid_cells, const cells& keys, const cells& doors);
std::ostream& printKeyRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &keys);
std::ostream& printDoorRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &doors);
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,
const cells &keys,
const cells &doors);
std::ostream& printKeyModule(std::ostream &os, const cell &key, const coordinates &boundaries, AgentName agentName);
std::ostream& printKeyActions(std::ostream &os, const cell& key ,const std::string &keyIdentifier, AgentName agentName);
std::ostream& printDoorModule(std::ostream &os, const cell &door, const coordinates &boundaries, AgentName agentName);
std::ostream& printDoorActions(std::ostream &os, const cell &door ,const std::string &doorIdentifier, AgentName agentName);
std::ostream& printConstants(std::ostream &os, const std::vector<std::string> &constants);
/*
* 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 AgentNameAndPositionMap &agents, const KeyNameAndPositionMap &keys, const cells &lockedDoors, const cells &unlockedDoors, prism::ModelType modelType);
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 = {},
const double faultyProbability = 0);
std::ostream& printMovementActions(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const bool agentWithView, const float &probability = 1.0, const double &stickyProbability = 0.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::ostream& printConfiguration(std::ostream &os, const std::vector<Configuration>& configurations);
std::ostream& printConfiguredActions(std::ostream &os, const AgentName &agentName);
std::string moveGuard(const size_t &agentIndex);
std::string pickupGuard(const AgentName &agentName, const std::string keyColor);
std::string dropGuard(const AgentName &agentName, const std::string keyColor, size_t view);
std::string moveUpdate(const size_t &agentIndex);
std::string unlockGuard(const AgentName &agentName, const cell& door);
std::string toggleGuard(const AgentName &agentName, const cell& door);
std::string viewVariable(const AgentName &agentName, const size_t &agentDirection, const bool agentWithView);
PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector<Configuration> config, const float probIntended, const float faultyProbability);
std::ostream& print();
void printModelType(const ModelType &modelType);
bool isGame() const;
private:
void printPortableObjectModule(const cell &object);
void printPortableObjectActions(const std::string &agentName, const std::string &identifier);
void printDoorModule(const cell &object, const bool &opened);
void printLockedDoorActions(const std::string &agentName, const std::string &identifier);
void printUnlockedDoorActions(const std::string &agentName, const std::string &identifier);
void printRobotModule(const AgentName &agentName, const coordinates &initialPosition);
void printPortableObjectActionsForRobot(const std::string &agentName, const std::string &identifier);
void printUnlockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier);
void printLockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier, const std::string &key);
void printMovementActionsForRobot(const std::string &a);
void printTurnActionsForRobot(const std::string &a);
void printSlipperyMovementActionsForRobot(const AgentName &a);
void printSlipperyMovementActionsForNorth(const AgentName &a);
void printSlipperyMovementActionsForEast(const AgentName &a);
void printSlipperyMovementActionsForSouth(const AgentName &a);
void printSlipperyMovementActionsForWest(const AgentName &a);
void printSlipperyTurnActionsForNorth(const AgentName &a);
void printSlipperyTurnActionsForEast(const AgentName &a);
void printSlipperyTurnActionsForSouth(const AgentName &a);
void printSlipperyTurnActionsForWest(const AgentName &a);
std::string printMovementGuard(const AgentName &a, const std::string &direction, const size_t &viewDirection);
std::string printMovementUpdate(const AgentName &a, const update &update) const;
std::string printTurnGuard(const AgentName &a, const std::string &direction, const ActionId &actionId, const std::string &cond = "");
std::string printTurnUpdate(const AgentName &a, const update &u, const ActionId &actionId) const;
std::string printSlipperyMovementGuard(const AgentName &a, const std::string &direction, const ViewDirection &viewDirection, const std::vector<std::string> &guards);
std::string printSlipperyMovementUpdate(const AgentName &a, const std::string &direction, const updates &u) const;
std::string printSlipperyTurnGuard(const AgentName &a, const std::string &direction, const ActionId &actionId, const std::vector<std::string> &guards, const std::string &cond);
std::string printSlipperyTurnUpdate(const AgentName &a, const updates &u);
void printFaultyMovementModule(const AgentName &a);
void printMoveModule();
void printConstants(const std::vector<std::string> &constants);
ModelType const& modelType;
const size_t numberOfPlayer;
bool enforceOneWays;
void printDoneActions(const AgentName &agentName);
void printPlayerStruct(const AgentName &agentName);
void printRewards(const AgentName &agentName, const std::map<coordinates, float> &stateRewards, const cells &lava, const cells &goals, const std::map<Color, cells> &backgroundTiles);
void printConfiguration(const std::vector<Configuration>& configurations);
void printConfiguredActions(const AgentName &agentName);
bool anyPortableObject() const;
bool faultyBehaviour() const;
bool slipperyBehaviour() const;
std::string moveGuard(const AgentName &agentName) const;
std::string faultyBehaviourGuard(const AgentName &agentName, const ActionId &actionId) const;
std::string faultyBehaviourUpdate(const AgentName &agentName, const ActionId &actionId) const;
std::string moveUpdate(const AgentName &agentName) const;
std::string updatesToString(const updates &updates) const;
std::string updateToString(const update &u) const;
std::string viewVariable(const AgentName &agentName, const size_t &agentDirection) const;
std::string buildConjunction(const AgentName &a, std::vector<std::string> formulae) const;
std::ostream &os;
std::stringstream actionStream;
ModelType const &modelType;
coordinates const &maxBoundaries;
AgentName agentName;
cells boxes;
cells balls;
cells lockedDoors;
cells unlockedDoors;
cells keys;
std::map<std::string, cells> slipperyTiles;
AgentNameAndPositionMap agentNameAndPositionMap;
std::map<AgentName, size_t> agentIndexMap;
size_t numberOfPlayer;
float const faultyProbability;
float const probIntended;
std::vector<Configuration> configuration;
std::map<int, std::string> viewDirectionMapping;
std::vector<ViewDirection> viewDirections = {0, 1, 2, 3};
std::map<AgentName, std::set<std::pair<ActionId, std::string>>> agentNameActionMap;
};
}

8
util/PrismPrinter.cpp
View File

@ -0,0 +1,8 @@
#include "PrismPrinter.h"
#include <algorithm>
std::string capitalize(std::string string) {
string[0] = std::toupper(string[0]);
return string;
}

8
util/PrismPrinter.h
View File

@ -1,14 +1,22 @@
#pragma once
#include <string>
#include <map>
#include "cell.h"
typedef std::string AgentName;
typedef size_t ViewDirection;
typedef std::pair<std::string, coordinates> AgentNameAndPosition;
typedef AgentNameAndPosition KeyNameAndPosition;
typedef std::map<AgentNameAndPosition::first_type, AgentNameAndPosition::second_type> AgentNameAndPositionMap;
typedef std::map<KeyNameAndPosition::first_type, KeyNameAndPosition::second_type> KeyNameAndPositionMap;
typedef std::pair<cell, std::string> CellAndCondition;
typedef std::pair<float, std::string> update;
typedef std::vector<update> updates;
typedef int8_t ActionId;
std::string capitalize(std::string string);
namespace prism {
enum class ModelType {

31
util/cell.cpp
View File

@ -4,10 +4,14 @@
std::ostream &operator<<(std::ostream &os, const cell &c) {
os << static_cast<char>(c.type) << static_cast<char>(c.color);
os << " at (" << c.row << "," << c.column << ")";
os << " at (" << c.column << "," << c.row << ")";
return os;
}
coordinates cell::getCoordinates() const {
return std::make_pair(column, row);
}
cell cell::getNorth(const std::vector<cell> &grid) const {
auto north = std::find_if(grid.begin(), grid.end(), [this](const cell &c) {
return this->row - 1 == c.row && this->column == c.column;
@ -52,10 +56,6 @@ cell cell::getWest(const std::vector<cell> &grid) const {
return *west;
}
coordinates cell::getCoordinates() const {
return std::make_pair(row, column);
}
std::string cell::getColor() const {
switch(color) {
case Color::Red: return "red";
@ -69,6 +69,27 @@ std::string cell::getColor() const {
}
}
std::string cell::getType() const {
switch(type) {
case Type::Wall: return "Wall";
case Type::Floor: return "Floor";
case Type::Door: return "Door";
case Type::LockedDoor: return "LockedDoor";
case Type::Key: return "Key";
case Type::Ball: return "Ball";
case Type::Box: return "Box";
case Type::Goal: return "Goal";
case Type::Lava: return "Lava";
case Type::Agent: return "Agent";
case Type::Adversary: return "Adversary";
case Type::SlipperyNorth: return "SlipperyNorth";
case Type::SlipperySouth: return "SlipperySouth";
case Type::SlipperyEast: return "SlipperyEast";
case Type::SlipperyWest: return "SlipperyWest";
default: return "";
}
}
std::string getColor(Color color) {
switch(color) {
case Color::Red: return "red";

9
util/cell.h
View File

@ -40,10 +40,10 @@ std::string getColor(Color color);
class cell {
public:
coordinates getNorth() const { return std::make_pair(row - 1, column); }
coordinates getSouth() const { return std::make_pair(row + 1, column); }
coordinates getEast() const { return std::make_pair(row, column + 1); }
coordinates getWest() const { return std::make_pair(row, column - 1); }
coordinates getNorth() const { return std::make_pair(column, row - 1); }
coordinates getSouth() const { return std::make_pair(column, row + 1); }
coordinates getEast() const { return std::make_pair(column + 1, row); }
coordinates getWest() const { return std::make_pair(column - 1, row); }
cell getNorth(const std::vector<cell> &grid) const;
cell getEast(const std::vector<cell> &grid) const;
@ -54,6 +54,7 @@ class cell {
coordinates getCoordinates() const;
std::string getColor() const;
std::string getType() const;
int row;
int column;

Write Preview
Loading…
Cancel
Save