diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index 0388e9610..c0f54f68b 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -33,8 +33,7 @@ namespace storm { */ template std::shared_ptr> loadDFTJsonString(std::string const& jsonString) { - storm::parser::DFTJsonParser parser; - return std::make_shared>(parser.parseJsonFromString(jsonString)); + return std::make_shared>(storm::parser::DFTJsonParser::parseJsonFromString(jsonString)); } /*! @@ -45,8 +44,7 @@ namespace storm { */ template std::shared_ptr> loadDFTJsonFile(std::string const& file) { - storm::parser::DFTJsonParser parser; - return std::make_shared>(parser.parseJsonFromFile(file)); + return std::make_shared>(storm::parser::DFTJsonParser::parseJsonFromFile(file)); } /*! diff --git a/src/storm-dft/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp index 2461fb9cb..865ed40bf 100644 --- a/src/storm-dft/parser/DFTGalileoParser.cpp +++ b/src/storm-dft/parser/DFTGalileoParser.cpp @@ -101,7 +101,7 @@ namespace storm { std::string name = parseName(tokens[0]); std::vector childNames; - for(unsigned i = 2; i < tokens.size(); ++i) { + for(size_t i = 2; i < tokens.size(); ++i) { childNames.push_back(parseName(tokens[i])); } bool success = true; @@ -113,12 +113,12 @@ namespace storm { } else if (type == "or") { success = builder.addOrElement(name, childNames); } else if (boost::starts_with(type, "vot")) { - unsigned threshold = storm::parser::parseNumber(type.substr(3)); + size_t threshold = storm::parser::parseNumber(type.substr(3)); success = builder.addVotElement(name, threshold, childNames); } else if (type.find("of") != std::string::npos) { size_t pos = type.find("of"); - unsigned threshold = storm::parser::parseNumber(type.substr(0, pos)); - unsigned count = storm::parser::parseNumber(type.substr(pos + 2)); + size_t threshold = storm::parser::parseNumber(type.substr(0, pos)); + size_t count = storm::parser::parseNumber(type.substr(pos + 2)); STORM_LOG_THROW(count == childNames.size(), storm::exceptions::WrongFormatException, "Voting gate number " << count << " does not correspond to number of children " << childNames.size() << " in line " << lineNo << "."); success = builder.addVotElement(name, threshold, childNames); } else if (type == "pand") { @@ -190,7 +190,7 @@ namespace storm { } template - std::pair DFTGalileoParser::parseNumber(std::string name, std::string& line) { + std::pair DFTGalileoParser::parseNumber(std::string name, std::string& line) { // Build regex for: name=(number) std::regex nameRegex(name + "\\s*=\\s*([[:digit:]]+)"); std::smatch match; @@ -198,7 +198,7 @@ namespace storm { std::string value = match.str(1); // Remove matched part line = std::regex_replace(line, nameRegex, ""); - return std::make_pair(true, storm::parser::parseNumber(value)); + return std::make_pair(true, storm::parser::parseNumber(value)); } else { // No match found return std::make_pair(false, 0); @@ -236,7 +236,7 @@ namespace storm { } } // Erlang distribution - std::pair resultNum = parseNumber("phases", line); + std::pair resultNum = parseNumber("phases", line); if (resultNum.first) { STORM_LOG_THROW(distribution == Distribution::None || distribution == Distribution::Exponential, storm::exceptions::WrongFormatException, "A different distribution was already defined for basic element '" << name << "' in line " << lineNo << "."); erlangPhases = resultNum.second; diff --git a/src/storm-dft/parser/DFTGalileoParser.h b/src/storm-dft/parser/DFTGalileoParser.h index 0c280fd88..664533cce 100644 --- a/src/storm-dft/parser/DFTGalileoParser.h +++ b/src/storm-dft/parser/DFTGalileoParser.h @@ -72,9 +72,9 @@ namespace storm { * @param name Name of BE. * @param input Input line. The parsed argument will be removed from the line. * - * @return Pair (success, value). Success is true iff the parsing was succesful. Then value contains the parsed value. + * @return Pair (success, value). Success is true iff the parsing was successful. Then value contains the parsed value. */ - static std::pair parseNumber(std::string name, std::string& line); + static std::pair parseNumber(std::string name, std::string& line); enum Distribution { None, Constant, Exponential, Erlang, Weibull, LogNormal }; }; diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index 9c84eee59..b682ee7d0 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -11,6 +11,7 @@ #include "storm/exceptions/NotSupportedException.h" #include "storm/utility/macros.h" #include "storm/utility/file.h" +#include "storm-parsers/parser/ValueParser.h" namespace storm { namespace parser { @@ -35,6 +36,10 @@ namespace storm { template storm::storage::DFT DFTJsonParser::parseJson(json const& jsonInput) { + // Init DFT builder and value parser + storm::builder::DFTBuilder builder; + ValueParser valueParser; + // Try to parse parameters if (jsonInput.find("parameters") != jsonInput.end()) { json parameters = jsonInput.at("parameters"); @@ -42,10 +47,8 @@ namespace storm { "Parameters only allowed when using rational functions."); for (auto it = parameters.begin(); it != parameters.end(); ++it) { std::string parameter = it.key(); - storm::expressions::Variable var = manager->declareRationalVariable(parameter); - identifierMapping.emplace(var.getName(), var); - parser.setIdentifierMapping(identifierMapping); - STORM_LOG_TRACE("Added parameter: " << var.getName()); + valueParser.addParameter(parameter); + STORM_LOG_TRACE("Added parameter: " << parameter); } } @@ -84,7 +87,7 @@ namespace storm { success = builder.addOrElement(name, childNames); } else if (type == "vot") { std::string votThreshold = parseJsonNumber(data.at("voting")); - success = builder.addVotElement(name, boost::lexical_cast(votThreshold), childNames); + success = builder.addVotElement(name, storm::parser::parseNumber(votThreshold), childNames); } else if (type == "pand") { success = builder.addPandElement(name, childNames); } else if (type == "por") { @@ -98,7 +101,7 @@ namespace storm { } else if (type == "fdep") { success = builder.addDepElement(name, childNames, storm::utility::one()); } else if (type == "pdep") { - ValueType probability = parseRationalExpression(parseJsonNumber(data.at("probability"))); + ValueType probability = valueParser.parseValue(parseJsonNumber(data.at("probability"))); success = builder.addDepElement(name, childNames, probability); } else if (boost::starts_with(type, "be")) { std::string distribution = "exp"; // Set default of exponential distribution @@ -108,8 +111,8 @@ namespace storm { STORM_LOG_THROW(type == "be" || "be_" + distribution == type, storm::exceptions::WrongFormatException, "BE type '" << type << "' and distribution '" << distribution << " do not agree."); if (distribution == "exp") { - ValueType failureRate = parseRationalExpression(parseJsonNumber(data.at("rate"))); - ValueType dormancyFactor = parseRationalExpression(parseJsonNumber(data.at("dorm"))); + ValueType failureRate = valueParser.parseValue(parseJsonNumber(data.at("rate"))); + ValueType dormancyFactor = valueParser.parseValue(parseJsonNumber(data.at("dorm"))); bool transient = false; if (data.count("transient") > 0) { transient = data.at("transient"); @@ -178,28 +181,6 @@ namespace storm { } } - template - ValueType DFTJsonParser::parseRationalExpression(std::string const& expr) { - STORM_LOG_ASSERT(false, "Specialized method should be called."); - return 0; - } - - template<> - double DFTJsonParser::parseRationalExpression(std::string const& expr) { - return boost::lexical_cast(expr); - } - - template<> - storm::RationalFunction DFTJsonParser::parseRationalExpression(std::string const& expr) { - STORM_LOG_TRACE("Translating expression: " << expr); - storm::expressions::Expression expression = parser.parseFromString(expr); - STORM_LOG_TRACE("Expression: " << expression); - storm::RationalFunction rationalFunction = evaluator.asRational(expression); - STORM_LOG_TRACE("Parsed expression: " << rationalFunction); - return rationalFunction; - } - - // Explicitly instantiate the class. template class DFTJsonParser; template class DFTJsonParser; diff --git a/src/storm-dft/parser/DFTJsonParser.h b/src/storm-dft/parser/DFTJsonParser.h index 801e80a88..c092d47eb 100644 --- a/src/storm-dft/parser/DFTJsonParser.h +++ b/src/storm-dft/parser/DFTJsonParser.h @@ -2,10 +2,6 @@ #include -#include "storm/storage/expressions/ExpressionManager.h" -#include "storm-parsers/parser/ExpressionParser.h" -#include "storm/storage/expressions/ExpressionEvaluator.h" - #include "storm-dft/storage/dft/DFT.h" #include "storm-dft/builder/DFTBuilder.h" @@ -19,32 +15,19 @@ namespace storm { template class DFTJsonParser { - storm::builder::DFTBuilder builder; - - std::shared_ptr manager; - - storm::parser::ExpressionParser parser; - - storm::expressions::ExpressionEvaluator evaluator; - - std::unordered_map identifierMapping; public: - DFTJsonParser() : manager(new storm::expressions::ExpressionManager()), parser(*manager), evaluator(*manager) { - } - storm::storage::DFT parseJsonFromString(std::string const& jsonString); + static storm::storage::DFT parseJsonFromString(std::string const& jsonString); - storm::storage::DFT parseJsonFromFile(std::string const& filename); + static storm::storage::DFT parseJsonFromFile(std::string const& filename); private: - storm::storage::DFT parseJson(json const& jsonInput); - - std::string generateUniqueName(std::string const& name); + static storm::storage::DFT parseJson(json const& jsonInput); - ValueType parseRationalExpression(std::string const& expr); + static std::string generateUniqueName(std::string const& name); - std::string parseJsonNumber(json number); + static std::string parseJsonNumber(json number); }; } }