From ec5480f670ed1593a493e385ef27b484bcf542d2 Mon Sep 17 00:00:00 2001 From: sp Date: Thu, 18 Jan 2024 13:07:39 +0100 Subject: [PATCH] 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 --- util/Grid.cpp | 14 +++------- util/PrismFormulaPrinter.cpp | 52 ++++++++++++++++++++++++++++++++++-- util/PrismFormulaPrinter.h | 11 +++++++- util/PrismModulesPrinter.cpp | 27 ++++++++----------- util/PrismPrinter.h | 6 +++++ 5 files changed, 81 insertions(+), 29 deletions(-) diff --git a/util/Grid.cpp b/util/Grid.cpp index d87fcc0..0fcf24e 100644 --- a/util/Grid.cpp +++ b/util/Grid.cpp @@ -154,22 +154,16 @@ void Grid::printToPrism(std::ostream& os, std::vector& configurat [](const std::map::value_type &pair){return pair.first;}); 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()); modules.printModelType(modelType); for(const auto &agentName : agentNames) { formulas.print(agentName); } - //std::vector 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(); diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp index 1317fe3..29b4a07 100644 --- a/util/PrismFormulaPrinter.cpp +++ b/util/PrismFormulaPrinter.cpp @@ -57,8 +57,8 @@ std::map> getRelativeSurroundingCells() { } namespace prism { - PrismFormulaPrinter::PrismFormulaPrinter(std::ostream &os, const std::map &restrictions, const cells &walls, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map &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 &restrictions, const cells &walls, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map &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) { @@ -159,6 +159,54 @@ namespace prism { 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) { return "formula " + formulaName + " = " + formula + (semicolon ? ";\n": ""); } diff --git a/util/PrismFormulaPrinter.h b/util/PrismFormulaPrinter.h index f1def2d..8e24578 100644 --- a/util/PrismFormulaPrinter.h +++ b/util/PrismFormulaPrinter.h @@ -21,7 +21,7 @@ std::map> getRelativeSurroundingCells(); namespace prism { class PrismFormulaPrinter { public: - PrismFormulaPrinter(std::ostream &os, const std::map &restrictions, const cells &walls, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map &slipperyTiles, const cells &lava, const cells &goals); + PrismFormulaPrinter(std::ostream &os, const std::map &restrictions, const cells &walls, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map &slipperyTiles, const cells &lava, const cells &goals, const AgentNameAndPositionMap &agentNameAndPositionMap, const bool faulty); void print(const AgentName &agentName); @@ -31,6 +31,11 @@ namespace prism { void printRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::map &coordinates, 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 printCollisionFormula(const std::string &agentName); + void printCollisionLabel(); + + void printInitStruct(); private: 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); @@ -55,7 +60,11 @@ namespace prism { cells lava; cells goals; + AgentNameAndPositionMap agentNameAndPositionMap; + std::vector conditionalMovementRestrictions; std::vector portableObjects; + + bool faulty; }; } diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index cf91edc..a12353b 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -3,11 +3,6 @@ #include #include -#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 southUpdate(const AgentName &a) { return "(row"+a+"'=row"+a+"+1)"; } @@ -104,8 +99,8 @@ namespace prism { void PrismModulesPrinter::printPortableObjectModule(const cell &object) { std::string identifier = capitalize(object.getColor()) + object.getType(); 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 << "\n"; @@ -136,7 +131,7 @@ namespace prism { void PrismModulesPrinter::printDoorModule(const cell &door, const bool &opened) { std::string identifier = capitalize(door.getColor()) + door.getType(); os << "\nmodule " << identifier << std::endl; - os << " " << identifier << "Open : bool init false;\n"; + os << " " << identifier << "Open : bool;\n"; os << "\n"; if(opened) { @@ -171,9 +166,9 @@ namespace prism { void PrismModulesPrinter::printRobotModule(const AgentName &agentName, const coordinates &initialPosition) { 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); printMovementActionsForRobot(agentName); @@ -192,19 +187,19 @@ namespace prism { for(const auto &key : keys) { 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); } for(const auto &ball : balls) { 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); } for(const auto &box : boxes) { 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); } @@ -464,7 +459,7 @@ namespace prism { void PrismModulesPrinter::printFaultyMovementModule(const AgentName &a) { 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)) { os << " " << actionName << faultyBehaviourGuard(a, actionId) << " -> " << faultyBehaviourUpdate(a, actionId) << ";\n"; @@ -474,7 +469,7 @@ namespace prism { void PrismModulesPrinter::printMoveModule() { 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 [actionId, actionName] : actions) { diff --git a/util/PrismPrinter.h b/util/PrismPrinter.h index 572cb40..a75e9f1 100644 --- a/util/PrismPrinter.h +++ b/util/PrismPrinter.h @@ -5,6 +5,12 @@ #include "cell.h" +#define NOFAULT 3 +#define LEFT 0 +#define RIGHT 1 +#define FORWARD 2 + + typedef std::string AgentName; typedef size_t ViewDirection; typedef std::pair AgentNameAndPosition;