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

Merge pull request 'Towards First Stable Version' (#16) from modeltype into main 

Reviewed-on: #16
main
Stefan Pranger 4 months ago
parent
a57420a4ab 82849e5f67
commit
d69b4a41ca
8 changed files with 174 additions and 168 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 32
      main.cpp
  2. 42
      util/Grid.cpp
  3. 19
      util/Grid.h
  4. 73
      util/PrismFormulaPrinter.cpp
  5. 15
      util/PrismFormulaPrinter.h
  6. 141
      util/PrismModulesPrinter.cpp
  7. 10
      util/PrismModulesPrinter.h
  8. 10
      util/PrismPrinter.h

32
main.cpp
View File

@ -23,15 +23,15 @@ std::vector<std::string> 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<Probabi
if (start_pos != std::string::npos) {
auto end_pos = gridProperties.find('\n', start_pos);
auto value = gridProperties.substr(start_pos + identifier.length() + seperator.size(), end_pos - start_pos - identifier.length());
auto value = gridProperties.substr(start_pos + identifier.length() + seperator.size(), end_pos - start_pos - identifier.length());
prop = std::stod(value);
}
auto yaml_config_prop = std::find_if(configProperties.begin(), configProperties.end(), [&identifier](const Probability& obj) -> 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<Configuration> configurations;
std::vector<Probability> probabilities;
std::map<coordinates, float> 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;

42
util/Grid.cpp
View File

@ -3,19 +3,11 @@
#include <algorithm>
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<coordinates, float> &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<coordinates, float> &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<Configuration>& 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<Configuration>& configu
}
}
}
void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configuration ,const prism::ModelType& modelType) {
void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& 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<Configuration>& configurat
[](const std::map<AgentNameAndPosition::first_type,AgentNameAndPosition::second_type>::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<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);
if(agentNameAndPositionMap.size() > 1) formulas.printCollisionFormula(agentName);
formulas.printInitStruct();
modules.print();

19
util/Grid.h
View File

@ -6,29 +6,20 @@
#include <utility>
#include "MinigridGrammar.h"
#include "PrismPrinter.h"
#include "PrismModulesPrinter.h"
#include "PrismFormulaPrinter.h"
#include "ConfigYaml.h"
struct GridOptions {
std::vector<AgentName> agentsToBeConsidered;
std::vector<AgentName> agentsWithView;
std::vector<AgentName> agentsWithProbabilisticBehaviour;
std::vector<float> probabilitiesForActions;
bool enforceOneWays;
prism::ModelType getModelType() const;
};
class Grid {
public:
Grid(cells gridCells, cells background, const GridOptions &gridOptions, const std::map<coordinates, float> &stateRewards = {}, const float probIntended = 1.0, const float faultyProbability = 0);
Grid(cells gridCells, cells background, const std::map<coordinates, float> &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>& configuration, const prism::ModelType& modelType);
void printToPrism(std::ostream &os, std::vector<Configuration>& configuration);
void applyOverwrites(std::string& str, std::vector<Configuration>& configuration);
std::array<bool, 8> 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;

73
util/PrismFormulaPrinter.cpp
View File

@ -57,11 +57,12 @@ std::map<std::string, std::pair<int, int>> getRelativeSurroundingCells() {
}
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 &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), 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<int, int> 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();
}
}

15
util/PrismFormulaPrinter.h
View File

@ -21,7 +21,7 @@ std::map<std::string, std::pair<int, int>> getRelativeSurroundingCells();
namespace prism {
class PrismFormulaPrinter {
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 &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);
@ -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<ViewDirection, coordinates> &coordinates);
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 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<std::string, cells> 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<std::string> conditionalMovementRestrictions;
std::vector<std::string> portableObjects;
bool faulty;
};
}

141
util/PrismModulesPrinter.cpp
View File

@ -3,11 +3,6 @@
#include <map>
#include <string>
#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<std::string, cells> &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector<Configuration> 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<std::string, cells> &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector<Configuration> 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<std::string> &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<size_t> 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 {

10
util/PrismModulesPrinter.h
View File

@ -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<std::string, cells> &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector<Configuration> 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<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();
@ -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> configuration;
std::vector<ViewDirection> viewDirections = {0, 1, 2, 3};
std::map<ViewDirection, std::string> viewDirectionToString = {{0, "East"}, {1, "South"}, {2, "West"}, {3, "North"}};
std::vector<std::pair<size_t, std::string>> nonMovementActions = { {PICKUP, "pickup"}, {DROP, "drop"}, {TOGGLE, "toggle"}, {DONE, "done"} };
std::map<AgentName, std::set<std::pair<ActionId, std::string>>> agentNameActionMap;
};

10
util/PrismPrinter.h
View File

@ -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<std::string, coordinates> AgentNameAndPosition;

Write Preview
Loading…
Cancel
Save