added formula parser grammar for shields

src/storm-parsers/parser/FormulaParserGrammar.cpp

@@ -140,19 +140,34 @@ namespace storm {
             gameFormula = (qi::lit("<<") > playerCoalition > qi::lit(">>") > operatorFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGameFormula, phoenix::ref(*this), qi::_1, qi::_2)];
             gameFormula.name("game formula");
 
+            shieldExpression = (qi::lit("<") > shieldingType > qi::lit(",") > shieldComparison > qi::lit(">"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldExpression, phoenix::ref(*this), qi::_1, qi::_2)];
+
+            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]);
+            shieldingType.name("shielding type");
+
+            shieldComparison = ((qi::lit("lambda")[qi::_a = storm::logic::ShieldComparison::Relative] |
+                                 qi::lit("gamma")[qi::_a = storm::logic::ShieldComparison::Absolute]) > qi::lit("=") > qi::double_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldComparisonStruct, phoenix::ref(*this), qi::_a, qi::_1)];
+            shieldComparison.name("shield comparison type");
+
             stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula);
             stateFormula.name("state formula");
 
             formulaName = qi::lit("\"") >> identifier >> qi::lit("\"") >> qi::lit(":");
             formulaName.name("formula name");
 
+
+
             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");
 
 #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(",") > stateFormula > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] | (-formulaName >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)];
+            filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula > qi::lit(",") > stateFormula > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] | (-formulaName >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)] | (-formulaName >> shieldExpression >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldingProperty, phoenix::ref(*this), qi::_1, qi::_3, qi::_2)];
             filterProperty.name("filter property");
 
 #pragma clang diagnostic pop
@@ -490,6 +505,23 @@ namespace storm {
             }
         }
 
+        std::pair<storm::logic::ShieldComparison, double> FormulaParserGrammar::createShieldComparisonStruct(storm::logic::ShieldComparison comparisonType, double value) {
+            return std::make_pair(comparisonType, value);
+        }
+
+        storm::logic::ShieldExpression FormulaParserGrammar::createShieldExpression(storm::logic::ShieldingType type, std::pair<storm::logic::ShieldComparison, double> comparisonStruct) {
+            return storm::logic::ShieldExpression(type, comparisonStruct.first, comparisonStruct.second);
+        }
+
+        storm::jani::Property FormulaParserGrammar::createShieldingProperty(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula, storm::logic::ShieldExpression 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<boost::variant<std::string, storm::storage::PlayerIndex>> const& playerIds) const {
             return storm::logic::PlayerCoalition(playerIds);
         }

src/storm-parsers/parser/FormulaParserGrammar.h

@@ -205,12 +205,19 @@ namespace storm {
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> quantileFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> gameFormula;
 
+            qi::rule<Iterator, storm::logic::ShieldExpression, Skipper> shieldExpression;
+            qi::rule<Iterator, storm::logic::ShieldingType, Skipper> shieldingType;
+            qi::rule<Iterator, std::pair<storm::logic::ShieldComparison, double>, qi::locals<storm::logic::ShieldComparison>, Skipper> shieldComparison;
+
             // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser).
             boost::spirit::qi::real_parser<double, boost::spirit::qi::strict_real_policies<double>> strict_double;
 
             storm::logic::PlayerCoalition createPlayerCoalition(std::vector<boost::variant<std::string, storm::storage::PlayerIndex>> const& playerIds) const;
             std::shared_ptr<storm::logic::Formula const> createGameFormula(storm::logic::PlayerCoalition const& coalition, std::shared_ptr<storm::logic::Formula const> const& subformula) const;
 
+            std::pair<storm::logic::ShieldComparison, double> createShieldComparisonStruct(storm::logic::ShieldComparison comparisonType, double value);
+            storm::logic::ShieldExpression createShieldExpression(storm::logic::ShieldingType type, std::pair<storm::logic::ShieldComparison, double> comparisonStruct);
+
             bool areConstantDefinitionsAllowed() const;
             void addConstant(std::string const& name, ConstantDataType type, boost::optional<storm::expressions::Expression> const& expression);
             void addProperty(std::vector<storm::jani::Property>& properties, boost::optional<std::string> const& name, std::shared_ptr<storm::logic::Formula const> const& formula);
@@ -246,6 +253,7 @@ namespace storm {
             std::set<storm::expressions::Variable> getUndefinedConstants(std::shared_ptr<storm::logic::Formula const> const& formula) const;
             storm::jani::Property createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states);
             storm::jani::Property createPropertyWithDefaultFilterTypeAndStates(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula);
+            storm::jani::Property createShieldingProperty(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula, storm::logic::ShieldExpression);
 
             // An error handler function.
             phoenix::function<SpiritErrorHandler> handler;