adding support for manually injecting groups of refinement predicates

src/storm/abstraction/MenuGameRefiner.cpp

@@ -99,10 +99,6 @@ namespace storm {
             }
             
             if (abstractionSettings.isInjectRefinementPredicatesSet()) {
-                std::string predicatesString = abstractionSettings.getInjectedRefinementPredicates();
-                std::vector<std::string> predicatesAsStrings;
-                boost::split(predicatesAsStrings, predicatesString, boost::is_any_of(";"));
-                
                 auto const& expressionManager = abstractor.getAbstractionInformation().getExpressionManager();
                 storm::parser::ExpressionParser expressionParser(expressionManager);
                 std::unordered_map<std::string, storm::expressions::Expression> variableMapping;
@@ -111,10 +107,24 @@ namespace storm {
                 }
                 expressionParser.setIdentifierMapping(variableMapping);
 
-                for (auto const& predicateString : predicatesAsStrings) {
-                    storm::expressions::Expression predicate = expressionParser.parseFromString(predicateString);
-                    STORM_LOG_TRACE("Adding special (user-provided) refinement predicate " << predicateString << ".");
-                    refinementPredicatesToInject.emplace_back(predicate);
+                std::string predicatesString = abstractionSettings.getInjectedRefinementPredicates();
+                std::vector<std::string> predicateGroupsAsStrings;
+                boost::split(predicateGroupsAsStrings, predicatesString, boost::is_any_of(";"));
+
+                for (auto const& predicateGroupString : predicateGroupsAsStrings) {
+                    std::vector<std::string> predicatesAsStrings;
+                    boost::split(predicatesAsStrings, predicateGroupString, boost::is_any_of(":"));
+                    
+                    refinementPredicatesToInject.emplace_back();
+                    for (auto const& predicateString : predicatesAsStrings) {
+                        storm::expressions::Expression predicate = expressionParser.parseFromString(predicateString);
+                        STORM_LOG_TRACE("Adding special (user-provided) refinement predicate " << predicateString << ".");
+                        refinementPredicatesToInject.back().emplace_back(predicate);
+                    }
+                    STORM_LOG_THROW(!refinementPredicatesToInject.back().empty(), storm::exceptions::InvalidArgumentException, "Expecting non-empty list of predicates to inject for each (mentioned) refinement step.");
+
+                    // Finally reverse the list, because we take the predicates from the back.
+                    std::reverse(refinementPredicatesToInject.back().begin(), refinementPredicatesToInject.back().end());
                 }
 
                 // Finally reverse the list, because we take the predicates from the back.
@@ -1639,8 +1649,13 @@ namespace storm {
         template<storm::dd::DdType Type, typename ValueType>
         void MenuGameRefiner<Type, ValueType>::performRefinement(std::vector<RefinementCommand> const& refinementCommands, bool allowInjection) const {
             if (!refinementPredicatesToInject.empty() && allowInjection) {
-                STORM_LOG_INFO("Refining with (injected) predicate " << refinementPredicatesToInject.back() << ".");
-                abstractor.get().refine(RefinementCommand({refinementPredicatesToInject.back()}));
+                STORM_LOG_INFO("Refining with (injected) predicates.");
+
+                for (auto const& predicate : refinementPredicatesToInject.back()) {
+                    STORM_LOG_INFO(predicate);
+                }
+
+                abstractor.get().refine(RefinementCommand(refinementPredicatesToInject.back()));
                 refinementPredicatesToInject.pop_back();
             } else {
                 for (auto const& command : refinementCommands) {

src/storm/abstraction/MenuGameRefiner.h

@@ -198,9 +198,9 @@ namespace storm {
             /// A flag indicating whether all guards have been used to refine the abstraction.
             bool addedAllGuardsFlag;
 
-            /// A vector of refinement predicates that are injected (starting with the *last* one in this list). If
-            // empty, the predicates are derived as usual.
-            mutable std::vector<storm::expressions::Expression> refinementPredicatesToInject;
+            /// A vector of vectors of refinement predicates that are injected (starting with the *last* one in this
+            /// list). If empty, the predicates are derived as usual.
+            mutable std::vector<std::vector<storm::expressions::Expression>> refinementPredicatesToInject;
             
             /// The heuristic to use for pivot block selection.
             storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic;