Merge branch 'future' of https://sselab.de/lab9/private/git/storm into future

Former-commit-id: 127847ebd9

src/modelchecker/reachability/MenuGameMdpModelChecker.cpp

@@ -0,0 +1,61 @@
+#include "src/modelchecker/reachability/MenuGameMdpModelChecker.h"
+
+#include "src/utility/macros.h"
+
+#include "src/exceptions/NotSupportedException.h"
+
+#include "src/modelchecker/results/CheckResult.h"
+
+namespace storm {
+    namespace modelchecker {
+        MenuGameMdpModelChecker::MenuGameMdpModelChecker(storm::prism::Program const& program, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory) : originalProgram(program), smtSolverFactory(std::move(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.");
+            
+            // Start by preparing the program. That is, we flatten the modules if there is more than one.
+            if (originalProgram.getNumberOfModules() > 1) {
+                preprocessedProgram = originalProgram.flattenModules(smtSolverFactory);
+            } else {
+                preprocessedProgram = originalProgram;
+            }
+        }
+        
+        bool MenuGameMdpModelChecker::canHandle(storm::logic::Formula const& formula) const {
+            if (formula.isProbabilityOperatorFormula()) {
+                storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula();
+                return this->canHandle(probabilityOperatorFormula.getSubformula());
+            } else if (formula.isUntilFormula() || formula.isEventuallyFormula()) {
+                if (formula.isUntilFormula()) {
+                    storm::logic::UntilFormula const& untilFormula = formula.asUntilFormula();
+                    if (untilFormula.getLeftSubformula().isPropositionalFormula() && untilFormula.getRightSubformula().isPropositionalFormula()) {
+                        return true;
+                    }
+                } else if (formula.isEventuallyFormula()) {
+                    storm::logic::EventuallyFormula const& eventuallyFormula = formula.asEventuallyFormula();
+                    if (eventuallyFormula.getSubformula().isPropositionalFormula()) {
+                        return true;
+                    }
+                }
+            }
+            return false;
+        }
+        
+        std::unique_ptr<CheckResult> MenuGameMdpModelChecker::checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula) {
+            // Depending on whether or not there is a bound, we do something slightly different here.
+            
+            return nullptr;
+        }
+        
+        std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
+            // TODO
+            
+            return nullptr;
+        }
+
+        std::unique_ptr<CheckResult> computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
+            // TODO
+
+            return nullptr;
+        }
+
+    }
+}

src/modelchecker/reachability/MenuGameMdpModelChecker.h

@@ -0,0 +1,59 @@
+#ifndef STORM_MODELCHECKER_MENUGAMEMDPMODELCHECKER_H_
+#define STORM_MODELCHECKER_MENUGAMEMDPMODELCHECKER_H_
+
+#include "src/modelchecker/AbstractModelChecker.h"
+
+#include "src/storage/prism/Program.h"
+
+#include "src/utility/solver.h"
+
+namespace storm {
+    namespace modelchecker {
+        class MenuGameMdpModelChecker : public AbstractModelChecker {
+        public:
+            /*!
+             * Constructs a model checker whose underlying model is implicitly given by the provided program. All
+             * verification calls will be answererd with respect to this model.
+             *
+             * @param program The program that implicitly specifies the model to check.
+             * @param smtSolverFactory A factory used to create SMT solver when necessary.
+             */
+            explicit MenuGameMdpModelChecker(storm::prism::Program const& program, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory);
+            
+            virtual bool canHandle(storm::logic::Formula const& formula) const override;
+            
+            virtual std::unique_ptr<CheckResult> checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula) override;
+            
+            virtual std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>()) override;
+            virtual std::unique_ptr<CheckResult> computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>()) override;
+
+        private:
+            /*!
+             * Performs game-based abstraction refinement on the model until either the precision is met or the provided
+             * proof goal was successfully proven.
+             *
+             * @param filterPredicate A predicate that needs to hold until the target predicate holds.
+             * @param targetPredicate A predicate characterizing the target states.
+             * @param precision The precision to use. This governs what difference between lower and upper bounds is
+             * acceptable.
+             * @param proofGoal A proof goal that says the probability must only be established to be above/below a given
+             * threshold. If the proof goal is met before the precision is achieved, the refinement procedure will abort
+             * and return the current result.
+             * @return A pair of values, that are under- and over-approximations of the actual probability, respectively.
+             */
+            std::pair<double, double> performGameBasedRefinement(storm::expressions::Expression const& filterPredicate, storm::expressions::Expression const& targetPredicate, double precision, boost::optional<std::pair<double, storm::logic::ComparisonType>> const& proofGoal);
+            
+            // The original program that was used to create this model checker.
+            storm::prism::Program originalProgram;
+            
+            // The preprocessed program that contains only one module and otherwhise corresponds to the semantics of the
+            // original program.
+            storm::prism::Program preprocessedProgram;
+            
+            // A factory that is used for creating SMT solvers when needed.
+            std::unique_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
+        };
+    }
+}
+
+#endif /* STORM_MODELCHECKER_MENUGAMEMDPMODELCHECKER_H_ */

src/models/sparse/Ctmc.cpp

@@ -11,7 +11,7 @@ namespace storm {
             Ctmc<ValueType, RewardModelType>::Ctmc(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::models::sparse::StateLabeling const& stateLabeling,
                                   std::unordered_map<std::string, RewardModelType> const& rewardModels,
                                   boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
-            : DeterministicModel<ValueType>(storm::models::ModelType::Ctmc, rateMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) {
+            : DeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::Ctmc, rateMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) {
                 exitRates = createExitRateVector(this->getTransitionMatrix());
             }
             
@@ -19,7 +19,7 @@ namespace storm {
             Ctmc<ValueType, RewardModelType>::Ctmc(storm::storage::SparseMatrix<ValueType>&& rateMatrix, storm::models::sparse::StateLabeling&& stateLabeling,
                                   std::unordered_map<std::string, RewardModelType>&& rewardModels,
                                   boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
-            : DeterministicModel<ValueType>(storm::models::ModelType::Ctmc, std::move(rateMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) {
+            : DeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::Ctmc, std::move(rateMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) {
                 // It is important to refer to the transition matrix here, because the given rate matrix has been move elsewhere.
                 exitRates = createExitRateVector(this->getTransitionMatrix());
             }
@@ -41,6 +41,8 @@ namespace storm {
             template class Ctmc<double>;
 
 #ifdef STORM_HAVE_CARL
+            template class Ctmc<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
+
             template class Ctmc<storm::RationalFunction>;
 #endif
             

src/models/sparse/DeterministicModel.cpp

@@ -12,7 +12,7 @@ namespace storm {
                                                               storm::models::sparse::StateLabeling const& stateLabeling,
                                                               std::unordered_map<std::string, RewardModelType> const& rewardModels,
                                                               boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
-            : Model<ValueType>(modelType, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) {
+            : Model<ValueType, RewardModelType>(modelType, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) {
                 // Intentionally left empty.
             }
             
@@ -22,13 +22,13 @@ namespace storm {
                                                               storm::models::sparse::StateLabeling&& stateLabeling,
                                                               std::unordered_map<std::string, RewardModelType>&& rewardModels,
                                                               boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
-            : Model<ValueType>(modelType, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) {
+            : Model<ValueType, RewardModelType>(modelType, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) {
                 // Intentionally left empty.
             }
             
             template <typename ValueType, typename RewardModelType>
             void DeterministicModel<ValueType, RewardModelType>::writeDotToStream(std::ostream& outStream, bool includeLabeling, storm::storage::BitVector const* subsystem, std::vector<ValueType> const* firstValue, std::vector<ValueType> const* secondValue, std::vector<uint_fast64_t> const* stateColoring, std::vector<std::string> const* colors, std::vector<uint_fast64_t>* scheduler, bool finalizeOutput) const {
-                Model<ValueType>::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false);
+                Model<ValueType, RewardModelType>::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false);
                 
                 // Simply iterate over all transitions and draw the arrows with probability information attached.
                 auto rowIt = this->getTransitionMatrix().begin();
@@ -59,6 +59,8 @@ namespace storm {
             template class DeterministicModel<float>;
             
 #ifdef STORM_HAVE_CARL
+            template class DeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
+
             template class DeterministicModel<storm::RationalFunction>;
 #endif
             

src/models/sparse/DeterministicModel.h

@@ -49,7 +49,7 @@ namespace storm {
                 
 #ifndef WINDOWS
                 DeterministicModel(DeterministicModel<ValueType, RewardModelType>&& other) = default;
-                DeterministicModel<ValueType>& operator=(DeterministicModel<ValueType, RewardModelType>&& model) = default;
+                DeterministicModel<ValueType, RewardModelType>& operator=(DeterministicModel<ValueType, RewardModelType>&& model) = default;
 #endif
                 
                 virtual void reduceToStateBasedRewards() override;

src/models/sparse/Dtmc.cpp

@@ -14,14 +14,14 @@ namespace storm {
                  storm::models::sparse::StateLabeling const& stateLabeling,
                  std::unordered_map<std::string, RewardModelType> const& rewardModels,
                  boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
-            : DeterministicModel<ValueType>(storm::models::ModelType::Dtmc, probabilityMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) {
+            : DeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::Dtmc, probabilityMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) {
                 STORM_LOG_THROW(probabilityMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid.");
             }
             
             template <typename ValueType, typename RewardModelType>
             Dtmc<ValueType, RewardModelType>::Dtmc(storm::storage::SparseMatrix<ValueType>&& probabilityMatrix, storm::models::sparse::StateLabeling&& stateLabeling,
                 std::unordered_map<std::string, RewardModelType>&& rewardModels, boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
-            : DeterministicModel<ValueType>(storm::models::ModelType::Dtmc, std::move(probabilityMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) {
+            : DeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::Dtmc, std::move(probabilityMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) {
                 STORM_LOG_THROW(probabilityMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid.");
             }
             
@@ -225,6 +225,8 @@ namespace storm {
             template class Dtmc<float>;
 
 #ifdef STORM_HAVE_CARL
+            template class Dtmc<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
+
             template class Dtmc<storm::RationalFunction>;
 #endif
 

src/models/sparse/MarkovAutomaton.cpp

@@ -15,7 +15,7 @@ namespace storm {
                                                         std::vector<ValueType> const& exitRates,
                                                         std::unordered_map<std::string, RewardModelType> const& rewardModels,
                                                         boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
-            : NondeterministicModel<ValueType>(storm::models::ModelType::MarkovAutomaton, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling), markovianStates(markovianStates), exitRates(exitRates), closed(false) {
+            : NondeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::MarkovAutomaton, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling), markovianStates(markovianStates), exitRates(exitRates), closed(false) {
                 this->turnRatesToProbabilities();
             }
             
@@ -26,7 +26,7 @@ namespace storm {
                                                         std::vector<ValueType> const& exitRates,
                                                         std::unordered_map<std::string, RewardModelType>&& rewardModels,
                                                         boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
-            : NondeterministicModel<ValueType>(storm::models::ModelType::MarkovAutomaton, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)), closed(false) {
+            : NondeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::MarkovAutomaton, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)), closed(false) {
                 this->turnRatesToProbabilities();
             }
             
@@ -124,7 +124,7 @@ namespace storm {
             
             template <typename ValueType, typename RewardModelType>
             void MarkovAutomaton<ValueType, RewardModelType>::writeDotToStream(std::ostream& outStream, bool includeLabeling, storm::storage::BitVector const* subsystem, std::vector<ValueType> const* firstValue, std::vector<ValueType> const* secondValue, std::vector<uint_fast64_t> const* stateColoring, std::vector<std::string> const* colors, std::vector<uint_fast64_t>* scheduler, bool finalizeOutput) const {
-                NondeterministicModel<ValueType>::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false);
+                NondeterministicModel<ValueType, RewardModelType>::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false);
                 
                 // Write the probability distributions for all the states.
                 for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
@@ -205,7 +205,7 @@ namespace storm {
             
             template <typename ValueType, typename RewardModelType>
             std::size_t MarkovAutomaton<ValueType, RewardModelType>::getSizeInBytes() const {
-                return NondeterministicModel<ValueType>::getSizeInBytes() + markovianStates.getSizeInBytes() + exitRates.size() * sizeof(ValueType);
+                return NondeterministicModel<ValueType, RewardModelType>::getSizeInBytes() + markovianStates.getSizeInBytes() + exitRates.size() * sizeof(ValueType);
             }
             
             template <typename ValueType, typename RewardModelType>
@@ -220,9 +220,11 @@ namespace storm {
             template class MarkovAutomaton<double>;
 //            template class MarkovAutomaton<float>;
             
-//#ifdef STORM_HAVE_CARL
-//            template class MarkovAutomaton<storm::RationalFunction>;
-//#endif
+#ifdef STORM_HAVE_CARL
+            template class MarkovAutomaton<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
+
+            template class MarkovAutomaton<storm::RationalFunction>;
+#endif
 
         } // namespace sparse
     } // namespace models

src/models/sparse/MarkovAutomaton.h

@@ -12,7 +12,7 @@ namespace storm {
              * This class represents a Markov automaton.
              */
             template<class ValueType, typename RewardModelType = StandardRewardModel<ValueType>>
-            class MarkovAutomaton : public NondeterministicModel<ValueType> {
+            class MarkovAutomaton : public NondeterministicModel<ValueType, RewardModelType> {
             public:
                 /*!
                  * Constructs a model from the given data.

src/models/sparse/Mdp.cpp

@@ -9,42 +9,42 @@
 namespace storm {
     namespace models {
         namespace sparse {
-            
+
             template <typename ValueType, typename RewardModelType>
             Mdp<ValueType, RewardModelType>::Mdp(storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
                                 storm::models::sparse::StateLabeling const& stateLabeling,
                                 std::unordered_map<std::string, RewardModelType> const& rewardModels,
                                 boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
-            : NondeterministicModel<ValueType>(storm::models::ModelType::Mdp, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) {
+            : NondeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::Mdp, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) {
                 STORM_LOG_THROW(transitionMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid.");
             }
-            
-            
+
+
             template <typename ValueType, typename RewardModelType>
             Mdp<ValueType, RewardModelType>::Mdp(storm::storage::SparseMatrix<ValueType>&& transitionMatrix,
                                 storm::models::sparse::StateLabeling&& stateLabeling,
                                 std::unordered_map<std::string, RewardModelType>&& rewardModels,
                                 boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
-            : NondeterministicModel<ValueType>(storm::models::ModelType::Mdp, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) {
+            : NondeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::Mdp, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) {
                 STORM_LOG_THROW(transitionMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid.");
             }
-            
+
             template <typename ValueType, typename RewardModelType>
-            Mdp<ValueType> Mdp<ValueType, RewardModelType>::restrictChoiceLabels(LabelSet const& enabledChoiceLabels) const {
+            Mdp<ValueType, RewardModelType> Mdp<ValueType, RewardModelType>::restrictChoiceLabels(LabelSet const& enabledChoiceLabels) const {
                 STORM_LOG_THROW(this->hasChoiceLabeling(), storm::exceptions::InvalidArgumentException, "Restriction to label set is impossible for unlabeled model.");
-                
+
                 std::vector<LabelSet> const& choiceLabeling = this->getChoiceLabeling();
-                
+
                 storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, this->getTransitionMatrix().getColumnCount(), 0, true, true);
                 std::vector<LabelSet> newChoiceLabeling;
-                
+
                 // Check for each choice of each state, whether the choice labels are fully contained in the given label set.
                 uint_fast64_t currentRow = 0;
                 for(uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
                     bool stateHasValidChoice = false;
                     for (uint_fast64_t choice = this->getTransitionMatrix().getRowGroupIndices()[state]; choice < this->getTransitionMatrix().getRowGroupIndices()[state + 1]; ++choice) {
                         bool choiceValid = std::includes(enabledChoiceLabels.begin(), enabledChoiceLabels.end(), choiceLabeling[choice].begin(), choiceLabeling[choice].end());
-                        
+
                         // If the choice is valid, copy over all its elements.
                         if (choiceValid) {
                             if (!stateHasValidChoice) {
@@ -58,7 +58,7 @@ namespace storm {
                             ++currentRow;
                         }
                     }
-                    
+
                     // If no choice of the current state may be taken, we insert a self-loop to the state instead.
                     if (!stateHasValidChoice) {
                         transitionMatrixBuilder.newRowGroup(currentRow);
@@ -67,27 +67,29 @@ namespace storm {
                         ++currentRow;
                     }
                 }
-                
-                Mdp<ValueType> restrictedMdp(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(this->getStateLabeling()),
-                                             std::unordered_map<std::string, RewardModelType>(this->getRewardModels()), boost::optional<std::vector<LabelSet>>(newChoiceLabeling));
-                
+
+                Mdp<ValueType, RewardModelType> restrictedMdp(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(this->getStateLabeling()),
+                                                              std::unordered_map<std::string, RewardModelType>(this->getRewardModels()), boost::optional<std::vector<LabelSet>>(newChoiceLabeling));
+
                 return restrictedMdp;
             }
-            
+
             template <typename ValueType, typename RewardModelType>
-            Mdp<ValueType> Mdp<ValueType, RewardModelType>::restrictActions(storm::storage::BitVector const& enabledActions) const {
+            Mdp<ValueType, RewardModelType> Mdp<ValueType, RewardModelType>::restrictActions(storm::storage::BitVector const& enabledActions) const {
                 storm::storage::SparseMatrix<ValueType> restrictedTransitions = this->getTransitionMatrix().restrictRows(enabledActions);
                 std::unordered_map<std::string, RewardModelType> newRewardModels;
                 for (auto const& rewardModel : this->getRewardModels()) {
                     newRewardModels.emplace(rewardModel.first, rewardModel.second.restrictActions(enabledActions));
                 }
-                return Mdp<ValueType>(restrictedTransitions, this->getStateLabeling(), newRewardModels, this->getOptionalChoiceLabeling());
+                return Mdp<ValueType, RewardModelType>(restrictedTransitions, this->getStateLabeling(), newRewardModels, this->getOptionalChoiceLabeling());
             }
-            
+
             template class Mdp<double>;
             template class Mdp<float>;
 
 #ifdef STORM_HAVE_CARL
+            template class Mdp<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
+
             template class Mdp<storm::RationalFunction>;
 #endif
 

src/models/sparse/Mdp.h

@@ -57,7 +57,7 @@ namespace storm {
                  * and which ones need to be ignored.
                  * @return A restricted version of the current MDP that only uses choice labels from the given set.
                  */
-                Mdp<ValueType> restrictChoiceLabels(LabelSet const& enabledChoiceLabels) const;
+                Mdp<ValueType, RewardModelType> restrictChoiceLabels(LabelSet const& enabledChoiceLabels) const;
                 
                 /*!
                  * Constructs an MDP by copying the current MDP and restricting the choices of each state to the ones given by the bitvector.
@@ -65,7 +65,7 @@ namespace storm {
                  * @param enabledActions A BitVector of lenght numberOfChoices(), which is one iff the action should be kept.
                  * @return A subMDP.
                  */
-                Mdp<ValueType> restrictActions(storm::storage::BitVector const& enabledActions) const;
+                Mdp<ValueType, RewardModelType> restrictActions(storm::storage::BitVector const& enabledActions) const;
             };
             
         } // namespace sparse

src/models/sparse/Model.cpp

@@ -300,6 +300,8 @@ namespace storm {
             template class Model<float>;
             
 #ifdef STORM_HAVE_CARL
+            template class Model<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
+
             template class Model<storm::RationalFunction>;
 #endif
             

src/models/sparse/NondeterministicModel.cpp

@@ -16,7 +16,7 @@ namespace storm {
                                                                     storm::models::sparse::StateLabeling const& stateLabeling,
                                                                     std::unordered_map<std::string, RewardModelType> const& rewardModels,
                                                                     boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
-            : Model<ValueType>(modelType, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) {
+            : Model<ValueType, RewardModelType>(modelType, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) {
                 // Intentionally left empty.
             }
             
@@ -26,7 +26,7 @@ namespace storm {
                                                                     storm::models::sparse::StateLabeling&& stateLabeling,
                                                                     std::unordered_map<std::string, RewardModelType>&& rewardModels,
                                                                     boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
-            : Model<ValueType>(modelType, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels),
+            : Model<ValueType, RewardModelType>(modelType, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels),
                                std::move(optionalChoiceLabeling)) {
                 // Intentionally left empty.
             }
@@ -79,7 +79,7 @@ namespace storm {
             
             template<typename ValueType, typename RewardModelType>
             void NondeterministicModel<ValueType, RewardModelType>::writeDotToStream(std::ostream& outStream, bool includeLabeling, storm::storage::BitVector const* subsystem, std::vector<ValueType> const* firstValue, std::vector<ValueType> const* secondValue, std::vector<uint_fast64_t> const* stateColoring, std::vector<std::string> const* colors, std::vector<uint_fast64_t>* scheduler, bool finalizeOutput) const {
-                Model<ValueType>::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false);
+                Model<ValueType, RewardModelType>::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false);
                 
                 // Write the probability distributions for all the states.
                 for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
@@ -151,6 +151,8 @@ namespace storm {
             template class NondeterministicModel<float>;
 
 #ifdef STORM_HAVE_CARL
+            template class NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
+
             template class NondeterministicModel<storm::RationalFunction>;
 #endif
 

src/models/sparse/StochasticTwoPlayerGame.cpp

@@ -15,7 +15,7 @@ namespace storm {
                                                                                          std::unordered_map<std::string, RewardModelType> const& rewardModels,
                                                                                          boost::optional<std::vector<LabelSet>> const& optionalPlayer1ChoiceLabeling,
                                                                                          boost::optional<std::vector<LabelSet>> const& optionalPlayer2ChoiceLabeling)
-            : NondeterministicModel<ValueType>(storm::models::ModelType::S2pg, player2Matrix, stateLabeling, rewardModels, optionalPlayer2ChoiceLabeling), player1Matrix(player1Matrix), player1Labels(optionalPlayer1ChoiceLabeling) {
+            : NondeterministicModel<ValueType>(storm::models::ModelType::S2pg, player2Matrix, stateLabeling, rewardModels, optionalPlayer2ChoiceLabeling), player1Matrix(player1Matrix), player1ChoiceLabeling(optionalPlayer1ChoiceLabeling) {
                 // Intentionally left empty.
             }
             
@@ -27,16 +27,46 @@ namespace storm {
                                                                                          std::unordered_map<std::string, RewardModelType>&& rewardModels,
                                                                                          boost::optional<std::vector<LabelSet>>&& optionalPlayer1ChoiceLabeling,
                                                                                          boost::optional<std::vector<LabelSet>>&& optionalPlayer2ChoiceLabeling)
-            : NondeterministicModel<ValueType>(storm::models::ModelType::S2pg, std::move(player2Matrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalPlayer2ChoiceLabeling)), player1Matrix(std::move(player1Matrix)), player1Labels(std::move(optionalPlayer1ChoiceLabeling)) {
+            : NondeterministicModel<ValueType>(storm::models::ModelType::S2pg, std::move(player2Matrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalPlayer2ChoiceLabeling)), player1Matrix(std::move(player1Matrix)), player1ChoiceLabeling(std::move(optionalPlayer1ChoiceLabeling)) {
                 // Intentionally left empty.
             }
             
+            template <typename ValueType, typename RewardModelType>
+            storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& StochasticTwoPlayerGame<ValueType, RewardModelType>::getPlayer1Matrix() const {
+                return player1Matrix;
+            }
+            
+            template <typename ValueType, typename RewardModelType>
+            storm::storage::SparseMatrix<ValueType> const& StochasticTwoPlayerGame<ValueType, RewardModelType>::getPlayer2Matrix() const {
+                return this->getTransitionMatrix();
+            }
+            
+            template <typename ValueType, typename RewardModelType>
+            bool StochasticTwoPlayerGame<ValueType, RewardModelType>::hasPlayer1ChoiceLabeling() const {
+                return static_cast<bool>(player1ChoiceLabeling);
+            }
+            
+            template <typename ValueType, typename RewardModelType>
+            std::vector<LabelSet> const& StochasticTwoPlayerGame<ValueType, RewardModelType>::getPlayer1ChoiceLabeling() const {
+                return player1ChoiceLabeling.get();
+            }
+
+            template <typename ValueType, typename RewardModelType>
+            bool StochasticTwoPlayerGame<ValueType, RewardModelType>::hasPlayer2ChoiceLabeling() const {
+                return this->hasChoiceLabeling();
+            }
+            
+            template <typename ValueType, typename RewardModelType>
+            std::vector<LabelSet> const& StochasticTwoPlayerGame<ValueType, RewardModelType>::getPlayer2ChoiceLabeling() const {
+                return this->getChoiceLabeling();
+            }
+            
             template class StochasticTwoPlayerGame<double>;
 //            template class StochasticTwoPlayerGame<float>;
             
-//#ifdef STORM_HAVE_CARL
+#ifdef STORM_HAVE_CARL
 //            template class StochasticTwoPlayerGame<storm::RationalFunction>;
-//#endif
+#endif
             
         } // namespace sparse
     } // namespace models

src/models/sparse/StochasticTwoPlayerGame.h

@@ -57,6 +57,49 @@ namespace storm {
                 StochasticTwoPlayerGame& operator=(StochasticTwoPlayerGame&& other) = default;
 #endif
                 
+                /*!
+                 * Retrieves the matrix representing the choices in player 1 states.
+                 *
+                 * @return A matrix representing the choices in player 1 states.
+                 */
+                storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& getPlayer1Matrix() const;
+
+                /*!
+                 * Retrieves the matrix representing the choices in player 2 states and the associated probability
+                 * distributions.
+                 *
+                 * @return A matrix representing the choices in player 2 states.
+                 */
+                storm::storage::SparseMatrix<ValueType> const& getPlayer2Matrix() const;
+                
+                /*!
+                 * Retrieves the whether the game has labels attached to the choices in player 1 states.
+                 *
+                 * @return True if the game has player 1 choice labels.
+                 */
+                bool hasPlayer1ChoiceLabeling() const;
+                
+                /*!
+                 * Retrieves the labels attached to the choices of player 1 states.
+                 *
+                 * @return A vector containing the labels of each player 1 choice.
+                 */
+                std::vector<LabelSet> const& getPlayer1ChoiceLabeling() const;
+
+                /*!
+                 * Retrieves whether the game has labels attached to player 2 states.
+                 *
+                 * @return True if the game has player 2 labels.
+                 */
+                bool hasPlayer2ChoiceLabeling() const;
+
+                /*!
+                 * Retrieves the labels attached to the choices of player 2 states.
+                 *
+                 * @return A vector containing the labels of each player 2 choice.
+                 */
+                std::vector<LabelSet> const& getPlayer2ChoiceLabeling() const;
+                
             private:
                 // A matrix that stores the player 1 choices. This matrix contains a row group for each player 1 node. Every
                 // row group contains a row for each choice in that player 1 node. Each such row contains exactly one
@@ -66,7 +109,7 @@ namespace storm {
                 
                 // An (optional) vector of labels attached to the choices of player 1. Each row of the matrix can be equipped
                 // with a set of labels to tag certain choices.
-                boost::optional<std::vector<LabelSet>> player1Labels;
+                boost::optional<std::vector<LabelSet>> player1ChoiceLabeling;
                 
                 // The matrix and labels for player 2 are stored in the superclass.
             };

src/parser/AutoParser.cpp

@@ -10,6 +10,8 @@
 #include "src/utility/macros.h"
 #include "src/exceptions/WrongFormatException.h"
 
+#include "src/adapters/CarlAdapter.h"
+
 #include "src/utility/cstring.h"
 #include "src/utility/OsDetection.h"
 
@@ -19,7 +21,7 @@ namespace storm {
         using namespace storm::utility::cstring;
 
         template<typename ValueType, typename RewardValueType>
-        std::shared_ptr<storm::models::sparse::Model<double>> AutoParser<ValueType, RewardValueType>::parseModel(std::string const& transitionsFilename,
+        std::shared_ptr<storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>> AutoParser<ValueType, RewardValueType>::parseModel(std::string const& transitionsFilename,
                 std::string const& labelingFilename,
                 std::string const& stateRewardFilename,
                 std::string const& transitionRewardFilename,
@@ -33,22 +35,22 @@ namespace storm {
             switch (type) {
                 case storm::models::ModelType::Dtmc:
                 {
-                    model.reset(new storm::models::sparse::Dtmc<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>(std::move(DeterministicModelParser<ValueType, RewardValueType>::parseDtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))));
+                    model = std::shared_ptr<storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>>(new storm::models::sparse::Dtmc<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>(std::move(DeterministicModelParser<ValueType, RewardValueType>::parseDtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))));
                     break;
                 }
                 case storm::models::ModelType::Ctmc:
                 {
-                    model.reset(new storm::models::sparse::Ctmc<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>(std::move(DeterministicModelParser<ValueType, RewardValueType>::parseCtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))));
+                    model = std::shared_ptr<storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>>(new storm::models::sparse::Ctmc<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>(std::move(DeterministicModelParser<ValueType, RewardValueType>::parseCtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))));
                     break;
                 }
                 case storm::models::ModelType::Mdp:
                 {
-                    model.reset(new storm::models::sparse::Mdp<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>(std::move(NondeterministicModelParser<ValueType, RewardValueType>::parseMdp(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename, choiceLabelingFilename))));
+                    model = std::shared_ptr<storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>>(new storm::models::sparse::Mdp<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>(std::move(NondeterministicModelParser<ValueType, RewardValueType>::parseMdp(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename, choiceLabelingFilename))));
                     break;
                 }
                 case storm::models::ModelType::MarkovAutomaton:
                 {
-                    model.reset(new storm::models::sparse::MarkovAutomaton<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>(storm::parser::MarkovAutomatonParser<ValueType, RewardValueType>::parseMarkovAutomaton(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)));
+                    model = std::shared_ptr<storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>>(new storm::models::sparse::MarkovAutomaton<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>(std::move(storm::parser::MarkovAutomatonParser<ValueType, RewardValueType>::parseMarkovAutomaton(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))));
                     break;
                 }
                 default:
@@ -94,6 +96,10 @@ namespace storm {
 
         // Explicitly instantiate the parser.
         template class AutoParser<double, double>;
+
+#ifdef STORM_HAVE_CARL
+        template class AutoParser<double, storm::Interval>;
+#endif
         
     } // namespace parser
 } // namespace storm

src/parser/AutoParser.h

@@ -47,7 +47,7 @@ namespace storm {
              * is meaningful, this file will not be parsed.
              * @return A shared_ptr containing the resulting model.
              */
-            static std::shared_ptr<storm::models::sparse::Model<double>> parseModel(std::string const& transitionsFilename,
+            static std::shared_ptr<storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>> parseModel(std::string const& transitionsFilename,
                     std::string const& labelingFilename,
                     std::string const& stateRewardFilename = "",
                     std::string const& transitionRewardFilename = "",

src/parser/DeterministicModelParser.cpp

@@ -9,6 +9,8 @@
 #include "src/parser/AtomicPropositionLabelingParser.h"
 #include "src/parser/SparseStateRewardParser.h"
 
+#include "src/adapters/CarlAdapter.h"
+
 namespace storm {
     namespace parser {
 
@@ -62,6 +64,10 @@ namespace storm {
         }
 
         template class DeterministicModelParser<double, double>;
+
+#ifdef STORM_HAVE_CARL
+        template class DeterministicModelParser<double, storm::Interval>;
+#endif
         
     } /* namespace parser */
 } /* namespace storm */

src/parser/DeterministicSparseTransitionParser.cpp

@@ -16,6 +16,8 @@
 #include "src/settings/SettingsManager.h"
 #include "src/settings/modules/GeneralSettings.h"
 
+#include "src/adapters/CarlAdapter.h"
+
 #include "log4cplus/logger.h"
 #include "log4cplus/loggingmacros.h"
 extern log4cplus::Logger logger;
@@ -297,5 +299,12 @@ namespace storm {
         template class DeterministicSparseTransitionParser<double>;
         template storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser<double>::parseDeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix<double> const& transitionMatrix);
         template storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser<double>::parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix<double> const& transitionMatrix);
+
+#ifdef STORM_HAVE_CARL
+        template class DeterministicSparseTransitionParser<storm::Interval>;
+
+        template storm::storage::SparseMatrix<storm::Interval> DeterministicSparseTransitionParser<storm::Interval>::parseDeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix<double> const& transitionMatrix);
+        template storm::storage::SparseMatrix<storm::Interval> DeterministicSparseTransitionParser<storm::Interval>::parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix<double> const& transitionMatrix);
+#endif
     } // namespace parser
 } // namespace storm

src/parser/MarkovAutomatonParser.cpp

@@ -6,6 +6,8 @@
 
 #include "src/exceptions/WrongFormatException.h"
 
+#include "src/adapters/CarlAdapter.h"
+
 #include "log4cplus/logger.h"
 #include "log4cplus/loggingmacros.h"
 extern log4cplus::Logger logger;
@@ -31,7 +33,7 @@ namespace storm {
                 stateRewards.reset(storm::parser::SparseStateRewardParser<RewardValueType>::parseSparseStateReward(transitionMatrix.getColumnCount(), stateRewardFilename));
             }
             std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<RewardValueType>> rewardModels;
-            rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel<RewardValueType>(stateRewards, boost::optional<std::vector<double>>(), boost::optional<storm::storage::SparseMatrix<double>>())));
+            rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel<RewardValueType>(stateRewards, boost::optional<std::vector<RewardValueType>>(), boost::optional<storm::storage::SparseMatrix<RewardValueType>>())));
 
             // Since Markov Automata do not support transition rewards no path should be given here.
             if (transitionRewardFilename != "") {
@@ -46,6 +48,10 @@ namespace storm {
         }
 
         template class MarkovAutomatonParser<double, double>;
-        
+
+#ifdef STORM_HAVE_CARL
+        template class MarkovAutomatonParser<double, storm::Interval>;
+#endif
+
     } // namespace parser
 } // namespace storm

src/parser/MarkovAutomatonSparseTransitionParser.cpp

@@ -8,7 +8,6 @@
 #include "src/utility/cstring.h"
 #include "src/utility/macros.h"
 
-
 namespace storm {
     namespace parser {
 

src/parser/NondeterministicModelParser.cpp

@@ -10,6 +10,8 @@
 #include "src/parser/SparseStateRewardParser.h"
 #include "src/parser/SparseChoiceLabelingParser.h"
 
+#include "src/adapters/CarlAdapter.h"
+
 namespace storm {
     namespace parser {
 
@@ -31,7 +33,7 @@ namespace storm {
             }
 
             // Only parse transition rewards if a file is given.
-            boost::optional<storm::storage::SparseMatrix<double>> transitionRewards;
+            boost::optional<storm::storage::SparseMatrix<RewardValueType>> transitionRewards;
             if (!transitionRewardFilename.empty()) {
                 transitionRewards = std::move(storm::parser::NondeterministicSparseTransitionParser<RewardValueType>::parseNondeterministicTransitionRewards(transitionRewardFilename, transitions));
             }
@@ -61,6 +63,10 @@ namespace storm {
         }
 
         template class NondeterministicModelParser<double, double>;
-        
+
+#ifdef STORM_HAVE_CARL
+        template class NondeterministicModelParser<double, storm::Interval>;
+#endif
+
     } /* namespace parser */
 } /* namespace storm */

src/parser/NondeterministicSparseTransitionParser.cpp

@@ -13,6 +13,8 @@
 
 #include "src/utility/cstring.h"
 
+#include "src/adapters/CarlAdapter.h"
+
 #include "log4cplus/logger.h"
 #include "log4cplus/loggingmacros.h"
 extern log4cplus::Logger logger;
@@ -189,7 +191,7 @@ namespace storm {
             // Finally, build the actual matrix, test and return it.
             storm::storage::SparseMatrix<ValueType> resultMatrix = matrixBuilder.build();
 
-            // Since we cannot do the testing if each transition for which there is a reward in the reward file also exists in the transition matrix during parsing, we have to do it afterwards.
+            // Since we cannot check if each transition for which there is a reward in the reward file also exists in the transition matrix during parsing, we have to do it afterwards.
             if (isRewardFile && !resultMatrix.isSubmatrixOf(modelInformation)) {
                 LOG4CPLUS_ERROR(logger, "There are rewards for non existent transitions given in the reward file.");
                 throw storm::exceptions::WrongFormatException() << "There are rewards for non existent transitions given in the reward file.";
@@ -336,6 +338,13 @@ namespace storm {
         template class NondeterministicSparseTransitionParser<double>;
         template storm::storage::SparseMatrix<double> NondeterministicSparseTransitionParser<double>::parseNondeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix<double> const& modelInformation);
         template storm::storage::SparseMatrix<double> NondeterministicSparseTransitionParser<double>::parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix<double> const& modelInformation);
-        
+
+#ifdef STORM_HAVE_CARL
+        template class NondeterministicSparseTransitionParser<storm::Interval>;
+
+        template storm::storage::SparseMatrix<storm::Interval> NondeterministicSparseTransitionParser<storm::Interval>::parseNondeterministicTransitionRewards<double>(std::string const& filename, storm::storage::SparseMatrix<double> const& modelInformation);
+        template storm::storage::SparseMatrix<storm::Interval> NondeterministicSparseTransitionParser<storm::Interval>::parse<double>(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix<double> const& modelInformation);
+#endif
+
     } // namespace parser
 } // namespace storm

src/parser/SparseStateRewardParser.cpp

@@ -6,6 +6,9 @@
 #include "src/exceptions/FileIoException.h"
 #include "src/utility/cstring.h"
 #include "src/parser/MappedFile.h"
+
+#include "src/adapters/CarlAdapter.h"
+
 #include "log4cplus/logger.h"
 #include "log4cplus/loggingmacros.h"
 extern log4cplus::Logger logger;
@@ -27,7 +30,7 @@ namespace storm {
             char const* buf = file.getData();
 
             // Create state reward vector with given state count.
-            std::vector<double> stateRewards(stateCount);
+            std::vector<ValueType> stateRewards(stateCount);
 
             // Now parse state reward assignments.
             uint_fast64_t state = 0;
@@ -71,5 +74,9 @@ namespace storm {
         
         template class SparseStateRewardParser<double>;
 
+#ifdef STORM_HAVE_CARL
+        template class SparseStateRewardParser<storm::Interval>;
+#endif
+
     } // namespace parser
 } // namespace storm

src/settings/modules/GeneralSettings.cpp

@@ -42,6 +42,7 @@ namespace storm {
             const std::string GeneralSettings::timeoutOptionShortName = "t";
             const std::string GeneralSettings::eqSolverOptionName = "eqsolver";
             const std::string GeneralSettings::lpSolverOptionName = "lpsolver";
+            const std::string GeneralSettings::smtSolverOptionName = "smtsolver";
             const std::string GeneralSettings::constantsOptionName = "constants";
             const std::string GeneralSettings::constantsOptionShortName = "const";
             const std::string GeneralSettings::statisticsOptionName = "statistics";
@@ -102,6 +103,9 @@ namespace storm {
                 std::vector<std::string> lpSolvers = {"gurobi", "glpk"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, false, "Sets which LP solver is preferred.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an LP solver. Available are: gurobi and glpk.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(lpSolvers)).setDefaultValueString("glpk").build()).build());
+                std::vector<std::string> smtSolvers = {"z3", "mathsat"};
+                this->addOption(storm::settings::OptionBuilder(moduleName, smtSolverOptionName, false, "Sets which SMT solver is preferred.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an SMT solver. Available are: z3 and mathsat.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(smtSolvers)).setDefaultValueString("z3").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that Note that this requires the model to be given as an symbolic model (i.e., via --" + symbolicOptionName + ").").setShortName(constantsOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, false, "Sets whether to display statistics if available.").setShortName(statisticsOptionShortName).build());
@@ -256,6 +260,16 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown LP solver '" << lpSolverName << "'.");
             }
             
+            storm::solver::SmtSolverType GeneralSettings::getSmtSolver() const {
+                std::string smtSolverName = this->getOption(smtSolverOptionName).getArgumentByName("name").getValueAsString();
+                if (smtSolverName == "z3") {
+                    return storm::solver::SmtSolverType::Z3;
+                } else if (smtSolverName == "mathsat") {
+                    return storm::solver::SmtSolverType::Mathsat;
+                }
+                STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown SMT solver '" << smtSolverName << "'.");
+            }
+            
             bool GeneralSettings::isConstantsSet() const {
                 return this->getOption(constantsOptionName).getHasOptionBeenSet();
             }

src/settings/modules/GeneralSettings.h

@@ -9,6 +9,7 @@ namespace storm {
         enum class EquationSolverType;
         enum class LpSolverType;
         enum class MinMaxTechnique;
+        enum class SmtSolverType;
     }
 
     namespace settings {
@@ -268,6 +269,13 @@ namespace storm {
                  */
                 storm::solver::LpSolverType getLpSolver() const;
 
+                /*!
+                 * Retrieves the selected SMT solver.
+                 *
+                 * @return The selected SMT solver.
+                 */
+                storm::solver::SmtSolverType getSmtSolver() const;
+                
                 /*!
                  * Retrieves whether the export-to-dot option was set.
                  *
@@ -374,6 +382,7 @@ namespace storm {
                 static const std::string timeoutOptionShortName;
                 static const std::string eqSolverOptionName;
                 static const std::string lpSolverOptionName;
+                static const std::string smtSolverOptionName;
                 static const std::string constantsOptionName;
                 static const std::string constantsOptionShortName;
                 static const std::string statisticsOptionName;

src/solver/SolverSelectionOptions.cpp

@@ -11,7 +11,8 @@ namespace storm {
             }
             
         }
-         std::string toString(LpSolverType t) {
+        
+        std::string toString(LpSolverType t) {
             switch(t) {
                 case LpSolverType::Gurobi:
                     return "Gurobi";
@@ -19,7 +20,7 @@ namespace storm {
                     return "Glpk";
             }
         }
-
+        
         std::string toString(EquationSolverType t) {
             switch(t) {
                 case EquationSolverType::Native:
@@ -30,5 +31,14 @@ namespace storm {
                     return "Topological";
             }
         }
+        
+        std::string toString(SmtSolverType t) {
+            switch(t) {
+                case SmtSolverType::Z3:
+                    return "Z3";
+                case SmtSolverType::Mathsat:
+                    return "Mathsat";
+            }
+        }
     }
 }

src/solver/SolverSelectionOptions.h

@@ -1,4 +1,3 @@
-
 #ifndef SOLVERSELECTIONOPTIONS_H
 #define	SOLVERSELECTIONOPTIONS_H
 
@@ -7,13 +6,11 @@
 
 namespace storm {
     namespace solver {
-         ExtendEnumsWithSelectionField(MinMaxTechnique, PolicyIteration, ValueIteration)
+        ExtendEnumsWithSelectionField(MinMaxTechnique, PolicyIteration, ValueIteration)
         
-                 
         ExtendEnumsWithSelectionField(LpSolverType, Gurobi, Glpk)
         ExtendEnumsWithSelectionField(EquationSolverType, Native, Gmmxx, Topological)
-                 
-        
+        ExtendEnumsWithSelectionField(SmtSolverType, Z3, Mathsat)
     }
 } 
 

src/storage/SparseMatrix.cpp

@@ -1081,7 +1081,8 @@ namespace storm {
         }
         
         template<typename ValueType>
-        bool SparseMatrix<ValueType>::isSubmatrixOf(SparseMatrix<ValueType> const& matrix) const {
+        template<typename OtherValueType>
+        bool SparseMatrix<ValueType>::isSubmatrixOf(SparseMatrix<OtherValueType> const& matrix) const {
             // Check for matching sizes.
             if (this->getRowCount() != matrix.getRowCount()) return false;
             if (this->getColumnCount() != matrix.getColumnCount()) return false;
@@ -1089,7 +1090,9 @@ namespace storm {
             
             // Check the subset property for all rows individually.
             for (index_type row = 0; row < this->getRowCount(); ++row) {
-                for (const_iterator it1 = this->begin(row), ite1 = this->end(row), it2 = matrix.begin(row), ite2 = matrix.end(row); it1 != ite1; ++it1) {
+                auto it2 = matrix.begin(row);
+                auto ite2 = matrix.end(row);
+                for (const_iterator it1 = this->begin(row), ite1 = this->end(row); it1 != ite1; ++it1) {
                     // Skip over all entries of the other matrix that are before the current entry in the current matrix.
                     while (it2 != ite2 && it2->getColumn() < it1->getColumn()) {
                         ++it2;
@@ -1165,14 +1168,16 @@ namespace storm {
         template class SparseMatrix<double>;
         template std::ostream& operator<<(std::ostream& out, SparseMatrix<double> const& matrix);
         template std::vector<double> SparseMatrix<double>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<double> const& otherMatrix) const;
-        
-        // float
+        template bool SparseMatrix<double>::isSubmatrixOf(SparseMatrix<double> const& matrix) const;
+
+            // float
         template class MatrixEntry<typename SparseMatrix<float>::index_type, float>;
         template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, float> const& entry);
         template class SparseMatrixBuilder<float>;
         template class SparseMatrix<float>;
         template std::ostream& operator<<(std::ostream& out, SparseMatrix<float> const& matrix);
         template std::vector<float> SparseMatrix<float>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<float> const& otherMatrix) const;
+        template bool SparseMatrix<float>::isSubmatrixOf(SparseMatrix<float> const& matrix) const;
 
         // int
         template class MatrixEntry<typename SparseMatrix<int>::index_type, int>;
@@ -1180,6 +1185,7 @@ namespace storm {
         template class SparseMatrixBuilder<int>;
         template class SparseMatrix<int>;
         template std::ostream& operator<<(std::ostream& out, SparseMatrix<int> const& matrix);
+        template bool SparseMatrix<int>::isSubmatrixOf(SparseMatrix<int> const& matrix) const;
 
 #ifdef STORM_HAVE_CARL
         // Rat Function
@@ -1192,6 +1198,7 @@ namespace storm {
         template std::vector<storm::RationalFunction> SparseMatrix<double>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::RationalFunction> const& otherMatrix) const;
         template std::vector<storm::RationalFunction> SparseMatrix<float>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::RationalFunction> const& otherMatrix) const;
         template std::vector<storm::RationalFunction> SparseMatrix<int>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::RationalFunction> const& otherMatrix) const;
+        template bool SparseMatrix<storm::RationalFunction>::isSubmatrixOf(SparseMatrix<storm::RationalFunction> const& matrix) const;
 
         // Intervals
         template std::vector<storm::Interval> SparseMatrix<double>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::Interval> const& otherMatrix) const;
@@ -1201,6 +1208,9 @@ namespace storm {
         template class SparseMatrix<Interval>;
         template std::ostream& operator<<(std::ostream& out, SparseMatrix<Interval> const& matrix);
         template std::vector<storm::Interval> SparseMatrix<Interval>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::Interval> const& otherMatrix) const;
+        template bool SparseMatrix<storm::Interval>::isSubmatrixOf(SparseMatrix<storm::Interval> const& matrix) const;
+
+        template bool SparseMatrix<storm::Interval>::isSubmatrixOf(SparseMatrix<double> const& matrix) const;
 #endif
         
         

src/storage/SparseMatrix.h

@@ -753,7 +753,8 @@ namespace storm {
              * @param matrix The matrix that possibly is a supermatrix of the current matrix.
              * @return True iff the current matrix is a submatrix of the given matrix.
              */
-            bool isSubmatrixOf(SparseMatrix<value_type> const& matrix) const;
+            template<typename OtherValueType>
+            bool isSubmatrixOf(SparseMatrix<OtherValueType> const& matrix) const;
             
             template<typename TPrime>
             friend std::ostream& operator<<(std::ostream& out, SparseMatrix<TPrime> const& matrix);

src/storage/expressions/ExpressionManager.cpp

@@ -205,7 +205,7 @@ namespace storm {
             std::string newName = prefix + std::to_string(freshVariableCounter++);
             return declareOrGetVariable(newName, variableType, auxiliary, false);
         }
-
+        
         Variable ExpressionManager::declareFreshBooleanVariable(bool auxiliary, const std::string& prefix) {
             return declareFreshVariable(this->getBooleanType(), auxiliary, prefix);
         }

src/storage/prism/Program.cpp

@@ -1,15 +1,18 @@
 #include "src/storage/prism/Program.h"
 
 #include <algorithm>
+#include <sstream>
 
 #include "src/storage/expressions/ExpressionManager.h"
 #include "src/settings/SettingsManager.h"
 #include "src/settings/modules/GeneralSettings.h"
 #include "src/utility/macros.h"
+#include "src/utility/solver.h"
 #include "src/exceptions/InvalidArgumentException.h"
 #include "src/exceptions/OutOfRangeException.h"
 #include "src/exceptions/WrongFormatException.h"
 #include "src/exceptions/InvalidTypeException.h"
+#include "src/solver/SmtSolver.h"
 
 namespace storm {
     namespace prism {
@@ -878,6 +881,250 @@ namespace storm {
             return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, getActionNameToIndexMapping(), getRewardModels(), false, getInitialConstruct(), getLabels(), "", 0, false);
         }
         
+        Program Program::flattenModules(std::unique_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);
+            }
+            
+            STORM_LOG_THROW(this->getModelType() == ModelType::DTMC || this->getModelType() == ModelType::MDP, storm::exceptions::InvalidTypeException, "Unable to flatten modules for model of type '" << this->getModelType() << "'.");
+            
+            // Otherwise, we need to actually flatten the contained modules.
+            
+            // Get an SMT solver for computing the possible guard combinations.
+            std::unique_ptr<storm::solver::SmtSolver> solver = smtSolverFactory->create(*manager);
+            
+            // Set up the data we need to gather to create the flat module.
+            std::stringstream newModuleName;
+            std::vector<storm::prism::BooleanVariable> allBooleanVariables;
+            std::vector<storm::prism::IntegerVariable> allIntegerVariables;
+            std::vector<storm::prism::Command> newCommands;
+            uint_fast64_t nextCommandIndex = 0;
+            uint_fast64_t nextUpdateIndex = 0;
+            
+            // Assert the values of the constants.
+            for (auto const& constant : this->getConstants()) {
+                if (constant.isDefined()) {
+                    solver->add(constant.getExpressionVariable() == constant.getExpression());
+                }
+            }
+            
+            // Assert the bounds of the global variables.
+            for (auto const& variable : this->getGlobalIntegerVariables()) {
+                solver->add(variable.getExpression() >= variable.getLowerBoundExpression());
+                solver->add(variable.getExpression() <= variable.getUpperBoundExpression());
+            }
+            
+            // Make the global variables local, such that the resulting module covers all occurring variables. Note that
+            // this is just for simplicity and is not needed.
+            allBooleanVariables.insert(allBooleanVariables.end(), this->getGlobalBooleanVariables().begin(), this->getGlobalBooleanVariables().end());
+            allIntegerVariables.insert(allIntegerVariables.end(), this->getGlobalIntegerVariables().begin(), this->getGlobalIntegerVariables().end());
+            
+            // Now go through the modules, gather the variables, construct the name of the new module and assert the
+            // bounds of the discovered variables.
+            for (auto const& module : this->getModules()) {
+                newModuleName << module.getName() << "_";
+                allBooleanVariables.insert(allBooleanVariables.end(), module.getBooleanVariables().begin(), module.getBooleanVariables().end());
+                allIntegerVariables.insert(allIntegerVariables.end(), module.getIntegerVariables().begin(), module.getIntegerVariables().end());
+                
+                for (auto const& variable : module.getIntegerVariables()) {
+                    solver->add(variable.getExpression() >= variable.getLowerBoundExpression());
+                    solver->add(variable.getExpression() <= variable.getUpperBoundExpression());
+                }
+                
+                // The commands without a synchronizing action name, can simply be copied (plus adjusting the global
+                // indices of the command and its updates).
+                for (auto const& command : module.getCommands()) {
+                    if (!command.isLabeled()) {
+                        std::vector<storm::prism::Update> updates;
+                        updates.reserve(command.getUpdates().size());
+                        
+                        for (auto const& update : command.getUpdates()) {
+                            updates.push_back(storm::prism::Update(nextUpdateIndex, update.getLikelihoodExpression(), update.getAssignments(), update.getFilename(), 0));
+                            ++nextUpdateIndex;
+                        }
+                        
+                        newCommands.push_back(storm::prism::Command(nextCommandIndex, command.isMarkovian(), actionToIndexMap.find("")->second, "", command.getGuardExpression(), updates, command.getFilename(), 0));
+                        ++nextCommandIndex;
+                    }
+                }
+            }
+            
+            // Save state of solver so that we can always restore the point where we have exactly the constant values
+            // and variables bounds on the assertion stack.
+            solver->push();
+            
+            // Now we need to enumerate all possible combinations of synchronizing commands. For this, we iterate over
+            // all actions and let the solver enumerate the possible combinations of commands that can be enabled together.
+            for (auto const& actionIndex : this->getSynchronizingActionIndices()) {
+                bool noCombinationsForAction = false;
+                
+                // Prepare the list that stores for each module the list of commands with the given action.
+                std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>> possibleCommands;
+                
+                for (auto const& module : this->getModules()) {
+                    // If the module has no command with this action, we can skip it.
+                    if (!module.hasActionIndex(actionIndex)) {
+                        continue;
+                    }
+                    
+                    std::set<uint_fast64_t> const& commandIndices = module.getCommandIndicesByActionIndex(actionIndex);
+                    
+                    // If there is no command even though the module has this action, there is no valid command
+                    // combination with this action.
+                    if (commandIndices.empty()) {
+                        noCombinationsForAction = true;
+                        break;
+                    }
+                    
+                    // Prepare empty list of commands for this module.
+                    possibleCommands.push_back(std::vector<std::reference_wrapper<storm::prism::Command const>>());
+                    
+                    // Add references to the commands labeled with the current action.
+                    for (auto const& commandIndex : commandIndices) {
+                        possibleCommands.back().push_back(module.getCommand(commandIndex));
+                    }
+                }
+                
+                // If there are no valid combinations for the action, we need to skip the generation of synchronizing
+                // commands.
+                if (!noCombinationsForAction) {
+                    // Save the solver state to be able to restore it when this action index is done.
+                    solver->push();
+                    
+                    // Start by creating a fresh auxiliary variable for each command and link it with the guard.
+                    std::vector<std::vector<storm::expressions::Variable>> commandVariables(possibleCommands.size());
+                    std::vector<storm::expressions::Variable> allCommandVariables;
+                    for (uint_fast64_t outerIndex = 0; outerIndex < possibleCommands.size(); ++outerIndex) {
+                        // Create auxiliary variables and link them with the guards.
+                        for (uint_fast64_t innerIndex = 0; innerIndex < possibleCommands[outerIndex].size(); ++innerIndex) {
+                            commandVariables[outerIndex].push_back(manager->declareFreshBooleanVariable());
+                            allCommandVariables.push_back(commandVariables[outerIndex].back());
+                            solver->add(implies(commandVariables[outerIndex].back(), possibleCommands[outerIndex][innerIndex].get().getGuardExpression()));
+                        }
+                        
+                        storm::expressions::Expression atLeastOneCommandFromModule = manager->boolean(false);
+                        for (auto const& commandVariable : commandVariables[outerIndex]) {
+                            atLeastOneCommandFromModule = atLeastOneCommandFromModule || commandVariable;
+                        }
+                        solver->add(atLeastOneCommandFromModule);
+                    }
+                    
+                    // Now we are in a position to start the enumeration over all command variables.
+                    uint_fast64_t modelCount = 0;
+                    solver->allSat(allCommandVariables, [&] (storm::solver::SmtSolver::ModelReference& modelReference) -> bool {
+                        // Now we need to reconstruct the chosen commands from the valuation of the command variables.
+                        std::vector<std::vector<std::reference_wrapper<Command const>>> chosenCommands(possibleCommands.size());
+
+                        for (uint_fast64_t outerIndex = 0; outerIndex < commandVariables.size(); ++outerIndex) {
+                            for (uint_fast64_t innerIndex = 0; innerIndex < commandVariables[outerIndex].size(); ++innerIndex) {
+                                if (modelReference.getBooleanValue(commandVariables[outerIndex][innerIndex])) {
+                                    chosenCommands[outerIndex].push_back(possibleCommands[outerIndex][innerIndex]);
+                                }
+                            }
+                        }
+                        
+                        // Now that we have retrieved the commands, we need to build their synchronizations and add them
+                        // to the flattened module.
+                        std::vector<std::vector<std::reference_wrapper<Command const>>::const_iterator> iterators;
+                        for (auto const& element : chosenCommands) {
+                            iterators.push_back(element.begin());
+                        }
+                        
+                        bool movedAtLeastOneIterator = false;
+                        std::vector<std::reference_wrapper<Command const>> commandCombination(chosenCommands.size(), chosenCommands.front().front());
+                        do {
+                            for (uint_fast64_t index = 0; index < iterators.size(); ++index) {
+                                commandCombination[index] = *iterators[index];
+                            }
+
+                            newCommands.push_back(synchronizeCommands(nextCommandIndex, actionIndex, nextUpdateIndex, indexToActionMap.find(actionIndex)->second, commandCombination));
+                            
+                            // Move the counters appropriately.
+                            ++nextCommandIndex;
+                            nextUpdateIndex += newCommands.back().getNumberOfUpdates();
+
+                            movedAtLeastOneIterator = false;
+                            for (uint_fast64_t index = 0; index < iterators.size(); ++index) {
+                                ++iterators[index];
+                                if (iterators[index] != chosenCommands[index].cend()) {
+                                    movedAtLeastOneIterator = true;
+                                    break;
+                                } else {
+                                    iterators[index] = chosenCommands[index].cbegin();
+                                }
+                            }
+                        } while (movedAtLeastOneIterator);
+                        
+                        return true;
+                    });
+                    
+                    solver->pop();
+                }
+            }
+            
+            // Finally, we can create the module and the program and return it.
+            storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, newCommands, this->getFilename(), 0);
+            return Program(manager, this->getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(), std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), false, this->getInitialConstruct(), this->getLabels(), this->getFilename(), 0, true);
+        }
+        
+        Command Program::synchronizeCommands(uint_fast64_t newCommandIndex, uint_fast64_t actionIndex, uint_fast64_t firstUpdateIndex, std::string const& actionName, std::vector<std::reference_wrapper<Command const>> const& commands) const {
+            // To construct the synchronous product of the commands, we need to store a list of its updates.
+            std::vector<storm::prism::Update> newUpdates;
+            uint_fast64_t numberOfUpdates = 1;
+            for (uint_fast64_t i = 0; i < commands.size(); ++i) {
+                numberOfUpdates *= commands[i].get().getNumberOfUpdates();
+            }
+            newUpdates.reserve(numberOfUpdates);
+            
+            // Initialize all update iterators.
+            std::vector<std::vector<storm::prism::Update>::const_iterator> updateIterators;
+            for (uint_fast64_t i = 0; i < commands.size(); ++i) {
+                updateIterators.push_back(commands[i].get().getUpdates().cbegin());
+            }
+            
+            bool doneUpdates = false;
+            do {
+                // We create the new likelihood expression by multiplying the particapting updates' expressions.
+                storm::expressions::Expression newLikelihoodExpression = updateIterators[0]->getLikelihoodExpression();
+                for (uint_fast64_t i = 1; i < updateIterators.size(); ++i) {
+                    newLikelihoodExpression = newLikelihoodExpression * updateIterators[i]->getLikelihoodExpression();
+                }
+                
+                // Now concatenate all assignments of all participating updates.
+                std::vector<storm::prism::Assignment> newAssignments;
+                for (uint_fast64_t i = 0; i < updateIterators.size(); ++i) {
+                    newAssignments.insert(newAssignments.end(), updateIterators[i]->getAssignments().begin(), updateIterators[i]->getAssignments().end());
+                }
+                
+                // Then we are ready to create the new update.
+                newUpdates.push_back(storm::prism::Update(firstUpdateIndex, newLikelihoodExpression, newAssignments, this->getFilename(), 0));
+                ++firstUpdateIndex;
+                
+                // Now check whether there is some update combination we have not yet explored.
+                bool movedIterator = false;
+                for (int_fast64_t j = updateIterators.size() - 1; j >= 0; --j) {
+                    ++updateIterators[j];
+                    if (updateIterators[j] != commands[j].get().getUpdates().cend()) {
+                        movedIterator = true;
+                        break;
+                    } else {
+                        // Reset the iterator to the beginning of the list.
+                        updateIterators[j] = commands[j].get().getUpdates().cbegin();
+                    }
+                }
+                
+                doneUpdates = !movedIterator;
+            } while (!doneUpdates);
+            
+            storm::expressions::Expression newGuard = commands[0].get().getGuardExpression();
+            for (uint_fast64_t i = 1; i < commands.size(); ++i) {
+                newGuard = newGuard && commands[i].get().getGuardExpression();
+            }
+            
+            return Command(newCommandIndex, false, actionIndex, actionName, newGuard, newUpdates, this->getFilename(), 0);
+        }
+        
         storm::expressions::ExpressionManager const& Program::getManager() const {
             return *this->manager;
         }
@@ -886,17 +1133,20 @@ namespace storm {
             return *this->manager;
         }
 
-        std::ostream& operator<<(std::ostream& stream, Program const& program) {
-            switch (program.getModelType()) {
-                case Program::ModelType::UNDEFINED: stream << "undefined"; break;
-                case Program::ModelType::DTMC: stream << "dtmc"; break;
-                case Program::ModelType::CTMC: stream << "ctmc"; break;
-                case Program::ModelType::MDP: stream << "mdp"; break;
-                case Program::ModelType::CTMDP: stream << "ctmdp"; break;
-                case Program::ModelType::MA: stream << "ma"; break;
+        std::ostream& operator<<(std::ostream& out, Program::ModelType const& type) {
+            switch (type) {
+                case Program::ModelType::UNDEFINED: out << "undefined"; break;
+                case Program::ModelType::DTMC: out << "dtmc"; break;
+                case Program::ModelType::CTMC: out << "ctmc"; break;
+                case Program::ModelType::MDP: out << "mdp"; break;
+                case Program::ModelType::CTMDP: out << "ctmdp"; break;
+                case Program::ModelType::MA: out << "ma"; break;
             }
-            stream << std::endl;
-            
+            return out;
+        }
+        
+        std::ostream& operator<<(std::ostream& stream, Program const& program) {
+            stream << program.getModelType() << std::endl;
             for (auto const& constant : program.getConstants()) {
                 stream << constant << std::endl;
             }

src/storage/prism/Program.h

@@ -12,6 +12,7 @@
 #include "src/storage/prism/Module.h"
 #include "src/storage/prism/RewardModel.h"
 #include "src/storage/prism/InitialConstruct.h"
+#include "src/utility/solver.h"
 #include "src/utility/OsDetection.h"
 
 namespace storm {
@@ -419,6 +420,14 @@ namespace storm {
              */
             void checkValidity(Program::ValidityCheckLevel lvl = Program::ValidityCheckLevel::READYFORPROCESSING) const;
             
+            /*!
+             * Creates an equivalent program that contains exactly one module.
+             *
+             * @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;
+            
             friend std::ostream& operator<<(std::ostream& stream, Program const& program);
             
             /*!
@@ -436,6 +445,18 @@ namespace storm {
             storm::expressions::ExpressionManager& getManager();
             
         private:
+            /*!
+             * This function builds a command that corresponds to the synchronization of the given list of commands.
+             *
+             * @param newCommandIndex The index of the command to construct.
+             * @param actionIndex The index of the action of the resulting command.
+             * @param firstUpdateIndex The index of the first update of the resulting command.
+             * @param actionName The name of the action of the resulting command.
+             * @param commands The commands to synchronize.
+             * @return The resulting command.
+             */
+            Command synchronizeCommands(uint_fast64_t newCommandIndex, uint_fast64_t actionIndex, uint_fast64_t firstUpdateIndex, std::string const& actionName, std::vector<std::reference_wrapper<Command const>> const& commands) const;
+            
             // The manager responsible for the variables/expressions of the program.
             std::shared_ptr<storm::expressions::ExpressionManager> manager;
             
@@ -517,6 +538,8 @@ namespace storm {
             Program replaceModulesAndConstantsInProgram(std::vector<Module> const& newModules, std::vector<Constant> const& newConstants);
         };
         
+        std::ostream& operator<<(std::ostream& out, Program::ModelType const& type);
+        
     } // namespace prism
 } // namespace storm
 

src/utility/solver.cpp

@@ -16,13 +16,14 @@
 #include "src/solver/GurobiLpSolver.h"
 #include "src/solver/GlpkLpSolver.h"
 
+#include "src/solver/Z3SmtSolver.h"
+#include "src/solver/MathsatSmtSolver.h"
 #include "src/settings/SettingsManager.h"
 #include "src/settings/modules/GeneralSettings.h"
 #include "src/settings/modules/NativeEquationSolverSettings.h"
 
 #include "src/exceptions/InvalidSettingsException.h"
 
-
 namespace storm {
     namespace utility {
         namespace solver {
@@ -163,7 +164,27 @@ namespace storm {
                 return factory->create(name, solvType);
             }
             
+            std::unique_ptr<storm::solver::SmtSolver> SmtSolverFactory::create(storm::expressions::ExpressionManager& manager) const {
+                storm::solver::SmtSolverType smtSolverType = storm::settings::generalSettings().getSmtSolver();
+                switch (smtSolverType) {
+                    case storm::solver::SmtSolverType::Z3: return std::unique_ptr<storm::solver::SmtSolver>(new storm::solver::Z3SmtSolver(manager));
+                    case storm::solver::SmtSolverType::Mathsat: return std::unique_ptr<storm::solver::SmtSolver>(new storm::solver::MathsatSmtSolver(manager));
+                }
+            }
+            
+            std::unique_ptr<storm::solver::SmtSolver> Z3SmtSolverFactory::create(storm::expressions::ExpressionManager& manager) const {
+                return std::unique_ptr<storm::solver::SmtSolver>(new storm::solver::Z3SmtSolver(manager));
+            }
             
+            std::unique_ptr<storm::solver::SmtSolver> MathsatSmtSolverFactory::create(storm::expressions::ExpressionManager& manager) const {
+                return std::unique_ptr<storm::solver::SmtSolver>(new storm::solver::MathsatSmtSolver(manager));
+            }
+            
+            std::unique_ptr<storm::solver::SmtSolver> getSmtSolver(storm::expressions::ExpressionManager& manager) {
+                std::unique_ptr<storm::utility::solver::SmtSolverFactory> factory(new MathsatSmtSolverFactory());
+                return factory->create(manager);
+            }
+
             template class SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>;
             template class SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>;
             template class SymbolicGameSolverFactory<storm::dd::DdType::CUDD>;

src/utility/solver.h

@@ -16,10 +16,12 @@ namespace storm {
         template<typename V> class LinearEquationSolver;
         template<typename V> class MinMaxLinearEquationSolver;
         class LpSolver;
+        class SmtSolver;
         
         template<typename ValueType> class NativeLinearEquationSolver;
         enum class NativeLinearEquationSolverSolutionMethod;
     }
+
     namespace storage {
         template<typename V> class SparseMatrix;
     }
@@ -28,8 +30,10 @@ namespace storm {
         template<storm::dd::DdType T> class Add;
         template<storm::dd::DdType T> class Bdd;
     }
+    
     namespace expressions {
         class Variable;
+        class ExpressionManager;
     }
     
     namespace utility {
@@ -126,6 +130,30 @@ namespace storm {
             };
             
             std::unique_ptr<storm::solver::LpSolver> getLpSolver(std::string const& name, storm::solver::LpSolverTypeSelection solvType = storm::solver::LpSolverTypeSelection::FROMSETTINGS) ;
+
+            class SmtSolverFactory {
+            public:
+                /*!
+                 * Creates a new SMT solver instance.
+                 *
+                 * @param manager The expression manager responsible for the expressions that will be given to the SMT
+                 * solver.
+                 * @return A pointer to the newly created solver.
+                 */
+                virtual std::unique_ptr<storm::solver::SmtSolver> create(storm::expressions::ExpressionManager& manager) const;
+            };
+            
+            class Z3SmtSolverFactory : public SmtSolverFactory {
+            public:
+                virtual std::unique_ptr<storm::solver::SmtSolver> create(storm::expressions::ExpressionManager& manager) const;
+            };
+
+            class MathsatSmtSolverFactory : public SmtSolverFactory {
+            public:
+                virtual std::unique_ptr<storm::solver::SmtSolver> create(storm::expressions::ExpressionManager& manager) const;
+            };
+            
+            std::unique_ptr<storm::solver::SmtSolver> getSmtSolver(storm::expressions::ExpressionManager& manager);
         }
     }
 }

test/functional/parser/PrismParserTest.cpp

@@ -4,11 +4,9 @@
 
 TEST(PrismParser, StandardModelTest) {
     storm::prism::Program result;
-    result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/coin2.nm");
     EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/coin2.nm"));
     EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/crowds5_5.pm"));
     EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/csma2_2.nm"));
-    result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/die.pm");
     EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/die.pm"));
     EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/firewire.nm"));
     EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/leader3.nm"));

test/functional/storage/PrismProgramTest.cpp

@@ -0,0 +1,24 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+#include "src/parser/PrismParser.h"
+
+#include "src/utility/solver.h"
+
+#ifdef STORM_HAVE_MSAT
+TEST(PrismProgramTest, FlattenModules) {
+    storm::prism::Program result;
+    ASSERT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/leader3.nm"));
+
+    std::unique_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory(new storm::utility::solver::MathsatSmtSolverFactory());
+    
+    ASSERT_NO_THROW(result = result.flattenModules(smtSolverFactory));
+    EXPECT_EQ(1, result.getNumberOfModules());
+    EXPECT_EQ(74, result.getModule(0).getNumberOfCommands());
+
+    ASSERT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/wlan0_collide.nm"));
+    
+    ASSERT_NO_THROW(result = result.flattenModules(smtSolverFactory));
+    EXPECT_EQ(1, result.getNumberOfModules());
+    EXPECT_EQ(180, result.getModule(0).getNumberOfCommands());
+}
+#endif