From 1318bea87ab29f9fc9ad8ea3762288374f8fb6da Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 1 Jun 2018 23:03:34 +0200
Subject: [PATCH] adding support for manually injecting groups of refinement
 predicates

---
 src/storm/abstraction/MenuGameRefiner.cpp | 37 ++++++++++++++++-------
 src/storm/abstraction/MenuGameRefiner.h   |  6 ++--
 2 files changed, 29 insertions(+), 14 deletions(-)

diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp
index 3ccae8ab4..f829ff440 100644
--- a/src/storm/abstraction/MenuGameRefiner.cpp
+++ b/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;
@@ -110,11 +106,25 @@ namespace storm {
                     variableMapping[variableTypePair.first.getName()] = variableTypePair.first;
                 }
                 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) {
diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h
index c906fa9cd..cb6d48fd4 100644
--- a/src/storm/abstraction/MenuGameRefiner.h
+++ b/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;