Browse Source

switched to col and row instead of x and y

pull/9/head
sp 11 months ago
parent
commit
0a1f5ac405
  1. 10
      util/PrismFormulaPrinter.cpp
  2. 12
      util/PrismModulesPrinter.cpp

10
util/PrismFormulaPrinter.cpp

@ -20,26 +20,26 @@ std::string vectorToDisjunction(const std::vector<std::string> &formulae) {
} }
std::string cellToConjunction(const AgentName &agentName, const cell &c) { std::string cellToConjunction(const AgentName &agentName, const cell &c) {
return "x" + agentName + "=" + std::to_string(c.column) + "&y" + agentName + "=" + std::to_string(c.row);
return "col" + agentName + "=" + std::to_string(c.column) + "&row" + agentName + "=" + std::to_string(c.row);
} }
std::string cellToConjunctionWithOffset(const AgentName &agentName, const cell &c, const std::string &xOffset, const std::string &yOffset){ std::string cellToConjunctionWithOffset(const AgentName &agentName, const cell &c, const std::string &xOffset, const std::string &yOffset){
return "x" + agentName + xOffset + "=" + std::to_string(c.column) + "&y" + agentName + yOffset + "=" + std::to_string(c.row);
return "col" + agentName + xOffset + "=" + std::to_string(c.column) + "&row" + agentName + yOffset + "=" + std::to_string(c.row);
} }
std::string coordinatesToConjunction(const AgentName &agentName, const coordinates &c, const ViewDirection viewDirection) { std::string coordinatesToConjunction(const AgentName &agentName, const coordinates &c, const ViewDirection viewDirection) {
return "x" + agentName + "=" + std::to_string(c.first) + "&y" + agentName + "=" + std::to_string(c.second) + "&view" + agentName + "=" + std::to_string(viewDirection);
return "col" + agentName + "=" + std::to_string(c.first) + "&row" + agentName + "=" + std::to_string(c.second) + "&view" + agentName + "=" + std::to_string(viewDirection);
} }
std::string objectPositionToConjunction(const AgentName &agentName, const std::string &identifier, const std::pair<int, int> &relativePosition) { std::string objectPositionToConjunction(const AgentName &agentName, const std::string &identifier, const std::pair<int, int> &relativePosition) {
std::string xOffset = oneOffToString(relativePosition.first); std::string xOffset = oneOffToString(relativePosition.first);
std::string yOffset = oneOffToString(relativePosition.second); std::string yOffset = oneOffToString(relativePosition.second);
return "x" + agentName + xOffset + "=x" + identifier + "&y" + agentName + yOffset + "=y" + identifier;
return "col" + agentName + xOffset + "=col" + identifier + "&row" + agentName + yOffset + "=row" + identifier;
} }
std::string objectPositionToConjunction(const AgentName &agentName, const std::string &identifier, const std::pair<int, int> &relativePosition, const ViewDirection viewDirection) { std::string objectPositionToConjunction(const AgentName &agentName, const std::string &identifier, const std::pair<int, int> &relativePosition, const ViewDirection viewDirection) {
std::string xOffset = oneOffToString(relativePosition.first); std::string xOffset = oneOffToString(relativePosition.first);
std::string yOffset = oneOffToString(relativePosition.second); std::string yOffset = oneOffToString(relativePosition.second);
return "x" + agentName + xOffset + "=x" + identifier + "&y" + agentName + yOffset + "=y" + identifier + "&view" + agentName + "=" + std::to_string(viewDirection);
return "col" + agentName + xOffset + "=col" + identifier + "&row" + agentName + yOffset + "=row" + identifier + "&view" + agentName + "=" + std::to_string(viewDirection);
} }
std::map<ViewDirection, coordinates> getAdjacentCells(const cell &c) { std::map<ViewDirection, coordinates> getAdjacentCells(const cell &c) {

12
util/PrismModulesPrinter.cpp

@ -9,10 +9,10 @@
#define FORWARD 2 #define FORWARD 2
std::string northUpdate(const AgentName &a) { return "(y"+a+"'=y"+a+"-1)"; }
std::string southUpdate(const AgentName &a) { return "(y"+a+"'=y"+a+"+1)"; }
std::string eastUpdate(const AgentName &a) { return "(x"+a+"'=x"+a+"+1)"; }
std::string westUpdate(const AgentName &a) { return "(x"+a+"'=x"+a+"-1)"; }
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)"; }
namespace prism { namespace prism {
@ -167,8 +167,8 @@ namespace prism {
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 << "\tx" << agentName << " : [1.." << maxBoundaries.second << "] init " << initialPosition.second << ";\n";
os << "\ty" << agentName << " : [1.." << maxBoundaries.first << "] init " << initialPosition.first << ";\n";
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 << "\tview" << agentName << " : [0..3] init 1;\n";
printTurnActionsForRobot(agentName); printTurnActionsForRobot(agentName);

Loading…
Cancel
Save