diff --git a/main.cpp b/main.cpp index 2760259..012f2e6 100644 --- a/main.cpp +++ b/main.cpp @@ -23,15 +23,15 @@ std::vector parseCommaSeparatedString(std::string const& str) { struct printer { - typedef boost::spirit::utf8_string string; + typedef boost::spirit::utf8_string string; - void element(string const& tag, string const& value, int depth) const { - for (int i = 0; i < (depth*4); ++i) std::cout << ' '; + void element(string const& tag, string const& value, int depth) const { + for (int i = 0; i < (depth*4); ++i) std::cout << ' '; - std::cout << "tag: " << tag; - if (value != "") std::cout << ", value: " << value; - std::cout << std::endl; - } + std::cout << "tag: " << tag; + if (value != "") std::cout << ", value: " << value; + std::cout << std::endl; + } }; void print_info(boost::spirit::info const& what) { @@ -48,14 +48,14 @@ void setProbability(const std::string& gridProperties, const std::vector bool {return obj.probability_ == identifier;} ); if (yaml_config_prop != configProperties.end()) { - prop = (*yaml_config_prop).value_; + prop = (*yaml_config_prop).value_; } } @@ -83,7 +83,6 @@ int main(int argc, char* argv[]) { return EXIT_FAILURE; } - GridOptions gridOptions = { {}, {} }; std::fstream file {outputFilename->value(0), file.trunc | file.out}; std::fstream infile {inputFilename->value(0), infile.in}; std::string line, content, background, rewards, properties; @@ -130,9 +129,9 @@ int main(int argc, char* argv[]) { std::vector configurations; std::vector probabilities; std::map stateRewards; - float faultyProbability = 0.1; - float probIntended = 0.9; - float probTurnIntended = 1; + float faultyProbability = 0.0; + float probIntended = 1.0; + float probTurnIntended = 1.0; try { bool ok = phrase_parse(contentIter, contentLast, contentParser, qi::space, contentCells); @@ -164,12 +163,11 @@ int main(int argc, char* argv[]) { setProbability(properties, probabilities, probTurnIntendedIdentifier, probTurnIntended); } if(ok) { - Grid grid(contentCells, backgroundCells, gridOptions, stateRewards, probIntended, faultyProbability); + Grid grid(contentCells, backgroundCells, stateRewards, probIntended, faultyProbability); - // grid.printToPrism(std::cout, configurations , gridOptions.getModelType()); + //grid.printToPrism(std::cout, configurations); std::stringstream ss; - // grid.printToPrism(file, configurations ,prism::ModelType::MDP); - grid.printToPrism(ss, configurations , gridOptions.getModelType()); + grid.printToPrism(ss, configurations); std::string str = ss.str(); grid.applyOverwrites(str, configurations); file << str; diff --git a/util/Grid.cpp b/util/Grid.cpp index f9ebdac..8f83703 100644 --- a/util/Grid.cpp +++ b/util/Grid.cpp @@ -3,19 +3,11 @@ #include -prism::ModelType GridOptions::getModelType() const -{ - if (agentsWithView.size() > 1) { - return prism::ModelType::SMG; - } - return prism::ModelType::MDP; -} - -Grid::Grid(cells gridCells, cells background, const GridOptions &gridOptions, const std::map &stateRewards, const float probIntended, const float faultyProbability) - : allGridCells(gridCells), background(background), gridOptions(gridOptions), stateRewards(stateRewards), probIntended(probIntended), faultyProbability(faultyProbability) +Grid::Grid(cells gridCells, cells background, const std::map &stateRewards, const float probIntended, const float faultyProbability) + : allGridCells(gridCells), background(background), stateRewards(stateRewards), probIntended(probIntended), faultyProbability(faultyProbability) { cell max = allGridCells.at(allGridCells.size() - 1); - maxBoundaries = std::make_pair(max.row - 1, max.column - 1); + maxBoundaries = std::make_pair(max.column - 1, max.row - 1); std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(walls), [](cell c) { return c.type == Type::Wall; }); std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(lava), [](cell c) { return c.type == Type::Lava; }); std::copy_if(gridCells.begin(), gridCells.end(), std::back_inserter(floor), [](cell c) { return c.type == Type::Floor; }); // TODO CHECK IF ALL AGENTS ARE ADDED TO FLOOR @@ -38,7 +30,6 @@ Grid::Grid(cells gridCells, cells background, const GridOptions &gridOptions, co std::string color = adversary.getColor(); color.at(0) = std::toupper(color.at(0)); try { - if(gridOptions.agentsToBeConsidered.size() != 0 && std::find(gridOptions.agentsToBeConsidered.begin(), gridOptions.agentsToBeConsidered.end(), color) == gridOptions.agentsToBeConsidered.end()) continue; auto success = agentNameAndPositionMap.insert({ color, adversary.getCoordinates() }); floor.push_back(adversary); if(!success.second) { @@ -70,6 +61,12 @@ Grid::Grid(cells gridCells, cells background, const GridOptions &gridOptions, co backgroundTiles.emplace(color, cellsOfColor); } } + + if(adversaries.empty()) { + modelType = prism::ModelType::MDP; + } else { + modelType = prism::ModelType::SMG; + } } std::ostream& operator<<(std::ostream& os, const Grid& grid) { @@ -106,7 +103,7 @@ void Grid::applyOverwrites(std::string& str, std::vector& configu } for (auto& index : config.indexes_) { size_t start_pos; - std::string search; + std::string search; if (config.type_ == ConfigType::Formula) { search = "formula " + config.identifier_; @@ -130,9 +127,8 @@ void Grid::applyOverwrites(std::string& str, std::vector& configu } } } -void Grid::printToPrism(std::ostream& os, std::vector& configuration ,const prism::ModelType& modelType) { +void Grid::printToPrism(std::ostream& os, std::vector& configuration) { cells northRestriction, eastRestriction, southRestriction, westRestriction; - cells walkable = floor; walkable.insert(walkable.end(), goals.begin(), goals.end()); walkable.insert(walkable.end(), boxes.begin(), boxes.end()); @@ -158,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::PrismModulesPrinter modules(os, modelType, maxBoundaries, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, agentNameAndPositionMap, configuration, probIntended, faultyProbability, !lava.empty(), !goals.empty()); + prism::PrismFormulaPrinter formulas(os, wallRestrictions, walls, lockedDoors, unlockedDoors, keys, slipperyTiles, lava, goals, agentNameAndPositionMap, faultyProbability > 0.0); + prism::PrismModulesPrinter modules(os, modelType, maxBoundaries, 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); + if(agentNameAndPositionMap.size() > 1) formulas.printCollisionFormula(agentName); + formulas.printInitStruct(); + modules.print(); diff --git a/util/Grid.h b/util/Grid.h index eb95437..da593ba 100644 --- a/util/Grid.h +++ b/util/Grid.h @@ -6,29 +6,20 @@ #include #include "MinigridGrammar.h" +#include "PrismPrinter.h" #include "PrismModulesPrinter.h" #include "PrismFormulaPrinter.h" #include "ConfigYaml.h" -struct GridOptions { - std::vector agentsToBeConsidered; - std::vector agentsWithView; - std::vector agentsWithProbabilisticBehaviour; - std::vector probabilitiesForActions; - bool enforceOneWays; - - prism::ModelType getModelType() const; -}; - class Grid { public: - Grid(cells gridCells, cells background, const GridOptions &gridOptions, const std::map &stateRewards = {}, const float probIntended = 1.0, const float faultyProbability = 0); + Grid(cells gridCells, cells background, const std::map &stateRewards = {}, const float probIntended = 1.0, const float faultyProbability = 0); cells getGridCells(); bool isBlocked(coordinates p); bool isWall(coordinates p); - void printToPrism(std::ostream &os, std::vector& configuration, const prism::ModelType& modelType); + void printToPrism(std::ostream &os, std::vector& configuration); void applyOverwrites(std::string& str, std::vector& configuration); std::array getWalkableDirOf8Neighborhood(cell c); @@ -36,12 +27,12 @@ class Grid { friend std::ostream& operator<<(std::ostream& os, const Grid &grid); private: - GridOptions gridOptions; - cells allGridCells; cells background; coordinates maxBoundaries; + prism::ModelType modelType; + cell agent; cells adversaries; AgentNameAndPositionMap agentNameAndPositionMap; diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp index 1317fe3..bbb9a0c 100644 --- a/util/PrismFormulaPrinter.cpp +++ b/util/PrismFormulaPrinter.cpp @@ -57,11 +57,12 @@ 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 &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), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), lava(lava), goals(goals), agentNameAndPositionMap(agentNameAndPositionMap), faulty(faulty) { } void PrismFormulaPrinter::print(const AgentName &agentName) { + conditionalMovementRestrictions.clear(); for(const auto& [direction, cells] : restrictions) { printRestrictionFormula(agentName, direction, cells); } @@ -82,21 +83,10 @@ namespace prism { if(!lava.empty()) printIsOnFormula(agentName, "Lava", lava); if(!goals.empty()) printIsOnFormula(agentName, "Goal", goals); - for(const auto& ball : balls) { - std::string identifier = capitalize(ball.getColor()) + ball.getType(); - printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp"); - portableObjects.push_back(agentName + "Carrying" + identifier); - } - - for(const auto& box : boxes) { - std::string identifier = capitalize(box.getColor()) + box.getType(); - printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp"); - portableObjects.push_back(agentName + "Carrying" + identifier); - } for(const auto& key : keys) { std::string identifier = capitalize(key.getColor()) + key.getType(); - printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp"); + printRelativeIsInFrontOfFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp"); portableObjects.push_back(agentName + "Carrying" + identifier); } @@ -135,30 +125,57 @@ namespace prism { conditionalMovementRestrictions.push_back(agentName + "CannotMove" + reason); } - void PrismFormulaPrinter::printRelativeRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::string &condition) { - os << buildFormula(agentName + "CannotMove" + reason, "(" + buildDisjunction(agentName, reason) + ") & " + condition); - conditionalMovementRestrictions.push_back(agentName + "CannotMove" + reason); + void PrismFormulaPrinter::printRelativeIsInFrontOfFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::string &condition) { + os << buildFormula(agentName + "IsInFrontOf" + reason, "(" + buildDisjunction(agentName, reason) + ") & " + condition); } void PrismFormulaPrinter::printSlipRestrictionFormula(const AgentName &agentName, const std::string &direction) { std::pair slipCell = getRelativeSurroundingCells().at(direction); bool semicolon = anyPortableObject() ? false : true; os << buildFormula(agentName + "CannotSlip" + direction, buildDisjunction(agentName, walls, slipCell), semicolon); - for(auto const key : keys) { - std::string identifier = capitalize(key.getColor()) + key.getType(); - os << " | " << objectPositionToConjunction(agentName, identifier, slipCell); + 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(); } - for(auto const ball : balls) { - std::string identifier = capitalize(ball.getColor()) + ball.getType(); - os << " | " << objectPositionToConjunction(agentName, identifier, slipCell); + } + + void PrismFormulaPrinter::printCollisionLabel() { + if(!agentNameAndPositionMap.empty()) { + os << "label \"collision\" = collision;\n"; } - for(auto const box : boxes) { - std::string identifier = capitalize(box.getColor()) + box.getType(); - os << " | " << objectPositionToConjunction(agentName, identifier, slipCell); + } + + 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 << ")"; } - if(!semicolon) os << ";\n"; + 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)+"&"+identifier+"PickedUp=false) "; + } + 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": ""); } @@ -215,6 +232,6 @@ namespace prism { return !slipperyTiles.at("North").empty() || !slipperyTiles.at("East").empty() || !slipperyTiles.at("South").empty() || !slipperyTiles.at("West").empty(); } bool PrismFormulaPrinter::anyPortableObject() const { - return !keys.empty() || !boxes.empty() || !balls.empty(); + return !keys.empty(); } } diff --git a/util/PrismFormulaPrinter.h b/util/PrismFormulaPrinter.h index f1def2d..e0c5a62 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 &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); @@ -29,8 +29,13 @@ namespace prism { void printIsOnFormula(const AgentName &agentName, const std::string &type, const cells &grid_cells, const std::string &direction = ""); void printIsNextToFormula(const AgentName &agentName, const std::string &type, const std::map &coordinates); 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 printRelativeIsInFrontOfFormulaWithCondition(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); @@ -46,8 +51,6 @@ namespace prism { std::ostream &os; std::map restrictions; cells walls; - cells boxes; - cells balls; cells lockedDoors; cells unlockedDoors; cells keys; @@ -55,7 +58,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 f360cbc..01c8431 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -3,11 +3,6 @@ #include #include -#define NOFAULT -1 -#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)"; } @@ -16,8 +11,8 @@ std::string westUpdate(const AgentName &a) { return "(col"+a+"'=col"+a+"-1)"; } namespace prism { - 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 std::map &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector config, const float probIntended, const float faultyProbability, const bool anyLava, const bool anyGoals) - : os(os), modelType(modelType), maxBoundaries(maxBoundaries), boxes(boxes), balls(balls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), agentNameAndPositionMap(agentNameAndPositionMap), configuration(config), probIntended(probIntended), faultyProbability(faultyProbability), anyLava(anyLava), anyGoals(anyGoals) { + PrismModulesPrinter::PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector config, const float probIntended, const float faultyProbability, const bool anyLava, const bool anyGoals) + : os(os), modelType(modelType), maxBoundaries(maxBoundaries), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), agentNameAndPositionMap(agentNameAndPositionMap), configuration(config), probIntended(probIntended), faultyProbability(faultyProbability), anyLava(anyLava), anyGoals(anyGoals) { numberOfPlayer = agentNameAndPositionMap.size(); size_t index = 0; for(auto begin = agentNameAndPositionMap.begin(); begin != agentNameAndPositionMap.end(); begin++, index++) { @@ -45,12 +40,6 @@ namespace prism { for(const auto &key : keys) { printPortableObjectModule(key); } - for(const auto &ball : balls) { - printPortableObjectModule(ball); - } - for(const auto &box : boxes) { - printPortableObjectModule(box); - } for(const auto &door : unlockedDoors) { printDoorModule(door, true); } @@ -104,8 +93,8 @@ namespace prism { void PrismModulesPrinter::printPortableObjectModule(const cell &object) { std::string identifier = capitalize(object.getColor()) + object.getType(); os << "\nmodule " << identifier << std::endl; - os << " x" << identifier << " : [-1.." << maxBoundaries.second << "] init " << object.column << ";\n"; - os << " y" << identifier << " : [-1.." << maxBoundaries.first << "] 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"; @@ -115,28 +104,30 @@ namespace prism { os << "endmodule\n\n"; } - void PrismModulesPrinter::printPortableObjectActions(const std::string &agentName, const std::string &identifier) { + void PrismModulesPrinter::printPortableObjectActions(const std::string &agentName, const std::string &identifier, const bool canBeDroped) { std::string actionName = "[" + agentName + "_pickup_" + identifier + "]"; - agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); - os << " " << actionName << " true -> (x" << identifier << "'=-1) & (y" << identifier << "'=-1) & (" << identifier << "PickedUp'=true);\n"; - actionName = "[" + agentName + "_drop_" + identifier + "_north]"; - agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); - os << " " << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << ") & (y" << identifier << "'=y" << agentName << "-1) & (" << identifier << "PickedUp'=false);\n"; - actionName = "[" + agentName + "_drop_" + identifier + "_west]"; - agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); - os << " " << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << "-1) & (y" << identifier << "'=y" << agentName << ") & (" << identifier << "PickedUp'=false);\n"; - actionName = "[" + agentName + "_drop_" + identifier + "_south]"; - agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); - os << " " << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << ") & (y" << identifier << "'=y" << agentName << "+1) & (" << identifier << "PickedUp'=false);\n"; - actionName = "[" + agentName + "_drop_" + identifier + "_east]"; - agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); - os << " " << actionName << " " << " ttrue -> (x" << identifier << "'=x" << agentName << "+1) & (y" << identifier << "'=y" << agentName << ") & (" << identifier << "PickedUp'=false);\n"; + agentNameActionMap.at(agentName).insert({PICKUP, actionName}); + os << " " << actionName << " true -> (col" << identifier << "'=-1) & (row" << identifier << "'=-1) & (" << identifier << "PickedUp'=true);\n"; + if(canBeDroped) { + actionName = "[" + agentName + "_drop_" + identifier + "_north]"; + agentNameActionMap.at(agentName).insert({DROP, actionName}); + os << " " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << ") & (row" << identifier << "'=row" << agentName << "-1) & (" << identifier << "PickedUp'=false);\n"; + actionName = "[" + agentName + "_drop_" + identifier + "_west]"; + agentNameActionMap.at(agentName).insert({DROP, actionName}); + os << " " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << "-1) & (row" << identifier << "'=row" << agentName << ") & (" << identifier << "PickedUp'=false);\n"; + actionName = "[" + agentName + "_drop_" + identifier + "_south]"; + agentNameActionMap.at(agentName).insert({DROP, actionName}); + os << " " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << ") & (row" << identifier << "'=row" << agentName << "+1) & (" << identifier << "PickedUp'=false);\n"; + actionName = "[" + agentName + "_drop_" + identifier + "_east]"; + agentNameActionMap.at(agentName).insert({DROP, actionName}); + os << " " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << "+1) & (row" << identifier << "'=row" << agentName << ") & (" << identifier << "PickedUp'=false);\n"; + } } 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 +162,9 @@ namespace prism { void PrismModulesPrinter::printRobotModule(const AgentName &agentName, const coordinates &initialPosition) { os << "\nmodule " << agentName << std::endl; - 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"; + 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,34 +183,29 @@ 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"; - printPortableObjectActionsForRobot(agentName, identifier); - } + printNonMovementActionsForRobot(agentName); - for(const auto &box : boxes) { - std::string identifier = capitalize(box.getColor()) + box.getType(); - os << " " << agentName << "Carrying" << identifier << " : bool init false;\n"; - printPortableObjectActionsForRobot(agentName, identifier); - } os << "\n" << actionStream.str(); actionStream.str(std::string()); + + if(agentNameAndPositionMap.size() > 1 && agentName == "Agent") printDoneActions(agentName); os << "endmodule\n\n"; } - void PrismModulesPrinter::printPortableObjectActionsForRobot(const std::string &a, const std::string &i) { - 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"; + void PrismModulesPrinter::printPortableObjectActionsForRobot(const std::string &a, const std::string &i, const bool canBeDroped) { + actionStream << " [" << a << "_pickup_" << i << "] " << " !" << a << "IsCarrying & " << a << "IsInFrontOf" << i << " -> (" << a << "Carrying" << i << "'=true);\n"; + if(canBeDroped) { + 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"; + } } void PrismModulesPrinter::printUnlockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier) { @@ -276,13 +262,25 @@ namespace prism { std::string PrismModulesPrinter::printTurnGuard(const AgentName &a, const std::string &direction, const ActionId &actionId, const std::string &cond) { std::string actionName = "[" + a + "_turn_" + direction + "]"; agentNameActionMap.at(a).insert({actionId, actionName}); - return " " + actionName + " " + cond + " -> "; + std::string guard = " " + actionName; + if(slipperyBehaviour()) guard += " !" + a + "IsOnSlippery & "; + if(anyLava) guard += " !" + a + "IsOnLava &"; + guard += cond + " -> "; + return guard; } std::string PrismModulesPrinter::printTurnUpdate(const AgentName &a, const update &u, const ActionId &actionId) const { return updateToString(u) + ";\n"; } + void PrismModulesPrinter::printNonMovementActionsForRobot(const AgentName &agentName) { + for(auto const [actionId, action] : nonMovementActions) { + std::string actionName = "[" + agentName + "_" + action + "]"; + agentNameActionMap.at(agentName).insert({actionId, actionName}); + actionStream << " " << actionName << " true -> true;\n"; + } + } + void PrismModulesPrinter::printSlipperyMovementActionsForRobot(const AgentName &a) { if(!slipperyTiles.at("North").empty()) { printSlipperyMovementActionsForNorth(a); @@ -322,10 +320,8 @@ namespace prism { actionStream << printSlipperyMovementGuard(a, "North", 0, {"!"+a+"CannotSlipEast", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "North", { {1, eastUpdate(a) } }) << ";\n"; actionStream << printSlipperyMovementGuard(a, "North", 0, { a+"CannotSlipEast", a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "North", {}) << ";\n"; - actionStream << printSlipperyMovementGuard(a, "North", 1, {"!"+a+"CannotSlipSouth", "!"+a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, southUpdate(a) }, {1 - probIntended, northUpdate(a)} }) << ";\n"; - actionStream << printSlipperyMovementGuard(a, "North", 1, { a+"CannotSlipSouth", "!"+a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "North", { {1, northUpdate(a)} }) << ";\n"; - actionStream << printSlipperyMovementGuard(a, "North", 1, {"!"+a+"CannotSlipSouth", a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "North", { {1, southUpdate(a)} }) << ";\n"; - actionStream << printSlipperyMovementGuard(a, "North", 1, { a+"CannotSlipSouth", a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "North", {}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "North", 1, {"!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, southUpdate(a) }, {1 - probIntended, "true"} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "North", 1, { a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "North", { {1, "true"} }) << ";\n"; } void PrismModulesPrinter::printSlipperyMovementActionsForEast(const AgentName &a) { @@ -348,10 +344,8 @@ namespace prism { actionStream << printSlipperyMovementGuard(a, "East", 1, {"!"+a+"CannotSlipSouth", a+"CannotSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, southUpdate(a) } }) << ";\n"; actionStream << printSlipperyMovementGuard(a, "East", 1, { a+"CannotSlipSouth", a+"CannotSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", {}) << ";\n"; - actionStream << printSlipperyMovementGuard(a, "East", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a) }, {1 - probIntended, westUpdate(a)} }) << ";\n"; - actionStream << printSlipperyMovementGuard(a, "East", 2, { a+"CannotSlipWest", "!"+a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)} }) << ";\n"; - actionStream << printSlipperyMovementGuard(a, "East", 2, {"!"+a+"CannotSlipWest", a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {1, westUpdate(a)} }) << ";\n"; - actionStream << printSlipperyMovementGuard(a, "East", 2, { a+"CannotSlipWest", a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", {}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "East", 2, {"!"+a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a) }, {1 - probIntended, "true"} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "East", 2, { a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {1, "true"} }) << ";\n"; } void PrismModulesPrinter::printSlipperyMovementActionsForSouth(const AgentName &a) { @@ -374,10 +368,8 @@ namespace prism { actionStream << printSlipperyMovementGuard(a, "South", 0, {"!"+a+"CannotSlipEast", a+"CannotSlipSouthEast"}) << printSlipperyMovementUpdate(a, "South", { {1, eastUpdate(a) } }) << ";\n"; actionStream << printSlipperyMovementGuard(a, "South", 0, { a+"CannotSlipEast", a+"CannotSlipSouthEast"}) << printSlipperyMovementUpdate(a, "South", {}) << ";\n"; - actionStream << printSlipperyMovementGuard(a, "South", 3, {"!"+a+"CannotSlipSouth", "!"+a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a) }, {1 - probIntended, northUpdate(a)} }) << ";\n"; - actionStream << printSlipperyMovementGuard(a, "South", 3, { a+"CannotSlipSouth", "!"+a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "South", { {1, northUpdate(a)} }) << ";\n"; - actionStream << printSlipperyMovementGuard(a, "South", 3, {"!"+a+"CannotSlipSouth", a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "South", { {1, southUpdate(a)} }) << ";\n"; - actionStream << printSlipperyMovementGuard(a, "South", 3, { a+"CannotSlipSouth", a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "South", {}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "South", 3, {"!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, northUpdate(a) }, {1 - probIntended, "true"} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "South", 3, { a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "South", { {1, "true"} }) << ";\n"; } void PrismModulesPrinter::printSlipperyMovementActionsForWest(const AgentName &a) { @@ -400,10 +392,8 @@ namespace prism { actionStream << printSlipperyMovementGuard(a, "West", 1, {"!"+a+"CannotSlipSouth", a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, southUpdate(a) } }) << ";\n"; actionStream << printSlipperyMovementGuard(a, "West", 1, { a+"CannotSlipSouth", a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", {}) << ";\n"; - actionStream << printSlipperyMovementGuard(a, "West", 0, {"!"+a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a) }, {1 - probIntended, eastUpdate(a)} }) << ";\n"; - actionStream << printSlipperyMovementGuard(a, "West", 0, { a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)} }) << ";\n"; - actionStream << printSlipperyMovementGuard(a, "West", 0, {"!"+a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {1, eastUpdate(a)} }) << ";\n"; - actionStream << printSlipperyMovementGuard(a, "West", 0, { a+"CannotSlipEast", a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", {}) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "West", 0, {"!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a) }, {1 - probIntended, "true"} }) << ";\n"; + actionStream << printSlipperyMovementGuard(a, "West", 0, { a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", {{1, "true"}}) << ";\n"; } void PrismModulesPrinter::printSlipperyTurnActionsForNorth(const AgentName &a) { @@ -459,7 +449,7 @@ namespace prism { std::string PrismModulesPrinter::printSlipperyTurnGuard(const AgentName &a, const std::string &direction, const ActionId &actionId, const std::vector &guards, const std::string &cond) { std::string actionName = "[" + a + "_turn_" + direction + "]"; agentNameActionMap.at(a).insert({actionId, actionName}); - return " " + actionName + " " + buildConjunction(a, guards) + " & " + cond + " -> "; + return " " + actionName + " " + a + "IsOnSlippery & " + buildConjunction(a, guards) + " & " + cond + " -> "; } std::string PrismModulesPrinter::printSlipperyTurnUpdate(const AgentName &a, const updates &u) { @@ -468,9 +458,11 @@ namespace prism { void PrismModulesPrinter::printFaultyMovementModule(const AgentName &a) { os << "\nmodule " << a << "FaultyBehaviour" << std::endl; - os << " previousAction" << a << " : [-1..2] init -1;\n"; + os << " previousAction" << a << " : [0.." + std::to_string(NOFAULT) + "];\n"; + std::set exclude = {PICKUP, DROP, TOGGLE, DONE}; for(const auto [actionId, actionName] : agentNameActionMap.at(a)) { + if(exclude.count(actionId) > 0) continue; os << " " << actionName << faultyBehaviourGuard(a, actionId) << " -> " << faultyBehaviourUpdate(a, actionId) << ";\n"; } os << "endmodule\n\n"; @@ -478,7 +470,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) { @@ -499,7 +491,7 @@ namespace prism { } void PrismModulesPrinter::printDoneActions(const AgentName &agentName) { - os << " [" << agentName << "_done]" << moveGuard(agentName) << agentName << "IsInGoal | " << agentName << "IsInLava -> (" << agentName << "Done'=true);\n"; + os << " [" << agentName << "_on_goal]" << agentName << "IsOnGoal & clock=0 -> true;\n"; } void PrismModulesPrinter::printPlayerStruct(const AgentName &agentName) { @@ -510,6 +502,7 @@ namespace prism { else os << ", "; os << actionName; } + if(agentName == "Agent") os << ", [Agent_on_goal]"; os << "\nendplayer\n"; } @@ -629,7 +622,7 @@ namespace prism { } bool PrismModulesPrinter::anyPortableObject() const { - return !keys.empty() || !boxes.empty() || !balls.empty(); + return !keys.empty(); } bool PrismModulesPrinter::faultyBehaviour() const { diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h index c0d192a..618833a 100644 --- a/util/PrismModulesPrinter.h +++ b/util/PrismModulesPrinter.h @@ -16,7 +16,7 @@ std::string westUpdate(const AgentName &a); namespace prism { class PrismModulesPrinter { 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 &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector config, const float probIntended, const float faultyProbability, const bool anyLava, const bool anyGoals); + PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector config, const float probIntended, const float faultyProbability, const bool anyLava, const bool anyGoals); std::ostream& print(); @@ -26,18 +26,19 @@ namespace prism { bool isGame() const; private: void printPortableObjectModule(const cell &object); - void printPortableObjectActions(const std::string &agentName, const std::string &identifier); + void printPortableObjectActions(const std::string &agentName, const std::string &identifier, const bool canBeDroped = false); 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 printPortableObjectActionsForRobot(const std::string &agentName, const std::string &identifier, const bool canBeDroped = false); void printUnlockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier); void printLockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier, const std::string &key); void printMovementActionsForRobot(const std::string &a); void printTurnActionsForRobot(const std::string &a); + void printNonMovementActionsForRobot(const AgentName &agentName); void printSlipperyMovementActionsForRobot(const AgentName &a); void printSlipperyMovementActionsForNorth(const AgentName &a); void printSlipperyMovementActionsForEast(const AgentName &a); @@ -91,8 +92,6 @@ namespace prism { ModelType const &modelType; coordinates const &maxBoundaries; AgentName agentName; - cells boxes; - cells balls; cells lockedDoors; cells unlockedDoors; cells keys; @@ -109,6 +108,7 @@ namespace prism { std::vector configuration; std::vector viewDirections = {0, 1, 2, 3}; std::map viewDirectionToString = {{0, "East"}, {1, "South"}, {2, "West"}, {3, "North"}}; + std::vector> nonMovementActions = { {PICKUP, "pickup"}, {DROP, "drop"}, {TOGGLE, "toggle"}, {DONE, "done"} }; std::map>> agentNameActionMap; }; diff --git a/util/PrismPrinter.h b/util/PrismPrinter.h index 572cb40..c12b585 100644 --- a/util/PrismPrinter.h +++ b/util/PrismPrinter.h @@ -5,6 +5,16 @@ #include "cell.h" +#define NOFAULT 7 +#define LEFT 0 +#define RIGHT 1 +#define FORWARD 2 +#define PICKUP 3 +#define DROP 4 +#define TOGGLE 5 +#define DONE 6 + + typedef std::string AgentName; typedef size_t ViewDirection; typedef std::pair AgentNameAndPosition;