further debugging of game-based abstraction

src/storm/abstraction/MenuGameRefiner.cpp

@@ -14,6 +14,8 @@
 #include "storm/utility/solver.h"
 #include "storm/utility/shortestPaths.h"
 
+#include "storm/parser/ExpressionParser.h"
+
 #include "storm/solver/MathsatSmtSolver.h"
 
 #include "storm/models/symbolic/StandardRewardModel.h"
@@ -76,7 +78,7 @@ namespace storm {
             addPredicatesEagerly = abstractionSettings.isUseEagerRefinementSet();
             
             equivalenceChecker.addConstraints(abstractor.getAbstractionInformation().getConstraints());
-            if (storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isAddAllGuardsSet()) {
+            if (abstractionSettings.isAddAllGuardsSet()) {
                 std::vector<storm::expressions::Expression> guards;
                 
                 std::pair<uint64_t, uint64_t> player1Choices = this->abstractor.get().getPlayer1ChoiceRange();
@@ -91,11 +93,34 @@ namespace storm {
                 this->abstractor.get().notifyGuardsArePredicates();
                 addedAllGuardsFlag = true;
             }
+            
+            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;
+                for (auto const& variableTypePair : expressionManager) {
+                    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);
+                }
+
+                // Finally reverse the list, because we take the predicates from the back.
+                std::reverse(refinementPredicatesToInject.begin(), refinementPredicatesToInject.end());
+            }
         }
         
         template<storm::dd::DdType Type, typename ValueType>
-        void MenuGameRefiner<Type, ValueType>::refine(std::vector<storm::expressions::Expression> const& predicates) const {
-            performRefinement(createGlobalRefinement(preprocessPredicates(predicates, RefinementPredicates::Source::Manual)));
+        void MenuGameRefiner<Type, ValueType>::refine(std::vector<storm::expressions::Expression> const& predicates, bool allowInjection) const {
+            performRefinement(createGlobalRefinement(preprocessPredicates(predicates, RefinementPredicates::Source::Manual)), allowInjection);
         }
         
         template<storm::dd::DdType Type, typename ValueType>
@@ -279,10 +304,6 @@ namespace storm {
                 // Decode both choices to explicit mappings.
                 std::map<uint64_t, std::pair<storm::storage::BitVector, ValueType>> lowerChoiceUpdateToSuccessorMapping = abstractionInformation.template decodeChoiceToUpdateSuccessorMapping<ValueType>(lowerChoice);
                 std::map<uint64_t, std::pair<storm::storage::BitVector, ValueType>> upperChoiceUpdateToSuccessorMapping = abstractionInformation.template decodeChoiceToUpdateSuccessorMapping<ValueType>(upperChoice);
-                
-                lowerChoice.template toAdd<ValueType>().exportToDot("lower.dot");
-                upperChoice.template toAdd<ValueType>().exportToDot("upper.dot");
-
                 STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode (" << lowerChoiceUpdateToSuccessorMapping.size() << " vs. " << upperChoiceUpdateToSuccessorMapping.size() << ").");
                 
                 // First, sort updates according to probability mass.
@@ -536,7 +557,11 @@ namespace storm {
                 if (additionalPredicates.get().getSource() == RefinementPredicates::Source::Guard) {
                     return additionalPredicates.get();
                 } else {
-                    predicates.get().addPredicates(additionalPredicates.get().getPredicates());
+                    if (!predicates) {
+                        predicates = additionalPredicates;
+                    } else {
+                        predicates.get().addPredicates(additionalPredicates.get().getPredicates());
+                    }
                 }
             }
             
@@ -1569,14 +1594,20 @@ namespace storm {
         }
         
         template<storm::dd::DdType Type, typename ValueType>
-        void MenuGameRefiner<Type, ValueType>::performRefinement(std::vector<RefinementCommand> const& refinementCommands) const {
-            for (auto const& command : refinementCommands) {
-                STORM_LOG_INFO("Refining with " << command.getPredicates().size() << " predicates.");
-                for (auto const& predicate : command.getPredicates()) {
-                    STORM_LOG_INFO(predicate);
-                }
-                if (!command.getPredicates().empty()) {
-                    abstractor.get().refine(command);
+        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()}));
+                refinementPredicatesToInject.pop_back();
+            } else {
+                for (auto const& command : refinementCommands) {
+                    STORM_LOG_INFO("Refining with " << command.getPredicates().size() << " predicates.");
+                    for (auto const& predicate : command.getPredicates()) {
+                        STORM_LOG_INFO(predicate);
+                    }
+                    if (!command.getPredicates().empty()) {
+                        abstractor.get().refine(command);
+                    }
                 }
             }
             

src/storm/abstraction/MenuGameRefiner.h

@@ -107,8 +107,10 @@ namespace storm {
              * Refines the abstractor with the given predicates.
              *
              * @param predicates The predicates to use for refinement.
+             * @param allowInjection If true, the refiner is free to inject manually-specified refinement predicates
+             * instead of the provided ones.
              */
-            void refine(std::vector<storm::expressions::Expression> const& predicates) const;
+            void refine(std::vector<storm::expressions::Expression> const& predicates, bool allowInjection = true) const;
             
             /*!
              * Refines the abstractor based on the qualitative result by trying to derive suitable predicates.
@@ -170,7 +172,7 @@ namespace storm {
             boost::optional<RefinementPredicates> derivePredicatesFromInterpolationKShortestPaths(storm::dd::Odd const& odd, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Grouping, std::vector<uint64_t> const& player1Labeling, std::vector<uint64_t> const& player2Labeling, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ValueType minProbability, ValueType maxProbability, ExplicitGameStrategyPair const& maxStrategyPair) const;
             boost::optional<RefinementPredicates> derivePredicatesFromInterpolationReversedPath(storm::dd::Odd const& odd, storm::expressions::ExpressionManager& interpolationManager, std::vector<uint64_t> const& reversedPath, std::vector<uint64_t> const& stateToOffset, std::vector<uint64_t> const& player1Labels) const;
 
-            void performRefinement(std::vector<RefinementCommand> const& refinementCommands) const;
+            void performRefinement(std::vector<RefinementCommand> const& refinementCommands, bool allowInjection = true) const;
             
             /// The underlying abstractor to refine.
             std::reference_wrapper<MenuGameAbstractor<Type, ValueType>> abstractor;
@@ -193,6 +195,10 @@ 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;
+            
             /// The heuristic to use for pivot block selection.
             storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic;
             

src/storm/abstraction/prism/CommandAbstractor.cpp

@@ -23,7 +23,7 @@ namespace storm {
     namespace abstraction {
         namespace prism {
             template <storm::dd::DdType DdType, typename ValueType>
-            CommandAbstractor<DdType, ValueType>::CommandAbstractor(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), useDecomposition(useDecomposition), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!command.getGuardExpression()}, smtSolverFactory) {
+            CommandAbstractor<DdType, ValueType>::CommandAbstractor(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition, bool debug) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), useDecomposition(useDecomposition), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!command.getGuardExpression()}, smtSolverFactory), debug(debug) {
                 
                 // Make the second component of relevant predicates have the right size.
                 relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates());
@@ -205,16 +205,22 @@ namespace storm {
                 relevantBlockPartition = std::move(cleanedRelevantBlockPartition);
                 
                 STORM_LOG_TRACE("Decomposition into " << relevantBlockPartition.size() << " blocks.");
-//                for (auto const& block : relevantBlockPartition) {
-//                    std::set<uint64_t> blockPredicateIndices;
-//                    for (auto const& innerBlock : block) {
-//                        blockPredicateIndices.insert(localExpressionInformation.getExpressionBlock(innerBlock).begin(), localExpressionInformation.getExpressionBlock(innerBlock).end());
-//                    }
-//                    
-//                    for (auto const& predicateIndex : blockPredicateIndices) {
-//                        STORM_LOG_TRACE(abstractionInformation.get().getPredicateByIndex(predicateIndex));
-//                    }
-//                }
+                if (this->debug) {
+                    uint64_t blockIndex = 0;
+                    for (auto const& block : relevantBlockPartition) {
+                        STORM_LOG_TRACE("Predicates of block " << blockIndex << ":");
+                        std::set<uint64_t> blockPredicateIndices;
+                        for (auto const& innerBlock : block) {
+                            blockPredicateIndices.insert(localExpressionInformation.getExpressionBlock(innerBlock).begin(), localExpressionInformation.getExpressionBlock(innerBlock).end());
+                        }
+                        
+                        for (auto const& predicateIndex : blockPredicateIndices) {
+                            STORM_LOG_TRACE(abstractionInformation.get().getPredicateByIndex(predicateIndex));
+                        }
+                        
+                        ++blockIndex;
+                    }
+                }
                 
                 std::set<storm::expressions::Variable> variablesContainedInGuard = command.get().getGuardExpression().getVariables();
                 

src/storm/abstraction/prism/CommandAbstractor.h

@@ -56,7 +56,7 @@ namespace storm {
                  * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
                  * @param useDecomposition A flag indicating whether to use the decomposition during abstraction.
                  */
-                CommandAbstractor(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition);
+                CommandAbstractor(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition, bool debug);
                                
                 /*!
                  * Refines the abstract command with the given predicates.
@@ -268,6 +268,9 @@ namespace storm {
                 
                 // A state-set abstractor used to determine the bottom states if not all guards were added.
                 StateSetAbstractor<DdType, ValueType> bottomStateAbstractor;
+                
+                // A flag that indicates whether or not debug mode is enabled.
+                bool debug;
             };
         }
     }

src/storm/abstraction/prism/ModuleAbstractor.cpp

@@ -23,12 +23,12 @@ namespace storm {
             using storm::settings::modules::AbstractionSettings;
             
             template <storm::dd::DdType DdType, typename ValueType>
-            ModuleAbstractor<DdType, ValueType>::ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) {
+            ModuleAbstractor<DdType, ValueType>::ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition, bool debug) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) {
                 
                 // For each concrete command, we create an abstract counterpart.
                 uint64_t counter = 0;
                 for (auto const& command : module.getCommands()) {
-                    commands.emplace_back(command, abstractionInformation, smtSolverFactory, useDecomposition);
+                    commands.emplace_back(command, abstractionInformation, smtSolverFactory, useDecomposition, debug);
                     ++counter;
                 }
             }

src/storm/abstraction/prism/ModuleAbstractor.h

@@ -38,7 +38,7 @@ namespace storm {
                  * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
                  * @param useDecomposition A flag that governs whether to use the decomposition in the abstraction.
                  */
-                ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition);
+                ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition, bool debug);
                 
                 ModuleAbstractor(ModuleAbstractor const&) = default;
                 ModuleAbstractor& operator=(ModuleAbstractor const&) = default;

src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -65,9 +65,11 @@ namespace storm {
                 abstractionInformation.createEncodingVariables(static_cast<uint_fast64_t>(std::ceil(std::log2(totalNumberOfCommands))), 64, static_cast<uint_fast64_t>(std::ceil(std::log2(maximalUpdateCount))));
                 
                 // For each module of the concrete program, we create an abstract counterpart.
-                bool useDecomposition = storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isUseDecompositionSet();
+                auto const& settings = storm::settings::getModule<storm::settings::modules::AbstractionSettings>();
+                bool useDecomposition = settings.isUseDecompositionSet();
+                bool debug = settings.isDebugSet();
                 for (auto const& module : program.getModules()) {
-                    this->modules.emplace_back(module, abstractionInformation, this->smtSolverFactory, useDecomposition);
+                    this->modules.emplace_back(module, abstractionInformation, this->smtSolverFactory, useDecomposition, debug);
                 }
                 
                 // Retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later.
@@ -154,10 +156,12 @@ namespace storm {
                                 
                 // Construct a set of all unnecessary variables, so we can abstract from it.
                 std::set<storm::expressions::Variable> variablesToAbstract(abstractionInformation.getPlayer1VariableSet(abstractionInformation.getPlayer1VariableCount()));
+                std::set<storm::expressions::Variable> successorAndAuxVariables(abstractionInformation.getSuccessorVariables());
                 auto player2Variables = abstractionInformation.getPlayer2VariableSet(game.numberOfPlayer2Variables);
                 variablesToAbstract.insert(player2Variables.begin(), player2Variables.end());
                 auto auxVariables = abstractionInformation.getAuxVariableSet(0, abstractionInformation.getAuxVariableCount());
                 variablesToAbstract.insert(auxVariables.begin(), auxVariables.end());
+                successorAndAuxVariables.insert(auxVariables.begin(), auxVariables.end());
                 
                 storm::utility::Stopwatch relevantStatesWatch(true);
                 storm::dd::Bdd<DdType> nonTerminalStates = this->abstractionInformation.getDdManager().getBddOne();
@@ -173,16 +177,17 @@ namespace storm {
                 relevantStatesWatch.stop();
                 
                 storm::dd::Bdd<DdType> validBlocks = validBlockAbstractor.getValidBlocks();
+
+                // Compute the choices with only valid successors so we can restrict the game to these.
+                
+                auto choicesWithOnlyValidSuccessors = !game.bdd.andExists(!validBlocks.swapVariables(abstractionInformation.getSourceSuccessorVariablePairs()), successorAndAuxVariables) && game.bdd.existsAbstract(successorAndAuxVariables);
                 
                 // Do a reachability analysis on the raw transition relation.
-                storm::dd::Bdd<DdType> transitionRelation = nonTerminalStates && game.bdd.existsAbstract(variablesToAbstract);
-                storm::dd::Bdd<DdType> initialStates = initialStateAbstractor.getAbstractStates();
-                if (program.get().hasInitialConstruct()) {
-                    initialStates &= validBlocks;
-                }
+                storm::dd::Bdd<DdType> extendedTransitionRelation = validBlocks && nonTerminalStates && game.bdd && choicesWithOnlyValidSuccessors;
+                storm::dd::Bdd<DdType> transitionRelation = extendedTransitionRelation.existsAbstract(variablesToAbstract);
+                storm::dd::Bdd<DdType> initialStates = initialStateAbstractor.getAbstractStates() && validBlocks;
                 initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables());
                 storm::dd::Bdd<DdType> reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables());
-                reachableStates &= validBlocks;
 
                 relevantStatesWatch.start();
                 if (this->isRestrictToRelevantStatesSet() && this->hasTargetStateExpression()) {
@@ -222,7 +227,7 @@ namespace storm {
                 // Construct the transition matrix by cutting away the transitions of unreachable states.
                 // Note that we also restrict the successor states of transitions, because there might be successors
                 // that are not in the relevant we restrict to.
-                storm::dd::Add<DdType, ValueType> transitionMatrix = (game.bdd && reachableStates && reachableStates.swapVariables(abstractionInformation.getSourceSuccessorVariablePairs())).template toAdd<ValueType>();
+                storm::dd::Add<DdType, ValueType> transitionMatrix = (extendedTransitionRelation && reachableStates && reachableStates.swapVariables(abstractionInformation.getSourceSuccessorVariablePairs())).template toAdd<ValueType>();
                 transitionMatrix *= commandUpdateProbabilitiesAdd;
                 transitionMatrix += deadlockTransitions;
                 

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -372,7 +372,7 @@ namespace storm {
                 // Extend the values of the maybe states by the qualitative values.
                 result.values += min ? qualitativeResult.prob1Min.getPlayer1States().template toAdd<ValueType>() : qualitativeResult.prob1Max.getPlayer1States().template toAdd<ValueType>();
             } else {
-                STORM_LOG_TRACE("No maybe states.");
+                STORM_LOG_TRACE("No " << (player2Direction == storm::OptimizationDirection::Minimize ? "min" : "max") << " maybe states.");
 
                 // Extend the values of the maybe states by the qualitative values.
                 result.values += min ? qualitativeResult.prob1Min.getPlayer1States().template toAdd<ValueType>() : qualitativeResult.prob1Max.getPlayer1States().template toAdd<ValueType>();
@@ -545,7 +545,7 @@ namespace storm {
             
             // Create a refiner that can be used to refine the abstraction when needed.
             storm::abstraction::MenuGameRefiner<Type, ValueType> refiner(*abstractor, smtSolverFactory->create(preprocessedModel.getManager()));
-            refiner.refine(initialPredicates);
+            refiner.refine(initialPredicates, false);
 
             storm::dd::Bdd<Type> globalConstraintStates = abstractor->getStates(constraintExpression);
             storm::dd::Bdd<Type> globalTargetStates = abstractor->getStates(targetStateExpression);

src/storm/settings/modules/AbstractionSettings.cpp

@@ -28,6 +28,8 @@ namespace storm {
             const std::string AbstractionSettings::rankRefinementPredicatesOptionName = "rankpred";
             const std::string AbstractionSettings::constraintsOptionName = "constraints";
             const std::string AbstractionSettings::useEagerRefinementOptionName = "eagerref";
+            const std::string AbstractionSettings::debugOptionName = "debug";
+            const std::string AbstractionSettings::injectRefinementPredicatesOption = "injectref";
             
             AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> methods = {"games", "bisimulation", "bisim"};
@@ -104,6 +106,14 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("constraints", "The constraints to use.").build())
                                 .build());
 
+                this->addOption(storm::settings::OptionBuilder(moduleName, injectRefinementPredicatesOption, true, "Specifies predicates used by the refinement instead of the derived predicates.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("predicates", "The (semicolon-separated) refinement predicates to use.").build())
+                                .build());
+                
+                this->addOption(storm::settings::OptionBuilder(moduleName, debugOptionName, true, "Sets whether to enable debug mode.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff))
+                                             .setDefaultValueString("off").build())
+                                .build());
             }
             
             AbstractionSettings::Method AbstractionSettings::getAbstractionRefinementMethod() const {
@@ -210,6 +220,18 @@ namespace storm {
                 return this->getOption(useEagerRefinementOptionName).getArgumentByName("value").getValueAsString() == "on";
             }
             
+            bool AbstractionSettings::isDebugSet() const {
+                return this->getOption(debugOptionName).getArgumentByName("value").getValueAsString() == "on";
+            }
+            
+            bool AbstractionSettings::isInjectRefinementPredicatesSet() const {
+                return this->getOption(injectRefinementPredicatesOption).getHasOptionBeenSet();
+            }
+            
+            std::string AbstractionSettings::getInjectedRefinementPredicates() const {
+                return this->getOption(injectRefinementPredicatesOption).getArgumentByName("predicates").getValueAsString();
+            }
+            
         }
     }
 }

src/storm/settings/modules/AbstractionSettings.h

@@ -147,6 +147,21 @@ namespace storm {
                  */
                 bool isUseEagerRefinementSet() const;
                 
+                /*!
+                 * Retrieves whether the debug option was set.
+                 */
+                bool isDebugSet() const;
+                
+                /*!
+                 * Retrieves whether the option to inject the refinement predicates is set.
+                 */
+                bool isInjectRefinementPredicatesSet() const;
+                
+                /*!
+                 * Retrieves a string containing refinement predicates to inject (if there are any).
+                 */
+                std::string getInjectedRefinementPredicates() const;
+                
                 const static std::string moduleName;
                 
             private:
@@ -165,6 +180,8 @@ namespace storm {
                 const static std::string rankRefinementPredicatesOptionName;
                 const static std::string constraintsOptionName;
                 const static std::string useEagerRefinementOptionName;
+                const static std::string debugOptionName;
+                const static std::string injectRefinementPredicatesOption;
             };
             
         }