diff --git a/main.cpp b/main.cpp
index abc86a9..1a74df5 100644
--- a/main.cpp
+++ b/main.cpp
@@ -42,7 +42,7 @@ void print_info(boost::spirit::info const& what) {
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);
std::string seperator = ";";
@@ -52,7 +52,7 @@ void setProbability(const std::string& gridProperties, const std::vector<Probabi
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()) {
prop = (*yaml_config_prop).value_;
@@ -127,7 +127,7 @@ int main(int argc, char* argv[]) {
cells contentCells;
cells backgroundCells;
std::vector<Configuration> configurations;
- std::vector<Probability> probabilities;
+ std::vector<Property> parsed_properties;
std::map<coordinates, float> stateRewards;
float faultyProbability = 0.0;
float probIntended = 1.0;
@@ -142,7 +142,7 @@ int main(int argc, char* argv[]) {
YamlConfigParser parser(configFilename->value(0));
auto parseResult = parser.parseConfiguration();
configurations = parseResult.configurations_;
- probabilities = parseResult.probabilities_;
+ parsed_properties = parseResult.properties_;
}
boost::escaped_list_separator<char> seps('\\', ';', '\n');
@@ -158,13 +158,25 @@ int main(int argc, char* argv[]) {
auto probForwardIntendedIdentifier = std::string("ProbForwardIntended");
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) {
- 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);
std::stringstream ss;
grid.printToPrism(ss, configurations);
diff --git a/util/ConfigYaml.cpp b/util/ConfigYaml.cpp
index 1cfb6d2..b558d32 100644
--- a/util/ConfigYaml.cpp
+++ b/util/ConfigYaml.cpp
@@ -202,22 +202,27 @@ bool YAML::convert<Constant>::decode(const YAML::Node& node, Constant& rhs) {
return true;
}
-YAML::Node YAML::convert<Probability>::encode(const Probability& rhs) {
+YAML::Node YAML::convert<Property>::encode(const Property& rhs) {
YAML::Node node;
- node.push_back(rhs.probability_);
+ node.push_back(rhs.property);
node.push_back(rhs.value_);
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;
}
- 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;
}
@@ -227,7 +232,7 @@ const std::string Configuration::overwrite_identifier_{"; // Overwritten through
YamlConfigParseResult YamlConfigParser::parseConfiguration() {
std::vector<Configuration> configuration;
- std::vector<Probability> probabilities;
+ std::vector<Property> properties;
try {
YAML::Node config = YAML::LoadFile(file_);
@@ -250,8 +255,8 @@ YamlConfigParseResult YamlConfigParser::parseConfiguration() {
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) {
@@ -262,16 +267,16 @@ YamlConfigParseResult YamlConfigParser::parseConfiguration() {
}
for (auto& module : modules) {
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);
continue;
}
for (auto& command : module.commands_) {
Configuration config;
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()) {
- 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 {
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;
}
- return YamlConfigParseResult(configuration, probabilities);
+ return YamlConfigParseResult(configuration, properties);
}
\ No newline at end of file
diff --git a/util/ConfigYaml.h b/util/ConfigYaml.h
index 53eafea..80fe5c1 100644
--- a/util/ConfigYaml.h
+++ b/util/ConfigYaml.h
@@ -11,6 +11,8 @@ enum class ConfigType : char {
Label = 'L',
Formula = 'F',
Module = 'M',
+ UpdateOnly = 'U',
+ GuardOnly = 'G',
Constant = 'C'
};
@@ -27,7 +29,6 @@ struct Configuration
ConfigType type_ {ConfigType::Label};
bool overwrite_ {false};
- bool include_identifier_for_overwrite_{true};
Configuration() = default;
Configuration(std::string expression
@@ -36,8 +37,7 @@ struct Configuration
, bool overwrite = false
, std::string module = ""
, 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(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_;
+ 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 {
@@ -156,20 +157,20 @@ struct YAML::convert<Constant> {
};
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 {
- 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(const YamlConfigParseResult&) = default;
std::vector<Configuration> configurations_;
- std::vector<Probability> probabilities_;
+ std::vector<Property> properties_;
};
struct YamlConfigParser {
diff --git a/util/Grid.cpp b/util/Grid.cpp
index 8f83703..8ecfa44 100644
--- a/util/Grid.cpp
+++ b/util/Grid.cpp
@@ -3,7 +3,7 @@
#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)
{
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;
} else {
modelType = prism::ModelType::SMG;
@@ -111,14 +113,25 @@ void Grid::applyOverwrites(std::string& str, std::vector<Configuration>& configu
search = "label " + config.identifier_;
} else if (config.type_ == ConfigType::Module) {
search = config.identifier_;
+ } else if (config.type_ == ConfigType::UpdateOnly) {
+ search = config.identifier_;
}
else if (config.type_ == ConfigType::Constant) {
search = config.identifier_;
}
auto iter = boost::find_nth(str, search, index);
+ auto end_identifier = config.end_identifier_;
+
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) {
std::string expression = config.expression_;
diff --git a/util/Grid.h b/util/Grid.h
index da593ba..5c2f4d9 100644
--- a/util/Grid.h
+++ b/util/Grid.h
@@ -13,7 +13,7 @@
class Grid {
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();