sp
/
Minigrid2PRISM
1
0
Fork 0
Code Issues 5 Pull Requests 1 Projects Releases Wiki Activity
Browse Source

added slippery tiles and fixed faulty probability passing

overwrites
sp 3 weeks ago
parent
8c38856faf
commit
1d43c1d506
5 changed files with 85 additions and 33 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. 5
      main.cpp
  2. 8
      util/Grid.cpp
  3. 3
      util/Grid.h
  4. 97
      util/PrismModulesPrinter.cpp
  5. 5
      util/PrismModulesPrinter.h

5
main.cpp
View File

@ -3,6 +3,7 @@
#include "util/Grid.h"
#include "util/ConfigYaml.h"
#include <vector>
#include <iostream>
#include <fstream>
#include <filesystem>
@ -163,7 +164,7 @@ int main(int argc, char* argv[]) {
setProbability(properties, parsed_properties, probTurnIntendedIdentifier, probTurnIntended);
}
if(ok) {
Grid grid(contentCells, backgroundCells, stateRewards, probIntended, faultyProbability);
Grid grid(contentCells, backgroundCells, stateRewards, probIntended, probTurnIntended, faultyProbability);
auto modelTypeIter = std::find_if(parsed_properties.begin(), parsed_properties.end(), [](const Property& obj) -> bool {return obj.property == "modeltype";});
prism::ModelType modelType = prism::ModelType::MDP;;
@ -176,7 +177,7 @@ int main(int argc, char* argv[]) {
grid.setModelType(modelType);
}
//grid.printToPrism(std::cout, configurations);

8
util/Grid.cpp
View File

@ -3,15 +3,15 @@
#include <algorithm>
Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float> &stateRewards, const float probIntended, const float faultyProbability)
: allGridCells(gridCells), background(background), stateRewards(stateRewards), probIntended(probIntended), faultyProbability(faultyProbability)
Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float> &stateRewards, const float probIntended, const float probTurnIntended, const float faultyProbability)
: allGridCells(gridCells), background(background), stateRewards(stateRewards), probIntended(probIntended), probTurnIntended(probTurnIntended), faultyProbability(faultyProbability)
{
cell max = allGridCells.at(allGridCells.size() - 1);
maxBoundaries = std::make_pair(max.column - 1, max.row - 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; }); // TODO CHECK IF ALL AGENTS ARE ADDED TO FLOOR
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(slippery), [](cell c) { return c.type == Type::Slippery; });
std::copy_if(background.begin(), background.end(), std::back_inserter(slippery), [](cell c) { return c.type == Type::Slippery; });
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; });
@ -173,7 +173,7 @@ void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configurat
std::string agentName = agentNames.at(0);
prism::PrismFormulaPrinter formulas(os, wallRestrictions, walls, lockedDoors, unlockedDoors, keys, slipperyTiles, lava, goals, agentNameAndPositionMap, faultyProbability > 0.0);
prism::PrismModulesPrinter modules(os, modelType, maxBoundaries, lockedDoors, unlockedDoors, keys, slipperyTiles, agentNameAndPositionMap, configuration, probIntended, faultyProbability, !lava.empty(), !goals.empty());
prism::PrismModulesPrinter modules(os, modelType, maxBoundaries, lockedDoors, unlockedDoors, keys, slipperyTiles, agentNameAndPositionMap, configuration, probIntended, probTurnIntended, faultyProbability, !lava.empty(), !goals.empty());
modules.printModelType(modelType);
for(const auto &agentName : agentNames) {

3
util/Grid.h
View File

@ -13,7 +13,7 @@
class Grid {
public:
Grid(cells gridCells, cells background, const std::map<coordinates, float> &stateRewards = {}, const float probIntended = 1.0, const float faultyProbability = 0);
Grid(cells gridCells, cells background, const std::map<coordinates, float> &stateRewards = {}, const float probIntended = 1.0, const float probTurnIntended = 1.0, const float faultyProbability = 0);
cells getGridCells();
@ -64,5 +64,6 @@ class Grid {
std::map<coordinates, float> stateRewards;
const float probIntended;
const float probTurnIntended;
const float faultyProbability;
};

97
util/PrismModulesPrinter.cpp
View File

@ -12,8 +12,8 @@ std::string westUpdate(const AgentName &a) { return "(col"+a+"'=col"+a+"-1)"; }
namespace prism {
PrismModulesPrinter::PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, 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, const bool anyLava, const bool anyGoals)
: os(os), modelType(modelType), maxBoundaries(maxBoundaries), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), agentNameAndPositionMap(agentNameAndPositionMap), configuration(config), probIntended(probIntended), faultyProbability(faultyProbability), anyLava(anyLava), anyGoals(anyGoals) {
PrismModulesPrinter::PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, 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 probTurnIntended, const float faultyProbability, const bool anyLava, const bool anyGoals)
: os(os), modelType(modelType), maxBoundaries(maxBoundaries), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), agentNameAndPositionMap(agentNameAndPositionMap), configuration(config), probIntended(probIntended), probTurnIntended(probTurnIntended), faultyProbability(faultyProbability), anyLava(anyLava), anyGoals(anyGoals) {
numberOfPlayer = agentNameAndPositionMap.size();
size_t index = 0;
for(auto begin = agentNameAndPositionMap.begin(); begin != agentNameAndPositionMap.end(); begin++, index++) {
@ -283,6 +283,10 @@ namespace prism {
}
void PrismModulesPrinter::printSlipperyMovementActionsForRobot(const AgentName &a) {
if(!slipperyTiles.at("Slippery").empty()) {
printSlipperyMovementActionsForSlippery(a);
printSlipperyTurnActionsForSlippery(a);
}
if(!slipperyTiles.at("North").empty()) {
printSlipperyMovementActionsForNorth(a);
printSlipperyTurnActionsForNorth(a);
@ -316,10 +320,47 @@ namespace prism {
printSlipperyTurnActionsForSouthWest(a);
}
}
void PrismModulesPrinter::printSlipperyMovementActionsForSlippery(const AgentName &a) {
actionStream << printSlipperyMovementGuard(a, "Slippery", 0, {"!"+a+"CannotSlipEast", "!"+a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {probIntended, eastUpdate(a)}, {(1 - probIntended) * 0.5, northUpdate(a)}, {(1 - probIntended) * 0.5, southUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 0, { a+"CannotSlipEast", "!"+a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {0.5 , northUpdate(a)}, {0.5 , southUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 0, {"!"+a+"CannotSlipEast", a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, eastUpdate(a)}, {(1 - probIntended) * 0.5, southUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 0, {"!"+a+"CannotSlipEast", "!"+a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, eastUpdate(a)}, {(1 - probIntended) * 0.5, northUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 0, { a+"CannotSlipEast", a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { { 1 , southUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 0, {"!"+a+"CannotSlipEast", a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {1 , eastUpdate(a)}, }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 0, { a+"CannotSlipEast", "!"+a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {1 , northUpdate(a)}, }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 0, { a+"CannotSlipEast", a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 1, {"!"+a+"CannotSlipSouth", "!"+a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {probIntended, southUpdate(a)}, {(1 - probIntended) * 0.5, eastUpdate(a)}, {(1 - probIntended) * 0.5, westUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 1, { a+"CannotSlipSouth", "!"+a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {0.5 , eastUpdate(a)}, {0.5 , westUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 1, {"!"+a+"CannotSlipSouth", a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, southUpdate(a)}, {(1 - probIntended) * 0.5, westUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 1, {"!"+a+"CannotSlipSouth", "!"+a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, southUpdate(a)}, {(1 - probIntended) * 0.5, eastUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 1, { a+"CannotSlipSouth", a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { { 1 , westUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 1, {"!"+a+"CannotSlipSouth", a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {1 , southUpdate(a)}, }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 1, { a+"CannotSlipSouth", "!"+a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {1 , eastUpdate(a)}, }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 1, { a+"CannotSlipSouth", a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {probIntended, westUpdate(a)}, {(1 - probIntended) * 0.5, northUpdate(a)}, {(1 - probIntended) * 0.5, southUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {0.5 , northUpdate(a)}, {0.5 , southUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, westUpdate(a)}, {(1 - probIntended) * 0.5, southUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, westUpdate(a)}, {(1 - probIntended) * 0.5, northUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 2, { a+"CannotSlipWest", a+"CannotSlipNorth", "!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { { 1 , southUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {1 , westUpdate(a)}, }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { {1 , northUpdate(a)}, }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 2, { a+"CannotSlipWest", a+"CannotSlipNorth", a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "", { }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 3, {"!"+a+"CannotSlipNorth", "!"+a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {probIntended, northUpdate(a)}, {(1 - probIntended) * 0.5, eastUpdate(a)}, {(1 - probIntended) * 0.5, westUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 3, { a+"CannotSlipNorth", "!"+a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {0.5 , eastUpdate(a)}, {0.5 , westUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 3, {"!"+a+"CannotSlipNorth", a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, northUpdate(a)}, {(1 - probIntended) * 0.5, westUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 3, {"!"+a+"CannotSlipNorth", "!"+a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {probIntended + (1 - probIntended) * 0.5, northUpdate(a)}, {(1 - probIntended) * 0.5, eastUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 3, { a+"CannotSlipNorth", a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { { 1 , westUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 3, {"!"+a+"CannotSlipNorth", a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {1 , northUpdate(a)}, }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 3, { a+"CannotSlipNorth", "!"+a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { {1 , eastUpdate(a)}, }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "Slippery", 3, { a+"CannotSlipNorth", a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "", { }) << ";\n";
}
void PrismModulesPrinter::printSlipperyMovementActionsForNorth(const AgentName &a) {
actionStream << printSlipperyMovementGuard(a, "North", 3, {"!"+a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, northUpdate(a)}, {(1 - probIntended) * 1/2, northUpdate(a)+"&"+eastUpdate(a)}, {(1 - probIntended) * 1/2, northUpdate(a)+"&"+westUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "North", 3, { a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1/2, northUpdate(a)+"&"+eastUpdate(a)}, {1/2, northUpdate(a)+"&"+westUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "North", 3, {"!"+a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, northUpdate(a)}, {(1 - probIntended) * 0.5, northUpdate(a)+"&"+eastUpdate(a)}, {(1 - probIntended) * 0.5, northUpdate(a)+"&"+westUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "North", 3, { a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {0.5, northUpdate(a)+"&"+eastUpdate(a)}, {0.5, northUpdate(a)+"&"+westUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "North", 3, {"!"+a+"CannotSlipNorth", a+"CannotSlipNorthEast", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, northUpdate(a)}, {(1 - probIntended), northUpdate(a)+"&"+westUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "North", 3, {"!"+a+"CannotSlipNorth", "!"+a+"CannotSlipNorthEast", a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, northUpdate(a)}, {(1 - probIntended), northUpdate(a)+"&"+eastUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "North", 3, { a+"CannotSlipNorth", a+"CannotSlipNorthEast", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "North", { {1, northUpdate(a)+"&"+westUpdate(a) } }) << ";\n";
@ -342,8 +383,8 @@ namespace prism {
}
void PrismModulesPrinter::printSlipperyMovementActionsForEast(const AgentName &a) {
actionStream << printSlipperyMovementGuard(a, "East", 0, {"!"+a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a)}, {(1 - probIntended) * 1/2, eastUpdate(a)+"&"+southUpdate(a)}, {(1 - probIntended) * 1/2, eastUpdate(a)+"&"+northUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "East", 0, { a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1/2, eastUpdate(a)+"&"+southUpdate(a)}, {1/2, eastUpdate(a)+"&"+northUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "East", 0, {"!"+a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a)}, {(1 - probIntended) * 0.5, eastUpdate(a)+"&"+southUpdate(a)}, {(1 - probIntended) * 0.5, eastUpdate(a)+"&"+northUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "East", 0, { a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {0.5, eastUpdate(a)+"&"+southUpdate(a)}, {0.5, eastUpdate(a)+"&"+northUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "East", 0, {"!"+a+"CannotSlipEast", a+"CannotSlipSouthEast", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a)}, {(1 - probIntended), eastUpdate(a)+"&"+northUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "East", 0, {"!"+a+"CannotSlipEast", "!"+a+"CannotSlipSouthEast", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a)}, {(1 - probIntended), eastUpdate(a)+"&"+southUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "East", 0, { a+"CannotSlipEast", a+"CannotSlipSouthEast", "!"+a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)+"&"+northUpdate(a) } }) << ";\n";
@ -361,13 +402,13 @@ namespace prism {
actionStream << printSlipperyMovementGuard(a, "East", 1, {"!"+a+"CannotSlipSouth", a+"CannotSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, southUpdate(a) } }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "East", 1, { a+"CannotSlipSouth", a+"CannotSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", {}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "East", 2, {"!"+a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a) }, {1 - probIntended, "true"} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "East", 2, {"!"+a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, westUpdate(a) }, {1 - probIntended, "true"} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "East", 2, { a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {1, "true"} }) << ";\n";
}
void PrismModulesPrinter::printSlipperyMovementActionsForSouth(const AgentName &a) {
actionStream << printSlipperyMovementGuard(a, "South", 1, {"!"+a+"CannotSlipSouth", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a)}, {(1 - probIntended) * 1/2, southUpdate(a)+"&"+eastUpdate(a)}, {(1 - probIntended) * 1/2, southUpdate(a)+"&"+westUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "South", 1, { a+"CannotSlipSouth", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1/2, southUpdate(a)+"&"+eastUpdate(a)}, {1/2, southUpdate(a)+"&"+westUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "South", 1, {"!"+a+"CannotSlipSouth", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a)}, {(1 - probIntended) * 0.5, southUpdate(a)+"&"+eastUpdate(a)}, {(1 - probIntended) * 0.5, southUpdate(a)+"&"+westUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "South", 1, { a+"CannotSlipSouth", "!"+a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {0.5, southUpdate(a)+"&"+eastUpdate(a)}, {0.5, southUpdate(a)+"&"+westUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "South", 1, {"!"+a+"CannotSlipSouth", a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a)}, {(1 - probIntended), southUpdate(a)+"&"+westUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "South", 1, {"!"+a+"CannotSlipSouth", "!"+a+"CannotSlipSouthEast", a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a)}, {(1 - probIntended), southUpdate(a)+"&"+eastUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "South", 1, { a+"CannotSlipSouth", a+"CannotSlipSouthEast", "!"+a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "South", { {1, southUpdate(a)+"&"+westUpdate(a) } }) << ";\n";
@ -390,8 +431,8 @@ namespace prism {
}
void PrismModulesPrinter::printSlipperyMovementActionsForWest(const AgentName &a) {
actionStream << printSlipperyMovementGuard(a, "West", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipSouthWest", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a)}, {(1 - probIntended) * 1/2, westUpdate(a)+"&"+southUpdate(a)}, {(1 - probIntended) * 1/2, westUpdate(a)+"&"+northUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "West", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipSouthWest", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1/2, westUpdate(a)+"&"+southUpdate(a)}, {1/2, westUpdate(a)+"&"+northUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "West", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipSouthWest", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a)}, {(1 - probIntended) * 0.5, westUpdate(a)+"&"+southUpdate(a)}, {(1 - probIntended) * 0.5, westUpdate(a)+"&"+northUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "West", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipSouthWest", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {0.5, westUpdate(a)+"&"+southUpdate(a)}, {0.5, westUpdate(a)+"&"+northUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "West", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipSouthWest", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a)}, {(1 - probIntended), westUpdate(a)+"&"+northUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "West", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipSouthWest", a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a)}, {(1 - probIntended), westUpdate(a)+"&"+southUpdate(a)} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "West", 2, { a+"CannotSlipWest", a+"CannotSlipSouthWest", "!"+a+"CannotSlipNorthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)+"&"+northUpdate(a) } }) << ";\n";
@ -409,46 +450,52 @@ namespace prism {
actionStream << printSlipperyMovementGuard(a, "West", 1, {"!"+a+"CannotSlipSouth", a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, southUpdate(a) } }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "West", 1, { a+"CannotSlipSouth", a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", {}) << ";\n";
actionStream << printSlipperyMovementGuard(a, "West", 0, {"!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a) }, {1 - probIntended, "true"} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "West", 0, {"!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, eastUpdate(a) }, {1 - probIntended, "true"} }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "West", 0, { a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", {{1, "true"}}) << ";\n";
}
void PrismModulesPrinter::printSlipperyTurnActionsForSlippery(const AgentName &a) {
actionStream << printSlipperyTurnGuard(a, "right", "Slippery", RIGHT, {}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "Slippery", LEFT, {}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "Slippery", LEFT, {}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n";
}
void PrismModulesPrinter::printSlipperyTurnActionsForNorth(const AgentName &a) {
actionStream << printSlipperyTurnGuard(a, "right", "North", RIGHT, {"!"+a+"CannotSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, northUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", "North", RIGHT, {"!"+a+"CannotSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probTurnIntended, northUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", "North", RIGHT, { a+"CannotSlipNorth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, {"!"+a+"CannotSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, northUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, {"!"+a+"CannotSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, northUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, {"!"+a+"CannotSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probTurnIntended, northUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, {"!"+a+"CannotSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=3)"}, {1 - probTurnIntended, northUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, { a+"CannotSlipNorth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, { a+"CannotSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n";
}
void PrismModulesPrinter::printSlipperyTurnActionsForEast(const AgentName &a) {
actionStream << printSlipperyTurnGuard(a, "right", "East", RIGHT, {"!"+a+"CannotSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, eastUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", "East", RIGHT, {"!"+a+"CannotSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probTurnIntended, eastUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", "East", RIGHT, { a+"CannotSlipEast"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, {"!"+a+"CannotSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, eastUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, {"!"+a+"CannotSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, eastUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, {"!"+a+"CannotSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probTurnIntended, eastUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, {"!"+a+"CannotSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=3)"}, {1 - probTurnIntended, eastUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, { a+"CannotSlipEast"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, { a+"CannotSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n";
}
void PrismModulesPrinter::printSlipperyTurnActionsForSouth(const AgentName &a) {
actionStream << printSlipperyTurnGuard(a, "right", "South", RIGHT, {"!"+a+"CannotSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, southUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", "South", RIGHT, {"!"+a+"CannotSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probTurnIntended, southUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", "South", RIGHT, { a+"CannotSlipSouth"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, {"!"+a+"CannotSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, southUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, {"!"+a+"CannotSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, southUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, {"!"+a+"CannotSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probTurnIntended, southUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, {"!"+a+"CannotSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=3)"}, {1 - probTurnIntended, southUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, { a+"CannotSlipSouth"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, { a+"CannotSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n";
}
void PrismModulesPrinter::printSlipperyTurnActionsForWest(const AgentName &a) {
actionStream << printSlipperyTurnGuard(a, "right", "West", RIGHT, {"!"+a+"CannotSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probIntended, westUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", "West", RIGHT, {"!"+a+"CannotSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=mod(view"+a+"+1,4))"}, { 1 - probTurnIntended, westUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "right", "West", RIGHT, { a+"CannotSlipWest"}, "true") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=mod(view"+a+"+1,4))"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, {"!"+a+"CannotSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probIntended, westUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, {"!"+a+"CannotSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probIntended, "(view"+a+"'=3)"}, {1 - probIntended, westUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, {"!"+a+"CannotSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=view"+a+"-1)"}, {1 - probTurnIntended, westUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, {"!"+a+"CannotSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {probTurnIntended, "(view"+a+"'=3)"}, {1 - probTurnIntended, westUpdate(a)} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, { a+"CannotSlipWest"}, "view"+a+">0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=view"+a+"-1)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, { a+"CannotSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\n";
}
@ -720,7 +767,7 @@ namespace prism {
}
bool PrismModulesPrinter::slipperyBehaviour() const {
return !slipperyTiles.at("North").empty() || !slipperyTiles.at("East").empty() || !slipperyTiles.at("South").empty() || !slipperyTiles.at("West").empty();
return !slipperyTiles.at("Slippery").empty() || !slipperyTiles.at("North").empty() || !slipperyTiles.at("East").empty() || !slipperyTiles.at("South").empty() || !slipperyTiles.at("West").empty();
}
bool PrismModulesPrinter::isGame() const {

5
util/PrismModulesPrinter.h
View File

@ -16,7 +16,7 @@ std::string westUpdate(const AgentName &a);
namespace prism {
class PrismModulesPrinter {
public:
PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, 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, const bool anyLava, const bool anyGoals);
PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, 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 probTurnIntended, const float faultyProbability, const bool anyLava, const bool anyGoals);
std::ostream& print();
@ -40,10 +40,12 @@ namespace prism {
void printTurnActionsForRobot(const std::string &a);
void printNonMovementActionsForRobot(const AgentName &agentName);
void printSlipperyMovementActionsForRobot(const AgentName &a);
void printSlipperyMovementActionsForSlippery(const AgentName &a);
void printSlipperyMovementActionsForNorth(const AgentName &a);
void printSlipperyMovementActionsForEast(const AgentName &a);
void printSlipperyMovementActionsForSouth(const AgentName &a);
void printSlipperyMovementActionsForWest(const AgentName &a);
void printSlipperyTurnActionsForSlippery(const AgentName &a);
void printSlipperyTurnActionsForNorth(const AgentName &a);
void printSlipperyTurnActionsForEast(const AgentName &a);
void printSlipperyTurnActionsForSouth(const AgentName &a);
@ -113,6 +115,7 @@ namespace prism {
size_t numberOfPlayer;
float const faultyProbability;
float const probIntended;
float const probTurnIntended;
std::vector<Configuration> configuration;
std::vector<ViewDirection> viewDirections = {0, 1, 2, 3};
std::map<ViewDirection, std::string> viewDirectionToString = {{0, "East"}, {1, "South"}, {2, "West"}, {3, "North"}};

Write Preview
Loading…
Cancel
Save