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

switched most tabs to two whitespaces in output

remove_unnecessary_guards
sp 12 months ago
parent
34a399972d
commit
92d7d11daa
2 changed files with 42 additions and 39 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 Download Patch File Download Diff File
  1. 76
      util/PrismModulesPrinter.cpp
  2. 5
      util/PrismModulesPrinter.h

76
util/PrismModulesPrinter.cpp
View File

@ -104,9 +104,9 @@ namespace prism {
void PrismModulesPrinter::printPortableObjectModule(const cell &object) { void PrismModulesPrinter::printPortableObjectModule(const cell &object) {
std::string identifier = capitalize(object.getColor()) + object.getType(); std::string identifier = capitalize(object.getColor()) + object.getType();
os << "\nmodule " << identifier << std::endl; 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 << " x" << identifier << " : [-1.." << maxBoundaries.second << "] init " << object.column << ";\n";
os << " y" << identifier << " : [-1.." << maxBoundaries.first << "] init " << object.row << ";\n";
os << " " << identifier << "PickedUp : bool;\n";
os << "\n"; os << "\n";
for(const auto [name, position] : agentNameAndPositionMap) { for(const auto [name, position] : agentNameAndPositionMap) {
@ -118,25 +118,25 @@ namespace prism {
void PrismModulesPrinter::printPortableObjectActions(const std::string &agentName, const std::string &identifier) { void PrismModulesPrinter::printPortableObjectActions(const std::string &agentName, const std::string &identifier) {
std::string actionName = "[" + agentName + "_pickup_" + identifier + "]"; std::string actionName = "[" + agentName + "_pickup_" + identifier + "]";
agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
os << "\t" << actionName << " true -> (x" << identifier << "'=-1) & (y" << identifier << "'=-1) & (" << identifier << "PickedUp'=true);\n";
os << " " << actionName << " true -> (x" << identifier << "'=-1) & (y" << identifier << "'=-1) & (" << identifier << "PickedUp'=true);\n";
actionName = "[" + agentName + "_drop_" + identifier + "_north]"; actionName = "[" + agentName + "_drop_" + identifier + "_north]";
agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
os << "\t" << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << ") & (y" << identifier << "'=y" << agentName << "-1) & (" << identifier << "PickedUp'=false);\n";
os << " " << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << ") & (y" << identifier << "'=y" << agentName << "-1) & (" << identifier << "PickedUp'=false);\n";
actionName = "[" + agentName + "_drop_" + identifier + "_west]"; actionName = "[" + agentName + "_drop_" + identifier + "_west]";
agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
os << "\t" << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << "-1) & (y" << identifier << "'=y" << agentName << ") & (" << identifier << "PickedUp'=false);\n";
os << " " << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << "-1) & (y" << identifier << "'=y" << agentName << ") & (" << identifier << "PickedUp'=false);\n";
actionName = "[" + agentName + "_drop_" + identifier + "_south]"; actionName = "[" + agentName + "_drop_" + identifier + "_south]";
agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
os << "\t" << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << ") & (y" << identifier << "'=y" << agentName << "+1) & (" << identifier << "PickedUp'=false);\n";
os << " " << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << ") & (y" << identifier << "'=y" << agentName << "+1) & (" << identifier << "PickedUp'=false);\n";
actionName = "[" + agentName + "_drop_" + identifier + "_east]"; actionName = "[" + agentName + "_drop_" + identifier + "_east]";
agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
os << "\t" << actionName << " " << " ttrue -> (x" << identifier << "'=x" << agentName << "+1) & (y" << identifier << "'=y" << agentName << ") & (" << identifier << "PickedUp'=false);\n";
os << " " << actionName << " " << " ttrue -> (x" << identifier << "'=x" << agentName << "+1) & (y" << identifier << "'=y" << agentName << ") & (" << identifier << "PickedUp'=false);\n";
} }
void PrismModulesPrinter::printDoorModule(const cell &door, const bool &opened) { void PrismModulesPrinter::printDoorModule(const cell &door, const bool &opened) {
std::string identifier = capitalize(door.getColor()) + door.getType(); std::string identifier = capitalize(door.getColor()) + door.getType();
os << "\nmodule " << identifier << std::endl; os << "\nmodule " << identifier << std::endl;
os << "\t" << identifier << "Open : bool init false;\n";
os << " " << identifier << "Open : bool init false;\n";
os << "\n"; os << "\n";
if(opened) { if(opened) {
@ -154,26 +154,26 @@ namespace prism {
void PrismModulesPrinter::printLockedDoorActions(const std::string &agentName, const std::string &identifier) { void PrismModulesPrinter::printLockedDoorActions(const std::string &agentName, const std::string &identifier) {
std::string actionName = "[" + agentName + "_unlock_" + identifier + "]"; std::string actionName = "[" + agentName + "_unlock_" + identifier + "]";
agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
os << "\t" << actionName << " !" << identifier << "Open -> (" << identifier << "Open'=true);\n";
os << " " << actionName << " !" << identifier << "Open -> (" << identifier << "Open'=true);\n";
actionName = "[" + agentName + "_close_" + identifier + "]"; actionName = "[" + agentName + "_close_" + identifier + "]";
agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
os << "\t" << actionName << " " << identifier << "Open -> (" << identifier << "Open'=false);\n";
os << " " << actionName << " " << identifier << "Open -> (" << identifier << "Open'=false);\n";
} }
void PrismModulesPrinter::printUnlockedDoorActions(const std::string &agentName, const std::string &identifier) { void PrismModulesPrinter::printUnlockedDoorActions(const std::string &agentName, const std::string &identifier) {
std::string actionName = "[" + agentName + "_open_" + identifier + "]"; std::string actionName = "[" + agentName + "_open_" + identifier + "]";
agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
os << "\t !" << identifier << "Open -> (" << identifier << "Open'=true);\n";
os << " !" << identifier << "Open -> (" << identifier << "Open'=true);\n";
actionName = "[" + agentName + "_close_" + identifier + "]"; actionName = "[" + agentName + "_close_" + identifier + "]";
agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
os << "\t" << agentName << " " << identifier << "Open -> (" << identifier << "Open'=false);\n";
os << " " << agentName << " " << identifier << "Open -> (" << identifier << "Open'=false);\n";
} }
void PrismModulesPrinter::printRobotModule(const AgentName &agentName, const coordinates &initialPosition) { void PrismModulesPrinter::printRobotModule(const AgentName &agentName, const coordinates &initialPosition) {
os << "\nmodule " << agentName << std::endl; os << "\nmodule " << agentName << std::endl;
os << "\tcol" << agentName << " : [1.." << maxBoundaries.second << "] init " << initialPosition.second << ";\n";
os << "\trow" << agentName << " : [1.." << maxBoundaries.first << "] init " << initialPosition.first << ";\n";
os << "\tview" << agentName << " : [0..3] init 1;\n";
os << " col" << agentName << " : [1.." << maxBoundaries.second << "] init " << initialPosition.second << ";\n";
os << " row" << agentName << " : [1.." << maxBoundaries.first << "] init " << initialPosition.first << ";\n";
os << " view" << agentName << " : [0..3] init 1;\n";
printTurnActionsForRobot(agentName); printTurnActionsForRobot(agentName);
printMovementActionsForRobot(agentName); printMovementActionsForRobot(agentName);
@ -192,19 +192,19 @@ namespace prism {
for(const auto &key : keys) { for(const auto &key : keys) {
std::string identifier = capitalize(key.getColor()) + key.getType(); std::string identifier = capitalize(key.getColor()) + key.getType();
os << "\t" << agentName << "Carrying" << identifier << " : bool init false;\n";
os << " " << agentName << "Carrying" << identifier << " : bool init false;\n";
printPortableObjectActionsForRobot(agentName, identifier); printPortableObjectActionsForRobot(agentName, identifier);
} }
for(const auto &ball : balls) { for(const auto &ball : balls) {
std::string identifier = capitalize(ball.getColor()) + ball.getType(); std::string identifier = capitalize(ball.getColor()) + ball.getType();
os << "\t" << agentName << "Carrying" << identifier << " : bool init false;\n";
os << " " << agentName << "Carrying" << identifier << " : bool init false;\n";
printPortableObjectActionsForRobot(agentName, identifier); printPortableObjectActionsForRobot(agentName, identifier);
} }
for(const auto &box : boxes) { for(const auto &box : boxes) {
std::string identifier = capitalize(box.getColor()) + box.getType(); std::string identifier = capitalize(box.getColor()) + box.getType();
os << "\t" << agentName << "Carrying" << identifier << " : bool init false;\n";
os << " " << agentName << "Carrying" << identifier << " : bool init false;\n";
printPortableObjectActionsForRobot(agentName, identifier); printPortableObjectActionsForRobot(agentName, identifier);
} }
@ -214,23 +214,23 @@ namespace prism {
} }
void PrismModulesPrinter::printPortableObjectActionsForRobot(const std::string &a, const std::string &i) { void PrismModulesPrinter::printPortableObjectActionsForRobot(const std::string &a, const std::string &i) {
actionStream << "\t[" << a << "_pickup_" << i << "] " << " !" << a << "IsCarrying & " << a << "CannotMove" << i << " -> (" << a << "Carrying" << i << "'=true);\n";
actionStream << "\t[" << a << "_drop_" << i << "_north]\t" << a << "Carrying" << i << " & view" << a << "=3 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveNorthWall -> (" << a << "Carrying" << i << "'=false);\n";
actionStream << "\t[" << a << "_drop_" << i << "_west] \t" << a << "Carrying" << i << " & view" << a << "=2 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveWestWall -> (" << a << "Carrying" << i << "'=false);\n";
actionStream << "\t[" << a << "_drop_" << i << "_south]\t" << a << "Carrying" << i << " & view" << a << "=1 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveSouthWall -> (" << a << "Carrying" << i << "'=false);\n";
actionStream << "\t[" << a << "_drop_" << i << "_east] \t" << a << "Carrying" << i << " & view" << a << "=0 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveEastWall -> (" << a << "Carrying" << i << "'=false);\n";
actionStream << " [" << a << "_pickup_" << i << "] " << " !" << a << "IsCarrying & " << a << "CannotMove" << i << " -> (" << a << "Carrying" << i << "'=true);\n";
actionStream << " [" << a << "_drop_" << i << "_north]\t" << a << "Carrying" << i << " & view" << a << "=3 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveNorthWall -> (" << a << "Carrying" << i << "'=false);\n";
actionStream << " [" << a << "_drop_" << i << "_west] \t" << a << "Carrying" << i << " & view" << a << "=2 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveWestWall -> (" << a << "Carrying" << i << "'=false);\n";
actionStream << " [" << a << "_drop_" << i << "_south]\t" << a << "Carrying" << i << " & view" << a << "=1 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveSouthWall -> (" << a << "Carrying" << i << "'=false);\n";
actionStream << " [" << a << "_drop_" << i << "_east] \t" << a << "Carrying" << i << " & view" << a << "=0 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveEastWall -> (" << a << "Carrying" << i << "'=false);\n";
actionStream << "\n"; actionStream << "\n";
} }
void PrismModulesPrinter::printUnlockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier) { 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 << " [" << agentName << "_open_" << identifier << "] " << agentName << "CannotMove" << identifier << " -> true;\n";
actionStream << " [" << agentName << "_close_" << identifier << "] " << agentName << "IsNextTo" << identifier << " -> true;\n";
actionStream << "\n"; actionStream << "\n";
} }
void PrismModulesPrinter::printLockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier, const std::string &key) { void PrismModulesPrinter::printLockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier, const std::string &key) {
actionStream << "\t[" << agentName << "_unlock_" << identifier << "] " << agentName << "CannotMove" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n";
actionStream << "\t[" << agentName << "_close_" << identifier << "] " << agentName << "IsNextTo" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n";
actionStream << " [" << agentName << "_unlock_" << identifier << "] " << agentName << "CannotMove" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n";
actionStream << " [" << agentName << "_close_" << identifier << "] " << agentName << "IsNextTo" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n";
actionStream << "\n"; actionStream << "\n";
} }
@ -248,7 +248,7 @@ namespace prism {
if(faultyBehaviour()) { if(faultyBehaviour()) {
std::string actionName = "[" + a + "_stuck]"; std::string actionName = "[" + a + "_stuck]";
agentNameActionMap.at(a).insert({FORWARD, actionName}); agentNameActionMap.at(a).insert({FORWARD, actionName});
actionStream << "\t" << actionName << " " << "previousAction" << a << "=" << std::to_string(FORWARD);
actionStream << " " << actionName << " " << "previousAction" << a << "=" << std::to_string(FORWARD);
actionStream << " & ((view" << a << "=0 & " << a << "CannotMoveEastWall) |"; actionStream << " & ((view" << a << "=0 & " << a << "CannotMoveEastWall) |";
actionStream << " (view" << a << "=1 & " << a << "CannotMoveSouthWall) |"; actionStream << " (view" << a << "=1 & " << a << "CannotMoveSouthWall) |";
actionStream << " (view" << a << "=2 & " << a << "CannotMoveWestWall) |"; actionStream << " (view" << a << "=2 & " << a << "CannotMoveWestWall) |";
@ -276,7 +276,7 @@ namespace prism {
std::string PrismModulesPrinter::printTurnGuard(const AgentName &a, const std::string &direction, const ActionId &actionId, const std::string &cond) { std::string PrismModulesPrinter::printTurnGuard(const AgentName &a, const std::string &direction, const ActionId &actionId, const std::string &cond) {
std::string actionName = "[" + a + "_turn_" + direction + "]"; std::string actionName = "[" + a + "_turn_" + direction + "]";
agentNameActionMap.at(a).insert({actionId, actionName}); agentNameActionMap.at(a).insert({actionId, actionName});
return "\t" + actionName + " " + cond + " -> ";
return " " + actionName + " " + cond + " -> ";
} }
std::string PrismModulesPrinter::printTurnUpdate(const AgentName &a, const update &u, const ActionId &actionId) const { std::string PrismModulesPrinter::printTurnUpdate(const AgentName &a, const update &u, const ActionId &actionId) const {
@ -449,7 +449,7 @@ namespace prism {
std::string PrismModulesPrinter::printSlipperyMovementGuard(const AgentName &a, const std::string &direction, const ViewDirection &viewDirection, const std::vector<std::string> &guards) { std::string PrismModulesPrinter::printSlipperyMovementGuard(const AgentName &a, const std::string &direction, const ViewDirection &viewDirection, const std::vector<std::string> &guards) {
std::string actionName = "[" + a + "_move_" + viewDirectionToString.at(viewDirection) + "]"; std::string actionName = "[" + a + "_move_" + viewDirectionToString.at(viewDirection) + "]";
agentNameActionMap.at(a).insert({FORWARD, actionName}); agentNameActionMap.at(a).insert({FORWARD, actionName});
return "\t" + actionName + " " + viewVariable(a, viewDirection) + a + "IsOnSlippery" + direction + " & " + buildConjunction(a, guards) + " -> ";
return " " + actionName + " " + viewVariable(a, viewDirection) + " & " + a + "IsOnSlippery" + direction + " & " + buildConjunction(a, guards) + " -> ";
} }
std::string PrismModulesPrinter::printSlipperyMovementUpdate(const AgentName &a, const std::string &direction, const updates &u) const { std::string PrismModulesPrinter::printSlipperyMovementUpdate(const AgentName &a, const std::string &direction, const updates &u) const {
@ -459,7 +459,7 @@ namespace prism {
std::string PrismModulesPrinter::printSlipperyTurnGuard(const AgentName &a, const std::string &direction, const ActionId &actionId, const std::vector<std::string> &guards, const std::string &cond) { std::string PrismModulesPrinter::printSlipperyTurnGuard(const AgentName &a, const std::string &direction, const ActionId &actionId, const std::vector<std::string> &guards, const std::string &cond) {
std::string actionName = "[" + a + "_turn_" + direction + "]"; std::string actionName = "[" + a + "_turn_" + direction + "]";
agentNameActionMap.at(a).insert({actionId, actionName}); agentNameActionMap.at(a).insert({actionId, actionName});
return "\t" + actionName + " " + buildConjunction(a, guards) + " & " + cond + " -> ";
return " " + actionName + " " + buildConjunction(a, guards) + " & " + cond + " -> ";
} }
std::string PrismModulesPrinter::printSlipperyTurnUpdate(const AgentName &a, const updates &u) { std::string PrismModulesPrinter::printSlipperyTurnUpdate(const AgentName &a, const updates &u) {
@ -468,21 +468,21 @@ namespace prism {
void PrismModulesPrinter::printFaultyMovementModule(const AgentName &a) { void PrismModulesPrinter::printFaultyMovementModule(const AgentName &a) {
os << "\nmodule " << a << "FaultyBehaviour" << std::endl; os << "\nmodule " << a << "FaultyBehaviour" << std::endl;
os << "\tpreviousAction" << a << " : [-1..2] init -1;\n";
os << " previousAction" << a << " : [-1..2] init -1;\n";
for(const auto [actionId, actionName] : agentNameActionMap.at(a)) { for(const auto [actionId, actionName] : agentNameActionMap.at(a)) {
os << "\t" << actionName << faultyBehaviourGuard(a, actionId) << " -> " << faultyBehaviourUpdate(a, actionId) << ";\n";
os << " " << actionName << faultyBehaviourGuard(a, actionId) << " -> " << faultyBehaviourUpdate(a, actionId) << ";\n";
} }
os << "endmodule\n\n"; os << "endmodule\n\n";
} }
void PrismModulesPrinter::printMoveModule() { void PrismModulesPrinter::printMoveModule() {
os << "\nmodule " << "Arbiter" << std::endl; os << "\nmodule " << "Arbiter" << std::endl;
os << "\tclock : [0.." << agentIndexMap.size() - 1 << "] init 0;\n";
os << " clock : [0.." << agentIndexMap.size() - 1 << "] init 0;\n";
for(const auto [agentName, actions] : agentNameActionMap) { for(const auto [agentName, actions] : agentNameActionMap) {
for(const auto [actionId, actionName] : actions) { for(const auto [actionId, actionName] : actions) {
os << "\t" << actionName << " " << moveGuard(agentName) << " -> " << moveUpdate(agentName) << ";\n";
os << " " << actionName << " " << moveGuard(agentName) << " -> " << moveUpdate(agentName) << ";\n";
} }
} }
os << "endmodule\n\n"; os << "endmodule\n\n";
@ -499,7 +499,7 @@ namespace prism {
} }
void PrismModulesPrinter::printDoneActions(const AgentName &agentName) { void PrismModulesPrinter::printDoneActions(const AgentName &agentName) {
os << "\t[" << agentName << "_done]" << moveGuard(agentName) << agentName << "IsInGoal | " << agentName << "IsInLava -> (" << agentName << "Done'=true);\n";
os << " [" << agentName << "_done]" << moveGuard(agentName) << agentName << "IsInGoal | " << agentName << "IsInLava -> (" << agentName << "Done'=true);\n";
} }
void PrismModulesPrinter::printPlayerStruct(const AgentName &agentName) { void PrismModulesPrinter::printPlayerStruct(const AgentName &agentName) {
@ -625,7 +625,7 @@ namespace prism {
} }
std::string PrismModulesPrinter::viewVariable(const AgentName &agentName, const size_t &agentDirection) const { std::string PrismModulesPrinter::viewVariable(const AgentName &agentName, const size_t &agentDirection) const {
return "view" + agentName + "=" + std::to_string(agentDirection) + " & ";
return "view" + agentName + "=" + std::to_string(agentDirection);
} }
bool PrismModulesPrinter::anyPortableObject() const { bool PrismModulesPrinter::anyPortableObject() 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 &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector<Configuration> config, const float probIntended, const float faultyProbability);
PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector<Configuration> config, const float probIntended, const float faultyProbability, const bool anyLava, const bool anyGoals);
std::ostream& print(); std::ostream& print();
@ -98,6 +98,9 @@ namespace prism {
cells keys; cells keys;
std::map<std::string, cells> slipperyTiles; std::map<std::string, cells> slipperyTiles;
const bool anyLava;
const bool anyGoals;
AgentNameAndPositionMap agentNameAndPositionMap; AgentNameAndPositionMap agentNameAndPositionMap;
std::map<AgentName, size_t> agentIndexMap; std::map<AgentName, size_t> agentIndexMap;
size_t numberOfPlayer; size_t numberOfPlayer;

Write Preview
Loading…
Cancel
Save