From 3732cef1acb5c4d71e854a7b84333d5531dfbb28 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 10 Sep 2021 13:58:08 +0200 Subject: [PATCH] reintroduced shields to formula parser --- .../parser/FormulaParserGrammar.cpp | 127 ++++++++++++------ .../parser/FormulaParserGrammar.h | 11 ++ 2 files changed, 98 insertions(+), 40 deletions(-) diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 13b56d8a9..ea96f31a2 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -179,11 +179,29 @@ namespace storm { constantDefinition = (qi::lit("const") > -(qi::lit("int")[qi::_a = ConstantDataType::Integer] | qi::lit("bool")[qi::_a = ConstantDataType::Bool] | qi::lit("double")[qi::_a = ConstantDataType::Rational]) >> identifier >> -(qi::lit("=") > expressionParser))[phoenix::bind(&FormulaParserGrammar::addConstant, phoenix::ref(*this), qi::_1, qi::_a, qi::_2)]; constantDefinition.name("constant definition"); + // Shielding properties + shieldExpression = (qi::lit("<") > label > qi::lit(",") > shieldingType > -(qi::lit(",") > shieldComparison) > qi::lit(">"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldExpression, phoenix::ref(*this), qi::_2, qi::_1, qi::_3)]; + + shieldExpression.name("shield expression"); + + shieldingType = (qi::lit("PreSafety")[qi::_val = storm::logic::ShieldingType::PreSafety] | + qi::lit("PostSafety")[qi::_val = storm::logic::ShieldingType::PostSafety] | + qi::lit("Optimal")[qi::_val = storm::logic::ShieldingType::Optimal]) > -qi::lit("Shield"); + shieldingType.name("shielding type"); + + probability = qi::double_[qi::_pass = (qi::_1 >= 0) & (qi::_1 <= 1.0), qi::_val = qi::_1 ]; + probability.name("double between 0 and 1"); + + shieldComparison = ((qi::lit("lambda")[qi::_a = storm::logic::ShieldComparison::Relative] | + qi::lit("gamma")[qi::_a = storm::logic::ShieldComparison::Absolute]) > qi::lit("=") > probability)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldComparisonStruct, phoenix::ref(*this), qi::_a, qi::_1)]; + shieldComparison.name("shield comparison type"); + #pragma clang diagnostic push #pragma clang diagnostic ignored "-Woverloaded-shift-op-parentheses" filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > topLevelFormula > qi::lit(",") > formula(FormulaKind::State, storm::logic::FormulaContext::Undefined)> qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] | - (-formulaName >> topLevelFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)]; + (-formulaName >> topLevelFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)] | + (-formulaName >> shieldExpression >> topLevelFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldingProperty, phoenix::ref(*this), qi::_1, qi::_3, qi::_2)]; filterProperty.name("filter property"); #pragma clang diagnostic pop @@ -195,45 +213,45 @@ namespace storm { start.name("start"); // Enable the following lines to print debug output for most the rules. -// debug(rewardModelName) -// debug(rewardMeasureType) -// debug(operatorFormula) -// debug(labelFormula) -// debug(expressionFormula) -// debug(booleanLiteralFormula) -// debug(atomicPropositionFormula) -// debug(basicPropositionalFormula) -// debug(negationPropositionalFormula) -// debug(andLevelPropositionalFormula) -// debug(orLevelPropositionalFormula) -// debug(propositionalFormula) -// debug(timeBoundReference) -// debug(timeBound) -// debug(timeBounds) -// debug(eventuallyFormula) -// debug(nextFormula) -// debug(globallyFormula) -// debug(hoaPathFormula) -// debug(multiBoundedPathFormula) -// debug(prefixOperatorPathFormula) -// debug(basicPathFormula) -// debug(untilLevelPathFormula) -// debug(pathFormula) -// debug(longRunAverageRewardFormula) -// debug(instantaneousRewardFormula) -// debug(cumulativeRewardFormula) -// debug(totalRewardFormula) -// debug(playerCoalition) -// debug(gameFormula) -// debug(multiOperatorFormula) -// debug(quantileBoundVariable) -// debug(quantileFormula) -// debug(formula) -// debug(topLevelFormula) -// debug(formulaName) -// debug(filterProperty) -// debug(constantDefinition ) -// debug(start) + //debug(rewardModelName); + //debug(rewardMeasureType); + //debug(operatorFormula); + //debug(labelFormula); + //debug(expressionFormula); + //debug(booleanLiteralFormula); + //debug(atomicPropositionFormula); + //debug(basicPropositionalFormula); + //debug(negationPropositionalFormula); + //debug(andLevelPropositionalFormula); + //debug(orLevelPropositionalFormula); + //debug(propositionalFormula); + //debug(timeBoundReference); + //debug(timeBound); + //debug(timeBounds); + //debug(eventuallyFormula); + //debug(nextFormula); + //debug(globallyFormula); + //debug(hoaPathFormula); + //debug(multiBoundedPathFormula); + //debug(prefixOperatorPathFormula); + //debug(basicPathFormula); + //debug(untilLevelPathFormula); + //debug(pathFormula); + //debug(longRunAverageRewardFormula); + //debug(instantaneousRewardFormula); + //debug(cumulativeRewardFormula); + //debug(totalRewardFormula); + ////debug(playerCoalition); + //debug(gameFormula); + //debug(multiOperatorFormula); + //debug(quantileBoundVariable); + //debug(quantileFormula); + //debug(formula); + //debug(topLevelFormula); + //debug(formulaName); + //debug(filterProperty); + ////debug(constantDefinition); + //debug(start); // Enable error reporting. qi::on_error(rewardModelName, handler(qi::_1, qi::_2, qi::_3, qi::_4)); @@ -386,6 +404,11 @@ namespace storm { } } + 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(boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, std::shared_ptr const& subformula) const { if (timeBounds && !timeBounds.get().empty()) { std::vector> lowerBounds, upperBounds; @@ -401,6 +424,7 @@ namespace storm { 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)); @@ -619,6 +643,29 @@ namespace storm { } } + std::pair FormulaParserGrammar::createShieldComparisonStruct(storm::logic::ShieldComparison comparisonType, double value) { + return std::make_pair(comparisonType, value); + } + + std::shared_ptr FormulaParserGrammar::createShieldExpression(storm::logic::ShieldingType type, std::string name, boost::optional> comparisonStruct) { + if(comparisonStruct.is_initialized()) { + STORM_LOG_WARN_COND(type != storm::logic::ShieldingType::Optimal , "Comparison for optimal shield will be ignored."); + return std::shared_ptr(new storm::logic::ShieldExpression(type, name, comparisonStruct.get().first, comparisonStruct.get().second)); + } else { + STORM_LOG_THROW(type == storm::logic::ShieldingType::Optimal , storm::exceptions::WrongFormatException, "Construction of safety shield needs a comparison parameter (lambda or gamma)"); + return std::shared_ptr(new storm::logic::ShieldExpression(type, name)); + } + } + + storm::jani::Property FormulaParserGrammar::createShieldingProperty(boost::optional const& propertyName, std::shared_ptr const& formula, std::shared_ptr const& shieldExpression) { + ++propertyCount; + if (propertyName) { + return storm::jani::Property(propertyName.get(), formula, this->getUndefinedConstants(formula), shieldExpression); + } else { + return storm::jani::Property(std::to_string(propertyCount), formula, this->getUndefinedConstants(formula), shieldExpression); + } + } + storm::logic::PlayerCoalition FormulaParserGrammar::createPlayerCoalition(std::vector> const& playerIds) const { return storm::logic::PlayerCoalition(playerIds); } diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index fca3b3a1c..9f0953577 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -234,6 +234,12 @@ namespace storm { }; qi::rule, Skipper> constantDefinition; + // Shielding properties + qi::rule(), Skipper> shieldExpression; + qi::rule shieldingType; + qi::rule probability; + qi::rule, qi::locals, Skipper> shieldComparison; + // Start symbol qi::rule(), Skipper> start; @@ -242,6 +248,9 @@ namespace storm { storm::logic::PlayerCoalition createPlayerCoalition(std::vector> const& playerIds) const; std::shared_ptr createGameFormula(storm::logic::PlayerCoalition const& coalition, std::shared_ptr const& subformula) const; + std::pair createShieldComparisonStruct(storm::logic::ShieldComparison comparisonType, double value); + std::shared_ptr createShieldExpression(storm::logic::ShieldingType type, std::string name, boost::optional> comparisonStruct); + bool areConstantDefinitionsAllowed() const; void addConstant(std::string const& name, ConstantDataType type, boost::optional const& expression); void addProperty(std::vector& properties, boost::optional const& name, std::shared_ptr const& formula); @@ -259,6 +268,7 @@ namespace storm { std::shared_ptr createBooleanLiteralFormula(bool literal) const; std::shared_ptr createAtomicLabelFormula(std::string const& label) const; std::shared_ptr createEventuallyFormula(boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const; + //std::shared_ptr createGloballyFormula(boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, 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, boost::optional, std::shared_ptr>>> const& timeBounds, std::shared_ptr const& rightSubformula); @@ -285,6 +295,7 @@ namespace storm { std::set getUndefinedConstants(std::shared_ptr const& formula) const; storm::jani::Property createProperty(boost::optional const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr const& formula, std::shared_ptr const& states); storm::jani::Property createPropertyWithDefaultFilterTypeAndStates(boost::optional const& propertyName, std::shared_ptr const& formula); + storm::jani::Property createShieldingProperty(boost::optional const& propertyName, std::shared_ptr const& formula, std::shared_ptr const& shieldingExpression); bool isBooleanReturnType(std::shared_ptr const& formula, bool raiseErrorMessage = false); bool raiseAmbiguousNonAssociativeOperatorError(std::shared_ptr const& formula, std::string const& op);