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

3 Commits
b816a1badb ... a3413fe990

Author SHA1 Message Date
sp a3413fe990 changed behaviour when moving against wall
4 months ago
sp 1d43c1d506 added slippery tiles and fixed faulty probability passing
4 months ago
sp 8c38856faf started to add non-directional slippery tiles
6 months ago
9 changed files with 105 additions and 49 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats
  1. 3
      main.cpp
  2. 15
      util/Grid.cpp
  3. 4
      util/Grid.h
  4. 1
      util/MinigridGrammar.h
  5. 3
      util/PrismFormulaPrinter.cpp
  6. 107
      util/PrismModulesPrinter.cpp
  7. 5
      util/PrismModulesPrinter.h
  8. 9
      util/cell.cpp
  9. 1
      util/cell.h

3
main.cpp
View File

@ -3,6 +3,7 @@
#include "util/Grid.h" #include "util/Grid.h"
#include "util/ConfigYaml.h" #include "util/ConfigYaml.h"
#include <vector>
#include <iostream> #include <iostream>
#include <fstream> #include <fstream>
#include <filesystem> #include <filesystem>
@ -163,7 +164,7 @@ int main(int argc, char* argv[]) {
setProbability(properties, parsed_properties, probTurnIntendedIdentifier, probTurnIntended); setProbability(properties, parsed_properties, probTurnIntendedIdentifier, probTurnIntended);
} }
if(ok) { 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";}); 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;; prism::ModelType modelType = prism::ModelType::MDP;;

15
util/Grid.cpp
View File

@ -3,14 +3,15 @@
#include <algorithm> #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); cell max = allGridCells.at(allGridCells.size() - 1);
maxBoundaries = std::make_pair(max.column - 1, max.row - 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(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(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(floor), [](cell c) { return c.type == Type::Floor; }); // TODO CHECK IF ALL AGENTS ARE ADDED TO FLOOR
std::copy_if(background.begin(), background.end(), std::back_inserter(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(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(slipperyEast), [](cell c) { return c.type == Type::SlipperyEast; });
std::copy_if(background.begin(), background.end(), std::back_inserter(slipperySouth), [](cell c) { return c.type == Type::SlipperySouth; }); std::copy_if(background.begin(), background.end(), std::back_inserter(slipperySouth), [](cell c) { return c.type == Type::SlipperySouth; });
@ -26,6 +27,7 @@ Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float>
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(boxes), [](cell c) { return c.type == Type::Box; }); std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(boxes), [](cell c) { return c.type == Type::Box; });
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(balls), [](cell c) { return c.type == Type::Ball; }); std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(balls), [](cell c) { return c.type == Type::Ball; });
std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(adversaries), [](cell c) { return c.type == Type::Adversary; }); 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; }); agent = *std::find_if(gridCells.begin(), gridCells.end(), [](cell c) { return c.type == Type::Agent; });
floor.push_back(agent); floor.push_back(agent);
@ -161,7 +163,7 @@ void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configurat
std::map<std::string, cells> wallRestrictions = {{"North", northRestriction}, {"East", eastRestriction}, {"South", southRestriction}, {"West", westRestriction}}; 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}, {"NorthWest", slipperyNorthWest}, {"NorthEast", slipperyNorthEast},{"SouthWest", slipperySouthWest},{"SouthEast", slipperySouthEast}};
std::map<std::string, cells> slipperyTiles = {{"Slippery", slippery}, {"North", slipperyNorth}, {"East", slipperyEast}, {"South", slipperySouth}, {"West", slipperyWest}, {"NorthWest", slipperyNorthWest}, {"NorthEast", slipperyNorthEast},{"SouthWest", slipperySouthWest},{"SouthEast", slipperySouthEast}};
std::vector<AgentName> agentNames; std::vector<AgentName> agentNames;
std::transform(agentNameAndPositionMap.begin(), std::transform(agentNameAndPositionMap.begin(),
@ -171,7 +173,7 @@ void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configurat
std::string agentName = agentNames.at(0); std::string agentName = agentNames.at(0);
prism::PrismFormulaPrinter formulas(os, wallRestrictions, walls, lockedDoors, unlockedDoors, keys, slipperyTiles, lava, goals, agentNameAndPositionMap, faultyProbability > 0.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); modules.printModelType(modelType);
for(const auto &agentName : agentNames) { for(const auto &agentName : agentNames) {
@ -179,12 +181,11 @@ void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configurat
} }
if(agentNameAndPositionMap.size() > 1) formulas.printCollisionFormula(agentName); if(agentNameAndPositionMap.size() > 1) formulas.printCollisionFormula(agentName);
formulas.printInitStruct(); formulas.printInitStruct();
os << "const int WIDTH = " << maxBoundaries.first << ";\n";
os << "const int HEIGHT = " << maxBoundaries.second << ";\n";
modules.print(); modules.print();
//if(!stateRewards.empty()) { //if(!stateRewards.empty()) {
// modules.printRewards(os, agentName, stateRewards, lava, goals, backgroundTiles); // modules.printRewards(os, agentName, stateRewards, lava, goals, backgroundTiles);
//} //}

4
util/Grid.h
View File

@ -13,7 +13,7 @@
class Grid { class Grid {
public: 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(); cells getGridCells();
@ -42,6 +42,7 @@ class Grid {
cells walls; cells walls;
cells floor; cells floor;
cells slippery;
cells slipperyNorth; cells slipperyNorth;
cells slipperyEast; cells slipperyEast;
cells slipperySouth; cells slipperySouth;
@ -63,5 +64,6 @@ class Grid {
std::map<coordinates, float> stateRewards; std::map<coordinates, float> stateRewards;
const float probIntended; const float probIntended;
const float probTurnIntended;
const float faultyProbability; const float faultyProbability;
}; };

1
util/MinigridGrammar.h
View File

@ -62,6 +62,7 @@ template <typename It>
("B", Type::Box) ("B", Type::Box)
("G", Type::Goal) ("G", Type::Goal)
("V", Type::Lava) ("V", Type::Lava)
("S", Type::Slippery)
("n", Type::SlipperyNorth) ("n", Type::SlipperyNorth)
("e", Type::SlipperyEast) ("e", Type::SlipperyEast)
("s", Type::SlipperySouth) ("s", Type::SlipperySouth)

3
util/PrismFormulaPrinter.cpp
View File

@ -67,7 +67,6 @@ namespace prism {
for(const auto& [direction, cells] : restrictions) { for(const auto& [direction, cells] : restrictions) {
printRestrictionFormula(agentName, direction, cells); printRestrictionFormula(agentName, direction, cells);
} }
if(slipperyBehaviour()) { if(slipperyBehaviour()) {
for(const auto& [direction, cells] : slipperyTiles) { for(const auto& [direction, cells] : slipperyTiles) {
printIsOnFormula(agentName, "Slippery", cells, direction); printIsOnFormula(agentName, "Slippery", cells, direction);
@ -235,7 +234,7 @@ namespace prism {
} }
bool PrismFormulaPrinter::slipperyBehaviour() const { bool PrismFormulaPrinter::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 PrismFormulaPrinter::anyPortableObject() const { bool PrismFormulaPrinter::anyPortableObject() const {
return !keys.empty(); return !keys.empty();

107
util/PrismModulesPrinter.cpp
View File

@ -5,15 +5,15 @@
#include <stdexcept> #include <stdexcept>
std::string northUpdate(const AgentName &a) { return "(row"+a+"'=row"+a+"-1)"; }
std::string southUpdate(const AgentName &a) { return "(row"+a+"'=row"+a+"+1)"; }
std::string eastUpdate(const AgentName &a) { return "(col"+a+"'=col"+a+"+1)"; }
std::string westUpdate(const AgentName &a) { return "(col"+a+"'=col"+a+"-1)"; }
std::string northUpdate(const AgentName &a) { return "min(WIDTH, max(1, row"+a+"'=row"+a+"-1))"; }
std::string southUpdate(const AgentName &a) { return "min(WIDTH, max(1, row"+a+"'=row"+a+"+1))"; }
std::string eastUpdate(const AgentName &a) { return "min(HEIGHT, max(1, col"+a+"'=col"+a+"+1))"; }
std::string westUpdate(const AgentName &a) { return "min(HEIGHT, max(1, col"+a+"'=col"+a+"-1))"; }
namespace prism { 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(); numberOfPlayer = agentNameAndPositionMap.size();
size_t index = 0; size_t index = 0;
for(auto begin = agentNameAndPositionMap.begin(); begin != agentNameAndPositionMap.end(); begin++, index++) { for(auto begin = agentNameAndPositionMap.begin(); begin != agentNameAndPositionMap.end(); begin++, index++) {
@ -250,7 +250,7 @@ namespace prism {
if(slipperyBehaviour()) guard += " & !" + a + "IsOnSlippery"; if(slipperyBehaviour()) guard += " & !" + a + "IsOnSlippery";
if(anyLava) guard += " & !" + a + "IsOnLava"; if(anyLava) guard += " & !" + a + "IsOnLava";
if(anyGoals && a == "Agent") guard += " & !" + a + "IsOnGoal"; if(anyGoals && a == "Agent") guard += " & !" + a + "IsOnGoal";
guard += " & !" + a + "CannotMove" + direction + "Wall";
//guard += " & !" + a + "CannotMove" + direction + "Wall";
if(anyPortableObject() || !lockedDoors.empty() || !unlockedDoors.empty()) guard += " & !" + a + "CannotMoveConditionally"; if(anyPortableObject() || !lockedDoors.empty() || !unlockedDoors.empty()) guard += " & !" + a + "CannotMoveConditionally";
guard += " -> "; guard += " -> ";
return guard; return guard;
@ -283,6 +283,10 @@ namespace prism {
} }
void PrismModulesPrinter::printSlipperyMovementActionsForRobot(const AgentName &a) { void PrismModulesPrinter::printSlipperyMovementActionsForRobot(const AgentName &a) {
if(!slipperyTiles.at("Slippery").empty()) {
printSlipperyMovementActionsForSlippery(a);
printSlipperyTurnActionsForSlippery(a);
}
if(!slipperyTiles.at("North").empty()) { if(!slipperyTiles.at("North").empty()) {
printSlipperyMovementActionsForNorth(a); printSlipperyMovementActionsForNorth(a);
printSlipperyTurnActionsForNorth(a); printSlipperyTurnActionsForNorth(a);
@ -316,10 +320,47 @@ namespace prism {
printSlipperyTurnActionsForSouthWest(a); 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) { 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)+"&"+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", { {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"; 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) { 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)+"&"+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", { {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"; 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", { {1, southUpdate(a) } }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "East", 1, { a+"CannotSlipSouth", a+"CannotSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", {}) << ";\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"; actionStream << printSlipperyMovementGuard(a, "East", 2, { a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {1, "true"} }) << ";\n";
} }
void PrismModulesPrinter::printSlipperyMovementActionsForSouth(const AgentName &a) { 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)+"&"+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", { {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"; 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) { 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)+"&"+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", { {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"; 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", { {1, southUpdate(a) } }) << ";\n";
actionStream << printSlipperyMovementGuard(a, "West", 1, { a+"CannotSlipSouth", a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", {}) << ";\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"; 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) { 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, "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+"'=view"+a+"-1)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "North", LEFT, { a+"CannotSlipNorth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\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) { 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, "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+"'=view"+a+"-1)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "East", LEFT, { a+"CannotSlipEast"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\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) { 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, "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+"'=view"+a+"-1)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "South", LEFT, { a+"CannotSlipSouth"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\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) { 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, "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+"'=view"+a+"-1)"} }) << ";\n";
actionStream << printSlipperyTurnGuard(a, "left", "West", LEFT, { a+"CannotSlipWest"}, "view"+a+"=0") << printSlipperyTurnUpdate(a, { {1, "(view"+a+"'=3)"} }) << ";\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 { 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 { bool PrismModulesPrinter::isGame() const {

5
util/PrismModulesPrinter.h
View File

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

9
util/cell.cpp
View File

@ -72,17 +72,18 @@ std::string cell::getColor() const {
std::string cell::getType() const { std::string cell::getType() const {
switch(type) { switch(type) {
case Type::Wall: return "Wall";
case Type::Floor: return "Floor";
case Type::Door: return "Door";
case Type::Wall: return "Wall";
case Type::Floor: return "Floor";
case Type::Door: return "Door";
case Type::LockedDoor: return "LockedDoor"; case Type::LockedDoor: return "LockedDoor";
case Type::Key: return "Key";
case Type::Key: return "Key";
case Type::Ball: return "Ball"; case Type::Ball: return "Ball";
case Type::Box: return "Box"; case Type::Box: return "Box";
case Type::Goal: return "Goal"; case Type::Goal: return "Goal";
case Type::Lava: return "Lava"; case Type::Lava: return "Lava";
case Type::Agent: return "Agent"; case Type::Agent: return "Agent";
case Type::Adversary: return "Adversary"; case Type::Adversary: return "Adversary";
case Type::Slippery: return "Slippery";
case Type::SlipperyNorth: return "SlipperyNorth"; case Type::SlipperyNorth: return "SlipperyNorth";
case Type::SlipperySouth: return "SlipperySouth"; case Type::SlipperySouth: return "SlipperySouth";
case Type::SlipperyEast: return "SlipperyEast"; case Type::SlipperyEast: return "SlipperyEast";

1
util/cell.h
View File

@ -20,6 +20,7 @@ enum class Type : char {
Lava = 'V', Lava = 'V',
Agent = 'X', Agent = 'X',
Adversary = 'Z', Adversary = 'Z',
Slippery = 'S',
SlipperyNorth = 'n', SlipperyNorth = 'n',
SlipperySouth = 's', SlipperySouth = 's',
SlipperyEast = 'e', SlipperyEast = 'e',

Write Preview
Loading…
Cancel
Save