From f38eeff1efe25fd11cee3d6796066c56790320cb Mon Sep 17 00:00:00 2001 From: Mavo Date: Sat, 9 Jan 2016 11:19:34 +0100 Subject: [PATCH] First try on parsing of rational functions Former-commit-id: 63a6ae0d146bc81530ace58c314e5ed88b2ac01a --- src/builder/ExplicitDFTModelBuilder.cpp | 2 +- src/parser/DFTGalileoParser.cpp | 69 ++++++++++++++++--------- src/parser/DFTGalileoParser.h | 25 +++++++-- src/parser/ExpressionParser.cpp | 38 +++++++++++++- src/parser/ExpressionParser.h | 18 ++++++- src/storage/dft/DFTElements.h | 6 ++- src/storm-dyftee.cpp | 36 ++++++------- 7 files changed, 139 insertions(+), 55 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index e039b389f..b561bb716 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -79,7 +79,7 @@ namespace storm { while (!stateQueue.empty()) { // Initialization outgoingTransitions.clear(); - ValueType sum = 0; + ValueType sum = storm::utility::zero(); // Consider next state storm::storage::DFTState state = stateQueue.front(); diff --git a/src/parser/DFTGalileoParser.cpp b/src/parser/DFTGalileoParser.cpp index 97b095f22..89ad18ff6 100644 --- a/src/parser/DFTGalileoParser.cpp +++ b/src/parser/DFTGalileoParser.cpp @@ -4,9 +4,10 @@ #include #include #include -#include -#include "../exceptions/FileIoException.h" -#include "../exceptions/NotSupportedException.h" +#include "src/storage/expressions/ExpressionManager.h" +#include "src/exceptions/NotImplementedException.h" +#include "src/exceptions/FileIoException.h" +#include "src/exceptions/NotSupportedException.h" #include "src/utility/macros.h" namespace storm { @@ -15,7 +16,7 @@ namespace storm { template storm::storage::DFT DFTGalileoParser::parseDFT(const std::string& filename) { if(readFile(filename)) { - storm::storage::DFT dft = mBuilder.build(); + storm::storage::DFT dft = builder.build(); STORM_LOG_DEBUG("Elements:" << std::endl << dft.getElementsString()); STORM_LOG_DEBUG("Spare Modules:" << std::endl << dft.getSpareModulesString()); return dft; @@ -43,6 +44,7 @@ namespace storm { // constants std::string toplevelToken = "toplevel"; std::string toplevelId; + std::string parametricToken = "param"; std::ifstream file; file.exceptions ( std::ifstream::failbit ); @@ -73,8 +75,16 @@ namespace storm { if(boost::starts_with(line, toplevelToken)) { toplevelId = stripQuotsFromName(line.substr(toplevelToken.size() + 1)); } - else - { + else if (boost::starts_with(line, parametricToken)) { + if (!std::is_same::value) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters only allowed when using rational functions."); + } + std::string parameter = stripQuotsFromName(line.substr(parametricToken.size() + 1)); + storm::expressions::Variable var = manager->declareRationalVariable(parameter); + identifierMapping.emplace(var.getName(), var); + parser.setIdentifierMapping(identifierMapping); + STORM_LOG_TRACE("Added parameter: " << var.getName()); + } else { std::vector tokens; boost::split(tokens, line, boost::is_any_of(" ")); std::string name(stripQuotsFromName(tokens[0])); @@ -84,28 +94,19 @@ namespace storm { childNames.push_back(stripQuotsFromName(tokens[i])); } if(tokens[1] == "and") { - success = mBuilder.addAndElement(name, childNames); + success = builder.addAndElement(name, childNames); } else if(tokens[1] == "or") { - success = mBuilder.addOrElement(name, childNames); + success = builder.addOrElement(name, childNames); } else if(boost::starts_with(tokens[1], "vot")) { - success = mBuilder.addVotElement(name, boost::lexical_cast(tokens[1].substr(3)), childNames); + success = builder.addVotElement(name, boost::lexical_cast(tokens[1].substr(3)), childNames); } else if(tokens[1] == "pand") { - success = mBuilder.addPandElement(name, childNames); + success = builder.addPandElement(name, childNames); } else if(tokens[1] == "wsp" || tokens[1] == "csp") { - success = mBuilder.addSpareElement(name, childNames); + success = builder.addSpareElement(name, childNames); } else if(boost::starts_with(tokens[1], "lambda=")) { - ValueType failureRate = 0; - ValueType dormancyFactor = 0; - if (std::is_same::value) { - failureRate = boost::lexical_cast(tokens[1].substr(7)); - dormancyFactor = boost::lexical_cast(tokens[2].substr(5)); - } else { - // TODO Matthias: Parse RationalFunction - failureRate; - dormancyFactor; - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Parsing into rational function not supported."); - } - success = mBuilder.addBasicElement(name, failureRate, dormancyFactor); + ValueType failureRate = parseRationalExpression(tokens[1].substr(7)); + ValueType dormancyFactor = parseRationalExpression(tokens[2].substr(5)); + success = builder.addBasicElement(name, failureRate, dormancyFactor); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Type name: " + tokens[1] + " not recognized."); success = false; @@ -115,17 +116,37 @@ namespace storm { generalSuccess = success; } } - if(!mBuilder.setTopLevel(toplevelId)) { + if(!builder.setTopLevel(toplevelId)) { STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Top level id unknown."); } file.close(); return generalSuccess; } + template + ValueType DFTGalileoParser::parseRationalExpression(std::string const& expr) { + assert(false); + } + + template<> + double DFTGalileoParser::parseRationalExpression(std::string const& expr) { + return boost::lexical_cast(expr); + } + // Explicitly instantiate the class. template class DFTGalileoParser; #ifdef STORM_HAVE_CARL + template<> + storm::RationalFunction DFTGalileoParser::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; + } + template class DFTGalileoParser; #endif diff --git a/src/parser/DFTGalileoParser.h b/src/parser/DFTGalileoParser.h index 4f7da1566..557803465 100644 --- a/src/parser/DFTGalileoParser.h +++ b/src/parser/DFTGalileoParser.h @@ -1,8 +1,11 @@ #ifndef DFTGALILEOPARSER_H #define DFTGALILEOPARSER_H -#include "../storage/dft/DFT.h" -#include "../storage/dft/DFTBuilder.h" +#include "src/storage/dft/DFT.h" +#include "src/storage/dft/DFTBuilder.h" +#include "src/storage/expressions/ExpressionManager.h" +#include "src/parser/ExpressionParser.h" +#include "src/storage/expressions/ExpressionEvaluator.h" #include @@ -11,16 +14,30 @@ namespace storm { template class DFTGalileoParser { - storm::storage::DFTBuilder mBuilder; + storm::storage::DFTBuilder builder; + + std::shared_ptr manager; + + storm::parser::ExpressionParser parser; + + storm::expressions::ExpressionEvaluator evaluator; + + std::unordered_map identifierMapping; + public: + DFTGalileoParser() : manager(new storm::expressions::ExpressionManager()), parser(*manager), evaluator(*manager) { + } + storm::storage::DFT parseDFT(std::string const& filename); private: bool readFile(std::string const& filename); std::string stripQuotsFromName(std::string const& name); + + ValueType parseRationalExpression(std::string const& expr); }; -} + } } #endif /* DFTGALILEOPARSER_H */ diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp index c67f808e0..0e4d0fbb8 100644 --- a/src/parser/ExpressionParser.cpp +++ b/src/parser/ExpressionParser.cpp @@ -5,7 +5,7 @@ namespace storm { namespace parser { - ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols const& invalidIdentifiers_, bool allowBacktracking) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), powerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), trueFalse_(manager), manager(manager.getSharedPointer()), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) { + ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols const& invalidIdentifiers_, bool allowBacktracking) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), powerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), trueFalse_(manager), manager(manager.getSharedPointer()), createExpressions(false), acceptDoubleLiterals(true), deleteIdentifierMapping(false), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) { identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&ExpressionParser::isValidIdentifier, phoenix::ref(*this), qi::_1)]; identifier.name("identifier"); @@ -126,9 +126,23 @@ namespace storm { this->identifiers_ = nullptr; } } - + + void ExpressionParser::setIdentifierMapping(std::unordered_map const& identifierMapping) { + unsetIdentifierMapping(); + this->createExpressions = true; + this->identifiers_ = new qi::symbols(); + for (auto const& identifierExpressionPair : identifierMapping) { + this->identifiers_->add(identifierExpressionPair.first, identifierExpressionPair.second); + } + deleteIdentifierMapping = true; + } + void ExpressionParser::unsetIdentifierMapping() { this->createExpressions = false; + if (deleteIdentifierMapping) { + delete this->identifiers_; + deleteIdentifierMapping = false; + } this->identifiers_ = nullptr; } @@ -346,5 +360,25 @@ namespace storm { } return true; } + + storm::expressions::Expression ExpressionParser::parseFromString(std::string const& expressionString) const { + PositionIteratorType first(expressionString.begin()); + PositionIteratorType iter = first; + PositionIteratorType last(expressionString.end()); + + // Create empty result; + storm::expressions::Expression result; + + try { + // Start parsing. + bool succeeded = qi::phrase_parse(iter, last, *this, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result); + STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Could not parse expression."); + STORM_LOG_DEBUG("Parsed expression successfully."); + } catch (qi::expectation_failure const& e) { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, e.what_); + } + + return result; + } } } \ No newline at end of file diff --git a/src/parser/ExpressionParser.h b/src/parser/ExpressionParser.h index 19c129b4a..4d40467a0 100644 --- a/src/parser/ExpressionParser.h +++ b/src/parser/ExpressionParser.h @@ -25,7 +25,7 @@ namespace storm { * points it would typically allow. This can, for example, be used to prevent errors if the outer grammar * also parses boolean conjuncts that are erroneously consumed by the expression parser. */ - ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols const& invalidIdentifiers_, bool allowBacktracking = false); + ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols const& invalidIdentifiers_ = qi::symbols(), bool allowBacktracking = false); ExpressionParser(ExpressionParser const& other) = default; ExpressionParser& operator=(ExpressionParser const& other) = default; @@ -38,6 +38,15 @@ namespace storm { * @param identifiers_ A pointer to a mapping from identifiers to expressions. */ void setIdentifierMapping(qi::symbols const* identifiers_); + + /*! + * Sets an identifier mapping that is used to determine valid variables in the expression. The mapped-to + * expressions will be substituted wherever the key value appears in the parsed expression. After setting + * this, the parser will generate expressions. + * + * @param identifierMapping A mapping from identifiers to expressions. + */ + void setIdentifierMapping(std::unordered_map const& identifierMapping); /*! * Unsets a previously set identifier mapping. This will make the parser not generate expressions any more @@ -51,7 +60,9 @@ namespace storm { * @param flag If set to true, double literals are accepted. */ void setAcceptDoubleLiterals(bool flag); - + + storm::expressions::Expression parseFromString(std::string const& expressionString) const; + private: struct orOperatorStruct : qi::symbols { orOperatorStruct() { @@ -184,6 +195,9 @@ namespace storm { // A flag that indicates whether double literals are accepted. bool acceptDoubleLiterals; + // A flag that indicates whether the mapping must be deleted on unsetting. + bool deleteIdentifierMapping; + // The currently used mapping of identifiers to expressions. This is used if the parser is set to create // expressions. qi::symbols const* identifiers_; diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index 6296a176f..daa1d3d54 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -11,6 +11,8 @@ #include "DFTState.h" #include "DFTStateSpaceGenerationQueues.h" +#include "src/utility/constants.h" +#include "src/adapters/CarlAdapter.h" using std::size_t; @@ -313,9 +315,9 @@ namespace storm { } bool isColdBasicElement() const { - return mPassiveFailureRate == 0; + return storm::utility::isZero(mPassiveFailureRate); } - + virtual std::vector independentUnit() const { return {this->mId}; } diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index 1d2696594..906e9df21 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -5,7 +5,7 @@ #include "modelchecker/results/CheckResult.h" #include "utility/storm.h" -#define VALUE_TYPE double +#define VALUE_TYPE storm::RationalFunction /* * Entry point for the DyFTeE backend. @@ -15,6 +15,15 @@ int main(int argc, char** argv) { std::cout << "Storm-DyFTeE should be called with a filename as argument." << std::endl; return 1; } + // Construct PCTL forumla + std::string inputFormula; + if (argc < 3) { + // Set explicit reachability formula + inputFormula = "Pmax=?[true U \"failed\"]"; + } else { + // Read formula from input + inputFormula = argv[2]; + } storm::utility::setUp(); log4cplus::LogLevel level = log4cplus::TRACE_LOG_LEVEL; @@ -24,33 +33,20 @@ int main(int argc, char** argv) { std::cout << "Parsing DFT file..." << std::endl; storm::parser::DFTGalileoParser parser; storm::storage::DFT dft = parser.parseDFT(argv[1]); - std::cout << "Built data structure" << std::endl; + // Verify the model as CTMC std::cout << "Building CTMC..." << std::endl; storm::builder::ExplicitDFTModelBuilder builder(dft); std::shared_ptr> model = builder.buildCTMC(); std::cout << "Built CTMC" << std::endl; - std::cout << "Model checking..." << std::endl; - // Construct PCTL forumla - std::string inputFormula; - if (argc < 3) { - // Set explicit reachability formula - inputFormula = "Pmax=?[true U \"failed\"]"; - } else { - // Read formula from input - inputFormula = argv[2]; - } std::vector> formulas = storm::parseFormulasForExplicit(inputFormula); assert(formulas.size() == 1); - - // Verify the model - std::unique_ptr result(storm::verifySparseModel(model, formulas[0])); - assert(result); + std::unique_ptr resultCtmc(storm::verifySparseModel(model, formulas[0])); + assert(resultCtmc); std::cout << "Result (initial states): "; - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - std::cout << *result << std::endl; - - std::cout << "Checked model" << std::endl; + resultCtmc->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); + std::cout << *resultCtmc << std::endl; + std::cout << "Checked CTMC" << std::endl; }