From 6b931497a256a1a5a72376a1916bf0465fb98bd1 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 19 Jan 2017 16:32:35 +0100
Subject: [PATCH] added filters to parsers

---
 src/storm/cli/entrypoints.h               | 22 ++++++-------
 src/storm/parser/FormulaParserGrammar.cpp | 40 +++++++++++++++++------
 src/storm/parser/FormulaParserGrammar.h   | 25 ++++++++++++++
 src/storm/parser/PrismParser.cpp          |  2 +-
 src/storm/storage/jani/Property.h         |  5 ++-
 5 files changed, 71 insertions(+), 23 deletions(-)

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<ValueType>().sum());
-                        return;
+                        break;
                     case storm::modelchecker::FilterType::AVG:
                         STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult<ValueType>().average());
-                        return;
+                        break;
                     case storm::modelchecker::FilterType::MIN:
                         STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult<ValueType>().getMin());
-                        return;
+                        break;
                     case storm::modelchecker::FilterType::MAX:
                         STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult<ValueType>().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<typename ValueType>
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<storm::jani::Property>& properties, boost::optional<std::string> const& name, std::shared_ptr<storm::logic::Formula const> 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<bool>(manager);
         }
@@ -329,5 +328,26 @@ namespace storm {
         std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createMultiObjectiveFormula(std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas) {
             return std::shared_ptr<storm::logic::Formula const>(new storm::logic::MultiObjectiveFormula(subformulas));
         }
+                                               
+        storm::jani::Property FormulaParserGrammar::createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr<storm::logic::Formula const> 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<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> 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<char, storm::modelchecker::FilterType> {
+                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<storm::expressions::ExpressionManager const> constManager;
             std::shared_ptr<storm::expressions::ExpressionManager> manager;
@@ -135,6 +156,7 @@ namespace storm {
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> timeOperator;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> longRunAverageOperator;
             
+            qi::rule<Iterator, storm::jani::Property(), Skipper> filterProperty;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> simpleFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> stateFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> pathFormula;
@@ -201,6 +223,9 @@ namespace storm {
             std::shared_ptr<storm::logic::Formula const> createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType);
             std::shared_ptr<storm::logic::Formula const> createMultiObjectiveFormula(std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas);
             
+            storm::jani::Property createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr<storm::logic::Formula const> const& formula);
+            storm::jani::Property createPropertyWithDefaultFilterType(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula);
+            
             // An error handler function.
             phoenix::function<SpiritErrorHandler> 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<storm::logic::Formula const> formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES) : formula(formula), ft(ft) {}
+            FilterExpression() = default;
             
+            explicit FilterExpression(std::shared_ptr<storm::logic::Formula const> formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES) : formula(formula), ft(ft) {}
             
             std::shared_ptr<storm::logic::Formula const> const& getFormula() const {
                 return formula;
@@ -60,6 +61,8 @@ namespace storm {
         
         class Property {
         public:
+            Property() = default;
+            
             /**
              * Constructs the property
              * @param name the name