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

WIP major rework of PrismModulesPrinter 

will probably get squashed, otw summary in later commit
pull/1/head
sp 1 year ago
parent
5955bb9791
commit
ca70595b58
2 changed files with 161 additions and 487 deletions
Unified View
  1. 512
      util/PrismModulesPrinter.cpp
  2. 68
      util/PrismModulesPrinter.h

512
util/PrismModulesPrinter.cpp
View File

@ -5,11 +5,12 @@
namespace prism { namespace prism {
PrismModulesPrinter::PrismModulesPrinter(const ModelType &modelType, const size_t &numberOfPlayer, std::vector<Configuration> config, const bool enforceOneWays) PrismModulesPrinter::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 AgentNameAndPositionMap &agentNameAndPositionMap, std::vector<Configuration> config, const bool enforceOneWays)
: modelType(modelType), numberOfPlayer(numberOfPlayer), enforceOneWays(enforceOneWays), configuration(config), viewDirectionMapping({{0, "East"}, {1, "South"}, {2, "West"}, {3, "North"}}) { : os(os), modelType(modelType), maxBoundaries(maxBoundaries), boxes(boxes), balls(balls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), agentNameAndPositionMap(agentNameAndPositionMap), enforceOneWays(enforceOneWays), configuration(config), viewDirectionMapping({{0, "East"}, {1, "South"}, {2, "West"}, {3, "North"}}) {
numberOfPlayer = agentNameAndPositionMap.size();
} }
std::ostream& PrismModulesPrinter::printModel(std::ostream &os, const ModelType &modelType) { std::ostream& PrismModulesPrinter::printModelType(const ModelType &modelType) {
switch(modelType) { switch(modelType) {
case(ModelType::MDP): case(ModelType::MDP):
os << "mdp"; os << "mdp";
@ -22,394 +23,52 @@ namespace prism {
return os; return os;
} }
std::ostream& PrismModulesPrinter::printBackgroundLabels(std::ostream &os, const AgentName &agentName, const std::pair<Color, cells> &backgroundTiles) { std::ostream& PrismModulesPrinter::print() {
if(backgroundTiles.second.size() == 0) return os; for(const auto &key : keys) {
printPortableObjectModule(key);
bool first = true;
std::string color = getColor(backgroundTiles.first);
color.at(0) = std::toupper(color.at(0));
os << "formula " << agentName << "On" << color << " = ";
for(auto const& cell : backgroundTiles.second) {
if(first) first = false; else os << " | ";
os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
}
os << ";\n";
os << "label \"" << agentName << "On" << color << "\" = " << agentName << "On" << color << ";\n";
return os;
}
std::ostream& PrismModulesPrinter::printRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &grid_cells, const cells &keys, const cells &doors) {
bool first = true;
os << "formula " << agentName << "CannotMove" << direction << " = " ;
for(auto const& cell : grid_cells) {
if(first) first = false;
else os << " | ";
os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
}
if (!keys.empty()) {
os << " | " << agentName << "CannotMove" << direction << "BecauseOfKey";
}
if (!doors.empty()) {
os << " | " << agentName << "CannotMove" << direction << "BecauseOfDoor";
}
os << ";\n";
return os;
}
std::ostream& PrismModulesPrinter::printKeyRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &keys) {
bool first = true;
os << "formula " << agentName << "CannotMove" << direction << "BecauseOfKey" << " = ";
for (auto const& key : keys) {
if(first) first = false;
else os << " | ";
std::string keyColor = key.getColor();
std::string xKey = "xKey" + keyColor;
std::string yKey = "yKey" + keyColor;
coordinates coords;
os << "(!" << agentName << "_has_" << keyColor << "_key & ";
if (direction == "North") {
os << " x" << agentName << " = " << xKey << "&y" << agentName << "-1 = " << yKey << ")";
} else if (direction == "South") {
os << " x" << agentName << " = " << xKey << "&y" << agentName << "+1 = " << yKey << ")";
} else if (direction == "East") {
os << " x" << agentName << "+1 = " << xKey << "&y" << agentName << " = " << yKey << ")";
} else if (direction == "West") {
os << " x" << agentName << "-1 = " << xKey << "&y" << agentName << " = " << yKey << ")";
} else {
os << "Invalid Direction! in Key Restriction";
}
}
os << ";\n";
return os;
}
std::ostream& PrismModulesPrinter::printDoorRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &doors) {
bool first = true;
os << "formula " << agentName << "CannotMove" << direction << "BecauseOfDoor" << " = ";
for (auto const& door : doors) {
if (first) first = false;
else os << " | ";
std::string doorColor = door.getColor();
size_t y = door.getCoordinates().first;
size_t x = door.getCoordinates().second;
os << "(!Door" << doorColor << "open & ";
if (direction == "North") {
os << " x" << agentName << " = " << x << "&y" << agentName << "-1 = " << y << ")";
} else if (direction == "South") {
os << " x" << agentName << " = " << x << "&y" << agentName << "+1 = " << y << ")";
} else if (direction == "East") {
os << " x" << agentName << "+1 = " << x << "&y" << agentName << " = " << y << ")";
} else if (direction == "West") {
os << " x" << agentName << "-1 = " << y << "&y" << agentName << " = " << y << ")";
} else {
os << "Invalid Direction! in Key Restriction";
}
}
os << ";\n";
return os;
}
std::ostream& PrismModulesPrinter::printIsOnSlipperyFormula(std::ostream& os, const AgentName &agentName, const std::vector<std::reference_wrapper<cells>> &slipperyCollection, const cells &slipperyNorth, const cells &slipperyEast, const cells &slipperySouth, const cells &slipperyWest) {
if(std::find_if(slipperyCollection.cbegin(), slipperyCollection.cend(), [=](const std::reference_wrapper<cells>& c) { return !c.get().empty(); }) == slipperyCollection.cend()) {
os << "formula " << agentName << "IsOnSlippery = false;\n";
return os;
}
bool first = true;
if (!slipperyNorth.empty()) {
os << "formula " << agentName << "IsOnSlipperyNorth = ";
for (const auto& cell : slipperyNorth) {
if(first) first = false; else os << " | ";
os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
}
os << ";\n";
}
if (!slipperyEast.empty()) {
first = true;
os << "formula " << agentName << "IsOnSlipperyEast = ";
for (const auto& cell : slipperyEast) {
if(first) first = false; else os << " | ";
os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
}
os << ";\n";
}
if (!slipperySouth.empty()) {
first = true;
os << "formula " << agentName << "IsOnSlipperySouth = ";
for (const auto& cell : slipperySouth) {
if(first) first = false; else os << " | ";
os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
}
os << ";\n";
}
if (!slipperyWest.empty()) {
first = true;
os << "formula " << agentName << "IsOnSlipperyWest = ";
for (const auto& cell : slipperyWest) {
if(first) first = false; else os << " | ";
os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
}
os << ";\n";
}
first = true;
os << "formula " << agentName << "IsOnSlippery = ";
for (const auto& slippery: slipperyCollection) {
for(const auto& cell : slippery.get()) {
if(first) first = false; else os << " | ";
os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
}
}
os << ";\n";
if(enforceOneWays) {
first = true;
os << "formula " << agentName << "IsOnSlipperyNorth = ";
for (const auto& cell: slipperyNorth) {
if(first) first = false; else os << " | ";
os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
}
os << ";\n";
first = true;
os << "formula " << agentName << "IsOnSlipperyEast = ";
for (const auto& cell: slipperyEast) {
if(first) first = false; else os << " | ";
os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
}
os << ";\n";
first = true;
os << "formula " << agentName << "IsOnSlipperySouth = ";
for (const auto& cell: slipperySouth) {
if(first) first = false; else os << " | ";
os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
}
os << ";\n";
first = true;
os << "formula " << agentName << "IsOnSlipperyWest = ";
for (const auto& cell: slipperyWest) {
if(first) first = false; else os << " | ";
os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
}
os << ";\n";
}
return os;
}
std::ostream& PrismModulesPrinter::printIsInLavaFormula(std::ostream& os, const AgentName &agentName, const cells &lava) {
if(lava.size() == 0) {
os << "formula " << agentName << "IsInLava = false;\n";
return os;
}
bool first = true;
os << "formula " << agentName << "IsInLava = ";
for(auto const& cell : lava) {
if(first) first = false; else os << " | ";
os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
}
os << ";\n";
os << "formula " << agentName << "IsInLavaAndNotDone = " << agentName << "IsInLava & !" << agentName << "Done;\n";
os << "label \"" << agentName << "IsInLavaAndNotDone\" = " << agentName << "IsInLava & !" << agentName << "Done;\n";
return os;
}
std::ostream& PrismModulesPrinter::printTurningNotAllowedFormulas(std::ostream& os, const AgentName &agentName, const cells &noTurnFloor) {
if( (!enforceOneWays or noTurnFloor.size() == 0) or (noTurnFloor.size() == 0) ) {
os << "formula " << agentName << "CannotTurn = false;\n";
return os;
} }
bool first = true; for(const auto &ball : balls) {
os << "formula " << agentName << "CannotTurn = "; printPortableObjectModule(ball);
for(auto const& cell : noTurnFloor) {
if(first) first = false; else os << " | ";
os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
} }
os << " | " << agentName << "IsOnSlippery;\n"; for(const auto &box : boxes) {
return os; printPortableObjectModule(box);
} }
for(const auto &door : unlockedDoors) {
std::ostream& PrismModulesPrinter::printIsFixedFormulas(std::ostream& os, const AgentName &agentName) { printDoorModule(door, true);
os << "formula " << agentName << "IsFixed = false;\n";
os << "formula " << agentName << "SlipperyTurnLeftAllowed = true;\n";
os << "formula " << agentName << "SlipperyTurnRightAllowed = true;\n";
os << "formula " << agentName << "SlipperyMoveForwardAllowed = true;\n";
os << "label \"FixedStates" << agentName << "\" = " << agentName << "IsFixed | !" << agentName << "SlipperyTurnRightAllowed | !" << agentName << "SlipperyTurnLeftAllowed | !" << agentName << "SlipperyMoveForwardAllowed | " << agentName << "IsInGoal | " << agentName << "IsInLava";
if(enforceOneWays) {
os << " | " << agentName << "CannotTurn";
} }
os << ";\n"; for(const auto &door : lockedDoors) {
//os << "label \"FixedStates\" = " << agentName << "IsFixed | " << agentName << "IsOnSlippery | " << agentName << "IsInGoal | " << agentName << "IsInLava;\n"; printDoorModule(door, false);
return os;
} }
for(const auto [agentName, initialPosition] : agentNameAndPositionMap) {
std::ostream& PrismModulesPrinter::printWallFormula(std::ostream& os, const AgentName &agentName, const cells &walls) { printRobotModule(agentName, initialPosition);
os << "formula " << agentName << "IsOnWall = ";
bool first = true;
for(auto const& cell : walls) {
if(first) first = false; else os << " | ";
os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
}
os << ";\n";
return os;
}
std::ostream& PrismModulesPrinter::printFormulas(std::ostream& os,
const AgentName &agentName,
const cells &restrictionNorth,
const cells &restrictionEast,
const cells &restrictionSouth,
const cells &restrictionWest,
const std::vector<std::reference_wrapper<cells>> &slipperyCollection,
const cells &lava,
const cells &walls,
const cells &noTurnFloor,
const cells &slipperyNorth,
const cells &slipperyEast,
const cells &slipperySouth,
const cells &slipperyWest,
const cells &keys,
const cells &doors) {
printRestrictionFormula(os, agentName, "North", restrictionNorth, keys, doors);
printRestrictionFormula(os, agentName, "East", restrictionEast, keys, doors);
printRestrictionFormula(os, agentName, "South", restrictionSouth, keys, doors);
printRestrictionFormula(os, agentName, "West", restrictionWest, keys, doors);
if (!keys.empty()) {
printKeyRestrictionFormula(os, agentName, "North", keys);
printKeyRestrictionFormula(os, agentName, "East", keys);
printKeyRestrictionFormula(os, agentName, "South", keys);
printKeyRestrictionFormula(os, agentName, "West", keys);
}
if (!doors.empty()) {
printDoorRestrictionFormula(os, agentName, "North", doors);
printDoorRestrictionFormula(os, agentName, "East", doors);
printDoorRestrictionFormula(os, agentName, "South", doors);
printDoorRestrictionFormula(os, agentName, "West", doors);
}
printIsOnSlipperyFormula(os, agentName, slipperyCollection, slipperyNorth, slipperyEast, slipperySouth, slipperyWest);
printIsInLavaFormula(os, agentName, lava);
printWallFormula(os, agentName, walls);
printTurningNotAllowedFormulas(os, agentName, noTurnFloor);
printIsFixedFormulas(os, agentName);
os << "\n";
return os;
}
std::ostream& PrismModulesPrinter::printGoalLabel(std::ostream& os, const AgentName &agentName, const cells &goals) {
if(goals.size() == 0) {
os << "formula " << agentName << "IsInGoal = false;\n";
return os;
} }
bool first = true;
os << "formula " << agentName << "IsInGoal = ";
for(auto const& cell : goals) {
if(first) first = false; else os << " | ";
os << "(x" << agentName << "=" << cell.column << "&y" << agentName << "=" << cell.row << ")";
}
os << ";\n";
os << "formula " << agentName << "IsInGoalAndNotDone = " << agentName << "IsInGoal & !" << agentName << "Done;\n";
os << "label \"" << agentName << "IsInGoalAndNotDone\" = " << agentName << "IsInGoal & !" << agentName << "Done;\n";
return os; return os;
} }
std::ostream& PrismModulesPrinter::printCrashLabel(std::ostream &os, const std::vector<AgentName> agentNames) {
os << "label crash = ";
bool first = true;
for(auto const& agentName : agentNames) {
if(agentName == "Agent") continue;
if(first) first = false; else os << " | ";
os << "(xAgent=x" << agentName << ")&(yAgent=y" << agentName << ")";
}
os << ";\n\n";
return os;
}
std::ostream& PrismModulesPrinter::printConfiguration(std::ostream& os, const std::vector<Configuration>& configurations) { std::ostream& PrismModulesPrinter::printConfiguration(std::ostream& os, const std::vector<Configuration>& configurations) {
for (auto& configuration : configurations) { for (auto& configuration : configurations) {
if (configuration.overwrite_ || configuration.type_ == ConfigType::Module) { if (configuration.overwrite_ || configuration.type_ == ConfigType::Module) {
continue; continue;
} }
os << configuration.expression_ << std::endl; os << configuration.expression_ << std::endl;
} }
return os; return os;
} }
std::ostream& PrismModulesPrinter::printConstants(std::ostream &os, const std::vector<std::string> &constants) { std::ostream& PrismModulesPrinter::printConstants(std::ostream &os, const std::vector<std::string> &constants) {
for (auto& constant : constants) { for (auto& constant : constants) {
os << constant << std::endl; os << constant << std::endl;
} }
return os; return os;
} }
std::ostream& PrismModulesPrinter::printAvoidanceLabel(std::ostream &os, const std::vector<AgentName> agentNames, const int &distance) {
os << "label avoidance = ";
bool first = true;
for(auto const& agentName : agentNames) {
if(agentName == "Agent") continue;
if(first) first = false; else os << " | ";
os << "max(xAgent-x" << agentName << ",x" << agentName << "-xAgent)+";
os << "max(yAgent-y" << agentName << ",y" << agentName << "-yAgent) ";
}
os << ";\n\n";
return os;
}
// TODO this does not account for multiple agents yet, i.e. key can be picked up multiple times
std::ostream& PrismModulesPrinter::printKeysLabels(std::ostream& os, const AgentName &agentName, const cells &keys) {
if(keys.size() == 0) return os;
for(auto const& key : keys) {
std::string keyColor = key.getColor();
std::string xKey = "xKey" + keyColor;
std::string yKey = "yKey" + keyColor;
os << "label \"" << agentName << "PickedUp" << keyColor << "Key\" = " << agentName << "_has_" << keyColor << "_key = true;\n";
os << "formula " << agentName << "CanPickUp" << keyColor << "Key = ";
os << "((x" << agentName << "-1 = " << xKey << "&y" << agentName << " = " << yKey << "&view" << agentName << " = 2) |";
os << " (x" << agentName << "+1 = " << xKey << "&y" << agentName << " = " << yKey << "&view" << agentName << " = 0) |";
os << " (x" << agentName << " = " << xKey << "&y" << agentName << "-1 = " << yKey << "&view" << agentName << " = 3) |";
os << " (x" << agentName << " = " << xKey << "&y" << agentName << "+1 = " << yKey << "&view" << agentName << " = 1) ) &";
os << "!" << agentName << "_has_" << keyColor << "_key;";
}
os << "\n";
return os;
}
std::ostream& PrismModulesPrinter::printBooleansForKeys(std::ostream &os, const AgentName &agentName, const cells &keys) { std::ostream& PrismModulesPrinter::printBooleansForKeys(std::ostream &os, const AgentName &agentName, const cells &keys) {
for(auto const& key : keys) { for(auto const& key : keys) {
os << "\t" << agentName << "_has_"<< key.getColor() << "_key : bool;\n";//init false;\n"; os << "\t" << agentName << "_has_"<< key.getColor() << "_key : bool;\n";//init false;\n";
} }
os << "\n"; os << "\n";
return os; return os;
} }
@ -562,90 +221,115 @@ namespace prism {
return os; return os;
} }
std::ostream& PrismModulesPrinter::printKeyModule(std::ostream &os, const cell &key, const coordinates &boundaries, AgentName agentName) { void PrismModulesPrinter::printPortableObjectModule(const cell &object) {
std::string keyIdentifier = "Key" + key.getColor(); std::string identifier = capitalize(object.getColor()) + object.getType();
os << "\nmodule " << identifier << std::endl;
os << "\tx" << identifier << " : [-1.." << maxBoundaries.second << "] init " << object.column << ";\n";
os << "\ty" << identifier << " : [-1.." << maxBoundaries.first << "] init " << object.row << ";\n";
os << "\t" << identifier << "PickedUp : bool;\n";
os << "\n";
os << "module " << keyIdentifier << "\n"; for(const auto [name, position] : agentNameAndPositionMap) {
printPortableObjectActions(name, identifier);
}
os << "endmodule\n\n";
}
void PrismModulesPrinter::printPortableObjectActions(const std::string &agentName, const std::string &identifier) {
os << "\t[" << agentName << "_pickup_" << identifier << "]\ttrue -> (x" << identifier << "'=-1) & (y" << identifier << "'=-1) & (" << identifier << "PickedUp'=true);\n";
os << "\t[" << agentName << "_drop_" << identifier << "_north]\ttrue -> (x" << identifier << "'=x" << agentName << ") & (y" << identifier << "'=y" << agentName << "-1) & (" << identifier << "PickedUp'=false);\n";
os << "\t[" << agentName << "_drop_" << identifier << "_west]\ttrue -> (x" << identifier << "'=x" << agentName << "-1) & (y" << identifier << "'=y" << agentName << ") & (" << identifier << "PickedUp'=false);\n";
os << "\t[" << agentName << "_drop_" << identifier << "_south]\ttrue -> (x" << identifier << "'=x" << agentName << ") & (y" << identifier << "'=y" << agentName << "+1) & (" << identifier << "PickedUp'=false);\n";
os << "\t[" << agentName << "_drop_" << identifier << "_east]\ttrue -> (x" << identifier << "'=x" << agentName << "+1) & (y" << identifier << "'=y" << agentName << ") & (" << identifier << "PickedUp'=false);\n";
}
os << "\tx" << keyIdentifier << " : [-1.." << boundaries.second << "];\n";
os << "\ty" << keyIdentifier << " : [-1.." << boundaries.first << "];\n";
os << "\n";
printKeyActions(os, key ,keyIdentifier, agentName);
void PrismModulesPrinter::printDoorModule(const cell &door, const bool &opened) {
std::string identifier = capitalize(door.getColor()) + door.getType();
os << "\nmodule " << identifier << std::endl;
os << "\t" << identifier << "Open : bool init false;\n";
os << "\n"; os << "\n";
return os;
}
std::ostream& PrismModulesPrinter::printKeyActions(std::ostream &os, const cell &key ,const std::string &keyIdentifier, AgentName agentName) { if(opened) {
std::string keyColor = key.getColor(); for(const auto [name, position] : agentNameAndPositionMap) {
printUnlockedDoorActions(name, identifier);
}
} else {
for(const auto [name, position] : agentNameAndPositionMap) {
printLockedDoorActions(name, identifier);
}
}
os << "endmodule\n\n";
}
os << "\t[pickup_" << keyColor << "key]\t" << pickupGuard(agentName, keyColor) << "-> "; void PrismModulesPrinter::printLockedDoorActions(const std::string &agentName, const std::string &identifier) {
os << "(xKey" << keyColor << "'=-1) & (yKey" << keyColor << "'=-1)" << ";\n"; os << "\t[" << agentName << "_unlock_" << identifier << "] !" << identifier << "Open -> (" << identifier << "Open'=true);\n";
os << "\t[" << agentName << "_close_" << identifier << "] " << identifier << "Open -> (" << identifier << "Open'=false);\n";
}
os << "\t[drop_" << keyColor << "_key_north]\t" << dropGuard(agentName, keyColor, 3) << "-> "; void PrismModulesPrinter::printUnlockedDoorActions(const std::string &agentName, const std::string &identifier) {
os << "(xKey" << keyColor << "'=x" << agentName << ") & (yKey" << keyColor << "'=y" <<agentName << "-1) ;\n"; os << "\t[" << agentName << "_open_" << identifier << "] !" << identifier << "Open -> (" << identifier << "Open'=true);\n";
os << "\t[" << agentName << "_close_" << identifier << "] " << identifier << "Open -> (" << identifier << "Open'=false);\n";
}
os << "\t[drop_" << keyColor << "_key_west]\t" << dropGuard(agentName, keyColor, 2) << "-> "; void PrismModulesPrinter::printRobotModule(const AgentName &agentName, const coordinates &initialPosition) {
os << "(xKey" << keyColor << "'=x" << agentName << "-1) & (yKey" << keyColor << "'=y" <<agentName << ") ;\n"; os << "\nmodule " << agentName << std::endl;
os << "\tx" << agentName << " : [0.." << maxBoundaries.second << "] init " << initialPosition.second << ";\n";
os << "\ty" << agentName << " : [0.." << maxBoundaries.first << "] init " << initialPosition.first << ";\n";
os << "\tview" << agentName << " : [0..3] init 1;\n";
os << "\t[drop_" << keyColor << "_key_south]\t" << dropGuard(agentName, keyColor, 1) << "-> "; for(const auto &door : unlockedDoors) {
os << "(xKey" << keyColor << "'=x" << agentName << ") & (yKey" << keyColor << "'=y" <<agentName << "+1) ;\n"; std::string identifier = capitalize(door.getColor()) + door.getType();
printUnlockedDoorActionsForRobot(agentName, identifier);
}
os << "\t[drop_" << keyColor << "_key_east]\t" << dropGuard(agentName, keyColor, 0) << "-> "; for(const auto &door : lockedDoors) {
os << "(xKey" << keyColor << "'=x" << agentName << "+1) & (yKey" << keyColor << "'=y" <<agentName << ") ;\n"; std::string identifier = capitalize(door.getColor()) + door.getType();
std::string key = capitalize(door.getColor()) + "Key";
printLockedDoorActionsForRobot(agentName, identifier, key);
}
return os; for(const auto &key : keys) {
std::string identifier = capitalize(key.getColor()) + key.getType();
os << "\tCarrying" << identifier << " : bool init false;\n";
printPortableObjectActionsForRobot(agentName, identifier);
} }
std::ostream& PrismModulesPrinter::printDoorModule(std::ostream &os, const cell &door, const coordinates &boundaries, AgentName agent) { os << "\n" << actionStream.str();
std::string doorIdentifier = "Door" + door.getColor(); os << "endmodule\n\n";
os << "module " << doorIdentifier << "\n"; }
os << "\t" << doorIdentifier << "locked : bool;\n"; void PrismModulesPrinter::printPortableObjectActionsForRobot(const std::string &a, const std::string &i) {
os << "\t" << doorIdentifier << "open : bool;\n"; actionStream << "\t[" << a << "_pickup_" << i << "] " << a << "CannotMove" << i << " -> (Carrying" << i << "'=true);\n";
actionStream << "\t[" << a << "_drop_" << i << "_north]\tCarrying" << i << " & view" << a << "=3 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveNorthWall -> (Carrying" << i << "'=false);\n";
actionStream << "\t[" << a << "_drop_" << i << "_west] \tCarrying" << i << " & view" << a << "=2 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveWestWall -> (Carrying" << i << "'=false);\n";
actionStream << "\t[" << a << "_drop_" << i << "_south]\tCarrying" << i << " & view" << a << "=1 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveSouthWall -> (Carrying" << i << "'=false);\n";
actionStream << "\t[" << a << "_drop_" << i << "_east] \tCarrying" << i << " & view" << a << "=0 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveEastWall -> (Carrying" << i << "'=false);\n";
actionStream << "\n";
}
printDoorActions(os, door, doorIdentifier, agent); void PrismModulesPrinter::printUnlockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier) {
actionStream << "\t[" << agentName << "_open_" << identifier << "] " << agentName << "CannotMove" << identifier << " -> true;\n";
actionStream << "\t[" << agentName << "_close_" << identifier << "] " << agentName << "IsNextTo" << identifier << " -> true;\n";
actionStream << "\n";
}
return os; void PrismModulesPrinter::printLockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier, const std::string &key) {
actionStream << "\t[" << agentName << "_unlock_" << identifier << "] " << agentName << "CannotMove" << identifier << " & Carrying" << key << " -> true;\n";
actionStream << "\t[" << agentName << "_close_" << identifier << "] " << agentName << "IsNextTo" << identifier << " & Carrying" << key << " -> true;\n";
actionStream << "\n";
} }
std::ostream& PrismModulesPrinter::printDoorActions(std::ostream &os, const cell &door ,const std::string &doorIdentifier, AgentName agentName) {
os << "\t[" << "unlock_" << doorIdentifier << "]\t" << unlockGuard(agentName, door) << " -> ";
os << "(" << doorIdentifier << "locked'=false) & (" << doorIdentifier << "open'=true) ;\n";
os << "\t[" << "toggle_" << doorIdentifier << "]\t" << toggleGuard(agentName, door) << " -> ";
os << "(" << doorIdentifier << "open'=!" << doorIdentifier << "open) ;\n";
return os;
}
std::string PrismModulesPrinter::unlockGuard(const AgentName &agentName, const cell& door) {
std::string doorColor = door.getColor();
std::string ret;
ret += agentName + "_has_" + doorColor + "_key & ";
ret += "((" + viewVariable(agentName, 0, true) + "x" + agentName + "+ 1 = " + std::to_string(door.column) + " & y" + agentName + "= " + std::to_string(door.row) + ")";
ret += " | (" + viewVariable(agentName, 1, true) + "x" + agentName + " = " + std::to_string(door.column) + " & y" + agentName + " + 1 = " + std::to_string(door.row) + ")";
ret += " | (" + viewVariable(agentName, 2, true) + "x" + agentName + "- 1 = " + std::to_string(door.column) + " & y" + agentName + "= " + std::to_string(door.row) + ")";
ret += " | (" + viewVariable(agentName, 3, true) + "x" + agentName + " = " + std::to_string(door.column) + " & y" + agentName + " - 1 = " + std::to_string(door.row) + "))";
return ret;
}
std::string PrismModulesPrinter::toggleGuard(const AgentName &agentName, const cell& door) {
std::string doorColor = door.getColor();
std::string ret;
ret += "!Door" + doorColor + "locked & (";
ret += "(" + viewVariable(agentName, 0, true) + "x" + agentName + "+ 1 = " + std::to_string(door.column) + " & y" + agentName + "= " + std::to_string(door.row) + ")";
ret += " | (" + viewVariable(agentName, 1, true) + "x" + agentName + " = " + std::to_string(door.column) + " & y" + agentName + " + 1 = " + std::to_string(door.row) + ")";
ret += " | (" + viewVariable(agentName, 2, true) + "x" + agentName + "- 1 = " + std::to_string(door.column) + " & y" + agentName + "= " + std::to_string(door.row) + ")";
ret += " | (" + viewVariable(agentName, 3, true) + "x" + agentName + " = " + std::to_string(door.column) + " & y" + agentName + " - 1 = " + std::to_string(door.row) + "))";
return ret;
}

68
util/PrismModulesPrinter.h
View File

@ -9,43 +9,25 @@
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 AgentNameAndPositionMap &agentNameAndPositionMap, std::vector<Configuration> config, const bool enforceOneWays = false);
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); std::ostream& 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); void printPortableObjectModule(const cell &object);
std::ostream& printKeyActions(std::ostream &os, const cell& key ,const std::string &keyIdentifier, AgentName agentName); 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);
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); std::ostream& printConstants(std::ostream &os, const std::vector<std::string> &constants);
/* /*
* Representation for Slippery Tile. * Representation for Slippery Tile.
@ -72,7 +54,6 @@ namespace prism {
*/ */
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& 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& printBooleansForKeys(std::ostream &os, const AgentName &agentName, const cells &keys);
std::ostream& printActionsForKeys(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& printBooleansForBackground(std::ostream &os, const AgentName &agentName, const std::map<Color, cells> &backgroundTiles);
@ -102,16 +83,25 @@ namespace prism {
std::string pickupGuard(const AgentName &agentName, const std::string keyColor); 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 dropGuard(const AgentName &agentName, const std::string keyColor, size_t view);
std::string moveUpdate(const size_t &agentIndex); 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); std::string viewVariable(const AgentName &agentName, const size_t &agentDirection, const bool agentWithView);
bool isGame() const; bool isGame() const;
private: private:
std::ostream &os;
std::stringstream actionStream;
ModelType const& modelType; ModelType const& modelType;
const size_t numberOfPlayer; coordinates const& maxBoundaries;
AgentName agentName;
cells boxes;
cells balls;
cells lockedDoors;
cells unlockedDoors;
cells keys;
AgentNameAndPositionMap agentNameAndPositionMap;
size_t numberOfPlayer;
bool enforceOneWays; bool enforceOneWays;
std::vector<Configuration> configuration; std::vector<Configuration> configuration;
std::map<int, std::string> viewDirectionMapping; std::map<int, std::string> viewDirectionMapping;

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