Browse Source

added example for module

overwrites
Thomas Knoll 10 months ago
committed by sp
parent
commit
acf32fbb98
  1. 17
      examples/example_module.txt
  2. 36
      examples/example_module.yaml
  3. 6
      main.cpp
  4. 9
      util/ConfigYaml.cpp
  5. 14
      util/Grid.cpp
  6. 4
      util/Grid.h

17
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
--------------
--------------

36
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);
...

6
main.cpp

@ -163,6 +163,8 @@ int main(int argc, char* argv[]) {
setProbability(properties, parsed_properties, probTurnIntendedIdentifier, probTurnIntended); setProbability(properties, parsed_properties, probTurnIntendedIdentifier, probTurnIntended);
} }
if(ok) { 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";}); 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;; prism::ModelType modelType = prism::ModelType::MDP;;
if (modelTypeIter != parsed_properties.end()) { if (modelTypeIter != parsed_properties.end()) {
@ -171,9 +173,9 @@ int main(int argc, char* argv[]) {
} else { } else {
modelType = prism::ModelType::MDP; modelType = prism::ModelType::MDP;
} }
}
Grid grid(contentCells, backgroundCells, stateRewards, probIntended, faultyProbability, modelType);
grid.setModelType(modelType);
}

9
util/ConfigYaml.cpp

@ -74,9 +74,14 @@ bool YAML::convert<Module>::decode(const YAML::Node& node, Module& rhs) {
if (!node.Type() == NodeType::Map) { if (!node.Type() == NodeType::Map) {
return false; return false;
} }
rhs.commands_ = node["commands"].as<std::vector<Command>>();
rhs.module_ = node["module"].as<std::string>(); rhs.module_ = node["module"].as<std::string>();
if (node["commands"]) {
rhs.commands_ = node["commands"].as<std::vector<Command>>();
}
if (node["module_text"]) { if (node["module_text"]) {
rhs.module_text_ = node["module_text"].as<std::string>(); rhs.module_text_ = node["module_text"].as<std::string>();
} }
@ -267,7 +272,7 @@ YamlConfigParseResult YamlConfigParser::parseConfiguration() {
} }
for (auto& module : modules) { for (auto& module : modules) {
if (module.overwrite_module) { 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); configuration.push_back(config);
continue; continue;
} }

14
util/Grid.cpp

@ -3,7 +3,7 @@
#include <algorithm> #include <algorithm>
Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float> &stateRewards, const float probIntended, const float faultyProbability, prism::ModelType mType)
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) : allGridCells(gridCells), background(background), stateRewards(stateRewards), probIntended(probIntended), faultyProbability(faultyProbability)
{ {
cell max = allGridCells.at(allGridCells.size() - 1); cell max = allGridCells.at(allGridCells.size() - 1);
@ -62,9 +62,7 @@ Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float>
} }
} }
if(mType != prism::ModelType::MDP) {
modelType = mType;
} else if (adversaries.empty()) {
if (adversaries.empty()) {
modelType = prism::ModelType::MDP; modelType = prism::ModelType::MDP;
} else { } else {
modelType = prism::ModelType::SMG; modelType = prism::ModelType::SMG;
@ -128,8 +126,7 @@ void Grid::applyOverwrites(std::string& str, std::vector<Configuration>& configu
start_pos = std::distance(str.begin(), iter.begin()); start_pos = std::distance(str.begin(), iter.begin());
size_t end_pos = str.find(end_identifier, start_pos); 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(); start_pos += search.length();
} else if (config.type_ == ConfigType::UpdateOnly) { } else if (config.type_ == ConfigType::UpdateOnly) {
start_pos = str.find("->", start_pos) + 2; start_pos = str.find("->", start_pos) + 2;
@ -192,3 +189,8 @@ void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configurat
// modules.printConfiguration(os, configuration); // modules.printConfiguration(os, configuration);
//} //}
} }
void Grid::setModelType(prism::ModelType type)
{
modelType = type;
}

4
util/Grid.h

@ -13,7 +13,7 @@
class Grid { class Grid {
public: public:
Grid(cells gridCells, cells background, const std::map<coordinates, float> &stateRewards = {}, const float probIntended = 1.0, const float faultyProbability = 0, prism::ModelType mType = prism::ModelType::MDP);
Grid(cells gridCells, cells background, const std::map<coordinates, float> &stateRewards = {}, const float probIntended = 1.0, const float faultyProbability = 0);
cells getGridCells(); cells getGridCells();
@ -22,6 +22,8 @@ class Grid {
void printToPrism(std::ostream &os, std::vector<Configuration>& configuration); void printToPrism(std::ostream &os, std::vector<Configuration>& configuration);
void applyOverwrites(std::string& str, std::vector<Configuration>& configuration); void applyOverwrites(std::string& str, std::vector<Configuration>& configuration);
void setModelType(prism::ModelType type);
std::array<bool, 8> getWalkableDirOf8Neighborhood(cell c); std::array<bool, 8> getWalkableDirOf8Neighborhood(cell c);
friend std::ostream& operator<<(std::ostream& os, const Grid &grid); friend std::ostream& operator<<(std::ostream& os, const Grid &grid);

Loading…
Cancel
Save