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 1 year ago
Conversation 0 Commits 38 Files Changed 13
13 changed files with 944 additions and 1282 deletions
Unified View
  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) cmake_minimum_required(VERSION 3.0...3.22)
set(CMAKE_BUILD_TYPE Debug)
project( project(
Minigrid2PRISM Minigrid2PRISM
VERSION 0.1 VERSION 0.1
LANGUAGES CXX) LANGUAGES CXX)
set(CMAKE_CXX_STANDARD 20)
find_package(yaml-cpp) include(util/CMakeLists.txt)
include(FetchContent)
add_executable(main FetchContent_Declare(
${SRCS} yaml-cpp
main.cpp GIT_REPOSITORY https://github.com/jbeder/yaml-cpp.git
) GIT_TAG master
OVERRIDE_FIND_PACKAGE
target_link_libraries(main pthread yaml-cpp) )
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 backgroundIter = backgroundFirst;
pos_iterator_t backgroundLast(background.end()); pos_iterator_t backgroundLast(background.end());
MinigridParser<pos_iterator_t> backgroundParser(backgroundFirst); MinigridParser<pos_iterator_t> backgroundParser(backgroundFirst);
cells contentCells; cells contentCells;
cells backgroundCells; cells backgroundCells;
std::vector<Configuration> configurations; std::vector<Configuration> configurations;
std::map<coordinates, float> stateRewards; std::map<coordinates, float> stateRewards;
double faultyProbability; float faultyProbability = 0.0;
float probIntended = 0.9;
try { try {
bool ok = phrase_parse(contentIter, contentLast, contentParser, qi::space, contentCells); 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); ok &= phrase_parse(backgroundIter, backgroundLast, backgroundParser, qi::space, backgroundCells);
// TODO } // TODO }
if (configFilename->is_set()) { if (configFilename->is_set()) {
YamlConfigParser parser(configFilename->value(0)); YamlConfigParser parser(configFilename->value(0));
configurations = parser.parseConfiguration(); configurations = parser.parseConfiguration();
} }
@ -181,8 +182,9 @@ int main(int argc, char* argv[]) {
} }
} }
if(ok) { if(ok) {
Grid grid(contentCells, backgroundCells, gridOptions, stateRewards, faultyProbability); Grid grid(contentCells, backgroundCells, gridOptions, stateRewards, probIntended, faultyProbability);
//grid.printToPrism(std::cout, prism::ModelType::MDP); grid.printToPrism(std::cout, configurations , gridOptions.getModelType());
std::stringstream ss; std::stringstream ss;
// grid.printToPrism(file, configurations ,prism::ModelType::MDP); // grid.printToPrism(file, configurations ,prism::ModelType::MDP);
grid.printToPrism(ss, configurations , gridOptions.getModelType()); 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}/cell.cpp
${CMAKE_CURRENT_LIST_DIR}/MinigridGrammar.h ${CMAKE_CURRENT_LIST_DIR}/MinigridGrammar.h
${CMAKE_CURRENT_LIST_DIR}/Grid.cpp ${CMAKE_CURRENT_LIST_DIR}/Grid.cpp
${CMAKE_CURRENT_LIST_DIR}/PrismPrinter.cpp
${CMAKE_CURRENT_LIST_DIR}/PrismModulesPrinter.cpp ${CMAKE_CURRENT_LIST_DIR}/PrismModulesPrinter.cpp
${CMAKE_CURRENT_LIST_DIR}/PrismFormulaPrinter.cpp
${CMAKE_CURRENT_LIST_DIR}/popl.hpp ${CMAKE_CURRENT_LIST_DIR}/popl.hpp
${CMAKE_CURRENT_LIST_DIR}/OptionParser.cpp ${CMAKE_CURRENT_LIST_DIR}/OptionParser.cpp
${CMAKE_CURRENT_LIST_DIR}/ConfigYaml.cpp ${CMAKE_CURRENT_LIST_DIR}/ConfigYaml.cpp

272
util/Grid.cpp
View File

@ -3,62 +3,36 @@
#include <algorithm> #include <algorithm>
prism::ModelType GridOptions::getModelType() const prism::ModelType GridOptions::getModelType() const
{ {
if (agentsWithView.size() > 1) { if (agentsWithView.size() > 1) {
return prism::ModelType::SMG; return prism::ModelType::SMG;
} }
return prism::ModelType::MDP; return prism::ModelType::MDP;
} }
Grid::Grid(cells gridCells, cells background, const GridOptions &gridOptions, const std::map<coordinates, float> &stateRewards, const double 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), faultyProbability(faultyProbability) : allGridCells(gridCells), background(background), gridOptions(gridOptions), stateRewards(stateRewards), probIntended(probIntended), faultyProbability(faultyProbability)
{ {
cell max = allGridCells.at(allGridCells.size() - 1); cell max = allGridCells.at(allGridCells.size() - 1);
maxBoundaries = std::make_pair(max.row - 1, max.column - 1); maxBoundaries = std::make_pair(max.row - 1, max.column - 1);
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(walls), [](cell c) { std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(walls), [](cell c) { return c.type == Type::Wall; });
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(gridCells.begin(), gridCells.end(), std::back_inserter(lava), [](cell c) { std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyNorth), [](cell c) { return c.type == Type::SlipperyNorth; });
return c.type == Type::Lava; 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(gridCells.begin(), gridCells.end(), std::back_inserter(floor), [](cell c) { std::copy_if(background.begin(), background.end(), std::back_inserter(slipperyWest), [](cell c) { return c.type == Type::SlipperyWest; });
return c.type == Type::Floor; 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(background.begin(), background.end(), std::back_inserter(slipperyNorth), [](cell c) { std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(goals), [](cell c) { return c.type == Type::Goal; });
return c.type == Type::SlipperyNorth; 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(background.begin(), background.end(), std::back_inserter(slipperyEast), [](cell c) { std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(balls), [](cell c) { return c.type == Type::Ball; });
return c.type == Type::SlipperyEast; 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; });
std::copy_if(background.begin(), background.end(), std::back_inserter(slipperySouth), [](cell c) { floor.push_back(agent);
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;
});
agentNameAndPositionMap.insert({ "Agent", agent.getCoordinates() }); agentNameAndPositionMap.insert({ "Agent", agent.getCoordinates() });
for(auto const& adversary : adversaries) { for(auto const& adversary : adversaries) {
std::string color = adversary.getColor(); std::string color = adversary.getColor();
@ -66,6 +40,7 @@ Grid::Grid(cells gridCells, cells background, const GridOptions &gridOptions, co
try { try {
if(gridOptions.agentsToBeConsidered.size() != 0 && std::find(gridOptions.agentsToBeConsidered.begin(), gridOptions.agentsToBeConsidered.end(), color) == gridOptions.agentsToBeConsidered.end()) continue; 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() }); auto success = agentNameAndPositionMap.insert({ color, adversary.getCoordinates() });
floor.push_back(adversary);
if(!success.second) { if(!success.second) {
throw std::logic_error("Agent with " + color + " already present\n"); throw std::logic_error("Agent with " + color + " already present\n");
} }
@ -113,43 +88,16 @@ cells Grid::getGridCells() {
} }
bool Grid::isBlocked(coordinates p) { bool Grid::isBlocked(coordinates p) {
return isWall(p); //|| isLockedDoor(p) || isKey(p); return isWall(p);
} }
bool Grid::isWall(coordinates p) { bool Grid::isWall(coordinates p) {
return std::find_if(walls.begin(), walls.end(), return std::find_if(walls.begin(), walls.end(),
[p](cell cell) { [p](cell cell) {
return cell.row == p.first && cell.column == p.second; return cell.row == p.second && cell.column == p.first;
}) != walls.end(); }) != 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) { void Grid::applyOverwrites(std::string& str, std::vector<Configuration>& configuration) {
for (auto& config : configuration) { for (auto& config : configuration) {
@ -157,7 +105,7 @@ void Grid::applyOverwrites(std::string& str, std::vector<Configuration>& configu
continue; continue;
} }
size_t start_pos; size_t start_pos;
if (config.type_ == ConfigType::Formula) { if (config.type_ == ConfigType::Formula) {
start_pos = str.find("formula " + config.identifier_); start_pos = str.find("formula " + config.identifier_);
} else if (config.type_ == ConfigType::Label) { } 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; size_t end_pos = str.find(';', start_pos) + 1;
std::string expression = config.expression_; std::string expression = config.expression_;
str.replace(start_pos, end_pos - start_pos , expression); str.replace(start_pos, end_pos - start_pos , expression);
} }
} }
void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configuration ,const prism::ModelType& modelType) { void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configuration ,const prism::ModelType& modelType) {
cells northRestriction; cells northRestriction, eastRestriction, southRestriction, westRestriction;
cells eastRestriction;
cells southRestriction;
cells westRestriction;
cells walkable = floor;
cells conditionallyWalkable;
cells walkable = floor;
walkable.insert(walkable.end(), goals.begin(), goals.end()); walkable.insert(walkable.end(), goals.begin(), goals.end());
walkable.insert(walkable.end(), boxes.begin(), boxes.end()); walkable.insert(walkable.end(), boxes.begin(), boxes.end());
walkable.push_back(agent);
walkable.insert(walkable.end(), adversaries.begin(), adversaries.end());
walkable.insert(walkable.end(), lava.begin(), lava.end()); walkable.insert(walkable.end(), lava.begin(), lava.end());
walkable.insert(walkable.end(), keys.begin(), keys.end());
conditionallyWalkable.insert(conditionallyWalkable.end(), keys.begin(), keys.end()); walkable.insert(walkable.end(), balls.begin(), balls.end());
conditionallyWalkable.insert(conditionallyWalkable.end(), lockedDoors.begin(), lockedDoors.end());
conditionallyWalkable.insert(conditionallyWalkable.end(), unlockedDoors.begin(), unlockedDoors.end());
for(auto const& c : walkable) { for(auto const& c : walkable) {
if(isBlocked(c.getNorth())) northRestriction.push_back(c); if(isWall(c.getNorth())) northRestriction.push_back(c);
if(isBlocked(c.getEast())) eastRestriction.push_back(c); if(isWall(c.getEast())) eastRestriction.push_back(c);
if(isBlocked(c.getSouth())) southRestriction.push_back(c); if(isWall(c.getSouth())) southRestriction.push_back(c);
if(isBlocked(c.getWest())) westRestriction.push_back(c); if(isWall(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);
} }
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::vector<AgentName> agentNames;
std::transform(agentNameAndPositionMap.begin(), std::transform(agentNameAndPositionMap.begin(),
agentNameAndPositionMap.end(), agentNameAndPositionMap.end(),
std::back_inserter(agentNames), std::back_inserter(agentNames),
[](const std::map<AgentNameAndPosition::first_type,AgentNameAndPosition::second_type>::value_type &pair){return pair.first;}); [](const std::map<AgentNameAndPosition::first_type,AgentNameAndPosition::second_type>::value_type &pair){return pair.first;});
if(modelType == prism::ModelType::SMG) { std::string agentName = agentNames.at(0);
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);
if(modelType == prism::ModelType::SMG) { prism::PrismFormulaPrinter formulas(os, wallRestrictions, walls, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, lava, goals);
if(agentWithProbabilisticBehaviour) printer.printPlayerStruct(os, agentNameAndPosition->first, agentWithView, gridOptions.probabilitiesForActions, slipperyActions); prism::PrismModulesPrinter modules(os, modelType, maxBoundaries, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, agentNameAndPositionMap, configuration, probIntended, faultyProbability);
else printer.printPlayerStruct(os, agentNameAndPosition->first, agentWithView, {}, slipperyActions);
}
//if(!stateRewards.empty()) {
printer.printRewards(os, agentName, stateRewards, lava, goals, backgroundTiles);
//}
modules.printModelType(modelType);
for(const auto &agentName : agentNames) {
formulas.print(agentName);
} }
//std::vector<std::string> constants {"const double prop_zero = 0/9;",
// "const double prop_intended = 6/9;",
// "const double prop_turn_intended = 6/9;",
// "const double prop_displacement = 3/9;",
// "const double prop_turn_displacement = 3/9;",
// "const int width = " + std::to_string(maxBoundaries.first) + ";",
// "const int height = " + std::to_string(maxBoundaries.second) + ";"
// };
//modules.printConstants(os, constants);
modules.print();
if (!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 */ { //if (!configuration.empty()) {
return (std::array<bool, 8>) // modules.printConfiguration(os, configuration);
{ //}
!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())
};
} }

11
util/Grid.h
View File

@ -7,6 +7,7 @@
#include "MinigridGrammar.h" #include "MinigridGrammar.h"
#include "PrismModulesPrinter.h" #include "PrismModulesPrinter.h"
#include "PrismFormulaPrinter.h"
#include "ConfigYaml.h" #include "ConfigYaml.h"
struct GridOptions { struct GridOptions {
@ -21,16 +22,12 @@ struct GridOptions {
class Grid { class Grid {
public: 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(); cells getGridCells();
bool isBlocked(coordinates p); bool isBlocked(coordinates p);
bool isWall(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 printToPrism(std::ostream &os, std::vector<Configuration>& configuration, const prism::ModelType& modelType);
void applyOverwrites(std::string& str, std::vector<Configuration>& configuration); void applyOverwrites(std::string& str, std::vector<Configuration>& configuration);
@ -59,6 +56,7 @@ class Grid {
cells lockedDoors; cells lockedDoors;
cells unlockedDoors; cells unlockedDoors;
cells boxes; cells boxes;
cells balls;
cells lava; cells lava;
cells goals; cells goals;
@ -67,5 +65,6 @@ class Grid {
std::map<Color, cells> backgroundTiles; std::map<Color, cells> backgroundTiles;
std::map<coordinates, float> stateRewards; 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 #pragma once
#include <iostream> #include <iostream>
#include <set>
#include <functional> #include <functional>
#include "MinigridGrammar.h" #include "MinigridGrammar.h"
#include "PrismPrinter.h" #include "PrismPrinter.h"
#include "ConfigYaml.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 { namespace prism {
class PrismModulesPrinter { class PrismModulesPrinter {
public: public:
PrismModulesPrinter(const ModelType &modelType, const size_t &numberOfPlayer, std::vector<Configuration> config ,const bool enforceOneWays = false); 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();
std::ostream& printRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &grid_cells, const cells& keys, const cells& doors); void printModelType(const ModelType &modelType);
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);
bool isGame() const; bool isGame() const;
private: 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; void printDoneActions(const AgentName &agentName);
const size_t numberOfPlayer; void printPlayerStruct(const AgentName &agentName);
bool enforceOneWays; void printRewards(const AgentName &agentName, const std::map<coordinates, float> &stateRewards, const cells &lava, const cells &goals, const std::map<Color, cells> &backgroundTiles);
void printConfiguration(const std::vector<Configuration>& configurations);
void printConfiguredActions(const AgentName &agentName);
bool anyPortableObject() const;
bool faultyBehaviour() const;
bool slipperyBehaviour() const;
std::string moveGuard(const AgentName &agentName) const;
std::string faultyBehaviourGuard(const AgentName &agentName, const ActionId &actionId) const;
std::string faultyBehaviourUpdate(const AgentName &agentName, const ActionId &actionId) const;
std::string moveUpdate(const AgentName &agentName) const;
std::string updatesToString(const updates &updates) const;
std::string updateToString(const update &u) const;
std::string viewVariable(const AgentName &agentName, const size_t &agentDirection) const;
std::string buildConjunction(const AgentName &a, std::vector<std::string> formulae) const;
std::ostream &os;
std::stringstream actionStream;
ModelType const &modelType;
coordinates const &maxBoundaries;
AgentName agentName;
cells boxes;
cells balls;
cells lockedDoors;
cells unlockedDoors;
cells keys;
std::map<std::string, cells> slipperyTiles;
AgentNameAndPositionMap agentNameAndPositionMap;
std::map<AgentName, size_t> agentIndexMap;
size_t numberOfPlayer;
float const faultyProbability;
float const probIntended;
std::vector<Configuration> configuration; std::vector<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 #pragma once
#include <string> #include <string>
#include <map>
#include "cell.h" #include "cell.h"
typedef std::string AgentName; typedef std::string AgentName;
typedef size_t ViewDirection;
typedef std::pair<std::string, coordinates> AgentNameAndPosition; typedef std::pair<std::string, coordinates> AgentNameAndPosition;
typedef AgentNameAndPosition KeyNameAndPosition; typedef AgentNameAndPosition KeyNameAndPosition;
typedef std::map<AgentNameAndPosition::first_type, AgentNameAndPosition::second_type> AgentNameAndPositionMap; typedef std::map<AgentNameAndPosition::first_type, AgentNameAndPosition::second_type> AgentNameAndPositionMap;
typedef std::map<KeyNameAndPosition::first_type, KeyNameAndPosition::second_type> KeyNameAndPositionMap; 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 { namespace prism {
enum class ModelType { enum class ModelType {

31
util/cell.cpp
View File

@ -4,10 +4,14 @@
std::ostream &operator<<(std::ostream &os, const cell &c) { std::ostream &operator<<(std::ostream &os, const cell &c) {
os << static_cast<char>(c.type) << static_cast<char>(c.color); 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; return os;
} }
coordinates cell::getCoordinates() const {
return std::make_pair(column, row);
}
cell cell::getNorth(const std::vector<cell> &grid) const { cell cell::getNorth(const std::vector<cell> &grid) const {
auto north = std::find_if(grid.begin(), grid.end(), [this](const cell &c) { auto north = std::find_if(grid.begin(), grid.end(), [this](const cell &c) {
return this->row - 1 == c.row && this->column == c.column; 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; return *west;
} }
coordinates cell::getCoordinates() const {
return std::make_pair(row, column);
}
std::string cell::getColor() const { std::string cell::getColor() const {
switch(color) { switch(color) {
case Color::Red: return "red"; 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) { std::string getColor(Color color) {
switch(color) { switch(color) {
case Color::Red: return "red"; case Color::Red: return "red";

9
util/cell.h
View File

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

Write Preview
|||||||
100:0
Loading…
Cancel
Save