Merge remote-tracking branch 'remotes/origin/menu_games' into sylvanRationalFunctions

# Conflicts:
#	src/abstraction/MenuGameAbstractor.cpp
#	src/abstraction/prism/AbstractCommand.cpp


Former-commit-id: 032244f923

src/abstraction/MenuGame.cpp

@@ -5,6 +5,7 @@
 
 #include "src/storage/dd/Bdd.h"
 #include "src/storage/dd/Add.h"
+#include "src/storage/dd/DdManager.h"
 
 #include "src/models/symbolic/StandardRewardModel.h"
 
@@ -44,6 +45,11 @@ namespace storm {
         
         template<storm::dd::DdType Type, typename ValueType>
         storm::dd::Bdd<Type> MenuGame<Type, ValueType>::getStates(storm::expressions::Expression const& expression, bool negated) const {
+            if (expression.isTrue()) {
+                return this->getReachableStates();
+            } else if (expression.isFalse()) {
+                return this->getManager().getBddZero();
+            }
             auto it = expressionToBddMap.find(expression);
             STORM_LOG_THROW(it != expressionToBddMap.end(), storm::exceptions::InvalidArgumentException, "The given expression was not used in the abstraction process and can therefore not be retrieved.");
             if (negated) {

src/abstraction/MenuGameAbstractor.cpp

@@ -1 +0,0 @@
-#include "src/abstraction/MenuGameAbstractor.h"

src/abstraction/MenuGameAbstractor.h

@@ -2,14 +2,16 @@
 
 #include "src/storage/dd/DdType.h"
 
+#include "src/abstraction/MenuGame.h"
+
 namespace storm {
     namespace abstraction {
         
         template <storm::dd::DdType DdType, typename ValueType>
         class MenuGameAbstractor {
-            
+        public:
-            
+            virtual storm::abstraction::MenuGame<DdType, ValueType> abstract() = 0;
-            
+            virtual void refine(std::vector<storm::expressions::Expression> const& predicates) = 0;
         };
         
     }

src/abstraction/StateSetAbstractor.cpp

@@ -14,7 +14,7 @@ namespace storm {
     namespace abstraction {
         
         template <storm::dd::DdType DdType, typename ValueType>
-        StateSetAbstractor<DdType, ValueType>::StateSetAbstractor(AbstractionInformation<DdType>& abstractionInformation, std::set<storm::expressions::Variable> const& allVariables, std::vector<storm::expressions::Expression> const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), localExpressionInformation(allVariables), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(abstractionInformation.getDdManager().getBddZero()), constraint(abstractionInformation.getDdManager().getBddOne()) {
+        StateSetAbstractor<DdType, ValueType>::StateSetAbstractor(AbstractionInformation<DdType>& abstractionInformation, std::set<storm::expressions::Variable> const& allVariables, std::vector<storm::expressions::Expression> const& statePredicates, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), localExpressionInformation(allVariables), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(abstractionInformation.getDdManager().getBddZero()), constraint(abstractionInformation.getDdManager().getBddOne()) {
             
             // Assert all state predicates.
             for (auto const& predicate : statePredicates) {

src/abstraction/StateSetAbstractor.h

@@ -8,6 +8,7 @@
 
 #include "src/storage/dd/DdType.h"
 
+#include "src/utility/solver.h"
 #include "src/solver/SmtSolver.h"
 
 #include "src/abstraction/LocalExpressionInformation.h"
@@ -51,7 +52,7 @@ namespace storm {
              * supposed to abstract.
              * @param smtSolverFactory A factory that can create new SMT solvers.
              */
-            StateSetAbstractor(AbstractionInformation<DdType>& abstractionInformation, std::set<storm::expressions::Variable> const& allVariables, std::vector<storm::expressions::Expression> const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
+            StateSetAbstractor(AbstractionInformation<DdType>& abstractionInformation, std::set<storm::expressions::Variable> const& allVariables, std::vector<storm::expressions::Expression> const& statePredicates, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
             
             /*!
              * Refines the abstractor by making the given predicates new abstract predicates.

src/abstraction/prism/AbstractCommand.cpp

@@ -35,7 +35,7 @@ namespace storm {
 
                 // Refine the command based on all initial predicates.
                 std::vector<uint_fast64_t> allPredicateIndices(abstractionInformation.getNumberOfPredicates());
-                for (decltype(abstractionInformation.getNumberOfPredicates()) index = 0; index < abstractionInformation.getNumberOfPredicates(); ++index) {
+                for (uint_fast64_t index = 0; index < abstractionInformation.getNumberOfPredicates(); ++index) {
                     allPredicateIndices[index] = index;
                 }
                 this->refine(allPredicateIndices);

src/abstraction/prism/AbstractProgram.cpp

@@ -20,11 +20,11 @@ namespace storm {
         namespace prism {
             
             template <storm::dd::DdType DdType, typename ValueType>
-            AbstractProgram<DdType, ValueType>::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program,
+            AbstractProgram<DdType, ValueType>::AbstractProgram(storm::prism::Program const& program,
                                                                 std::vector<storm::expressions::Expression> const& initialPredicates,
-                                                                std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory,
+                                                                std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory,
                                                                 bool addAllGuards)
-            : program(program), smtSolverFactory(std::move(smtSolverFactory)), abstractionInformation(expressionManager), modules(), initialStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), {program.getInitialConstruct().getInitialStatesExpression()}, *this->smtSolverFactory), addedAllGuards(addAllGuards), bottomStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), program.getAllGuards(true), *this->smtSolverFactory), currentGame(nullptr) {
+            : program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager()), modules(), initialStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), {program.getInitialConstruct().getInitialStatesExpression()}, this->smtSolverFactory), addedAllGuards(addAllGuards), bottomStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), program.getAllGuards(true), this->smtSolverFactory), currentGame(nullptr) {
                 
                 // For now, we assume that there is a single module. If the program has more than one module, it needs
                 // to be flattened before the procedure.

src/abstraction/prism/AbstractProgram.h

@@ -7,6 +7,8 @@
 #include "src/abstraction/MenuGame.h"
 #include "src/abstraction/prism/AbstractModule.h"
 
+#include "src/storage/dd/Add.h"
+
 #include "src/storage/expressions/Expression.h"
 
 namespace storm {
@@ -43,7 +45,7 @@ namespace storm {
                  * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
                  * @param addAllGuards A flag that indicates whether all guards of the program should be added to the initial set of predicates.
                  */
-                AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory = std::make_unique<storm::utility::solver::SmtSolverFactory>(), bool addAllGuards = false);
+                AbstractProgram(storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), bool addAllGuards = false);
                 
                 AbstractProgram(AbstractProgram const&) = default;
                 AbstractProgram& operator=(AbstractProgram const&) = default;
@@ -95,7 +97,7 @@ namespace storm {
                 std::reference_wrapper<storm::prism::Program const> program;
 
                 // A factory that can be used to create new SMT solvers.
-                std::unique_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
+                std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
                 
                 // An object containing all information about the abstraction like predicates and the corresponding DDs.
                 AbstractionInformation<DdType> abstractionInformation;

src/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -0,0 +1,31 @@
+#include "src/abstraction/prism/PrismMenuGameAbstractor.h"
+
+#include "src/models/symbolic/StandardRewardModel.h"
+
+#include "src/settings/SettingsManager.h"
+#include "src/settings/modules/AbstractionSettings.h"
+
+namespace storm {
+    namespace abstraction {
+        namespace prism {
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            PrismMenuGameAbstractor<DdType, ValueType>::PrismMenuGameAbstractor(storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : abstractProgram(program, initialPredicates, smtSolverFactory, storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isAddAllGuardsSet()) {
+                // Intentionally left empty.
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::abstraction::MenuGame<DdType, ValueType> PrismMenuGameAbstractor<DdType, ValueType>::abstract() {
+                return abstractProgram.getAbstractGame();
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            void PrismMenuGameAbstractor<DdType, ValueType>::refine(std::vector<storm::expressions::Expression> const& predicates) {
+                abstractProgram.refine(predicates);
+            }
+         
+            template class PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double>;
+            template class PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double>;
+        }
+    }
+}

src/abstraction/prism/PrismMenuGameAbstractor.h

@@ -0,0 +1,26 @@
+#pragma once
+
+#include "src/abstraction/MenuGameAbstractor.h"
+
+#include "src/abstraction/prism/AbstractProgram.h"
+
+namespace storm {
+    namespace abstraction {
+        namespace prism {
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            class PrismMenuGameAbstractor : public MenuGameAbstractor<DdType, ValueType> {
+            public:
+                PrismMenuGameAbstractor(storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
+                
+                virtual storm::abstraction::MenuGame<DdType, ValueType> abstract() override;
+                virtual void refine(std::vector<storm::expressions::Expression> const& predicates) override;
+
+            private:
+                /// The abstract program that performs the actual abstraction.
+                AbstractProgram<DdType, ValueType> abstractProgram;
+            };
+            
+        }
+    }
+}

src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -1,9 +1,14 @@
 #include "src/modelchecker/abstraction/GameBasedMdpModelChecker.h"
 
+#include "src/models/symbolic/StandardRewardModel.h"
+
 #include "src/storage/expressions/ExpressionManager.h"
 
+#include "src/abstraction/prism/PrismMenuGameAbstractor.h"
+
 #include "src/logic/FragmentSpecification.h"
 
+#include "src/utility/graph.h"
 #include "src/utility/macros.h"
 
 #include "src/exceptions/NotSupportedException.h"
@@ -14,8 +19,8 @@
 namespace storm {
     namespace modelchecker {
         template<storm::dd::DdType Type, typename ValueType>
-        GameBasedMdpModelChecker<Type, ValueType>::GameBasedMdpModelChecker(storm::prism::Program const& program, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory) : originalProgram(program), smtSolverFactory(std::move(smtSolverFactory)) {
+        GameBasedMdpModelChecker<Type, ValueType>::GameBasedMdpModelChecker(storm::prism::Program const& program, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : originalProgram(program), smtSolverFactory(smtSolverFactory) {
-            STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only MDPs are supported by the game-based model checker.");
+            STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/MDPs are supported by the game-based model checker.");
                         
             // Start by preparing the program. That is, we flatten the modules if there is more than one.
             if (originalProgram.getNumberOfModules() > 1) {
@@ -46,19 +51,38 @@ namespace storm {
         template<storm::dd::DdType Type, typename ValueType>
         std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
             storm::logic::EventuallyFormula const& pathFormula = checkTask.getFormula();
-            return performGameBasedAbstractionRefinement(CheckTask<storm::logic::Formula>(pathFormula), originalProgram.getManager().boolean(true), getExpression(pathFormula.getSubformula()));
+            return performGameBasedAbstractionRefinement(checkTask.substituteFormula<storm::logic::Formula>(pathFormula), originalProgram.getManager().boolean(true), getExpression(pathFormula.getSubformula()));
         }
         
         template<storm::dd::DdType Type, typename ValueType>
         std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::performGameBasedAbstractionRefinement(CheckTask<storm::logic::Formula> const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) {
-            
             STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException, "The game-based abstraction refinement model checker can only compute the result for the initial states.");
+
+            // Set up initial predicates.
+            std::vector<storm::expressions::Expression> initialPredicates;
+            initialPredicates.push_back(targetStateExpression);
+            if (!constraintExpression.isTrue() && !constraintExpression.isFalse()) {
+                initialPredicates.push_back(constraintExpression);
+            }
+            
+            // Derive the optimization direction for player 1 (assuming menu-game abstraction).
+            storm::OptimizationDirection player1Direction = checkTask.isOptimizationDirectionSet() ? checkTask.getOptimizationDirection() : storm::OptimizationDirection::Maximize;
+            
+            storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType> abstractor(preprocessedProgram, initialPredicates, smtSolverFactory);
+            
             
             // 1. build initial abstraction based on the the constraint expression (if not 'true') and the target state expression.
+            storm::abstraction::MenuGame<Type, ValueType> game = abstractor.abstract();
+            STORM_LOG_DEBUG("Initial abstraction has " << game.getNumberOfStates() << " (player 1) states and " << game.getNumberOfTransitions() << " transitions.");
             
             // 2. solve the game wrt. to min/max as given by checkTask and min/max for the abstraction player to obtain two bounds.
             // Note that we have to deal with bottom states if not all guards were added in the beginning.
             // Also note that it might be the case that not both bounds need to be computed if there is a bound given in checkTask.
+            computeProb01States(player1Direction, game, constraintExpression, targetStateExpression);
+            
+//            std::unique_ptr<storm::utility::solver::SymbolicGameSolverFactory<Type, ValueType>> gameSolverFactory = std::make_unique<storm::utility::solver::SymbolicGameSolverFactory<Type, ValueType>>();
+//            gameSolverFactory->create(game.getTransitionMatrix(), game.getReachableStates());
+//            storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables
             
             // 3. if the bounds suffice to complete checkTask, return result now.
             
@@ -67,6 +91,26 @@ namespace storm {
             return nullptr;
         }
         
+        template<storm::dd::DdType Type, typename ValueType>
+        void GameBasedMdpModelChecker<Type, ValueType>::computeProb01States(storm::OptimizationDirection player1Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) {
+            storm::dd::Bdd<Type> transitionMatrixBdd = game.getTransitionMatrix().toBdd();
+            storm::dd::Bdd<Type> bottomStatesBdd = game.getBottomStates();
+            game.getTransitionMatrix().exportToDot("trans.dot");
+            bottomStatesBdd.template toAdd<ValueType>().exportToDot("bottom.dot");
+            
+            // Start by computing the states with probability 0/1 for the case in which player 2 minimizes.
+            storm::utility::graph::GameProb01Result<Type> prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), game.getStates(targetStateExpression), player1Direction, storm::OptimizationDirection::Minimize, true);
+            storm::utility::graph::GameProb01Result<Type> prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), game.getStates(targetStateExpression), player1Direction, storm::OptimizationDirection::Minimize, true);
+            
+            // Now compute the states with probability 0/1 for the case in which player 2 maximizes.
+            storm::utility::graph::GameProb01Result<Type> prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), game.getStates(targetStateExpression), player1Direction, storm::OptimizationDirection::Maximize, true);
+            storm::utility::graph::GameProb01Result<Type> prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), game.getStates(targetStateExpression), player1Direction, storm::OptimizationDirection::Maximize, true);
+            
+            STORM_LOG_DEBUG("Min: " << prob0Min.states.getNonZeroCount() << " no states, " << prob1Min.states.getNonZeroCount() << " yes states.");
+            STORM_LOG_DEBUG("Max: " << prob0Max.states.getNonZeroCount() << " no states, " << prob1Max.states.getNonZeroCount() << " yes states.");
+            
+        }
+        
         template<storm::dd::DdType Type, typename ValueType>
         storm::expressions::Expression GameBasedMdpModelChecker<Type, ValueType>::getExpression(storm::logic::Formula const& formula) {
             STORM_LOG_THROW(formula.isAtomicExpressionFormula() || formula.isAtomicLabelFormula(), storm::exceptions::InvalidPropertyException, "The target states have to be given as label or an expression.");

src/modelchecker/abstraction/GameBasedMdpModelChecker.h

@@ -10,6 +10,11 @@
 #include "src/storage/dd/DdType.h"
 
 namespace storm {
+    namespace abstraction {
+        template<storm::dd::DdType Type, typename ValueType>
+        class MenuGame;
+    }
+    
     namespace modelchecker {
         template<storm::dd::DdType Type, typename ValueType>
         class GameBasedMdpModelChecker : public AbstractModelChecker {
@@ -21,7 +26,7 @@ namespace storm {
              * @param program The program that implicitly specifies the model to check.
              * @param smtSolverFactory A factory used to create SMT solver when necessary.
              */
-            explicit GameBasedMdpModelChecker(storm::prism::Program const& program, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory = std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+            explicit GameBasedMdpModelChecker(storm::prism::Program const& program, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
             
             virtual ~GameBasedMdpModelChecker() override;
                         
@@ -33,6 +38,8 @@ namespace storm {
         private:
             std::unique_ptr<CheckResult> performGameBasedAbstractionRefinement(CheckTask<storm::logic::Formula> const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression);
             
+            void computeProb01States(storm::OptimizationDirection player1Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression);
+            
             storm::expressions::Expression getExpression(storm::logic::Formula const& formula);
             
             // The original program that was used to create this model checker.
@@ -43,7 +50,7 @@ namespace storm {
             storm::prism::Program preprocessedProgram;
             
             // A factory that is used for creating SMT solvers when needed.
-            std::unique_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
+            std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
         };
     }
 }

src/models/symbolic/Model.cpp

@@ -75,6 +75,11 @@ namespace storm {
             
             template<storm::dd::DdType Type, typename ValueType>
             storm::dd::Bdd<Type> Model<Type, ValueType>::getStates(storm::expressions::Expression const& expression) const {
+                if (expression.isTrue()) {
+                    return this->getReachableStates();
+                } else if (expression.isFalse()) {
+                    return manager->getBddZero();
+                }
                 STORM_LOG_THROW(rowExpressionAdapter != nullptr, storm::exceptions::InvalidOperationException, "Cannot create BDD for expression without expression adapter.");
                 return rowExpressionAdapter->translateExpression(expression).toBdd() && this->reachableStates;
             }

src/settings/SettingsManager.cpp

@@ -32,6 +32,7 @@
 #include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h"
 #include "src/settings/modules/ExplorationSettings.h"
 #include "src/settings/modules/ResourceSettings.h"
+#include "src/settings/modules/AbstractionSettings.h"
 #include "src/utility/macros.h"
 #include "src/settings/Option.h"
 
@@ -522,6 +523,7 @@ namespace storm {
             storm::settings::addModule<storm::settings::modules::ParametricSettings>();
             storm::settings::addModule<storm::settings::modules::ExplorationSettings>();
             storm::settings::addModule<storm::settings::modules::ResourceSettings>();
+            storm::settings::addModule<storm::settings::modules::AbstractionSettings>();
         }
 
     }

src/settings/modules/AbstractionSettings.cpp

@@ -0,0 +1,23 @@
+#include "src/settings/modules/AbstractionSettings.h"
+
+#include "src/settings/Option.h"
+#include "src/settings/OptionBuilder.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+         
+            const std::string AbstractionSettings::moduleName = "abstraction";
+            const std::string AbstractionSettings::addAllGuardsOptionName = "allguards";
+            
+            AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) {
+                this->addOption(storm::settings::OptionBuilder(moduleName, addAllGuardsOptionName, true, "Sets whether all guards are added as initial predicates.").build());
+            }
+            
+            bool AbstractionSettings::isAddAllGuardsSet() const {
+                return this->getOption(addAllGuardsOptionName).getHasOptionBeenSet();
+            }
+            
+        }
+    }
+}

src/settings/modules/AbstractionSettings.h

@@ -0,0 +1,34 @@
+#pragma once
+
+#include "src/settings/modules/ModuleSettings.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            /*!
+             * This class represents the settings for the abstraction procedures.
+             */
+            class AbstractionSettings : public ModuleSettings {
+            public:
+                /*!
+                 * Creates a new set of abstraction settings.
+                 */
+                AbstractionSettings();
+                
+                /*!
+                 * Retrieves whether the option to add all guards was set.
+                 *
+                 * @return True iff the option was set.
+                 */
+                bool isAddAllGuardsSet() const;
+                
+                const static std::string moduleName;
+                
+            private:
+                const static std::string addAllGuardsOptionName;
+            };
+            
+        }
+    }
+}

src/storage/prism/Program.cpp

@@ -1231,7 +1231,7 @@ namespace storm {
             return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, getActionNameToIndexMapping(), getRewardModels(), getLabels(), getInitialConstruct(), this->getOptionalSystemCompositionConstruct());
         }
         
-        Program Program::flattenModules(std::unique_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) const {
+        Program Program::flattenModules(std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) const {
             // If the current program has only one module, we can simply return a copy.
             if (this->getNumberOfModules() == 1) {
                 return Program(*this);
@@ -1512,11 +1512,7 @@ namespace storm {
             return this->indexToActionMap.rbegin()->first;
         }
         
-        storm::expressions::ExpressionManager const& Program::getManager() const {
+        storm::expressions::ExpressionManager& Program::getManager() const {
-            return *this->manager;
-        }
-        
-        storm::expressions::ExpressionManager& Program::getManager() {
             return *this->manager;
         }
         

src/storage/prism/Program.h

@@ -546,7 +546,7 @@ namespace storm {
              * @param smtSolverFactory an SMT solver factory to use. If none is given, the default one is used.
              * @return The resulting program.
              */
-            Program flattenModules(std::unique_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::unique_ptr<storm::utility::solver::SmtSolverFactory>(new storm::utility::solver::SmtSolverFactory())) const;
+            Program flattenModules(std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::shared_ptr<storm::utility::solver::SmtSolverFactory>(new storm::utility::solver::SmtSolverFactory())) const;
             
             friend std::ostream& operator<<(std::ostream& stream, Program const& program);
             
@@ -555,14 +555,7 @@ namespace storm {
              *
              * @return The manager responsible for the expressions of this program.
              */
-            storm::expressions::ExpressionManager const& getManager() const;
+            storm::expressions::ExpressionManager& getManager() const;
-
-            /*!
-             * Retrieves the manager responsible for the expressions of this program.
-             *
-             * @return The manager responsible for the expressions of this program.
-             */
-            storm::expressions::ExpressionManager& getManager();
 
             /*!
              *

src/utility/storm.h

@@ -441,7 +441,7 @@ namespace storm {
     
     template<storm::dd::DdType DdType, typename ValueType>
     std::unique_ptr<storm::modelchecker::CheckResult> verifyProgramWithAbstractionRefinementEngine(storm::prism::Program const& program, std::shared_ptr<const storm::logic::Formula> const& formula, bool onlyInitialStatesRelevant = false) {
-        STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Cannot treat non-MDP model using the abstraction refinement engine.");
+        STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Can only treat DTMCs/MDPs using the abstraction refinement engine.");
         
         // FIXME: Cudd -> ValueType, double -> ValueType
         storm::modelchecker::GameBasedMdpModelChecker<storm::dd::DdType::CUDD, double> modelchecker(program);