diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index f27b91bbb..1653d76ea 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -22,20 +22,20 @@ namespace storm { if (result->isQuantitative()) { switch (ft) { case storm::modelchecker::FilterType::VALUES: - STORM_PRINT_AND_LOG(*result << std::endl); - return; + STORM_PRINT_AND_LOG(*result); + break; case storm::modelchecker::FilterType::SUM: STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult().sum()); - return; + break; case storm::modelchecker::FilterType::AVG: STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult().average()); - return; + break; case storm::modelchecker::FilterType::MIN: STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult().getMin()); - return; + break; case storm::modelchecker::FilterType::MAX: STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult().getMax()); - return; + break; case storm::modelchecker::FilterType::ARGMIN: case storm::modelchecker::FilterType::ARGMAX: STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Outputting states is not supported"); @@ -48,16 +48,16 @@ namespace storm { switch (ft) { case storm::modelchecker::FilterType::VALUES: STORM_PRINT_AND_LOG(*result << std::endl); - return; + break; case storm::modelchecker::FilterType::EXISTS: STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().existsTrue()); - return; + break; case storm::modelchecker::FilterType::FORALL: STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().forallTrue()); - return; + break; case storm::modelchecker::FilterType::COUNT: STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().count()); - return; + break; case storm::modelchecker::FilterType::ARGMIN: case storm::modelchecker::FilterType::ARGMAX: @@ -68,8 +68,8 @@ namespace storm { case storm::modelchecker::FilterType::MAX: STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "FilterType only defined for quantitative results"); } - } + STORM_PRINT_AND_LOG(std::endl); } template diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index 537a7f899..dcf1634a6 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -125,7 +125,15 @@ namespace storm { constantDefinition = (qi::lit("const") > qi::eps[qi::_a = true] > -(qi::lit("int") | qi::lit("double")[qi::_a = false]) >> identifier)[phoenix::bind(&FormulaParserGrammar::addConstant, phoenix::ref(*this), qi::_1, qi::_a)]; constantDefinition.name("constant definition"); - start = qi::eps > (((-formulaName >> stateFormula)[phoenix::bind(&FormulaParserGrammar::addProperty, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)] | qi::eps(phoenix::bind(&FormulaParserGrammar::areConstantDefinitionsAllowed, phoenix::ref(*this))) >> constantDefinition | qi::eps) % +(qi::char_("\n;"))) >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi; +#pragma clang diagnostic push +#pragma clang diagnostic ignored "-Woverloaded-shift-op-parentheses" + + filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula > -(qi::lit(",") > qi::lit("\"init\"") > qi::lit(")")))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)] | (-formulaName >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterType, phoenix::ref(*this), qi::_1, qi::_2)]; + filterProperty.name("filter property"); + +#pragma clang diagnostic pop + + start = ((qi::eps > filterProperty[phoenix::push_back(qi::_val, qi::_1)] | qi::eps(phoenix::bind(&FormulaParserGrammar::areConstantDefinitionsAllowed, phoenix::ref(*this))) >> constantDefinition | qi::eps) % +(qi::char_("\n;"))) >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi; start.name("start"); // Enable the following lines to print debug output for most the rules. @@ -197,15 +205,6 @@ namespace storm { addIdentifierExpression(name, newVariable); } - void FormulaParserGrammar::addProperty(std::vector& properties, boost::optional const& name, std::shared_ptr const& formula) { - if (name) { - properties.emplace_back(name.get(), formula); - } else { - properties.emplace_back(std::to_string(propertyCount), formula); - } - ++propertyCount; - } - bool FormulaParserGrammar::areConstantDefinitionsAllowed() const { return static_cast(manager); } @@ -329,5 +328,26 @@ namespace storm { std::shared_ptr FormulaParserGrammar::createMultiObjectiveFormula(std::vector> const& subformulas) { return std::shared_ptr(new storm::logic::MultiObjectiveFormula(subformulas)); } + + storm::jani::Property FormulaParserGrammar::createProperty(boost::optional const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr const& formula) { + storm::jani::FilterExpression filterExpression(formula, filterType); + + ++propertyCount; + if (propertyName) { + return storm::jani::Property(propertyName.get(), filterExpression); + } else { + return storm::jani::Property(std::to_string(propertyCount -1 ), filterExpression); + } + } + + storm::jani::Property FormulaParserGrammar::createPropertyWithDefaultFilterType(boost::optional const& propertyName, std::shared_ptr const& formula) { + ++propertyCount; + if (propertyName) { + return storm::jani::Property(propertyName.get(), formula); + } else { + return storm::jani::Property(std::to_string(propertyCount), formula); + } + } + } } diff --git a/src/storm/parser/FormulaParserGrammar.h b/src/storm/parser/FormulaParserGrammar.h index 4bd546199..79b272246 100644 --- a/src/storm/parser/FormulaParserGrammar.h +++ b/src/storm/parser/FormulaParserGrammar.h @@ -9,6 +9,8 @@ #include "storm/logic/Formulas.h" #include "storm/parser/ExpressionParser.h" +#include "storm/modelchecker/results/FilterType.h" + #include "storm/storage/expressions/ExpressionEvaluator.h" namespace storm { @@ -111,6 +113,25 @@ namespace storm { // A parser used for recognizing the reward measure types. rewardMeasureTypeStruct rewardMeasureType_; + struct filterTypeStruct : qi::symbols { + filterTypeStruct() { + add + ("min", storm::modelchecker::FilterType::MIN) + ("max", storm::modelchecker::FilterType::MAX) + ("sum", storm::modelchecker::FilterType::SUM) + ("avg", storm::modelchecker::FilterType::AVG) + ("count", storm::modelchecker::FilterType::COUNT) + ("forall", storm::modelchecker::FilterType::FORALL) + ("exists", storm::modelchecker::FilterType::EXISTS) + ("argmin", storm::modelchecker::FilterType::ARGMIN) + ("argmax", storm::modelchecker::FilterType::ARGMAX) + ("values", storm::modelchecker::FilterType::VALUES); + } + }; + + // A parser used for recognizing the filter type. + filterTypeStruct filterType_; + // The manager used to parse expressions. std::shared_ptr constManager; std::shared_ptr manager; @@ -135,6 +156,7 @@ namespace storm { qi::rule(), Skipper> timeOperator; qi::rule(), Skipper> longRunAverageOperator; + qi::rule filterProperty; qi::rule(), Skipper> simpleFormula; qi::rule(), Skipper> stateFormula; qi::rule(storm::logic::FormulaContext), Skipper> pathFormula; @@ -201,6 +223,9 @@ namespace storm { std::shared_ptr createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); std::shared_ptr createMultiObjectiveFormula(std::vector> const& subformulas); + storm::jani::Property createProperty(boost::optional const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr const& formula); + storm::jani::Property createPropertyWithDefaultFilterType(boost::optional const& propertyName, std::shared_ptr const& formula); + // An error handler function. phoenix::function handler; diff --git a/src/storm/parser/PrismParser.cpp b/src/storm/parser/PrismParser.cpp index b6241731a..436d27c5d 100644 --- a/src/storm/parser/PrismParser.cpp +++ b/src/storm/parser/PrismParser.cpp @@ -99,7 +99,7 @@ namespace storm { definedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool") >> identifier >> qi::lit("=")) > expression_ > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDefinedBooleanConstant, phoenix::ref(*this), qi::_1, qi::_2)]; definedBooleanConstantDefinition.name("defined boolean constant declaration"); - definedIntegerConstantDefinition = ((qi::lit("const") >> qi::lit("int") >> identifier >> qi::lit("=")) > expression_ >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDefinedIntegerConstant, phoenix::ref(*this), qi::_1, qi::_2)]; + definedIntegerConstantDefinition = ((qi::lit("const") >> -qi::lit("int") >> identifier >> qi::lit("=")) > expression_ >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDefinedIntegerConstant, phoenix::ref(*this), qi::_1, qi::_2)]; definedIntegerConstantDefinition.name("defined integer constant declaration"); definedDoubleConstantDefinition = ((qi::lit("const") >> qi::lit("double") >> identifier >> qi::lit("=")) > expression_ > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDefinedDoubleConstant, phoenix::ref(*this), qi::_1, qi::_2)]; diff --git a/src/storm/storage/jani/Property.h b/src/storm/storage/jani/Property.h index f97341c53..52db07fef 100644 --- a/src/storm/storage/jani/Property.h +++ b/src/storm/storage/jani/Property.h @@ -28,8 +28,9 @@ namespace storm { class FilterExpression { public: - explicit FilterExpression(std::shared_ptr formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES) : formula(formula), ft(ft) {} + FilterExpression() = default; + explicit FilterExpression(std::shared_ptr formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES) : formula(formula), ft(ft) {} std::shared_ptr const& getFormula() const { return formula; @@ -60,6 +61,8 @@ namespace storm { class Property { public: + Property() = default; + /** * Constructs the property * @param name the name