From acf32fbb98c9ccae82c132bd4f915810fdc5bc45 Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Thu, 18 Jan 2024 21:16:31 +0100 Subject: [PATCH] added example for module --- examples/example_module.txt | 17 +++++++++++++++++ examples/example_module.yaml | 36 ++++++++++++++++++++++++++++++++++++ main.cpp | 6 ++++-- util/ConfigYaml.cpp | 9 +++++++-- util/Grid.cpp | 16 +++++++++------- util/Grid.h | 4 +++- 6 files changed, 76 insertions(+), 12 deletions(-) create mode 100644 examples/example_module.txt create mode 100644 examples/example_module.yaml diff --git a/examples/example_module.txt b/examples/example_module.txt new file mode 100644 index 0000000..8d0e2d7 --- /dev/null +++ b/examples/example_module.txt @@ -0,0 +1,17 @@ +WGWGWGWGWGWGWG +WGZY XRWG +WG WG +WG WG +WG WGWGWGWGWG +WG AYGGWG +WGWGWGWGWGWGWG +-------------- +WGWGWGWGWGWGWG +WG WG +WG WG +WG WG +WG WGWGWGWGWG +WG WG +WGWGWGWGWGWGWG +-------------- +-------------- \ No newline at end of file diff --git a/examples/example_module.yaml b/examples/example_module.yaml new file mode 100644 index 0000000..9005c10 --- /dev/null +++ b/examples/example_module.yaml @@ -0,0 +1,36 @@ +--- + +properties: + - property: "modeltype" + value: "mdp" + +formulas: + - formula: "YellowMovesNorth" + content: "(rowYellow=2 | rowYellow=3 | rowYellow=4) & colYellow=1 & viewYellow=3" + - formula: "YellowMovesSouth" + content: "(rowYellow=2 | rowYellow=3 | rowYellow=4) & colYellow=1 & viewYellow=1" + +modules: + - module: "Yellow" + overwrite: True + module_text: | + colYellow : [1..5] init 1; + rowYellow : [1..5] init 1; + viewYellow : [0..3] init 1; + YellowCarryingYellowBall : bool init false; + + [Yellow_turn_right] (!YellowMovesSouth & !YellowMovesNorth) -> 1.000000: (viewYellow'=mod(viewYellow+1,4)); + [Yellow_turn_left] (!YellowMovesSouth & !YellowMovesNorth) -> 1.000000: (viewYellow'=viewYellow-1); + [Yellow_turn_left] (!YellowMovesSouth & !YellowMovesNorth) -> 1.000000: (viewYellow'=3); + [Yellow_move_North] !YellowMovesSouth & viewYellow=3 & !YellowIsOnGoal & !YellowCannotMoveNorthWall & !YellowCannotMoveConditionally -> 1.000000: (rowYellow'=rowYellow-1); + [Yellow_move_East] !(YellowMovesNorth|YellowMovesSouth) & viewYellow=0 & !YellowIsOnGoal & !YellowCannotMoveEastWall & !YellowCannotMoveConditionally -> 1.000000: (colYellow'=colYellow+1); + [Yellow_move_South] !YellowMovesNorth & viewYellow=1 & !YellowIsOnGoal & !YellowCannotMoveSouthWall & !YellowCannotMoveConditionally -> 1.000000: (rowYellow'=rowYellow+1); + [Yellow_move_West] !(YellowMovesNorth|YellowMovesSouth) & viewYellow=2 & !YellowIsOnGoal & !YellowCannotMoveWestWall & !YellowCannotMoveConditionally -> 1.000000: (colYellow'=colYellow-1); + [Yellow_pickup_YellowBall] !YellowIsCarrying & YellowCannotMoveYellowBall -> (YellowCarryingYellowBall'=true); + [Yellow_drop_YellowBall_north] YellowCarryingYellowBall & viewYellow=3 & !YellowCannotMoveConditionally & !YellowCannotMoveNorthWall -> (YellowCarryingYellowBall'=false); + [Yellow_drop_YellowBall_west] YellowCarryingYellowBall & viewYellow=2 & !YellowCannotMoveConditionally & !YellowCannotMoveWestWall -> (YellowCarryingYellowBall'=false); + [Yellow_drop_YellowBall_south] YellowCarryingYellowBall & viewYellow=1 & !YellowCannotMoveConditionally & !YellowCannotMoveSouthWall -> (YellowCarryingYellowBall'=false); + [Yellow_drop_YellowBall_east] YellowCarryingYellowBall & viewYellow=0 & !YellowCannotMoveConditionally & !YellowCannotMoveEastWall -> (YellowCarryingYellowBall'=false); + + +... \ No newline at end of file diff --git a/main.cpp b/main.cpp index 1a74df5..8228deb 100644 --- a/main.cpp +++ b/main.cpp @@ -163,6 +163,8 @@ int main(int argc, char* argv[]) { setProbability(properties, parsed_properties, probTurnIntendedIdentifier, probTurnIntended); } if(ok) { + Grid grid(contentCells, backgroundCells, stateRewards, probIntended, faultyProbability); + auto modelTypeIter = std::find_if(parsed_properties.begin(), parsed_properties.end(), [](const Property& obj) -> bool {return obj.property == "modeltype";}); prism::ModelType modelType = prism::ModelType::MDP;; if (modelTypeIter != parsed_properties.end()) { @@ -171,9 +173,9 @@ int main(int argc, char* argv[]) { } else { modelType = prism::ModelType::MDP; } + + grid.setModelType(modelType); } - Grid grid(contentCells, backgroundCells, stateRewards, probIntended, faultyProbability, modelType); - diff --git a/util/ConfigYaml.cpp b/util/ConfigYaml.cpp index b558d32..986d19e 100644 --- a/util/ConfigYaml.cpp +++ b/util/ConfigYaml.cpp @@ -74,8 +74,13 @@ bool YAML::convert::decode(const YAML::Node& node, Module& rhs) { if (!node.Type() == NodeType::Map) { return false; } - rhs.commands_ = node["commands"].as>(); + + rhs.module_ = node["module"].as(); + + if (node["commands"]) { + rhs.commands_ = node["commands"].as>(); + } if (node["module_text"]) { rhs.module_text_ = node["module_text"].as(); @@ -267,7 +272,7 @@ YamlConfigParseResult YamlConfigParser::parseConfiguration() { } for (auto& module : modules) { if (module.overwrite_module) { - Configuration config = Configuration("module " + module.module_text_, "module " + module.module_, ConfigType::Module, true, module.module_, {0}, "endmodule"); + Configuration config = Configuration(module.module_text_, "module " + module.module_ + "\n", ConfigType::Module, true, module.module_, {0}, "endmodule"); configuration.push_back(config); continue; } diff --git a/util/Grid.cpp b/util/Grid.cpp index 012b905..2f294c4 100644 --- a/util/Grid.cpp +++ b/util/Grid.cpp @@ -3,7 +3,7 @@ #include -Grid::Grid(cells gridCells, cells background, const std::map &stateRewards, const float probIntended, const float faultyProbability, prism::ModelType mType) +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); @@ -61,10 +61,8 @@ Grid::Grid(cells gridCells, cells background, const std::map backgroundTiles.emplace(color, cellsOfColor); } } - - if(mType != prism::ModelType::MDP) { - modelType = mType; - } else if (adversaries.empty()) { + + if (adversaries.empty()) { modelType = prism::ModelType::MDP; } else { modelType = prism::ModelType::SMG; @@ -128,8 +126,7 @@ void Grid::applyOverwrites(std::string& str, std::vector& configu start_pos = std::distance(str.begin(), iter.begin()); size_t end_pos = str.find(end_identifier, start_pos); - - if (config.type_ == ConfigType::GuardOnly) { + if (config.type_ == ConfigType::GuardOnly || config.type_ == ConfigType::Module) { start_pos += search.length(); } else if (config.type_ == ConfigType::UpdateOnly) { start_pos = str.find("->", start_pos) + 2; @@ -192,3 +189,8 @@ void Grid::printToPrism(std::ostream& os, std::vector& configurat // modules.printConfiguration(os, configuration); //} } + +void Grid::setModelType(prism::ModelType type) +{ + modelType = type; +} \ No newline at end of file diff --git a/util/Grid.h b/util/Grid.h index 5c2f4d9..3d7f23d 100644 --- a/util/Grid.h +++ b/util/Grid.h @@ -13,7 +13,7 @@ class Grid { public: - Grid(cells gridCells, cells background, const std::map &stateRewards = {}, const float probIntended = 1.0, const float faultyProbability = 0, prism::ModelType mType = prism::ModelType::MDP); + Grid(cells gridCells, cells background, const std::map &stateRewards = {}, const float probIntended = 1.0, const float faultyProbability = 0); cells getGridCells(); @@ -22,6 +22,8 @@ class Grid { void printToPrism(std::ostream &os, std::vector& configuration); void applyOverwrites(std::string& str, std::vector& configuration); + void setModelType(prism::ModelType type); + std::array getWalkableDirOf8Neighborhood(cell c); friend std::ostream& operator<<(std::ostream& os, const Grid &grid);