more interpolation work

src/storm/abstraction/AbstractionInformation.cpp

@@ -67,6 +67,7 @@ namespace storm {
             allPredicateIdentities &= predicateIdentities.back();
             sourceVariables.insert(newMetaVariable.first);
             successorVariables.insert(newMetaVariable.second);
+            orderedSourceVariables.push_back(newMetaVariable.first);
             orderedSuccessorVariables.push_back(newMetaVariable.second);
             ddVariableIndexToPredicateIndexMap[predicateIdentities.back().getIndex()] = predicateIndex;
             return predicateIndex;
@@ -121,6 +122,22 @@ namespace storm {
             return predicates;
         }
         
+        template<storm::dd::DdType DdType>
+        std::vector<storm::expressions::Expression> AbstractionInformation<DdType>::getPredicates(storm::storage::BitVector const& predicateValuation) const {
+            STORM_LOG_ASSERT(predicateValuation.size() == this->getNumberOfPredicates(), "Size of predicate valuation does not match number of predicates.");
+            
+            std::vector<storm::expressions::Expression> result;
+            for (uint64_t index = 0; index < this->getNumberOfPredicates(); ++index) {
+                if (predicateValuation[index]) {
+                    result.push_back(this->getPredicateByIndex(index));
+                } else {
+                    result.push_back(!this->getPredicateByIndex(index));
+                }
+            }
+            
+            return result;
+        }
+        
         template<storm::dd::DdType DdType>
         storm::expressions::Expression const& AbstractionInformation<DdType>::getPredicateByIndex(uint_fast64_t index) const {
             return predicates[index];
@@ -268,6 +285,11 @@ namespace storm {
             return orderedSuccessorVariables;
         }
         
+        template<storm::dd::DdType DdType>
+        std::vector<storm::expressions::Variable> const& AbstractionInformation<DdType>::getOrderedSourceVariables() const {
+            return orderedSourceVariables;
+        }
+        
         template<storm::dd::DdType DdType>
         storm::dd::Bdd<DdType> const& AbstractionInformation<DdType>::getAllPredicateIdentities() const {
             return allPredicateIdentities;
@@ -404,6 +426,25 @@ namespace storm {
             return result;
         }
         
+        template <storm::dd::DdType DdType>
+        storm::storage::BitVector AbstractionInformation<DdType>::decodeState(storm::dd::Bdd<DdType> const& state) const {
+            STORM_LOG_ASSERT(state.getNonZeroCount() == 1, "Wrong number of non-zero entries.");
+            
+            storm::storage::BitVector statePredicates(this->getNumberOfPredicates());
+            
+            storm::dd::Add<DdType, double> add = state.template toAdd<double>();
+            auto it = add.begin();
+            auto stateValuePair = *it;
+            for (uint_fast64_t index = 0; index < this->getOrderedSourceVariables().size(); ++index) {
+                auto const& successorVariable = this->getOrderedSourceVariables()[index];
+                if (stateValuePair.first.getBooleanValue(successorVariable)) {
+                    statePredicates.set(index);
+                }
+            }
+            
+            return statePredicates;
+        }
+        
         template <storm::dd::DdType DdType>
         std::map<uint_fast64_t, storm::storage::BitVector> AbstractionInformation<DdType>::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<DdType> const& choice) const {
             std::map<uint_fast64_t, storm::storage::BitVector> result;
@@ -412,28 +453,12 @@ namespace storm {
             for (auto const& successorValuePair : lowerChoiceAsAdd) {
                 uint_fast64_t updateIndex = this->decodeAux(successorValuePair.first, 0, this->getAuxVariableCount());
                 
-#ifdef LOCAL_DEBUG
-                std::cout << "update idx: " << updateIndex << std::endl;
-#endif
                 storm::storage::BitVector successor(this->getNumberOfPredicates());
                 for (uint_fast64_t index = 0; index < this->getOrderedSuccessorVariables().size(); ++index) {
                     auto const& successorVariable = this->getOrderedSuccessorVariables()[index];
-#ifdef LOCAL_DEBUG
-                    std::cout << successorVariable.getName() << " has value";
-#endif
                     if (successorValuePair.first.getBooleanValue(successorVariable)) {
                         successor.set(index);
-#ifdef LOCAL_DEBUG
-                        std::cout << " true";
-#endif
-                    } else {
-#ifdef LOCAL_DEBUG
-                        std::cout << " false";
-#endif
                     }
-#ifdef LOCAL_DEBUG
-                    std::cout << std::endl;
-#endif
                 }
                 
                 result[updateIndex] = successor;
@@ -442,40 +467,26 @@ namespace storm {
         }
         
         template <storm::dd::DdType DdType>
-        std::pair<storm::storage::BitVector, uint64_t> AbstractionInformation<DdType>::decodeStateAndUpdate(storm::dd::Bdd<DdType> const& state) const {
-            storm::storage::BitVector successor(this->getNumberOfPredicates());
+        std::tuple<storm::storage::BitVector, uint64_t, uint64_t> AbstractionInformation<DdType>::decodeStatePlayer1ChoiceAndUpdate(storm::dd::Bdd<DdType> const& stateChoiceAndUpdate) const {
+            stateChoiceAndUpdate.template toAdd<double>().exportToDot("out.dot");
+            STORM_LOG_ASSERT(stateChoiceAndUpdate.getNonZeroCount() == 1, "Wrong number of non-zero entries.");
             
-            storm::dd::Add<DdType, double> stateAsAdd = state.template toAdd<double>();
-            uint_fast64_t updateIndex = 0;
-            for (auto const& stateValuePair : stateAsAdd) {
-                uint_fast64_t updateIndex = this->decodeAux(stateValuePair.first, 0, this->getAuxVariableCount());
-                
-#ifdef LOCAL_DEBUG
-                std::cout << "update idx: " << updateIndex << std::endl;
-#endif
-                storm::storage::BitVector successor(this->getNumberOfPredicates());
-                for (uint_fast64_t index = 0; index < this->getOrderedSuccessorVariables().size(); ++index) {
-                    auto const& successorVariable = this->getOrderedSuccessorVariables()[index];
-#ifdef LOCAL_DEBUG
-                    std::cout << successorVariable.getName() << " has value";
-#endif
-                    if (stateValuePair.first.getBooleanValue(successorVariable)) {
-                        successor.set(index);
-#ifdef LOCAL_DEBUG
-                        std::cout << " true";
-#endif
-                    } else {
-#ifdef LOCAL_DEBUG
-                        std::cout << " false";
-#endif
-                    }
-#ifdef LOCAL_DEBUG
-                    std::cout << std::endl;
-#endif
+            storm::storage::BitVector statePredicates(this->getNumberOfPredicates());
+            
+            storm::dd::Add<DdType, double> add = stateChoiceAndUpdate.template toAdd<double>();
+            auto it = add.begin();
+            auto stateValuePair = *it;
+            uint64_t choiceIndex = this->decodePlayer1Choice(stateValuePair.first, this->getPlayer1VariableCount());
+            uint64_t updateIndex = this->decodeAux(stateValuePair.first, 0, this->getAuxVariableCount());
+            for (uint_fast64_t index = 0; index < this->getOrderedSourceVariables().size(); ++index) {
+                auto const& successorVariable = this->getOrderedSourceVariables()[index];
+
+                if (stateValuePair.first.getBooleanValue(successorVariable)) {
+                    statePredicates.set(index);
                 }
             }
             
-            return std::make_pair(successors, updateIndex);
+            return std::make_tuple(statePredicates, choiceIndex, updateIndex);
         }
         
         template class AbstractionInformation<storm::dd::DdType::CUDD>;

src/storm/abstraction/AbstractionInformation.h

@@ -141,6 +141,11 @@ namespace storm {
              */
             std::vector<storm::expressions::Expression> const& getPredicates() const;
 
+            /*!
+             * Retrieves a list of expression that corresponds to the given predicate valuation.
+             */
+            std::vector<storm::expressions::Expression> getPredicates(storm::storage::BitVector const& predicateValuation) const;
+            
             /*!
              * Retrieves the predicate with the given index.
              *
@@ -341,6 +346,13 @@ namespace storm {
              */
             std::set<storm::expressions::Variable> const& getSuccessorVariables() const;
 
+            /*!
+             * Retrieves the ordered collection of source meta variables.
+             *
+             * @return All source meta variables.
+             */
+            std::vector<storm::expressions::Variable> const& getOrderedSourceVariables() const;
+            
             /*!
              * Retrieves the ordered collection of successor meta variables.
              *
@@ -434,16 +446,22 @@ namespace storm {
              */
             std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> declareNewVariables(std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> const& oldPredicates, std::set<uint_fast64_t> const& newPredicates) const;
             
+            /*!
+             * Decodes the given state (given as a BDD over the source variables) into a a bit vector indicating the
+             * truth values of the predicates in the state.
+             */
+            storm::storage::BitVector decodeState(storm::dd::Bdd<DdType> const& state) const;
+            
             /*!
              * Decodes the choice in the form of a BDD over the destination variables.
              */
             std::map<uint_fast64_t, storm::storage::BitVector> decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<DdType> const& choice) const;
             
             /*!
-             * Decodes the given state-and-update BDD (state as source variables) into a bit vector indicating the truth values of
-             * the predicates in the state and the update index.
+             * Decodes the given BDD (over source, player 1 and aux variables) into a bit vector indicating the truth
+             * values of the predicates in the state and the choice/update indices.
              */
-            std::pair<storm::storage::BitVector, uint64_t> decodeStateAndUpdate(storm::dd::Bdd<DdType> const& stateAndUpdate) const;
+            std::tuple<storm::storage::BitVector, uint64_t, uint64_t> decodeStatePlayer1ChoiceAndUpdate(storm::dd::Bdd<DdType> const& stateChoiceAndUpdate) const;
             
         private:
             /*!
@@ -504,7 +522,10 @@ namespace storm {
             
             /// The set of all successor variables.
             std::set<storm::expressions::Variable> successorVariables;
-            
+
+            /// An ordered collection of the source variables.
+            std::vector<storm::expressions::Variable> orderedSourceVariables;
+
             /// An ordered collection of the successor variables.
             std::vector<storm::expressions::Variable> orderedSuccessorVariables;
             

src/storm/abstraction/MenuGameAbstractor.h

@@ -27,6 +27,7 @@ namespace storm {
             virtual storm::expressions::Expression const& getGuard(uint64_t player1Choice) const = 0;
             virtual std::pair<uint64_t, uint64_t> getPlayer1ChoiceRange() const = 0;
             virtual std::map<storm::expressions::Variable, storm::expressions::Expression> getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const = 0;
+            virtual storm::expressions::Expression getInitialExpression() const = 0;
             
             /// Methods to refine the abstraction.
             virtual void refine(RefinementCommand const& command) = 0;

src/storm/abstraction/MenuGameRefiner.cpp

@@ -5,6 +5,9 @@
 
 #include "storm/storage/dd/DdManager.h"
 #include "storm/utility/dd.h"
+#include "storm/utility/solver.h"
+
+#include "storm/solver/MathsatSmtSolver.h"
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/AbstractionSettings.h"
@@ -24,6 +27,18 @@ namespace storm {
             return predicates;
         }
         
+        template<storm::dd::DdType Type>
+        struct PivotStateCandidatesResult {
+            storm::dd::Bdd<Type> reachableTransitionsMin;
+            storm::dd::Bdd<Type> reachableTransitionsMax;
+            storm::dd::Bdd<Type> pivotStates;
+        };
+        
+        template<storm::dd::DdType Type>
+        PivotStateResult<Type>::PivotStateResult(storm::dd::Bdd<Type> const& pivotState, storm::OptimizationDirection fromDirection) : pivotState(pivotState), fromDirection(fromDirection) {
+            // Intentionally left empty.
+        }
+        
         template<storm::dd::DdType Type, typename ValueType>
         MenuGameRefiner<Type, ValueType>::MenuGameRefiner(MenuGameAbstractor<Type, ValueType>& abstractor, std::unique_ptr<storm::solver::SmtSolver>&& smtSolver) : abstractor(abstractor), splitPredicates(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isSplitPredicatesSet()), splitGuards(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isSplitGuardsSet()), splitter(), equivalenceChecker(std::move(smtSolver)) {
             
@@ -47,17 +62,17 @@ namespace storm {
         storm::dd::Bdd<Type> getMostProbablePathSpanningTree(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& targetState, storm::dd::Bdd<Type> const& transitionFilter) {
             storm::dd::Add<Type, ValueType> maxProbabilities = game.getInitialStates().template toAdd<ValueType>();
             
-            storm::dd::Add<Type, ValueType> border = game.getInitialStates().template toAdd<ValueType>();
+            storm::dd::Bdd<Type> border = game.getInitialStates();
             storm::dd::Bdd<Type> spanningTree = game.getManager().getBddZero();
 
-            storm::dd::Add<Type, ValueType> transitionMatrix = ((transitionFilter && game.getExtendedTransitionMatrix().maxAbstractRepresentative(game.getProbabilisticBranchingVariables())).template toAdd<ValueType>() * game.getExtendedTransitionMatrix());
-            transitionMatrix = transitionMatrix.sumAbstract(game.getNondeterminismVariables());
+            storm::dd::Add<Type, ValueType> transitionMatrix = ((transitionFilter && game.getExtendedTransitionMatrix().maxAbstractRepresentative(game.getProbabilisticBranchingVariables())).template toAdd<ValueType>() * game.getExtendedTransitionMatrix()).sumAbstract(game.getPlayer2Variables());
             
             std::set<storm::expressions::Variable> variablesToAbstract(game.getRowVariables());
+            variablesToAbstract.insert(game.getPlayer1Variables().begin(), game.getPlayer1Variables().end());
             variablesToAbstract.insert(game.getProbabilisticBranchingVariables().begin(), game.getProbabilisticBranchingVariables().end());
             while (!border.isZero() && (border && targetState).isZero()) {
                 // Determine the new maximal probabilities to all states.
-                storm::dd::Add<Type, ValueType> tmp = border * transitionMatrix * maxProbabilities;
+                storm::dd::Add<Type, ValueType> tmp = border.template toAdd<ValueType>() * transitionMatrix * maxProbabilities;
                 storm::dd::Bdd<Type> newMaxProbabilityChoices = tmp.maxAbstractRepresentative(variablesToAbstract);
                 storm::dd::Add<Type, ValueType> newMaxProbabilities = tmp.maxAbstract(variablesToAbstract).swapVariables(game.getRowColumnMetaVariablePairs());
 
@@ -72,14 +87,14 @@ namespace storm {
                 spanningTree |= updateStates.swapVariables(game.getRowColumnMetaVariablePairs()) && newMaxProbabilityChoices;
                 
                 // Continue exploration from states that have been updated.
-                border = updateStates.template toAdd<ValueType>();
+                border = updateStates;
             }
             
             return spanningTree;
         }
         
         template<storm::dd::DdType Type, typename ValueType>
-        std::pair<storm::dd::Bdd<Type>, storm::OptimizationDirection> pickPivotState(storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& transitionsMin, storm::dd::Bdd<Type> const& transitionsMax, std::set<storm::expressions::Variable> const& rowVariables, std::set<storm::expressions::Variable> const& columnVariables, storm::dd::Bdd<Type> const& pivotStates, boost::optional<QuantitativeResultMinMax<Type, ValueType>> const& quantitativeResult = boost::none) {
+        PivotStateResult<Type> pickPivotState(storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& transitionsMin, storm::dd::Bdd<Type> const& transitionsMax, std::set<storm::expressions::Variable> const& rowVariables, std::set<storm::expressions::Variable> const& columnVariables, storm::dd::Bdd<Type> const& pivotStates, boost::optional<QuantitativeResultMinMax<Type, ValueType>> const& quantitativeResult = boost::none) {
             
             // Set up used variables.
             storm::dd::Bdd<Type> frontierMin = initialStates;
@@ -91,14 +106,14 @@ namespace storm {
             bool foundPivotState = !frontierPivotStates.isZero();
             if (foundPivotState) {
                 STORM_LOG_TRACE("Picked pivot state from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total.");
-                return std::make_pair(frontierPivotStates.existsAbstractRepresentative(rowVariables), storm::OptimizationDirection::Minimize);
+                return PivotStateResult<Type>(frontierPivotStates.existsAbstractRepresentative(rowVariables), storm::OptimizationDirection::Minimize);
             } else {
-                
                 // Otherwise, we perform a simulatenous BFS in the sense that we make one step in both the min and max
                 // transitions and check for pivot states we encounter.
                 while (!foundPivotState) {
                     frontierMin = frontierMin.relationalProduct(transitionsMin, rowVariables, columnVariables);
                     frontierMax = frontierMax.relationalProduct(transitionsMax, rowVariables, columnVariables);
+                    ++level;
                     
                     storm::dd::Bdd<Type> frontierMinPivotStates = frontierMin && pivotStates;
                     storm::dd::Bdd<Type> frontierMaxPivotStates = frontierMax && pivotStates;
@@ -122,7 +137,7 @@ namespace storm {
                             }
                             
                             STORM_LOG_TRACE("Picked pivot state with difference " << diffValue << " from " << numberOfPivotStateCandidatesOnLevel << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total.");
-                            return std::make_pair(direction == storm::OptimizationDirection::Minimize ? diffMin.maxAbstractRepresentative(rowVariables) : diffMax.maxAbstractRepresentative(rowVariables), direction);
+                            return PivotStateResult<Type>(direction == storm::OptimizationDirection::Minimize ? diffMin.maxAbstractRepresentative(rowVariables) : diffMax.maxAbstractRepresentative(rowVariables), direction);
                         } else {
                             STORM_LOG_TRACE("Picked pivot state from " << numberOfPivotStateCandidatesOnLevel << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total.");
                             
@@ -133,15 +148,14 @@ namespace storm {
                                 direction = storm::OptimizationDirection::Maximize;
                             }
                             
-                            return std::make_pair(direction == storm::OptimizationDirection::Minimize ? frontierMinPivotStates.existsAbstractRepresentative(rowVariables) : frontierMaxPivotStates.existsAbstractRepresentative(rowVariables), direction);
+                            return PivotStateResult<Type>(direction == storm::OptimizationDirection::Minimize ? frontierMinPivotStates.existsAbstractRepresentative(rowVariables) : frontierMaxPivotStates.existsAbstractRepresentative(rowVariables), direction);
                         }
                     }
-                    ++level;
                 }
             }
             
             STORM_LOG_ASSERT(false, "This point must not be reached, because then no pivot state could be found.");
-            return std::make_pair(storm::dd::Bdd<Type>(), storm::OptimizationDirection::Minimize);
+            return PivotStateResult<Type>(storm::dd::Bdd<Type>(), storm::OptimizationDirection::Minimize);
         }
         
         template <storm::dd::DdType Type, typename ValueType>
@@ -206,17 +220,10 @@ namespace storm {
             return RefinementPredicates(fromGuard ? RefinementPredicates::Source::Guard : RefinementPredicates::Source::WeakestPrecondition, {newPredicate});
         }
         
-        template<storm::dd::DdType Type>
-        struct PivotStateResult {
-            storm::dd::Bdd<Type> reachableTransitionsMin;
-            storm::dd::Bdd<Type> reachableTransitionsMax;
-            storm::dd::Bdd<Type> pivotStates;
-        };
-        
         template<storm::dd::DdType Type, typename ValueType>
-        PivotStateResult<Type> computePivotStates(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& minPlayer1Strategy, storm::dd::Bdd<Type> const& minPlayer2Strategy, storm::dd::Bdd<Type> const& maxPlayer1Strategy, storm::dd::Bdd<Type> const& maxPlayer2Strategy) {
+        PivotStateCandidatesResult<Type> computePivotStates(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& minPlayer1Strategy, storm::dd::Bdd<Type> const& minPlayer2Strategy, storm::dd::Bdd<Type> const& maxPlayer1Strategy, storm::dd::Bdd<Type> const& maxPlayer2Strategy) {
             
-            PivotStateResult<Type> result;
+            PivotStateCandidatesResult<Type> result;
             
             // Build the fragment of transitions that is reachable by either the min or the max strategies.
             result.reachableTransitionsMin = (transitionMatrixBdd && minPlayer1Strategy && minPlayer2Strategy).existsAbstract(game.getNondeterminismVariables());
@@ -279,18 +286,127 @@ namespace storm {
         }
         
         template<storm::dd::DdType Type, typename ValueType>
-        storm::expressions::Expression MenuGameRefiner<Type, ValueType>::buildTraceFormula(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& spanningTree, storm::dd::Bdd<Type> const& pivotState) const {
+        std::vector<std::vector<storm::expressions::Expression>> MenuGameRefiner<Type, ValueType>::buildTrace(storm::expressions::ExpressionManager& expressionManager, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& spanningTree, storm::dd::Bdd<Type> const& pivotState) const {
+            std::vector<std::vector<storm::expressions::Expression>> result;
+            
+            // Prepare some variables.
             AbstractionInformation<Type> const& abstractionInformation = abstractor.get().getAbstractionInformation();
+            std::set<storm::expressions::Variable> variablesToAbstract(game.getColumnVariables());
+            variablesToAbstract.insert(game.getPlayer1Variables().begin(), game.getPlayer1Variables().end());
+            variablesToAbstract.insert(game.getProbabilisticBranchingVariables().begin(), game.getProbabilisticBranchingVariables().end());
 
-            storm::dd::Bdd<Type> currentState = pivotState;
+            std::map<storm::expressions::Variable, storm::expressions::Variable> oldToNewVariables;
+            for (auto const& variable : abstractionInformation.getExpressionManager().getVariables()) {
+                oldToNewVariables[variable] = expressionManager.getVariable(variable.getName());
+            }
+            std::map<storm::expressions::Variable, storm::expressions::Expression> lastSubstitution;
+            for (auto const& variable : oldToNewVariables) {
+                lastSubstitution[variable.second] = variable.second;
+            }
+            std::map<storm::expressions::Variable, storm::expressions::Variable> stepVariableToCopiedVariableMap;
             
+            // Start with the target state part of the trace.
+            storm::storage::BitVector decodedTargetState = abstractionInformation.decodeState(pivotState);
+            result.emplace_back(abstractionInformation.getPredicates(decodedTargetState));
+            for (auto& predicate : result.back()) {
+                predicate = predicate.changeManager(expressionManager);
+            }
+            
+            pivotState.template toAdd<ValueType>().exportToDot("pivot.dot");
+            
+            // Perform a backward search for an initial state.
+            storm::dd::Bdd<Type> currentState = pivotState;
+            uint64_t cnt = 0;
             while ((currentState && game.getInitialStates()).isZero()) {
                 storm::dd::Bdd<Type> predecessorTransition = currentState.swapVariables(game.getRowColumnMetaVariablePairs()) && spanningTree;
+                std::tuple<storm::storage::BitVector, uint64_t, uint64_t> decodedPredecessor = abstractionInformation.decodeStatePlayer1ChoiceAndUpdate(predecessorTransition);
+                std::cout << "got predecessor " << std::get<0>(decodedPredecessor) << ", choice " << std::get<1>(decodedPredecessor) << " and update " << std::get<2>(decodedPredecessor) << std::endl;
                 
+                // predecessorTransition.template toAdd<ValueType>().exportToDot("pred_" + std::to_string(cnt) + ".dot");
                 
+                // Create a new copy of each variable to use for this step.
+                std::map<storm::expressions::Variable, storm::expressions::Expression> substitution;
+                for (auto const& variablePair : oldToNewVariables) {
+                    storm::expressions::Variable variableCopy = expressionManager.declareVariableCopy(variablePair.second);
+                    substitution[variablePair.second] = variableCopy;
+                    stepVariableToCopiedVariableMap[variableCopy] = variablePair.second;
+                }
+                
+                // Retrieve the variable updates that the predecessor needs to perform to get to the current state.
+                auto variableUpdates = abstractor.get().getVariableUpdates(std::get<1>(decodedPredecessor), std::get<2>(decodedPredecessor));
+                for (auto const& update : variableUpdates) {
+                    storm::expressions::Variable newVariable = oldToNewVariables.at(update.first);
+                    if (update.second.hasBooleanType()) {
+                        result.back().push_back(storm::expressions::iff(lastSubstitution.at(oldToNewVariables.at(update.first)), update.second.changeManager(expressionManager).substitute(substitution)));
+                    } else {
+                        result.back().push_back(lastSubstitution.at(oldToNewVariables.at(update.first)) == update.second.changeManager(expressionManager).substitute(substitution));
+                    }
+                }
+                
+                // Add the guard of the choice.
+                result.back().push_back(abstractor.get().getGuard(std::get<1>(decodedPredecessor)).changeManager(expressionManager).substitute(substitution));
+                
+                // Retrieve the predicate valuation in the predecessor.
+                result.emplace_back(abstractionInformation.getPredicates(std::get<0>(decodedPredecessor)));
+                for (auto& predicate : result.back()) {
+                    predicate = predicate.changeManager(expressionManager).substitute(substitution);
+                }
+                
+                // Move backwards one step.
+                lastSubstitution = std::move(substitution);
+                currentState = predecessorTransition.existsAbstract(variablesToAbstract);
+                ++cnt;
             }
             
-            return storm::expressions::Expression();
+            result.back().push_back(abstractor.get().getInitialExpression().changeManager(expressionManager).substitute(lastSubstitution));
+            return result;
+        }
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        boost::optional<std::vector<storm::expressions::Expression>> MenuGameRefiner<Type, ValueType>::derivePredicatesFromInterpolation(storm::abstraction::MenuGame<Type, ValueType> const& game, PivotStateResult<Type> const& pivotStateResult, storm::dd::Bdd<Type> const& minPlayer1Strategy, storm::dd::Bdd<Type> const& minPlayer2Strategy, storm::dd::Bdd<Type> const& maxPlayer1Strategy, storm::dd::Bdd<Type> const& maxPlayer2Strategy) const {
+            
+            // Compute the most probable path from any initial state to the pivot state.
+            storm::dd::Bdd<Type> spanningTree = getMostProbablePathSpanningTree(game, pivotStateResult.pivotState, pivotStateResult.fromDirection == storm::OptimizationDirection::Minimize ? minPlayer1Strategy && minPlayer2Strategy : maxPlayer1Strategy && maxPlayer2Strategy);
+            
+            // Create a new expression manager that we can use for the interpolation.
+            std::shared_ptr<storm::expressions::ExpressionManager> interpolationManager = abstractor.get().getAbstractionInformation().getExpressionManager().clone();
+            
+            // Build the trace of the most probable path in terms of which predicates hold in each step.
+            std::vector<std::vector<storm::expressions::Expression>> trace = buildTrace(*interpolationManager, game, spanningTree, pivotStateResult.pivotState);
+
+            // Now encode the trace as an SMT problem.
+            storm::solver::MathsatSmtSolver interpolatingSolver(*interpolationManager, storm::solver::MathsatSmtSolver::Options(true, false, true));
+            
+            uint64_t stepCounter = 0;
+            for (auto const& step : trace) {
+                std::cout << "group " << stepCounter << std::endl;
+                interpolatingSolver.setInterpolationGroup(stepCounter);
+                for (auto const& predicate : step) {
+                    std::cout << predicate << std::endl;
+                    interpolatingSolver.add(predicate);
+                }
+                ++stepCounter;
+            }
+            
+            storm::solver::SmtSolver::CheckResult result = interpolatingSolver.check();
+            if (result == storm::solver::SmtSolver::CheckResult::Unsat) {
+                STORM_LOG_TRACE("Trace formula is unsatisfiable. Starting interpolation.");
+                
+                std::vector<storm::expressions::Expression> interpolants;
+                std::vector<uint64_t> prefix;
+                for (uint64_t step = stepCounter; step > 1; --step) {
+                    prefix.push_back(step - 1);
+                    storm::expressions::Expression interpolant = interpolatingSolver.getInterpolant(prefix);
+                    STORM_LOG_ASSERT(!interpolant.isTrue() && !interpolant.isFalse(), "Expected other interpolant.");
+                    interpolants.push_back(interpolant);
+                }
+                return boost::make_optional(interpolants);
+            } else {
+                STORM_LOG_TRACE("Trace formula is satisfiable.");
+                std::cout << interpolatingSolver.getModelAsValuation().toString(true) << std::endl;
+            }
+            
+            return boost::none;
         }
         
         template<storm::dd::DdType Type, typename ValueType>
@@ -307,28 +423,30 @@ namespace storm {
             minPlayer1Strategy = (maxPlayer1Strategy && qualitativeResult.prob0Min.getPlayer2States()).existsAbstract(game.getPlayer1Variables()).ite(maxPlayer1Strategy, minPlayer1Strategy);
             
             // Compute all reached pivot states.
-            PivotStateResult<Type> pivotStateResult = computePivotStates(game, transitionMatrixBdd, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
+            PivotStateCandidatesResult<Type> pivotStateCandidatesResult = computePivotStates(game, transitionMatrixBdd, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
             
             // We can only refine in case we have a reachable player 1 state with a player 2 successor (under either
             // player 1's min or max strategy) such that from this player 2 state, both prob0 min and prob1 max define
             // strategies and they differ. Hence, it is possible that we arrive at a point where no suitable pivot state
             // is found. In this case, we abort the qualitative refinement here.
-            if (pivotStateResult.pivotStates.isZero()) {
+            if (pivotStateCandidatesResult.pivotStates.isZero()) {
                 return false;
             }
-            STORM_LOG_ASSERT(!pivotStateResult.pivotStates.isZero(), "Unable to proceed without pivot state candidates.");
+            STORM_LOG_ASSERT(!pivotStateCandidatesResult.pivotStates.isZero(), "Unable to proceed without pivot state candidates.");
             
             // Now that we have the pivot state candidates, we need to pick one.
-            std::pair<storm::dd::Bdd<Type>, storm::OptimizationDirection> pivotState = pickPivotState<Type, ValueType>(game.getInitialStates(), pivotStateResult.reachableTransitionsMin, pivotStateResult.reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables(), pivotStateResult.pivotStates);
+            PivotStateResult<Type> pivotStateResult = pickPivotState<Type, ValueType>(game.getInitialStates(), pivotStateCandidatesResult.reachableTransitionsMin, pivotStateCandidatesResult.reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables(), pivotStateCandidatesResult.pivotStates);
             
-            // FIXME.
-            storm::dd::Bdd<Type> spanningTree = getMostProbablePathSpanningTree(game, pivotState.first, pivotState.second == storm::OptimizationDirection::Minimize ? minPlayer1Strategy && minPlayer2Strategy : maxPlayer1Strategy && maxPlayer2Strategy);
-            storm::expressions::Expression traceFormula = buildTraceFormula(game, spanningTree, pivotState.first);
-            
-            exit(-1);
+            boost::optional<std::vector<storm::expressions::Expression>> interpolationPredicates = derivePredicatesFromInterpolation(game, pivotStateResult, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
+            if (interpolationPredicates) {
+                std::cout << "Got interpolation predicates!" << std::endl;
+                for (auto const& pred : interpolationPredicates.get()) {
+                    std::cout << "pred: " << pred << std::endl;
+                }
+            }
             
             // Derive predicate based on the selected pivot state.
-            RefinementPredicates predicates = derivePredicatesFromPivotState(game, pivotState.first, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
+            RefinementPredicates predicates = derivePredicatesFromPivotState(game, pivotStateResult.pivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
             std::vector<storm::expressions::Expression> preparedPredicates = preprocessPredicates(predicates.getPredicates(), (predicates.getSource() == RefinementPredicates::Source::Guard && splitGuards) || (predicates.getSource() == RefinementPredicates::Source::WeakestPrecondition && splitPredicates));
             performRefinement(createGlobalRefinement(preparedPredicates));
             return true;
@@ -344,19 +462,23 @@ namespace storm {
             storm::dd::Bdd<Type> maxPlayer2Strategy = quantitativeResult.max.player2Strategy;
             
             // Compute all reached pivot states.
-            PivotStateResult<Type> pivotStateResult = computePivotStates(game, transitionMatrixBdd, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
+            PivotStateCandidatesResult<Type> pivotStateCandidatesResult = computePivotStates(game, transitionMatrixBdd, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
             
-            STORM_LOG_ASSERT(!pivotStateResult.pivotStates.isZero(), "Unable to refine without pivot state candidates.");
+            STORM_LOG_ASSERT(!pivotStateCandidatesResult.pivotStates.isZero(), "Unable to refine without pivot state candidates.");
             
             // Now that we have the pivot state candidates, we need to pick one.
-            std::pair<storm::dd::Bdd<Type>, storm::OptimizationDirection> pivotState = pickPivotState<Type, ValueType>(game.getInitialStates(), pivotStateResult.reachableTransitionsMin, pivotStateResult.reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables(), pivotStateResult.pivotStates);
+            PivotStateResult<Type> pivotStateResult = pickPivotState<Type, ValueType>(game.getInitialStates(), pivotStateCandidatesResult.reachableTransitionsMin, pivotStateCandidatesResult.reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables(), pivotStateCandidatesResult.pivotStates);
             
-            // FIXME.
-            getMostProbablePathSpanningTree(game, pivotState.first, pivotState.second == storm::OptimizationDirection::Minimize ? minPlayer1Strategy && minPlayer2Strategy : maxPlayer1Strategy && maxPlayer2Strategy);
-            exit(-1);
+            boost::optional<std::vector<storm::expressions::Expression>> interpolationPredicates = derivePredicatesFromInterpolation(game, pivotStateResult, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
+            if (interpolationPredicates) {
+                std::cout << "Got interpolation predicates!" << std::endl;
+                for (auto const& pred : interpolationPredicates.get()) {
+                    std::cout << "pred: " << pred << std::endl;
+                }
+            }
             
             // Derive predicate based on the selected pivot state.
-            RefinementPredicates predicates = derivePredicatesFromPivotState(game, pivotState.first, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
+            RefinementPredicates predicates = derivePredicatesFromPivotState(game, pivotStateResult.pivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
             std::vector<storm::expressions::Expression> preparedPredicates = preprocessPredicates(predicates.getPredicates(), (predicates.getSource() == RefinementPredicates::Source::Guard && splitGuards) || (predicates.getSource() == RefinementPredicates::Source::WeakestPrecondition && splitPredicates));
             performRefinement(createGlobalRefinement(preparedPredicates));
             return true;

src/storm/abstraction/MenuGameRefiner.h

@@ -4,6 +4,8 @@
 #include <vector>
 #include <memory>
 
+#include <boost/optional.hpp>
+
 #include "storm/abstraction/RefinementCommand.h"
 #include "storm/abstraction/QualitativeResultMinMax.h"
 #include "storm/abstraction/QuantitativeResultMinMax.h"
@@ -41,6 +43,14 @@ namespace storm {
             std::vector<storm::expressions::Expression> predicates;
         };
         
+        template<storm::dd::DdType Type>
+        struct PivotStateResult {
+            PivotStateResult(storm::dd::Bdd<Type> const& pivotState, storm::OptimizationDirection fromDirection);
+            
+            storm::dd::Bdd<Type> pivotState;
+            storm::OptimizationDirection fromDirection;
+        };
+        
         template<storm::dd::DdType Type, typename ValueType>
         class MenuGameRefiner {
         public:
@@ -82,7 +92,8 @@ namespace storm {
              */
             std::vector<RefinementCommand> createGlobalRefinement(std::vector<storm::expressions::Expression> const& predicates) const;
             
-            storm::expressions::Expression buildTraceFormula(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& spanningTree, storm::dd::Bdd<Type> const& pivotState) const;
+            boost::optional<std::vector<storm::expressions::Expression>> derivePredicatesFromInterpolation(storm::abstraction::MenuGame<Type, ValueType> const& game, PivotStateResult<Type> const& pivotStateResult, storm::dd::Bdd<Type> const& minPlayer1Strategy, storm::dd::Bdd<Type> const& minPlayer2Strategy, storm::dd::Bdd<Type> const& maxPlayer1Strategy, storm::dd::Bdd<Type> const& maxPlayer2Strategy) const;
+            std::vector<std::vector<storm::expressions::Expression>> buildTrace(storm::expressions::ExpressionManager& expressionManager, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& spanningTree, storm::dd::Bdd<Type> const& pivotState) const;
             
             void performRefinement(std::vector<RefinementCommand> const& refinementCommands) const;
             

src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -121,6 +121,11 @@ namespace storm {
                 return std::make_pair(0, modules.front().getCommands().size());
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::expressions::Expression PrismMenuGameAbstractor<DdType, ValueType>::getInitialExpression() const {
+                return program.get().getInitialStatesExpression();
+            }
+            
             template <storm::dd::DdType DdType, typename ValueType>
             storm::dd::Bdd<DdType> PrismMenuGameAbstractor<DdType, ValueType>::getStates(storm::expressions::Expression const& predicate) {
                 STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created.");

src/storm/abstraction/prism/PrismMenuGameAbstractor.h

@@ -84,6 +84,11 @@ namespace storm {
                  */
                 std::pair<uint64_t, uint64_t> getPlayer1ChoiceRange() const override;
                 
+                /*!
+                 * Retrieves the expression that characterizes the initial states.
+                 */
+                storm::expressions::Expression getInitialExpression() const override;
+                
                 /*!
                  * Retrieves the set of states (represented by a BDD) satisfying the given predicate, assuming that it
                  * was either given as an initial predicate or used as a refining predicate later.

src/storm/storage/expressions/ChangeManagerVisitor.cpp

@@ -0,0 +1,68 @@
+#include "storm/storage/expressions/ChangeManagerVisitor.h"
+
+#include "storm/storage/expressions/Expressions.h"
+
+namespace storm {
+    namespace expressions {
+        
+        ChangeManagerVisitor::ChangeManagerVisitor(ExpressionManager const& manager) : manager(manager) {
+            // Intentionally left empty.
+        }
+        
+        Expression ChangeManagerVisitor::changeManager(storm::expressions::Expression const& expression) {
+            return Expression(boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.accept(*this, boost::none)));
+        }
+        
+        boost::any ChangeManagerVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) {
+            auto newCondition = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getCondition()->accept(*this, data));
+            auto newThen = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getThenExpression()->accept(*this, data));
+            auto newElse = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getElseExpression()->accept(*this, data));
+            return std::shared_ptr<BaseExpression const>(new IfThenElseExpression(manager, expression.getType(), newCondition, newThen, newElse));
+        }
+        
+        boost::any ChangeManagerVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) {
+            auto newFirstOperand = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getFirstOperand()->accept(*this, data));
+            auto newSecondOperand = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getSecondOperand()->accept(*this, data));
+            return std::shared_ptr<BaseExpression const>(new BinaryBooleanFunctionExpression(manager, expression.getType(), newFirstOperand, newSecondOperand, expression.getOperatorType()));
+        }
+        
+        boost::any ChangeManagerVisitor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) {
+            auto newFirstOperand = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getFirstOperand()->accept(*this, data));
+            auto newSecondOperand = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getSecondOperand()->accept(*this, data));
+            return std::shared_ptr<BaseExpression const>(new BinaryNumericalFunctionExpression(manager, expression.getType(), newFirstOperand, newSecondOperand, expression.getOperatorType()));
+        }
+        
+        boost::any ChangeManagerVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) {
+            auto newFirstOperand = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getFirstOperand()->accept(*this, data));
+            auto newSecondOperand = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getSecondOperand()->accept(*this, data));
+            return std::shared_ptr<BaseExpression const>(new BinaryRelationExpression(manager, expression.getType(), newFirstOperand, newSecondOperand, expression.getRelationType()));
+        }
+        
+        boost::any ChangeManagerVisitor::visit(VariableExpression const& expression, boost::any const& data) {
+            return std::shared_ptr<BaseExpression const>(new VariableExpression(manager.getVariable(expression.getVariableName())));
+        }
+        
+        boost::any ChangeManagerVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
+            auto newOperand = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getOperand()->accept(*this, data));
+            return std::shared_ptr<BaseExpression const>(new UnaryBooleanFunctionExpression(manager, expression.getType(), newOperand, expression.getOperatorType()));
+        }
+        
+        boost::any ChangeManagerVisitor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) {
+            auto newOperand = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getOperand()->accept(*this, data));
+            return std::shared_ptr<BaseExpression const>(new UnaryNumericalFunctionExpression(manager, expression.getType(), newOperand, expression.getOperatorType()));
+        }
+        
+        boost::any ChangeManagerVisitor::visit(BooleanLiteralExpression const& expression, boost::any const& data) {
+            return std::shared_ptr<BaseExpression const>(new BooleanLiteralExpression(manager, expression.getValue()));
+        }
+        
+        boost::any ChangeManagerVisitor::visit(IntegerLiteralExpression const& expression, boost::any const& data) {
+            return std::shared_ptr<BaseExpression const>(new IntegerLiteralExpression(manager, expression.getValue()));
+        }
+        
+        boost::any ChangeManagerVisitor::visit(RationalLiteralExpression const& expression, boost::any const& data) {
+            return std::shared_ptr<BaseExpression const>(new RationalLiteralExpression(manager, expression.getValue()));
+        }
+        
+    }
+}

src/storm/storage/expressions/ChangeManagerVisitor.h

@@ -0,0 +1,33 @@
+#pragma once
+
+#include "storm/storage/expressions/ExpressionVisitor.h"
+#include "storm/storage/expressions/ExpressionManager.h"
+
+namespace storm {
+    namespace expressions {
+        
+        class Expression;
+        
+        class ChangeManagerVisitor : public ExpressionVisitor {
+        public:
+            ChangeManagerVisitor(ExpressionManager const& manager);
+            
+            Expression changeManager(storm::expressions::Expression const& expression);
+            
+            virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(BinaryRelationExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(VariableExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(BooleanLiteralExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override;
+            
+        private:
+            ExpressionManager const& manager;
+        };
+        
+    }
+}

src/storm/storage/expressions/Expression.cpp

@@ -6,6 +6,7 @@
 #include "storm/storage/expressions/SubstitutionVisitor.h"
 #include "storm/storage/expressions/LinearityCheckVisitor.h"
 #include "storm/storage/expressions/SyntacticalEqualityCheckVisitor.h"
+#include "storm/storage/expressions/ChangeManagerVisitor.h"
 #include "storm/storage/expressions/Expressions.h"
 #include "storm/exceptions/InvalidTypeException.h"
 #include "storm/exceptions/InvalidArgumentException.h"
@@ -32,6 +33,11 @@ namespace storm {
             // Intentionally left empty.
         }
         
+        Expression Expression::changeManager(ExpressionManager const& newExpressionManager) const {
+            ChangeManagerVisitor visitor(newExpressionManager);
+            return visitor.changeManager(*this);
+        }
+        
 		Expression Expression::substitute(std::map<Variable, Expression> const& identifierToExpressionMap) const {
             return SubstitutionVisitor<std::map<Variable, Expression>>(identifierToExpressionMap).substitute(*this);
         }

src/storm/storage/expressions/Expression.h

@@ -81,6 +81,11 @@ namespace storm {
             Expression& operator=(Expression&&) = default;
 #endif
             
+            /*!
+             * Converts the expression to an expression over the variables of the provided expression manager.
+             */
+            Expression changeManager(ExpressionManager const& newExpressionManager) const;
+            
             /*!
              * Substitutes all occurrences of the variables according to the given map. Note that this substitution is
              * done simultaneously, i.e., variables appearing in the expressions that were "plugged in" are not

src/storm/storage/expressions/ExpressionManager.cpp

@@ -56,6 +56,10 @@ namespace storm {
             // Intentionally left empty.
         }
         
+        std::shared_ptr<ExpressionManager> ExpressionManager::clone() const {
+            return std::shared_ptr<ExpressionManager>(new ExpressionManager(*this));
+        }
+        
         Expression ExpressionManager::boolean(bool value) const {
             return Expression(std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(*this, value)));
         }
@@ -125,6 +129,10 @@ namespace storm {
             return nameIndexPair != nameToIndexMapping.end();
         }
         
+        Variable ExpressionManager::declareVariableCopy(Variable const& variable) {
+            return declareFreshVariable(variable.getType(), true, "_" + variable.getName() + "_");
+        }
+        
         Variable ExpressionManager::declareVariable(std::string const& name, storm::expressions::Type const& variableType, bool auxiliary) {
             STORM_LOG_THROW(!variableExists(name), storm::exceptions::InvalidArgumentException, "Variable with name '" << name << "' already exists.");
             return declareOrGetVariable(name, variableType, auxiliary);
@@ -187,7 +195,9 @@ namespace storm {
                 nameToIndexMapping[name] = newIndex;
                 indexToNameMapping[newIndex] = name;
                 indexToTypeMapping[newIndex] = variableType;
-                return Variable(this->getSharedPointer(), newIndex);
+                Variable result(this->getSharedPointer(), newIndex);
+                variableSet.insert(result);
+                return result;
             }
         }
         
@@ -197,6 +207,10 @@ namespace storm {
             return Variable(this->getSharedPointer(), nameIndexPair->second);
         }
         
+        std::set<Variable> const& ExpressionManager::getVariables() const {
+            return variableSet;
+        }
+        
         Expression ExpressionManager::getVariableExpression(std::string const& name) const {
             return Expression(getVariable(name));
         }

src/storm/storage/expressions/ExpressionManager.h

@@ -71,16 +71,14 @@ namespace storm {
              */
             ExpressionManager();
             
-            // Explicitly delete copy construction/assignment, since the manager is supposed to be stored as a pointer
-            // of some sort. This is because the expression classes store a reference to the manager and it must
-            // therefore be guaranteed that they do not become invalid, because the manager has been copied.
-            ExpressionManager(ExpressionManager const& other) = delete;
-            ExpressionManager& operator=(ExpressionManager const& other) = delete;
-#ifndef WINDOWS
+            /*!
+             * Creates a new expression manager with the same set of variables.
+             */
+            std::shared_ptr<ExpressionManager> clone() const;
+            
             // Create default instantiations for the move construction/assignment.
             ExpressionManager(ExpressionManager&& other) = default;
             ExpressionManager& operator=(ExpressionManager&& other) = default;
-#endif
 
             /*!
              * Creates an expression that characterizes the given boolean literal.
@@ -147,7 +145,15 @@ namespace storm {
              * @return The rational type.
              */
             Type const& getRationalType() const;
-            
+
+            /*!
+             * Declares a variable that is a copy of the provided variable (i.e. has the same type).
+             *
+             * @param variable The variable of which to create a copy.
+             * @return The newly declared variable.
+             */
+            Variable declareVariableCopy(Variable const& variable);
+
             /*!
              * Declares a variable with a name that must not yet exist and its corresponding type. Note that the name
              * must not start with two underscores since these variables are reserved for internal use only.
@@ -218,6 +224,11 @@ namespace storm {
              */
             Variable getVariable(std::string const& name) const;
             
+            /*!
+             * Retrieves the set of all variables known to this manager.
+             */
+            std::set<Variable> const& getVariables() const;
+            
             /*!
              * Retrieves whether a variable with the given name is known to the manager.
              *
@@ -361,6 +372,12 @@ namespace storm {
             friend std::ostream& operator<<(std::ostream& out, ExpressionManager const& manager);
             
         private:
+            // Explicitly make copy construction/assignment private, since the manager is supposed to be stored as a pointer
+            // of some sort. This is because the expression classes store a reference to the manager and it must
+            // therefore be guaranteed that they do not become invalid, because the manager has been copied.
+            ExpressionManager(ExpressionManager const& other) = default;
+            ExpressionManager& operator=(ExpressionManager const& other) = default;
+            
             /*!
              * Checks whether the given variable name is valid.
              *
@@ -405,6 +422,9 @@ namespace storm {
              */
             uint_fast64_t getNumberOfAuxiliaryVariables(storm::expressions::Type const& variableType) const;
             
+            // The set of all known variables.
+            std::set<Variable> variableSet;
+            
             // A mapping from all variable names (auxiliary + normal) to their indices.
             std::unordered_map<std::string, uint_fast64_t> nameToIndexMapping;