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

more overwrites

Thomas Knoll 10 months ago
parent
d9679da353
commit
7ac8c7e798
5 changed files with 71 additions and 40 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 28
      main.cpp
  2. 31
      util/ConfigYaml.cpp
  3. 31
      util/ConfigYaml.h
  4. 19
      util/Grid.cpp
  5. 2
      util/Grid.h

28
main.cpp
View File

@ -42,7 +42,7 @@ void print_info(boost::spirit::info const& what) {
boost::apply_visitor(walker, what.value); boost::apply_visitor(walker, what.value);
} }
void setProbability(const std::string& gridProperties, const std::vector<Probability> configProperties, const std::string& identifier, float& prop) {
void setProbability(const std::string& gridProperties, const std::vector<Property> configProperties, const std::string& identifier, float& prop) {
auto start_pos = gridProperties.find(identifier); auto start_pos = gridProperties.find(identifier);
std::string seperator = ";"; std::string seperator = ";";
@ -52,7 +52,7 @@ void setProbability(const std::string& gridProperties, const std::vector<Probabi
prop = std::stod(value); prop = std::stod(value);
} }
auto yaml_config_prop = std::find_if(configProperties.begin(), configProperties.end(), [&identifier](const Probability& obj) -> bool {return obj.probability_ == identifier;} );
auto yaml_config_prop = std::find_if(configProperties.begin(), configProperties.end(), [&identifier](const Property& obj) -> bool {return obj.property == identifier;} );
if (yaml_config_prop != configProperties.end()) { if (yaml_config_prop != configProperties.end()) {
prop = (*yaml_config_prop).value_; prop = (*yaml_config_prop).value_;
@ -127,7 +127,7 @@ int main(int argc, char* argv[]) {
cells contentCells; cells contentCells;
cells backgroundCells; cells backgroundCells;
std::vector<Configuration> configurations; std::vector<Configuration> configurations;
std::vector<Probability> probabilities;
std::vector<Property> parsed_properties;
std::map<coordinates, float> stateRewards; std::map<coordinates, float> stateRewards;
float faultyProbability = 0.0; float faultyProbability = 0.0;
float probIntended = 1.0; float probIntended = 1.0;
@ -142,7 +142,7 @@ int main(int argc, char* argv[]) {
YamlConfigParser parser(configFilename->value(0)); YamlConfigParser parser(configFilename->value(0));
auto parseResult = parser.parseConfiguration(); auto parseResult = parser.parseConfiguration();
configurations = parseResult.configurations_; configurations = parseResult.configurations_;
probabilities = parseResult.probabilities_;
parsed_properties = parseResult.properties_;
} }
boost::escaped_list_separator<char> seps('\\', ';', '\n'); boost::escaped_list_separator<char> seps('\\', ';', '\n');
@ -158,12 +158,24 @@ int main(int argc, char* argv[]) {
auto probForwardIntendedIdentifier = std::string("ProbForwardIntended"); auto probForwardIntendedIdentifier = std::string("ProbForwardIntended");
auto probTurnIntendedIdentifier = std::string("ProbTurnIntended"); auto probTurnIntendedIdentifier = std::string("ProbTurnIntended");
setProbability(properties, probabilities, faultProbabilityIdentifier, faultyProbability);
setProbability(properties, probabilities, probForwardIntendedIdentifier, probIntended);
setProbability(properties, probabilities, probTurnIntendedIdentifier, probTurnIntended);
setProbability(properties, parsed_properties, faultProbabilityIdentifier, faultyProbability);
setProbability(properties, parsed_properties, probForwardIntendedIdentifier, probIntended);
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";});
prism::ModelType modelType = prism::ModelType::MDP;;
if (modelTypeIter != parsed_properties.end()) {
if ((*modelTypeIter).value_str_ == "smg") {
modelType = prism::ModelType::SMG;
} else {
modelType = prism::ModelType::MDP;
}
}
Grid grid(contentCells, backgroundCells, stateRewards, probIntended, faultyProbability, modelType);
//grid.printToPrism(std::cout, configurations); //grid.printToPrism(std::cout, configurations);
std::stringstream ss; std::stringstream ss;

31
util/ConfigYaml.cpp
View File

@ -202,22 +202,27 @@ bool YAML::convert<Constant>::decode(const YAML::Node& node, Constant& rhs) {
return true; return true;
} }
YAML::Node YAML::convert<Probability>::encode(const Probability& rhs) {
YAML::Node YAML::convert<Property>::encode(const Property& rhs) {
YAML::Node node; YAML::Node node;
node.push_back(rhs.probability_);
node.push_back(rhs.property);
node.push_back(rhs.value_); node.push_back(rhs.value_);
return node; return node;
} }
bool YAML::convert<Probability>::decode(const YAML::Node& node, Probability& rhs) {
if (!node.IsDefined() || !node["probability"] || !node["value"]) {
bool YAML::convert<Property>::decode(const YAML::Node& node, Property& rhs) {
if (!node.IsDefined() || !node["property"] || !node["value"]) {
return false; return false;
} }
rhs.probability_ = node["probability"].as<std::string>();
rhs.value_ = node["value"].as<double>();
rhs.property = node["property"].as<std::string>();
try {
rhs.value_ = node["value"].as<double>();
}
catch(const std::exception& e) {
rhs.value_str_ = node["value"].as<std::string>();
}
return true; return true;
} }
@ -227,7 +232,7 @@ const std::string Configuration::overwrite_identifier_{"; // Overwritten through
YamlConfigParseResult YamlConfigParser::parseConfiguration() { YamlConfigParseResult YamlConfigParser::parseConfiguration() {
std::vector<Configuration> configuration; std::vector<Configuration> configuration;
std::vector<Probability> probabilities;
std::vector<Property> properties;
try { try {
YAML::Node config = YAML::LoadFile(file_); YAML::Node config = YAML::LoadFile(file_);
@ -250,8 +255,8 @@ YamlConfigParseResult YamlConfigParser::parseConfiguration() {
constants = config["constants"].as<std::vector<Constant>>(); constants = config["constants"].as<std::vector<Constant>>();
} }
if (config["probabilities"]) {
probabilities = config["probabilities"].as<std::vector<Probability>>();
if (config["properties"]) {
properties = config["properties"].as<std::vector<Property>>();
} }
for (auto& label : labels) { for (auto& label : labels) {
@ -262,16 +267,16 @@ YamlConfigParseResult YamlConfigParser::parseConfiguration() {
} }
for (auto& module : modules) { for (auto& module : modules) {
if (module.overwrite_module) { if (module.overwrite_module) {
Configuration config = Configuration(module.module_text_, module.module_, ConfigType::Module, true, module.module_, {0}, "endmodule");
Configuration config = Configuration("module " + module.module_text_, "module " + module.module_, ConfigType::Module, true, module.module_, {0}, "endmodule");
configuration.push_back(config); configuration.push_back(config);
continue; continue;
} }
for (auto& command : module.commands_) { for (auto& command : module.commands_) {
Configuration config; Configuration config;
if (!command.guard_.empty() && !command.action_.empty() && command.update_.empty()) { if (!command.guard_.empty() && !command.action_.empty() && command.update_.empty()) {
config = Configuration(" " + command.guard_, command.action_, ConfigType::Module, true, module.module_, command.indexes_, "->", false);
config = Configuration(" " + command.guard_, command.action_, ConfigType::GuardOnly, true, module.module_, command.indexes_, "->");
} else if (!command.update_.empty() && !command.action_.empty() && command.guard_.empty()) { } else if (!command.update_.empty() && !command.action_.empty() && command.guard_.empty()) {
config = Configuration( " " + command.update_, command.action_, ConfigType::Module, true, module.module_, command.indexes_, ";", false);
config = Configuration( " " + command.update_, command.action_, ConfigType::UpdateOnly, true, module.module_, command.indexes_, ";");
} else { } else {
config = Configuration(command.createExpression(), command.action_, ConfigType::Module, command.overwrite_, module.module_, command.indexes_); config = Configuration(command.createExpression(), command.action_, ConfigType::Module, command.overwrite_, module.module_, command.indexes_);
} }
@ -290,5 +295,5 @@ YamlConfigParseResult YamlConfigParser::parseConfiguration() {
std::cout << "while parsing configuration " << file_ << std::endl; std::cout << "while parsing configuration " << file_ << std::endl;
} }
return YamlConfigParseResult(configuration, probabilities);
return YamlConfigParseResult(configuration, properties);
} }

31
util/ConfigYaml.h
View File

@ -11,6 +11,8 @@ enum class ConfigType : char {
Label = 'L', Label = 'L',
Formula = 'F', Formula = 'F',
Module = 'M', Module = 'M',
UpdateOnly = 'U',
GuardOnly = 'G',
Constant = 'C' Constant = 'C'
}; };
@ -27,7 +29,6 @@ struct Configuration
ConfigType type_ {ConfigType::Label}; ConfigType type_ {ConfigType::Label};
bool overwrite_ {false}; bool overwrite_ {false};
bool include_identifier_for_overwrite_{true};
Configuration() = default; Configuration() = default;
Configuration(std::string expression Configuration(std::string expression
@ -36,8 +37,7 @@ struct Configuration
, bool overwrite = false , bool overwrite = false
, std::string module = "" , std::string module = ""
, std::vector<int> indexes = {0} , std::vector<int> indexes = {0}
, std::string end_identifier = {";"}
, bool include_identifier_for_overwrite = true) : expression_(expression), identifier_(identifier), type_(type), overwrite_(overwrite), module_{module}, indexes_(indexes), end_identifier_{end_identifier}, include_identifier_for_overwrite_{include_identifier_for_overwrite} {}
, std::string end_identifier = {";"}) : expression_(expression), identifier_(identifier), type_(type), overwrite_(overwrite), module_{module}, indexes_(indexes), end_identifier_{end_identifier} {}
~Configuration() = default; ~Configuration() = default;
Configuration(const Configuration&) = default; Configuration(const Configuration&) = default;
@ -48,15 +48,16 @@ struct Configuration
} }
}; };
struct Probability {
Probability() = default;
Probability(const Probability&) = default;
~Probability() = default;
struct Property {
Property() = default;
Property(const Property&) = default;
~Property() = default;
std::string probability_;
std::string property;
double value_; double value_;
std::string value_str_;
friend std::ostream& operator <<(std::ostream& os, const Probability& property);
friend std::ostream& operator <<(std::ostream& os, const Property& property);
}; };
struct Constant { struct Constant {
@ -156,20 +157,20 @@ struct YAML::convert<Constant> {
}; };
template<> template<>
struct YAML::convert<Probability> {
static YAML::Node encode(const Probability& rhs);
static bool decode(const YAML::Node& node, Probability& rhs);
struct YAML::convert<Property> {
static YAML::Node encode(const Property& rhs);
static bool decode(const YAML::Node& node, Property& rhs);
}; };
struct YamlConfigParseResult { struct YamlConfigParseResult {
YamlConfigParseResult(std::vector<Configuration> configurations, std::vector<Probability> probabilities)
: configurations_(configurations), probabilities_(probabilities) {}
YamlConfigParseResult(std::vector<Configuration> configurations, std::vector<Property> probabilities)
: configurations_(configurations), properties_(probabilities) {}
~YamlConfigParseResult() = default; ~YamlConfigParseResult() = default;
YamlConfigParseResult(const YamlConfigParseResult&) = default; YamlConfigParseResult(const YamlConfigParseResult&) = default;
std::vector<Configuration> configurations_; std::vector<Configuration> configurations_;
std::vector<Probability> probabilities_;
std::vector<Property> properties_;
}; };
struct YamlConfigParser { struct YamlConfigParser {

19
util/Grid.cpp
View File

@ -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)
Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float> &stateRewards, const float probIntended, const float faultyProbability, prism::ModelType mType)
: 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,7 +62,9 @@ Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float>
} }
} }
if(adversaries.empty()) {
if(mType != prism::ModelType::MDP) {
modelType = mType;
} else if (adversaries.empty()) {
modelType = prism::ModelType::MDP; modelType = prism::ModelType::MDP;
} else { } else {
modelType = prism::ModelType::SMG; modelType = prism::ModelType::SMG;
@ -111,14 +113,25 @@ void Grid::applyOverwrites(std::string& str, std::vector<Configuration>& configu
search = "label " + config.identifier_; search = "label " + config.identifier_;
} else if (config.type_ == ConfigType::Module) { } else if (config.type_ == ConfigType::Module) {
search = config.identifier_; search = config.identifier_;
} else if (config.type_ == ConfigType::UpdateOnly) {
search = config.identifier_;
} }
else if (config.type_ == ConfigType::Constant) { else if (config.type_ == ConfigType::Constant) {
search = config.identifier_; search = config.identifier_;
} }
auto iter = boost::find_nth(str, search, index); auto iter = boost::find_nth(str, search, index);
auto end_identifier = config.end_identifier_;
start_pos = std::distance(str.begin(), iter.begin()); start_pos = std::distance(str.begin(), iter.begin());
size_t end_pos = str.find(';', start_pos) + 1;
size_t end_pos = str.find(end_identifier, start_pos);
if (config.type_ == ConfigType::GuardOnly) {
start_pos += search.length();
} else if (config.type_ == ConfigType::UpdateOnly) {
start_pos = str.find("->", start_pos) + 2;
}
if (end_pos != std::string::npos && end_pos != 0) { if (end_pos != std::string::npos && end_pos != 0) {
std::string expression = config.expression_; std::string expression = config.expression_;

2
util/Grid.h
View File

@ -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);
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);
cells getGridCells(); cells getGridCells();

Write Preview
Loading…
Cancel
Save