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

use init struct 

We do not know the view direction of all of the agents, hence we
iterate over all possible combinations as initial states
pull/16/head
sp 10 months ago
parent
4b8444f6aa
commit
ec5480f670
5 changed files with 81 additions and 29 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. 14
      util/Grid.cpp
  2. 52
      util/PrismFormulaPrinter.cpp
  3. 11
      util/PrismFormulaPrinter.h
  4. 27
      util/PrismModulesPrinter.cpp
  5. 6
      util/PrismPrinter.h

14
util/Grid.cpp
View File

@ -154,22 +154,16 @@ void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configurat
[](const std::map<AgentNameAndPosition::first_type,AgentNameAndPosition::second_type>::value_type &pair){return pair.first;}); [](const std::map<AgentNameAndPosition::first_type,AgentNameAndPosition::second_type>::value_type &pair){return pair.first;});
std::string agentName = agentNames.at(0); std::string agentName = agentNames.at(0);
prism::PrismFormulaPrinter formulas(os, wallRestrictions, walls, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, lava, goals);
prism::PrismFormulaPrinter formulas(os, wallRestrictions, walls, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, lava, goals, agentNameAndPositionMap, faultyProbability > 0.0);
prism::PrismModulesPrinter modules(os, modelType, maxBoundaries, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, agentNameAndPositionMap, configuration, probIntended, faultyProbability, !lava.empty(), !goals.empty()); prism::PrismModulesPrinter modules(os, modelType, maxBoundaries, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, agentNameAndPositionMap, configuration, probIntended, faultyProbability, !lava.empty(), !goals.empty());
modules.printModelType(modelType); modules.printModelType(modelType);
for(const auto &agentName : agentNames) { for(const auto &agentName : agentNames) {
formulas.print(agentName); formulas.print(agentName);
} }
//std::vector<std::string> constants {"const double prop_zero = 0/9;",
// "const double prop_intended = 6/9;",
// "const double prop_turn_intended = 6/9;",
// "const double prop_displacement = 3/9;",
// "const double prop_turn_displacement = 3/9;",
// "const int width = " + std::to_string(maxBoundaries.first) + ";",
// "const int height = " + std::to_string(maxBoundaries.second) + ";"
// };
//modules.printConstants(os, constants);
formulas.printCollisionFormula(agentName);
formulas.printInitStruct();
modules.print(); modules.print();

52
util/PrismFormulaPrinter.cpp
View File

@ -57,8 +57,8 @@ std::map<std::string, std::pair<int, int>> getRelativeSurroundingCells() {
} }
namespace prism { namespace prism {
PrismFormulaPrinter::PrismFormulaPrinter(std::ostream &os, const std::map<std::string, cells> &restrictions, const cells &walls, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const cells &lava, const cells &goals)
: os(os), restrictions(restrictions), walls(walls), boxes(boxes), balls(balls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), lava(lava), goals(goals)
PrismFormulaPrinter::PrismFormulaPrinter(std::ostream &os, const std::map<std::string, cells> &restrictions, const cells &walls, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const cells &lava, const cells &goals, const AgentNameAndPositionMap &agentNameAndPositionMap, const bool faulty)
: os(os), restrictions(restrictions), walls(walls), boxes(boxes), balls(balls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), lava(lava), goals(goals), agentNameAndPositionMap(agentNameAndPositionMap), faulty(faulty)
{ } { }
void PrismFormulaPrinter::print(const AgentName &agentName) { void PrismFormulaPrinter::print(const AgentName &agentName) {
@ -159,6 +159,54 @@ namespace prism {
if(!semicolon) os << ";\n"; if(!semicolon) os << ";\n";
} }
void PrismFormulaPrinter::printCollisionFormula(const AgentName &agentName) {
if(!agentNameAndPositionMap.empty()) {
os << "formula collision = ";
bool first = true;
for(auto const [name, coordinates] : agentNameAndPositionMap) {
if(name == agentName) continue;
if(first) first = false;
else os << " | ";
os << "(col"+agentName+"=col"+name+"&row"+agentName+"=row"+name+")";
}
os << ";\n";
printCollisionLabel();
}
}
void PrismFormulaPrinter::printCollisionLabel() {
if(!agentNameAndPositionMap.empty()) {
os << "label \"collision\" = collision;\n";
}
}
void PrismFormulaPrinter::printInitStruct() {
os << "init\n";
bool first = true;
for(auto const [a, coordinates] : agentNameAndPositionMap) {
if(first) first = false;
else os << " & ";
os << "(col"+a+"="+std::to_string(coordinates.first)+"&row"+a+"="+std::to_string(coordinates.second)+" & ";
os << "(view"+a+"=0|view"+a+"=1|view"+a+"=2|view"+a+"=3) ";
if(faulty) os << " & previousAction"+a+"="+std::to_string(NOFAULT);
os << ")";
}
for(auto const ball : balls) {
std::string identifier = capitalize(ball.getColor()) + ball.getType();
os << " & (col"+identifier+"="+std::to_string(ball.column)+"&row"+identifier+"="+std::to_string(ball.row)+") ";
}
for(auto const key : keys) {
std::string identifier = capitalize(key.getColor()) + key.getType();
os << " & (col"+identifier+"="+std::to_string(key.column)+"&row"+identifier+"="+std::to_string(key.row)+") ";
}
for(auto const box : boxes) {
std::string identifier = capitalize(box.getColor()) + box.getType();
os << " & (col"+identifier+"="+std::to_string(box.column)+"&row"+identifier+"="+std::to_string(box.row)+") ";
}
os << "endinit\n\n";
}
std::string PrismFormulaPrinter::buildFormula(const std::string &formulaName, const std::string &formula, const bool semicolon) { std::string PrismFormulaPrinter::buildFormula(const std::string &formulaName, const std::string &formula, const bool semicolon) {
return "formula " + formulaName + " = " + formula + (semicolon ? ";\n": ""); return "formula " + formulaName + " = " + formula + (semicolon ? ";\n": "");
} }

11
util/PrismFormulaPrinter.h
View File

@ -21,7 +21,7 @@ std::map<std::string, std::pair<int, int>> getRelativeSurroundingCells();
namespace prism { namespace prism {
class PrismFormulaPrinter { class PrismFormulaPrinter {
public: public:
PrismFormulaPrinter(std::ostream &os, const std::map<std::string, cells> &restrictions, const cells &walls, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const cells &lava, const cells &goals);
PrismFormulaPrinter(std::ostream &os, const std::map<std::string, cells> &restrictions, const cells &walls, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const cells &lava, const cells &goals, const AgentNameAndPositionMap &agentNameAndPositionMap, const bool faulty);
void print(const AgentName &agentName); void print(const AgentName &agentName);
@ -31,6 +31,11 @@ namespace prism {
void printRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::map<ViewDirection, coordinates> &coordinates, const std::string &condition); void printRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::map<ViewDirection, coordinates> &coordinates, const std::string &condition);
void printRelativeRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::string &condition); void printRelativeRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::string &condition);
void printSlipRestrictionFormula(const AgentName &agentName, const std::string &direction); void printSlipRestrictionFormula(const AgentName &agentName, const std::string &direction);
void printCollisionFormula(const std::string &agentName);
void printCollisionLabel();
void printInitStruct();
private: private:
std::string buildFormula(const std::string &formulaName, const std::string &formula, const bool semicolon = true); std::string buildFormula(const std::string &formulaName, const std::string &formula, const bool semicolon = true);
std::string buildLabel(const std::string &labelName, const std::string &label); std::string buildLabel(const std::string &labelName, const std::string &label);
@ -55,7 +60,11 @@ namespace prism {
cells lava; cells lava;
cells goals; cells goals;
AgentNameAndPositionMap agentNameAndPositionMap;
std::vector<std::string> conditionalMovementRestrictions; std::vector<std::string> conditionalMovementRestrictions;
std::vector<std::string> portableObjects; std::vector<std::string> portableObjects;
bool faulty;
}; };
} }

27
util/PrismModulesPrinter.cpp
View File

@ -3,11 +3,6 @@
#include <map> #include <map>
#include <string> #include <string>
#define NOFAULT 3
#define LEFT 0
#define RIGHT 1
#define FORWARD 2
std::string northUpdate(const AgentName &a) { return "(row"+a+"'=row"+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 southUpdate(const AgentName &a) { return "(row"+a+"'=row"+a+"+1)"; }
@ -104,8 +99,8 @@ 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 << " col" << identifier << " : [-1.." << maxBoundaries.first << "] init " << object.column << ";\n";
os << " row" << identifier << " : [-1.." << maxBoundaries.second << "] init " << object.row << ";\n";
os << " col" << identifier << " : [-1.." << maxBoundaries.first << "];\n";
os << " row" << identifier << " : [-1.." << maxBoundaries.second << "];\n";
os << " " << identifier << "PickedUp : bool;\n"; os << " " << identifier << "PickedUp : bool;\n";
os << "\n"; os << "\n";
@ -136,7 +131,7 @@ namespace prism {
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 << " " << identifier << "Open : bool init false;\n";
os << " " << identifier << "Open : bool;\n";
os << "\n"; os << "\n";
if(opened) { if(opened) {
@ -171,9 +166,9 @@ 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 << " col" << agentName << " : [1.." << maxBoundaries.first << "] init " << initialPosition.first << ";\n";
os << " row" << agentName << " : [1.." << maxBoundaries.second << "] init " << initialPosition.second << ";\n";
os << " view" << agentName << " : [0..3] init 1;\n";
os << " col" << agentName << " : [1.." << maxBoundaries.first << "];\n";
os << " row" << agentName << " : [1.." << maxBoundaries.second << "];\n";
os << " view" << agentName << " : [0..3];\n";
printTurnActionsForRobot(agentName); printTurnActionsForRobot(agentName);
printMovementActionsForRobot(agentName); printMovementActionsForRobot(agentName);
@ -192,19 +187,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 << " " << agentName << "Carrying" << identifier << " : bool init false;\n";
os << " " << agentName << "Carrying" << identifier << " : bool;\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 << " " << agentName << "Carrying" << identifier << " : bool init false;\n";
os << " " << agentName << "Carrying" << identifier << " : bool;\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 << " " << agentName << "Carrying" << identifier << " : bool init false;\n";
os << " " << agentName << "Carrying" << identifier << " : bool;\n";
printPortableObjectActionsForRobot(agentName, identifier); printPortableObjectActionsForRobot(agentName, identifier);
} }
@ -464,7 +459,7 @@ 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 << " previousAction" << a << " : [0.." + std::to_string(NOFAULT) + "] init " + std::to_string(NOFAULT) + ";\n";
os << " previousAction" << a << " : [0.." + std::to_string(NOFAULT) + "];\n";
for(const auto [actionId, actionName] : agentNameActionMap.at(a)) { for(const auto [actionId, actionName] : agentNameActionMap.at(a)) {
os << " " << actionName << faultyBehaviourGuard(a, actionId) << " -> " << faultyBehaviourUpdate(a, actionId) << ";\n"; os << " " << actionName << faultyBehaviourGuard(a, actionId) << " -> " << faultyBehaviourUpdate(a, actionId) << ";\n";
@ -474,7 +469,7 @@ namespace prism {
void PrismModulesPrinter::printMoveModule() { void PrismModulesPrinter::printMoveModule() {
os << "\nmodule " << "Arbiter" << std::endl; os << "\nmodule " << "Arbiter" << std::endl;
os << " clock : [0.." << agentIndexMap.size() - 1 << "] init 0;\n";
os << " clock : [0.." << agentIndexMap.size() - 1 << "];\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) {

6
util/PrismPrinter.h
View File

@ -5,6 +5,12 @@
#include "cell.h" #include "cell.h"
#define NOFAULT 3
#define LEFT 0
#define RIGHT 1
#define FORWARD 2
typedef std::string AgentName; typedef std::string AgentName;
typedef size_t ViewDirection; typedef size_t ViewDirection;
typedef std::pair<std::string, coordinates> AgentNameAndPosition; typedef std::pair<std::string, coordinates> AgentNameAndPosition;

Write Preview
Loading…
Cancel
Save