From bb408b2b29a77a7d1e6074842b6c623012cca5ed Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 27 Jan 2016 23:46:18 +0100 Subject: [PATCH] parser returns non-const formulae now Former-commit-id: ed23af516e50f6ed96becee6f373eb75e0d26420 --- src/cli/cli.cpp | 7 +- src/logic/ComparisonType.h | 21 ++-- src/logic/OperatorFormula.cpp | 10 +- src/logic/OperatorFormula.h | 4 +- src/parser/FormulaParser.cpp | 194 +++++++++++++++++----------------- src/parser/FormulaParser.h | 6 +- src/utility/storm.cpp | 6 +- src/utility/storm.h | 4 +- 8 files changed, 132 insertions(+), 120 deletions(-) diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index 7e53dde92..0909b25de 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -220,17 +220,18 @@ namespace storm { } // Then proceed to parsing the property (if given), since the model we are building may depend on the property. - std::vector> formulas; + std::vector> parsedFormulas; if (settings.isPropertySet()) { std::string properties = settings.getProperty(); if(program) { - formulas = storm::parseFormulasForProgram(properties, program.get()); + parsedFormulas = storm::parseFormulasForProgram(properties, program.get()); } else { - formulas = storm::parseFormulasForExplicit(properties); + parsedFormulas = storm::parseFormulasForExplicit(properties); } } + std::vector> formulas(parsedFormulas.begin(), parsedFormulas.end()); if (settings.isSymbolicSet()) { #ifdef STORM_HAVE_CARL diff --git a/src/logic/ComparisonType.h b/src/logic/ComparisonType.h index ccfff25b6..b91b2432b 100644 --- a/src/logic/ComparisonType.h +++ b/src/logic/ComparisonType.h @@ -5,16 +5,17 @@ namespace storm { namespace logic { - enum class ComparisonType { Less, LessEqual, Greater, GreaterEqual }; - - inline bool isStrict(ComparisonType t) { - return (t == ComparisonType::Less || t == ComparisonType::Greater); - } - - inline bool isLowerBound(ComparisonType t) { - return (t == ComparisonType::Greater || t == ComparisonType::GreaterEqual); - } - std::ostream& operator<<(std::ostream& out, ComparisonType const& comparisonType); + enum class ComparisonType { Less, LessEqual, Greater, GreaterEqual }; + + inline bool isStrict(ComparisonType t) { + return (t == ComparisonType::Less || t == ComparisonType::Greater); + } + + inline bool isLowerBound(ComparisonType t) { + return (t == ComparisonType::Greater || t == ComparisonType::GreaterEqual); + } + + std::ostream& operator<<(std::ostream& out, ComparisonType const& comparisonType); } } diff --git a/src/logic/OperatorFormula.cpp b/src/logic/OperatorFormula.cpp index 5997c957d..39fad071d 100644 --- a/src/logic/OperatorFormula.cpp +++ b/src/logic/OperatorFormula.cpp @@ -10,14 +10,22 @@ namespace storm { return static_cast(bound); } - ComparisonType const& OperatorFormula::getComparisonType() const { + ComparisonType OperatorFormula::getComparisonType() const { return comparisonType.get(); } + void OperatorFormula::setComparisonType(ComparisonType t) { + comparisonType = boost::optional(t); + } + double OperatorFormula::getBound() const { return bound.get(); } + void OperatorFormula::setBound(double b) { + bound = boost::optional(b); + } + bool OperatorFormula::hasOptimalityType() const { return static_cast(optimalityType); } diff --git a/src/logic/OperatorFormula.h b/src/logic/OperatorFormula.h index 8bdc14d21..a059ddb8b 100644 --- a/src/logic/OperatorFormula.h +++ b/src/logic/OperatorFormula.h @@ -18,8 +18,10 @@ namespace storm { } bool hasBound() const; - ComparisonType const& getComparisonType() const; + ComparisonType getComparisonType() const; + void setComparisonType(ComparisonType); double getBound() const; + void setBound(double); bool hasOptimalityType() const; OptimizationDirection const& getOptimalityType() const; diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index 96ceee55f..e3c0c9718 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -10,7 +10,7 @@ namespace storm { namespace parser { - class FormulaParserGrammar : public qi::grammar>(), Skipper> { + class FormulaParserGrammar : public qi::grammar>(), Skipper> { public: FormulaParserGrammar(std::shared_ptr const& manager = std::shared_ptr(new storm::expressions::ExpressionManager())); @@ -95,66 +95,66 @@ namespace storm { // they are to be replaced with. qi::symbols identifiers_; - qi::rule>(), Skipper> start; + qi::rule>(), Skipper> start; qi::rule, boost::optional, boost::optional>(), qi::locals, boost::optional, boost::optional>, Skipper> operatorInformation; - qi::rule(), Skipper> probabilityOperator; - qi::rule(), Skipper> rewardOperator; - qi::rule(), Skipper> expectedTimeOperator; - qi::rule(), Skipper> longRunAverageOperator; - - qi::rule(), Skipper> simpleFormula; - qi::rule(), Skipper> stateFormula; - qi::rule(), Skipper> pathFormula; - qi::rule(), Skipper> pathFormulaWithoutUntil; - qi::rule(), Skipper> simplePathFormula; - qi::rule(), Skipper> atomicStateFormula; - qi::rule(), Skipper> operatorFormula; + qi::rule(), Skipper> probabilityOperator; + qi::rule(), Skipper> rewardOperator; + qi::rule(), Skipper> expectedTimeOperator; + qi::rule(), Skipper> longRunAverageOperator; + + qi::rule(), Skipper> simpleFormula; + qi::rule(), Skipper> stateFormula; + qi::rule(), Skipper> pathFormula; + qi::rule(), Skipper> pathFormulaWithoutUntil; + qi::rule(), Skipper> simplePathFormula; + qi::rule(), Skipper> atomicStateFormula; + qi::rule(), Skipper> operatorFormula; qi::rule label; qi::rule rewardModelName; - qi::rule(), Skipper> andStateFormula; - qi::rule(), Skipper> orStateFormula; - qi::rule(), Skipper> notStateFormula; - qi::rule(), Skipper> labelFormula; - qi::rule(), Skipper> expressionFormula; - qi::rule(), qi::locals, Skipper> booleanLiteralFormula; - - qi::rule(), Skipper> conditionalFormula; - qi::rule(), Skipper> eventuallyFormula; - qi::rule(), Skipper> nextFormula; - qi::rule(), Skipper> globallyFormula; - qi::rule(), Skipper> untilFormula; + qi::rule(), Skipper> andStateFormula; + qi::rule(), Skipper> orStateFormula; + qi::rule(), Skipper> notStateFormula; + qi::rule(), Skipper> labelFormula; + qi::rule(), Skipper> expressionFormula; + qi::rule(), qi::locals, Skipper> booleanLiteralFormula; + + qi::rule(), Skipper> conditionalFormula; + qi::rule(), Skipper> eventuallyFormula; + qi::rule(), Skipper> nextFormula; + qi::rule(), Skipper> globallyFormula; + qi::rule(), Skipper> untilFormula; qi::rule, uint_fast64_t>(), Skipper> timeBound; - qi::rule(), Skipper> rewardPathFormula; - qi::rule(), Skipper> cumulativeRewardFormula; - qi::rule(), Skipper> reachabilityRewardFormula; - qi::rule(), Skipper> instantaneousRewardFormula; - qi::rule(), Skipper> longRunAverageRewardFormula; + qi::rule(), Skipper> rewardPathFormula; + qi::rule(), Skipper> cumulativeRewardFormula; + qi::rule(), Skipper> reachabilityRewardFormula; + qi::rule(), Skipper> instantaneousRewardFormula; + qi::rule(), Skipper> longRunAverageRewardFormula; // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). boost::spirit::qi::real_parser> strict_double; // Methods that actually create the expression objects. - std::shared_ptr createInstantaneousRewardFormula(boost::variant const& timeBound) const; - std::shared_ptr createCumulativeRewardFormula(boost::variant const& timeBound) const; - std::shared_ptr createReachabilityRewardFormula(std::shared_ptr const& stateFormula) const; - std::shared_ptr createLongRunAverageRewardFormula() const; - std::shared_ptr createAtomicExpressionFormula(storm::expressions::Expression const& expression) const; - std::shared_ptr createBooleanLiteralFormula(bool literal) const; - std::shared_ptr createAtomicLabelFormula(std::string const& label) const; - std::shared_ptr createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& subformula) const; - std::shared_ptr createGloballyFormula(std::shared_ptr const& subformula) const; - std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; - std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& rightSubformula); - std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) const; - std::shared_ptr createLongRunAverageOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createRewardOperatorFormula(boost::optional const& rewardModelName, std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createExpectedTimeOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula); - std::shared_ptr createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType); - std::shared_ptr createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); + std::shared_ptr createInstantaneousRewardFormula(boost::variant const& timeBound) const; + std::shared_ptr createCumulativeRewardFormula(boost::variant const& timeBound) const; + std::shared_ptr createReachabilityRewardFormula(std::shared_ptr const& stateFormula) const; + std::shared_ptr createLongRunAverageRewardFormula() const; + std::shared_ptr createAtomicExpressionFormula(storm::expressions::Expression const& expression) const; + std::shared_ptr createBooleanLiteralFormula(bool literal) const; + std::shared_ptr createAtomicLabelFormula(std::string const& label) const; + std::shared_ptr createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& subformula) const; + std::shared_ptr createGloballyFormula(std::shared_ptr const& subformula) const; + std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; + std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& rightSubformula); + std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) const; + std::shared_ptr createLongRunAverageOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createRewardOperatorFormula(boost::optional const& rewardModelName, std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createExpectedTimeOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula); + std::shared_ptr createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType); + std::shared_ptr createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); // An error handler function. phoenix::function handler; @@ -182,18 +182,18 @@ namespace storm { return *this; } - std::shared_ptr FormulaParser::parseSingleFormulaFromString(std::string const& formulaString) const { - std::vector> formulas = parseFromString(formulaString); + std::shared_ptr FormulaParser::parseSingleFormulaFromString(std::string const& formulaString) const { + std::vector> formulas = parseFromString(formulaString); STORM_LOG_THROW(formulas.size() == 1, storm::exceptions::WrongFormatException, "Expected exactly one formula, but found " << formulas.size() << " instead."); return formulas.front(); } - std::vector> FormulaParser::parseFromFile(std::string const& filename) const { + std::vector> FormulaParser::parseFromFile(std::string const& filename) const { // Open file and initialize result. std::ifstream inputFileStream(filename, std::ios::in); STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'."); - std::vector> formulas; + std::vector> formulas; // Now try to parse the contents of the file. try { @@ -210,13 +210,13 @@ namespace storm { return formulas; } - std::vector> FormulaParser::parseFromString(std::string const& formulaString) const { + std::vector> FormulaParser::parseFromString(std::string const& formulaString) const { PositionIteratorType first(formulaString.begin()); PositionIteratorType iter = first; PositionIteratorType last(formulaString.end()); // Create empty result; - std::vector> result; + std::vector> result; // Create grammar. try { @@ -390,108 +390,108 @@ namespace storm { this->identifiers_.add(identifier, expression); } - std::shared_ptr FormulaParserGrammar::createInstantaneousRewardFormula(boost::variant const& timeBound) const { + std::shared_ptr FormulaParserGrammar::createInstantaneousRewardFormula(boost::variant const& timeBound) const { if (timeBound.which() == 0) { - return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(static_cast(boost::get(timeBound)))); + return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(static_cast(boost::get(timeBound)))); } else { double timeBoundAsDouble = boost::get(timeBound); STORM_LOG_THROW(timeBoundAsDouble >= 0, storm::exceptions::WrongFormatException, "Cumulative reward property must have non-negative bound."); - return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(static_cast(timeBoundAsDouble))); + return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(static_cast(timeBoundAsDouble))); } } - std::shared_ptr FormulaParserGrammar::createCumulativeRewardFormula(boost::variant const& timeBound) const { + std::shared_ptr FormulaParserGrammar::createCumulativeRewardFormula(boost::variant const& timeBound) const { if (timeBound.which() == 0) { - return std::shared_ptr(new storm::logic::CumulativeRewardFormula(static_cast(boost::get(timeBound)))); + return std::shared_ptr(new storm::logic::CumulativeRewardFormula(static_cast(boost::get(timeBound)))); } else { double timeBoundAsDouble = boost::get(timeBound); STORM_LOG_THROW(timeBoundAsDouble >= 0, storm::exceptions::WrongFormatException, "Cumulative reward property must have non-negative bound."); - return std::shared_ptr(new storm::logic::CumulativeRewardFormula(static_cast(timeBoundAsDouble))); + return std::shared_ptr(new storm::logic::CumulativeRewardFormula(static_cast(timeBoundAsDouble))); } } - std::shared_ptr FormulaParserGrammar::createReachabilityRewardFormula(std::shared_ptr const& stateFormula) const { - return std::shared_ptr(new storm::logic::ReachabilityRewardFormula(stateFormula)); + std::shared_ptr FormulaParserGrammar::createReachabilityRewardFormula(std::shared_ptr const& stateFormula) const { + return std::shared_ptr(new storm::logic::ReachabilityRewardFormula(stateFormula)); } - std::shared_ptr FormulaParserGrammar::createLongRunAverageRewardFormula() const { - return std::shared_ptr(new storm::logic::LongRunAverageRewardFormula()); + std::shared_ptr FormulaParserGrammar::createLongRunAverageRewardFormula() const { + return std::shared_ptr(new storm::logic::LongRunAverageRewardFormula()); } - std::shared_ptr FormulaParserGrammar::createAtomicExpressionFormula(storm::expressions::Expression const& expression) const { + std::shared_ptr FormulaParserGrammar::createAtomicExpressionFormula(storm::expressions::Expression const& expression) const { STORM_LOG_THROW(expression.hasBooleanType(), storm::exceptions::WrongFormatException, "Expected expression of boolean type."); - return std::shared_ptr(new storm::logic::AtomicExpressionFormula(expression)); + return std::shared_ptr(new storm::logic::AtomicExpressionFormula(expression)); } - std::shared_ptr FormulaParserGrammar::createBooleanLiteralFormula(bool literal) const { - return std::shared_ptr(new storm::logic::BooleanLiteralFormula(literal)); + std::shared_ptr FormulaParserGrammar::createBooleanLiteralFormula(bool literal) const { + return std::shared_ptr(new storm::logic::BooleanLiteralFormula(literal)); } - std::shared_ptr FormulaParserGrammar::createAtomicLabelFormula(std::string const& label) const { - return std::shared_ptr(new storm::logic::AtomicLabelFormula(label)); + std::shared_ptr FormulaParserGrammar::createAtomicLabelFormula(std::string const& label) const { + return std::shared_ptr(new storm::logic::AtomicLabelFormula(label)); } - std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& subformula) const { + std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& subformula) const { if (timeBound) { if (timeBound.get().which() == 0) { std::pair const& bounds = boost::get>(timeBound.get()); - return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, bounds.first, bounds.second)); + return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, bounds.first, bounds.second)); } else { - return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, static_cast(boost::get(timeBound.get())))); + return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, static_cast(boost::get(timeBound.get())))); } } else { - return std::shared_ptr(new storm::logic::EventuallyFormula(subformula)); + return std::shared_ptr(new storm::logic::EventuallyFormula(subformula)); } } - std::shared_ptr FormulaParserGrammar::createGloballyFormula(std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::GloballyFormula(subformula)); + std::shared_ptr FormulaParserGrammar::createGloballyFormula(std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::GloballyFormula(subformula)); } - std::shared_ptr FormulaParserGrammar::createNextFormula(std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::NextFormula(subformula)); + std::shared_ptr FormulaParserGrammar::createNextFormula(std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::NextFormula(subformula)); } - std::shared_ptr FormulaParserGrammar::createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& rightSubformula) { + std::shared_ptr FormulaParserGrammar::createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& rightSubformula) { if (timeBound) { if (timeBound.get().which() == 0) { std::pair const& bounds = boost::get>(timeBound.get()); - return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, bounds.first, bounds.second)); + return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, bounds.first, bounds.second)); } else { - return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, static_cast(boost::get(timeBound.get())))); + return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, static_cast(boost::get(timeBound.get())))); } } else { - return std::shared_ptr(new storm::logic::UntilFormula(leftSubformula, rightSubformula)); + return std::shared_ptr(new storm::logic::UntilFormula(leftSubformula, rightSubformula)); } } - std::shared_ptr FormulaParserGrammar::createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) const { - return std::shared_ptr(new storm::logic::ConditionalPathFormula(leftSubformula, rightSubformula)); + std::shared_ptr FormulaParserGrammar::createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) const { + return std::shared_ptr(new storm::logic::ConditionalPathFormula(leftSubformula, rightSubformula)); } - std::shared_ptr FormulaParserGrammar::createLongRunAverageOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::LongRunAverageOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); + std::shared_ptr FormulaParserGrammar::createLongRunAverageOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::LongRunAverageOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); } - std::shared_ptr FormulaParserGrammar::createRewardOperatorFormula(boost::optional const& rewardModelName, std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::RewardOperatorFormula(rewardModelName, std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); + std::shared_ptr FormulaParserGrammar::createRewardOperatorFormula(boost::optional const& rewardModelName, std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::RewardOperatorFormula(rewardModelName, std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); } - std::shared_ptr FormulaParserGrammar::createExpectedTimeOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::ExpectedTimeOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); + std::shared_ptr FormulaParserGrammar::createExpectedTimeOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::ExpectedTimeOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); } - std::shared_ptr FormulaParserGrammar::createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) { - return std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); + std::shared_ptr FormulaParserGrammar::createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) { + return std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); } - std::shared_ptr FormulaParserGrammar::createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) { - return std::shared_ptr(new storm::logic::BinaryBooleanStateFormula(operatorType, leftSubformula, rightSubformula)); + std::shared_ptr FormulaParserGrammar::createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) { + return std::shared_ptr(new storm::logic::BinaryBooleanStateFormula(operatorType, leftSubformula, rightSubformula)); } - std::shared_ptr FormulaParserGrammar::createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType) { + std::shared_ptr FormulaParserGrammar::createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType) { if (operatorType) { - return std::shared_ptr(new storm::logic::UnaryBooleanStateFormula(operatorType.get(), subformula)); + return std::shared_ptr(new storm::logic::UnaryBooleanStateFormula(operatorType.get(), subformula)); } else { return subformula; } diff --git a/src/parser/FormulaParser.h b/src/parser/FormulaParser.h index b791e96fc..68ee3c5ab 100644 --- a/src/parser/FormulaParser.h +++ b/src/parser/FormulaParser.h @@ -31,7 +31,7 @@ namespace storm { * @param formulaString The formula as a string. * @return The resulting formula. */ - std::shared_ptr parseSingleFormulaFromString(std::string const& formulaString) const; + std::shared_ptr parseSingleFormulaFromString(std::string const& formulaString) const; /*! * Parses the formula given by the provided string. @@ -39,7 +39,7 @@ namespace storm { * @param formulaString The formula as a string. * @return The contained formulas. */ - std::vector> parseFromString(std::string const& formulaString) const; + std::vector> parseFromString(std::string const& formulaString) const; /*! * Parses the formulas in the given file. @@ -47,7 +47,7 @@ namespace storm { * @param filename The name of the file to parse. * @return The contained formulas. */ - std::vector> parseFromFile(std::string const& filename) const; + std::vector> parseFromFile(std::string const& filename) const; /*! * Adds an identifier and the expression it is supposed to be replaced with. This can, for example be used diff --git a/src/utility/storm.cpp b/src/utility/storm.cpp index 9a00c8f2c..a690af6f8 100644 --- a/src/utility/storm.cpp +++ b/src/utility/storm.cpp @@ -19,7 +19,7 @@ namespace storm { * @param FormulaParser * @return The formulas. */ - std::vector> parseFormulas(storm::parser::FormulaParser & formulaParser, std::string const& inputString) { + std::vector> parseFormulas(storm::parser::FormulaParser & formulaParser, std::string const& inputString) { // If the given property looks like a file (containing a dot and there exists a file with that name), // we try to parse it as a file, otherwise we assume it's a property. if (inputString.find(".") != std::string::npos && std::ifstream(inputString).good()) { @@ -29,12 +29,12 @@ namespace storm { } } - std::vector> parseFormulasForExplicit(std::string const& inputString) { + std::vector> parseFormulasForExplicit(std::string const& inputString) { storm::parser::FormulaParser formulaParser; return parseFormulas(formulaParser, inputString); } - std::vector> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program) { + std::vector> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program) { storm::parser::FormulaParser formulaParser(program); return parseFormulas(formulaParser, inputString); } diff --git a/src/utility/storm.h b/src/utility/storm.h index 6e4e82a18..7ffba8c85 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -81,8 +81,8 @@ namespace storm { } storm::prism::Program parseProgram(std::string const& path); - std::vector> parseFormulasForExplicit(std::string const& inputString); - std::vector> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program); + std::vector> parseFormulasForExplicit(std::string const& inputString); + std::vector> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program); template