template edges in JANI models

src/storm/abstraction/AbstractionInformation.cpp

@@ -443,7 +443,8 @@ namespace storm {
         }
         
         template <storm::dd::DdType DdType>
-        std::map<uint_fast64_t, std::pair<storm::storage::BitVector, double>> AbstractionInformation<DdType>::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<DdType> const& choice) const {
+        template <typename ValueType>
+        std::map<uint_fast64_t, std::pair<storm::storage::BitVector, ValueType>> AbstractionInformation<DdType>::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<DdType> const& choice) const {
             std::map<uint_fast64_t, std::pair<storm::storage::BitVector, double>> result;
             
             storm::dd::Add<DdType, double> lowerChoiceAsAdd = choice.template toAdd<double>();
@@ -487,5 +488,8 @@ namespace storm {
         
         template class AbstractionInformation<storm::dd::DdType::CUDD>;
         template class AbstractionInformation<storm::dd::DdType::Sylvan>;
+        
+        template std::map<uint_fast64_t, std::pair<storm::storage::BitVector, double>> AbstractionInformation<storm::dd::DdType::CUDD>::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<storm::dd::DdType::CUDD> const& choice) const;
+        template std::map<uint_fast64_t, std::pair<storm::storage::BitVector, double>> AbstractionInformation<storm::dd::DdType::Sylvan>::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<storm::dd::DdType::Sylvan> const& choice) const;
     }
 }

src/storm/abstraction/AbstractionInformation.h

@@ -456,7 +456,8 @@ namespace storm {
             /*!
              * Decodes the choice in the form of a BDD over the destination variables.
              */
-            std::map<uint_fast64_t, std::pair<storm::storage::BitVector, double>> decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<DdType> const& choice) const;
+            template<typename ValueType>
+            std::map<uint_fast64_t, std::pair<storm::storage::BitVector, ValueType>> decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<DdType> const& choice) const;
             
             /*!
              * Decodes the given BDD (over source, player 1 and aux variables) into a bit vector indicating the truth

src/storm/abstraction/MenuGameRefiner.cpp

@@ -15,6 +15,9 @@
 
 #include "storm/settings/SettingsManager.h"
 
+#include "storm-config.h"
+#include "storm/adapters/CarlAdapter.h"
+
 namespace storm {
     namespace abstraction {
         
@@ -252,8 +255,8 @@ namespace storm {
                 STORM_LOG_TRACE("No bottom state successor. Deriving a new predicate using weakest precondition.");
                 
                 // Decode both choices to explicit mappings.
-                std::map<uint64_t, std::pair<storm::storage::BitVector, ValueType>> lowerChoiceUpdateToSuccessorMapping = abstractionInformation.decodeChoiceToUpdateSuccessorMapping(lowerChoice);
-                std::map<uint64_t, std::pair<storm::storage::BitVector, ValueType>> upperChoiceUpdateToSuccessorMapping = abstractionInformation.decodeChoiceToUpdateSuccessorMapping(upperChoice);
+                std::map<uint64_t, std::pair<storm::storage::BitVector, ValueType>> lowerChoiceUpdateToSuccessorMapping = abstractionInformation.template decodeChoiceToUpdateSuccessorMapping<ValueType>(lowerChoice);
+                std::map<uint64_t, std::pair<storm::storage::BitVector, ValueType>> upperChoiceUpdateToSuccessorMapping = abstractionInformation.template decodeChoiceToUpdateSuccessorMapping<ValueType>(upperChoice);
                 STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode (" << lowerChoiceUpdateToSuccessorMapping.size() << " vs. " << upperChoiceUpdateToSuccessorMapping.size() << ").");
                 
                 // First, sort updates according to probability mass.
@@ -714,6 +717,11 @@ namespace storm {
         
         template class MenuGameRefiner<storm::dd::DdType::CUDD, double>;
         template class MenuGameRefiner<storm::dd::DdType::Sylvan, double>;
+
+#ifdef STORM_HAVE_CARL
+        // Currently, this instantiation does not work.
+        // template class MenuGameRefiner<storm::dd::DdType::Sylvan, storm::RationalFunction>;
+#endif
         
     }
 }

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -57,7 +57,7 @@ namespace storm {
                 STORM_LOG_THROW(originalModel.getModelType() == storm::jani::ModelType::DTMC || originalModel.getModelType() == storm::jani::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/MDPs are supported by the game-based model checker.");
                 
                 // Flatten the parallel composition.
-                preprocessedModel = model.flattenComposition();
+                preprocessedModel = model.asJaniModel().flattenComposition();
             }
             
             bool reuseAll = storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isReuseAllResultsSet();

src/storm/parser/JaniParser.cpp

@@ -1036,8 +1036,11 @@ namespace storm {
                     STORM_LOG_THROW(guardExpr.hasBooleanType(), storm::exceptions::InvalidJaniException, "Guard " << guardExpr << " does not have Boolean type.");
                 }
                 assert(guardExpr.isInitialized());
+                
+                std::shared_ptr<storm::jani::TemplateEdge> templateEdge = automaton.createTemplateEdge(guardExpr);
+                
                 STORM_LOG_THROW(edgeEntry.count("destinations") == 1, storm::exceptions::InvalidJaniException, "A single list of destinations must be given in edge from '" << sourceLoc << "' in automaton '" << name << "'");
-                std::vector<storm::jani::EdgeDestination> edgeDestinations;
+                std::vector<std::pair<uint64_t, storm::expressions::Expression>> destinationLocationsAndProbabilities;
                 for(auto const& destEntry : edgeEntry.at("destinations")) {
                     // target location
                     STORM_LOG_THROW(edgeEntry.count("location") == 1, storm::exceptions::InvalidJaniException, "Each destination in edge from '" << sourceLoc << "' in automaton '" << name << "' must have a target location");
@@ -1072,9 +1075,10 @@ namespace storm {
                             assignments.emplace_back(lhs, assignmentExpr);
                         }
                     }
-                    edgeDestinations.emplace_back(locIds.at(targetLoc), probExpr, assignments);
+                    destinationLocationsAndProbabilities.emplace_back(locIds.at(targetLoc), probExpr);
+                    templateEdge->addDestination(storm::jani::TemplateEdgeDestination(assignments));
                 }
-                automaton.addEdge(storm::jani::Edge(locIds.at(sourceLoc), parentModel.getActionIndex(action), rateExpr.isInitialized() ? boost::optional<storm::expressions::Expression>(rateExpr) : boost::none, guardExpr, edgeDestinations));
+                automaton.addEdge(storm::jani::Edge(locIds.at(sourceLoc), parentModel.getActionIndex(action), rateExpr.isInitialized() ? boost::optional<storm::expressions::Expression>(rateExpr) : boost::none, templateEdge, destinationLocationsAndProbabilities));
             }
 
             return automaton;

src/storm/storage/jani/Automaton.cpp

@@ -59,7 +59,7 @@ namespace storm {
             return name;
         }
 
-        Variable& Automaton::addVariable(Variable const &variable) {
+        Variable const& Automaton::addVariable(Variable const &variable) {
             if (variable.isBooleanVariable()) {
                 return addVariable(variable.asBooleanVariable());
             } else if (variable.isBoundedIntegerVariable()) {
@@ -293,6 +293,11 @@ namespace storm {
             return ConstEdges(it1, it2);
         }
         
+        std::shared_ptr<TemplateEdge> Automaton::createTemplateEdge(storm::expressions::Expression const& guard) {
+            templateEdges.emplace_back(std::make_shared<TemplateEdge>(guard));
+            return templateEdges.back();
+        }
+        
         void Automaton::addEdge(Edge const& edge) {
             STORM_LOG_THROW(edge.getSourceLocationIndex() < locations.size(), storm::exceptions::InvalidArgumentException, "Cannot add edge with unknown source location index '" << edge.getSourceLocationIndex() << "'.");
             
@@ -317,7 +322,6 @@ namespace storm {
             actionIndices.insert(edge.getActionIndex());
         }
         
-        
         std::vector<Edge>& Automaton::getEdges() {
             return edges;
         }
@@ -415,14 +419,17 @@ namespace storm {
             
             this->setInitialStatesRestriction(this->getInitialStatesRestriction().substitute(substitution));
             
+            for (auto& templateEdge : templateEdges) {
+                templateEdge->substitute(substitution);
+            }
             for (auto& edge : this->getEdges()) {
                 edge.substitute(substitution);
             }
         }
         
         void Automaton::finalize(Model const& containingModel) {
-            for (auto& edge : edges) {
-                edge.finalize(containingModel);
+            for (auto& templateEdge : templateEdges) {
+                templateEdge->finalize(containingModel);
             }
         }
         
@@ -450,8 +457,8 @@ namespace storm {
         }
         
         void Automaton::pushEdgeAssignmentsToDestinations() {
-            for (auto& edge : edges) {
-                edge.pushAssignmentsToDestinations();
+            for (auto& templateEdge : templateEdges) {
+                templateEdge->pushAssignmentsToDestinations();
             }
         }
         
@@ -465,8 +472,8 @@ namespace storm {
         }
         
         void Automaton::liftTransientEdgeDestinationAssignments() {
-            for (auto& edge : this->getEdges()) {
-                edge.liftTransientDestinationAssignments();
+            for (auto& templateEdge : templateEdges) {
+                templateEdge->liftTransientDestinationAssignments();
             }
         }
         

src/storm/storage/jani/Automaton.h

@@ -2,11 +2,13 @@
 
 #include <string>
 #include <cstdint>
+#include <vector>
 #include <unordered_map>
 #include <boost/container/flat_set.hpp>
 
 #include "storm/storage/jani/VariableSet.h"
 #include "storm/storage/jani/Edge.h"
+#include "storm/storage/jani/TemplateEdge.h"
 #include "storm/storage/jani/Location.h"
 
 namespace storm {
@@ -103,7 +105,7 @@ namespace storm {
             /*!
              * Adds the given variable to this automaton
              */
-            Variable& addVariable(Variable const& variable);
+            Variable const& addVariable(Variable const& variable);
 
             /*!
              * Adds the given Boolean variable to this automaton.
@@ -235,6 +237,11 @@ namespace storm {
              */
             ConstEdges getEdgesFromLocation(uint64_t locationIndex, uint64_t actionIndex) const;
             
+            /*!
+             * Creates a new template edge that can be used to create new edges.
+             */
+            std::shared_ptr<TemplateEdge> createTemplateEdge(storm::expressions::Expression const& guard);
+            
             /*!
              * Adds an edge to the automaton.
              */
@@ -358,6 +365,9 @@ namespace storm {
             /// All edges of the automaton
             std::vector<Edge> edges;
             
+            /// The templates for the contained edges.
+            std::vector<std::shared_ptr<TemplateEdge>> templateEdges;
+            
             /// A mapping from location indices to the starting indices. If l is mapped to i, it means that the edges
             /// leaving location l start at index i of the edges vector.
             std::vector<uint64_t> locationToStartingIndex;

src/storm/storage/jani/BoundedIntegerVariable.cpp

@@ -18,7 +18,7 @@ namespace storm {
         }
 
         std::unique_ptr<Variable> BoundedIntegerVariable::clone() const {
-            return std::make_unique<Variable>(*this);
+            return std::make_unique<BoundedIntegerVariable>(*this);
         }
         
         storm::expressions::Expression const& BoundedIntegerVariable::getLowerBound() const {

src/storm/storage/jani/Edge.cpp

@@ -8,8 +8,14 @@
 namespace storm {
     namespace jani {
         
-        Edge::Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional<storm::expressions::Expression> const& rate, storm::expressions::Expression const& guard, std::vector<EdgeDestination> destinations) : sourceLocationIndex(sourceLocationIndex), actionIndex(actionIndex), rate(rate), guard(guard), destinations(destinations), assignments(), writtenGlobalVariables() {
-            // Intentionally left empty.
+        Edge::Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional<storm::expressions::Expression> const& rate, std::shared_ptr<TemplateEdge const> const& templateEdge, std::vector<std::pair<uint64_t, storm::expressions::Expression>> const& destinationTargetLocationsAndProbabilities) : sourceLocationIndex(sourceLocationIndex), actionIndex(actionIndex), rate(rate), templateEdge(templateEdge) {
+            
+            // Create the concrete destinations from the template edge.
+            STORM_LOG_THROW(templateEdge->getNumberOfDestinations() == destinationTargetLocationsAndProbabilities.size(), storm::exceptions::InvalidArgumentException, "Sizes of template edge destinations and target locations mismatch.");
+            for (uint64_t i = 0; i < templateEdge->getNumberOfDestinations(); ++i) {
+                auto const& templateDestination = templateEdge->getDestination(i);
+                destinations.emplace_back(destinationTargetLocationsAndProbabilities[i].first, destinationTargetLocationsAndProbabilities[i].second, templateDestination);
+            }
         }
         
         uint64_t Edge::getSourceLocationIndex() const {
@@ -37,11 +43,7 @@ namespace storm {
         }
         
         storm::expressions::Expression const& Edge::getGuard() const {
-            return guard;
-        }
-        
-        void Edge::setGuard(storm::expressions::Expression const& guard) {
-            this->guard = guard;
+            return templateEdge->getGuard();
         }
         
         EdgeDestination const& Edge::getDestination(uint64_t index) const {
@@ -52,120 +54,41 @@ namespace storm {
             return destinations;
         }
         
-        std::vector<EdgeDestination>& Edge::getDestinations() {
-            return destinations;
-        }
-        
         std::size_t Edge::getNumberOfDestinations() const {
             return destinations.size();
         }
         
-        void Edge::addDestination(EdgeDestination const& destination) {
-            destinations.push_back(destination);
-        }
-        
         OrderedAssignments const& Edge::getAssignments() const {
-            return assignments;
+            return templateEdge->getAssignments();
         }
         
         void Edge::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
-            this->setGuard(this->getGuard().substitute(substitution));
             if (this->hasRate()) {
                 this->setRate(this->getRate().substitute(substitution));
             }
-            for (auto& assignment : this->getAssignments()) {
-                assignment.substitute(substitution);
-            }
-            for (auto& destination : this->getDestinations()) {
+            for (auto& destination : destinations) {
                 destination.substitute(substitution);
             }
         }
-        
-        void Edge::finalize(Model const& containingModel) {
-            for (auto const& destination : getDestinations()) {
-                for (auto const& assignment : destination.getOrderedAssignments().getAllAssignments()) {
-                    if (containingModel.getGlobalVariables().hasVariable(assignment.getExpressionVariable())) {
-                        writtenGlobalVariables.insert(assignment.getExpressionVariable());
-                    }
-                }
-            }
-        }
-        
+                
         bool Edge::hasSilentAction() const {
             return actionIndex == Model::SILENT_ACTION_INDEX;
         }
         
-        bool Edge::addTransientAssignment(Assignment const& assignment) {
-            STORM_LOG_THROW(assignment.isTransient(), storm::exceptions::InvalidArgumentException, "Must not add non-transient assignment to location.");
-            return assignments.add(assignment);
-        }
-        
-        void Edge::liftTransientDestinationAssignments() {
-            if (!destinations.empty()) {
-                auto const& destination = *destinations.begin();
-                
-                for (auto const& assignment : destination.getOrderedAssignments().getTransientAssignments()) {
-                    // Check if we can lift the assignment to the edge.
-                    bool canBeLifted = true;
-                    for (auto const& destination : destinations) {
-                        if (!destination.hasAssignment(assignment)) {
-                            canBeLifted = false;
-                            break;
-                        }
-                    }
-                    
-                    // If so, remove the assignment from all destinations.
-                    if (canBeLifted) {
-                        this->addTransientAssignment(assignment);
-                        for (auto& destination : destinations) {
-                            destination.removeAssignment(assignment);
-                        }
-                    }
-                }
-            }
-        }
-        
-        void Edge::pushAssignmentsToDestinations() {
-            STORM_LOG_ASSERT(!destinations.empty(), "Need non-empty destinations for this transformation.");
-            for (auto const& assignment : this->getAssignments()) {
-                for (auto& destination : destinations) {
-                    destination.addAssignment(assignment);
-                }
-            }
-            this->assignments.clear();
-        }
-        
         boost::container::flat_set<storm::expressions::Variable> const& Edge::getWrittenGlobalVariables() const {
-            return writtenGlobalVariables;
+            return templateEdge->getWrittenGlobalVariables();
         }
         
         bool Edge::usesVariablesInNonTransientAssignments(std::set<storm::expressions::Variable> const& variables) const {
-            for (auto const& destination : destinations) {
-                for (auto const& assignment : destination.getOrderedAssignments().getNonTransientAssignments()) {
-                    if (assignment.getAssignedExpression().containsVariable(variables)) {
-                        return true;
-                    }
-                }
-            }
-            return false;
+            return templateEdge->usesVariablesInNonTransientAssignments(variables);
         }
         
         bool Edge::hasTransientEdgeDestinationAssignments() const {
-            for (auto const& destination : this->getDestinations()) {
-                if (destination.hasTransientAssignment()) {
-                    return true;
-                }
-            }
-            return false;
+            return templateEdge->hasTransientEdgeDestinationAssignments();
         }
         
         bool Edge::usesAssignmentLevels() const {
-            for (auto const& destination : this->getDestinations()) {
-                if (destination.usesAssignmentLevels()) {
-                    return true;
-                }
-            }
-            return false;
+            return templateEdge->usesAssignmentLevels();
         }
     }
 }

src/storm/storage/jani/Edge.h

@@ -1,21 +1,21 @@
 #pragma once
 
+#include <memory>
+
 #include <boost/optional.hpp>
-#include <boost/container/flat_set.hpp>
 
+#include "storm/storage/jani/TemplateEdge.h"
 #include "storm/storage/jani/EdgeDestination.h"
 #include "storm/storage/jani/OrderedAssignments.h"
 
 namespace storm {
     namespace jani {
         
-        class Model;
-        
         class Edge {
         public:
             Edge() = default;
             
-            Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional<storm::expressions::Expression> const& rate, storm::expressions::Expression const& guard, std::vector<EdgeDestination> destinations = {});
+            Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional<storm::expressions::Expression> const& rate, std::shared_ptr<TemplateEdge const> const& templateEdge, std::vector<std::pair<uint64_t, storm::expressions::Expression>> const& destinationTargetLocationsAndProbabilities);
             
             /*!
              * Retrieves the index of the source location.
@@ -57,11 +57,6 @@ namespace storm {
              */
             storm::expressions::Expression const& getGuard() const;
             
-            /*!
-             * Sets a new guard for this edge.
-             */
-            void setGuard(storm::expressions::Expression const& guard);
-
             /*!
              * Retrieves the destination with the given index.
              */
@@ -71,63 +66,26 @@ namespace storm {
              * Retrieves the destinations of this edge.
              */
             std::vector<EdgeDestination> const& getDestinations() const;
-
-            /*!
-             * Retrieves the destinations of this edge.
-             */
-            std::vector<EdgeDestination>& getDestinations();
             
             /*!
              * Retrieves the number of destinations of this edge.
              */
             std::size_t getNumberOfDestinations() const;
             
-            /*!
-             * Adds the given destination to the destinations of this edge.
-             */
-            void addDestination(EdgeDestination const& destination);
-            
             /*!
              * Substitutes all variables in all expressions according to the given substitution.
              */
             void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
-            
+                        
             /*!
-             * Finalizes the building of this edge. Subsequent changes to the edge require another call to this
-             * method. Note that this method is invoked by a call to <code>finalize</code> to the containing model.
-             */
-            void finalize(Model const& containingModel);
-            
-            /*!
-             * Retrieves a set of (global) variables that are written by at least one of the edge's destinations. Note
-             * that prior to calling this, the edge has to be finalized.
+             * Retrieves a set of (global) variables that are written by at least one of the edge's destinations.
              */
             boost::container::flat_set<storm::expressions::Variable> const& getWrittenGlobalVariables() const;
-
-            /*!
-             * Adds a transient assignment to this edge.
-             *
-             * @param assignment The transient assignment to add.
-             * @return True if the assignment was added.
-             */
-            bool addTransientAssignment(Assignment const& assignment);
             
             /*!
              * Retrieves the assignments of this edge.
              */
             OrderedAssignments const& getAssignments() const;
-
-            /*!
-             * Finds the transient assignments common to all destinations and lifts them to the edge. Afterwards, these
-             * assignments are no longer contained in the destination. Note that this may modify the semantics of the
-             * model if assignment levels are being used somewhere in the model.
-             */
-            void liftTransientDestinationAssignments();
-            
-            /**
-             * Shifts the assingments from the edges to the destinations.
-             */
-            void pushAssignmentsToDestinations();
             
             /*!
              * Checks whether the provided variables appear on the right-hand side of non-transient assignments.
@@ -155,18 +113,11 @@ namespace storm {
             /// models, this must be set to none.
             boost::optional<storm::expressions::Expression> rate;
             
-            /// The guard that defines when this edge is enabled.
-            storm::expressions::Expression guard;
+            /// The template of this edge: guards and destinations.
+            std::shared_ptr<TemplateEdge const> templateEdge;
             
-            /// The destinations of this edge.
+            /// The concrete destination objects.
             std::vector<EdgeDestination> destinations;
-            
-            /// The assignments made when taking this edge.
-            OrderedAssignments assignments;
-            
-            /// A set of global variables that is written by at least one of the edge's destinations. This set is
-            /// initialized by the call to <code>finalize</code>.
-            boost::container::flat_set<storm::expressions::Variable> writtenGlobalVariables;
         };
         
     }

src/storm/storage/jani/EdgeDestination.cpp

@@ -6,7 +6,7 @@
 namespace storm {
     namespace jani {
         
-        EdgeDestination::EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, std::shared_ptr<TemplateEdgeDestination const> const& templateEdgeDestination) : locationIndex(locationIndex), probability(probability), templateEdgeDestination(templateEdgeDestination) {
+        EdgeDestination::EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, TemplateEdgeDestination const& templateEdgeDestination) : locationIndex(locationIndex), probability(probability), templateEdgeDestination(templateEdgeDestination) {
             // Intentionally left empty.
         }
         
@@ -33,7 +33,7 @@ namespace storm {
         }
         
         OrderedAssignments const& EdgeDestination::getOrderedAssignments() const {
-            return templateEdgeDestination->getOrderedAssignments();
+            return templateEdgeDestination.get().getOrderedAssignments();
         }
         
         void EdgeDestination::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
@@ -55,8 +55,8 @@ namespace storm {
             return this->getOrderedAssignments().getLowestLevel() != 0 || this->getOrderedAssignments().getHighestLevel() != 0;
         }
         
-        std::shared_ptr<TemplateEdgeDestination const> EdgeDestination::getTemplateEdgeDestination() const {
-            return templateEdgeDestination;
+        TemplateEdgeDestination const& EdgeDestination::getTemplateEdgeDestination() const {
+            return templateEdgeDestination.get();
         }
     }
 }

src/storm/storage/jani/EdgeDestination.h

@@ -14,7 +14,7 @@ namespace storm {
             /*!
              * Creates a new edge destination.
              */
-            EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, std::shared_ptr<TemplateEdgeDestination const> const& templateEdgeDestination);
+            EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, TemplateEdgeDestination const& templateEdgeDestination);
                         
             /*!
              * Retrieves the id of the destination location.
@@ -65,7 +65,7 @@ namespace storm {
             /*!
              * Retrieves the template destination for this destination.
              */
-            std::shared_ptr<TemplateEdgeDestination const> getTemplateEdgeDestination() const;
+            TemplateEdgeDestination const& getTemplateEdgeDestination() const;
             
         private:
             // The index of the destination location.
@@ -75,7 +75,7 @@ namespace storm {
             storm::expressions::Expression probability;
             
             // The template edge destination
-            std::shared_ptr<TemplateEdgeDestination const> templateEdgeDestination;
+            std::reference_wrapper<TemplateEdgeDestination const> templateEdgeDestination;
         };
         
     }

src/storm/storage/jani/Model.cpp

@@ -55,7 +55,7 @@ namespace storm {
             return name;
         }
         
-        void Model::flattenSynchronizationVector(Automaton& newAutomaton, std::unordered_map<std::vector<uint64_t>, uint64_t>& newLocations, std::unordered_map<std::string, uint64_t>& newActionToIndex, std::vector<std::set<uint64_t>>& synchronizingActionIndices, SynchronizationVector const& vector, std::vector<std::reference_wrapper<Automaton const>> const& composedAutomata, storm::solver::SmtSolver& solver) {
+        void Model::flattenSynchronizationVector(Automaton& newAutomaton, std::unordered_map<std::vector<uint64_t>, uint64_t, storm::utility::vector::VectorHash<uint64_t>>& newLocations, std::unordered_map<std::string, uint64_t>& newActionToIndex, std::vector<std::set<uint64_t>>& synchronizingActionIndices, SynchronizationVector const& vector, std::vector<std::reference_wrapper<Automaton const>> const& composedAutomata, storm::solver::SmtSolver& solver) const {
 
             // Gather all participating automata and the corresponding input symbols.
             std::vector<std::pair<std::reference_wrapper<Automaton const>, uint64_t>> participatingAutomataAndActions;
@@ -67,7 +67,6 @@ namespace storm {
                     synchronizingActionIndices[i].insert(actionIndex);
                 }
             }
-
         }
         
         Model Model::flattenComposition(std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) const {
@@ -134,7 +133,7 @@ namespace storm {
             }
 
             // Since we need to reduce a tuple of locations to a single location, we keep a hashmap for this.
-            std::unordered_map<std::vector<uint64_t>, uint64_t> newLocations;
+            std::unordered_map<std::vector<uint64_t>, uint64_t, storm::utility::vector::VectorHash<uint64_t>> newLocations;
             std::unordered_map<std::string, uint64_t> newActionToIndex;
             
             // Perform all necessary synchronizations and keep track which action indices participate in synchronization.

src/storm/storage/jani/Model.h

@@ -9,6 +9,7 @@
 #include "storm/storage/jani/Composition.h"
 
 #include "storm/utility/solver.h"
+#include "storm/utility/vector.h"
 
 namespace storm {
     namespace expressions {
@@ -396,7 +397,7 @@ namespace storm {
             /*!
              * Flattens the actions of the automata into new edges in the provided automaton.
              */
-            void flattenSynchronizationVector(Automaton& newAutomaton, std::unordered_map<std::vector<uint64_t>, uint64_t>& newLocations, std::unordered_map<std::string, uint64_t>& newActionToIndex, std::vector<std::set<uint64_t>>& synchronizingActionIndices, SynchronizationVector const& vector, std::vector<std::reference_wrapper<Automaton const>> const& composedAutomata, storm::solver::SmtSolver& solver);
+            void flattenSynchronizationVector(Automaton& newAutomaton, std::unordered_map<std::vector<uint64_t>, uint64_t, storm::utility::vector::VectorHash<uint64_t>>& newLocations, std::unordered_map<std::string, uint64_t>& newActionToIndex, std::vector<std::set<uint64_t>>& synchronizingActionIndices, SynchronizationVector const& vector, std::vector<std::reference_wrapper<Automaton const>> const& composedAutomata, storm::solver::SmtSolver& solver) const;
             
             /// The model name.
             std::string name;

src/storm/storage/jani/OrderedAssignments.cpp

@@ -73,7 +73,7 @@ namespace storm {
             if (allAssignments.empty()) {
                 return false;
             }
-            return getLowestLevel() == getHighestLevel();
+            return getLowestLevel() != getHighestLevel();
         }
         
         bool OrderedAssignments::empty() const {
@@ -115,6 +115,10 @@ namespace storm {
             return detail::ConstAssignments(nonTransientAssignments.begin(), nonTransientAssignments.end());
         }
         
+        bool OrderedAssignments::hasTransientAssignment() const {
+            return !transientAssignments.empty();
+        }
+        
         detail::Assignments::iterator OrderedAssignments::begin() {
             return detail::Assignments::make_iterator(allAssignments.begin());
         }

src/storm/storage/jani/OrderedAssignments.h

@@ -84,6 +84,11 @@ namespace storm {
              */
             detail::ConstAssignments getNonTransientAssignments() const;
 
+            /*!
+             * Retrieves whether the set of assignments has at least one transient assignment.
+             */
+            bool hasTransientAssignment() const;
+            
             /*!
              * Returns an iterator to the assignments.
              */

src/storm/storage/jani/TemplateEdge.cpp

@@ -1,12 +1,131 @@
 #include "storm/storage/jani/TemplateEdge.h"
 
+#include "storm/storage/jani/Model.h"
+
 namespace storm {
     namespace jani {
         
-        TemplateEdge::TemplateEdge(storm::expressions::Expression const& guard, std::vector<std::shared_ptr<TemplateEdgeDestination const>> destinations) : guard(guard), destinations(destinations) {
+        TemplateEdge::TemplateEdge(storm::expressions::Expression const& guard) : guard(guard) {
             // Intentionally left empty.
         }
         
+        void TemplateEdge::addDestination(TemplateEdgeDestination const& destination) {
+            destinations.emplace_back(destination);
+        }
+        
+        bool TemplateEdge::addTransientAssignment(Assignment const& assignment) {
+            return assignments.add(assignment);
+        }
+        
+        void TemplateEdge::finalize(Model const& containingModel) {
+            for (auto const& destination : getDestinations()) {
+                for (auto const& assignment : destination.getOrderedAssignments().getAllAssignments()) {
+                    if (containingModel.getGlobalVariables().hasVariable(assignment.getExpressionVariable())) {
+                        writtenGlobalVariables.insert(assignment.getExpressionVariable());
+                    }
+                }
+            }
+        }
+        
+        boost::container::flat_set<storm::expressions::Variable> const& TemplateEdge::getWrittenGlobalVariables() const {
+            return writtenGlobalVariables;
+        }
+        
+        storm::expressions::Expression const& TemplateEdge::getGuard() const {
+            return guard;
+        }
+        
+        std::size_t TemplateEdge::getNumberOfDestinations() const {
+            return destinations.size();
+        }
+        
+        std::vector<TemplateEdgeDestination> const& TemplateEdge::getDestinations() const {
+            return destinations;
+        }
+        
+        TemplateEdgeDestination const& TemplateEdge::getDestination(uint64_t index) const {
+            return destinations[index];
+        }
+
+        OrderedAssignments const& TemplateEdge::getAssignments() const {
+            return assignments;
+        }
+        
+        void TemplateEdge::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
+            guard = guard.substitute(substitution);
+
+            for (auto& assignment : assignments) {
+                assignment.substitute(substitution);
+            }
+
+            for (auto& destination : destinations) {
+                destination.substitute(substitution);
+            }
+        }
+
+        void TemplateEdge::liftTransientDestinationAssignments() {
+            if (!destinations.empty()) {
+                auto const& destination = *destinations.begin();
+                
+                for (auto const& assignment : destination.getOrderedAssignments().getTransientAssignments()) {
+                    // Check if we can lift the assignment to the edge.
+                    bool canBeLifted = true;
+                    for (auto const& destination : destinations) {
+                        if (!destination.hasAssignment(assignment)) {
+                            canBeLifted = false;
+                            break;
+                        }
+                    }
+                    
+                    // If so, remove the assignment from all destinations.
+                    if (canBeLifted) {
+                        this->addTransientAssignment(assignment);
+                        for (auto& destination : destinations) {
+                            destination.removeAssignment(assignment);
+                        }
+                    }
+                }
+            }
+        }
+        
+        void TemplateEdge::pushAssignmentsToDestinations() {
+            STORM_LOG_ASSERT(!destinations.empty(), "Need non-empty destinations for this transformation.");
+            for (auto const& assignment : this->getAssignments()) {
+                for (auto& destination : destinations) {
+                    destination.addAssignment(assignment);
+                }
+            }
+            this->assignments.clear();
+        }
+        
+        bool TemplateEdge::usesVariablesInNonTransientAssignments(std::set<storm::expressions::Variable> const& variables) const {
+            for (auto const& destination : destinations) {
+                for (auto const& assignment : destination.getOrderedAssignments().getNonTransientAssignments()) {
+                    if (assignment.getAssignedExpression().containsVariable(variables)) {
+                        return true;
+                    }
+                }
+            }
+            return false;
+        }
+        
+        bool TemplateEdge::hasTransientEdgeDestinationAssignments() const {
+            for (auto const& destination : this->getDestinations()) {
+                if (destination.hasTransientAssignment()) {
+                    return true;
+                }
+            }
+            return false;
+        }
+        
+        bool TemplateEdge::usesAssignmentLevels() const {
+            for (auto const& destination : this->getDestinations()) {
+                if (destination.usesAssignmentLevels()) {
+                    return true;
+                }
+            }
+            return false;
+        }
         
     }
 }

src/storm/storage/jani/TemplateEdge.h

@@ -3,24 +3,95 @@
 #include <vector>
 #include <memory>
 
+#include <boost/container/flat_set.hpp>
+
 #include "storm/storage/expressions/Expression.h"
 
 #include "storm/storage/jani/TemplateEdgeDestination.h"
 
 namespace storm {
     namespace jani {
+        class Model;
         
         class TemplateEdge {
         public:
             TemplateEdge() = default;
-            TemplateEdge(storm::expressions::Expression const& guard, std::vector<std::shared_ptr<TemplateEdgeDestination const>> destinations = {});
+            TemplateEdge(storm::expressions::Expression const& guard);
+
+            storm::expressions::Expression const& getGuard() const;
+
+            void addDestination(TemplateEdgeDestination const& destination);
+            
+            /*!
+             * Finalizes the building of this edge. Subsequent changes to the edge require another call to this
+             * method. Note that this method is invoked by a call to <code>finalize</code> to the containing model.
+             */
+            void finalize(Model const& containingModel);
+
+            std::size_t getNumberOfDestinations() const;
+            std::vector<TemplateEdgeDestination> const& getDestinations() const;
+            TemplateEdgeDestination const& getDestination(uint64_t index) const;
+            
+            OrderedAssignments const& getAssignments() const;
+            
+            /*!
+             * Adds a transient assignment to this edge.
+             *
+             * @param assignment The transient assignment to add.
+             * @return True if the assignment was added.
+             */
+            bool addTransientAssignment(Assignment const& assignment);
+            
+            /*!
+             * Retrieves a set of (global) variables that are written by at least one of the edge's destinations.
+             */
+            boost::container::flat_set<storm::expressions::Variable> const& getWrittenGlobalVariables() const;
+
+            /*!
+             * Substitutes all variables in all expressions according to the given substitution.
+             */
+            void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
+
+            /*!
+             * Finds the transient assignments common to all destinations and lifts them to the edge. Afterwards, these
+             * assignments are no longer contained in the destination. Note that this may modify the semantics of the
+             * model if assignment levels are being used somewhere in the model.
+             */
+            void liftTransientDestinationAssignments();
+            
+            /**
+             * Shifts the assingments from the edges to the destinations.
+             */
+            void pushAssignmentsToDestinations();
+            
+            /*!
+             * Checks whether the provided variables appear on the right-hand side of non-transient assignments.
+             */
+            bool usesVariablesInNonTransientAssignments(std::set<storm::expressions::Variable> const& variables) const;
             
+            /*!
+             * Retrieves whether there is any transient edge destination assignment in the edge.
+             */
+            bool hasTransientEdgeDestinationAssignments() const;
+            
+            /*!
+             * Retrieves whether the edge uses an assignment level other than zero.
+             */
+            bool usesAssignmentLevels() const;
+
         private:
             // The guard of the template edge.
             storm::expressions::Expression guard;
             
             // The destinations of the template edge.
-            std::vector<std::shared_ptr<TemplateEdgeDestination const>> destinations;
+            std::vector<TemplateEdgeDestination> destinations;
+            
+            /// The assignments made when taking this edge.
+            OrderedAssignments assignments;
+            
+            /// A set of global variables that is written by at least one of the edge's destinations. This set is
+            /// initialized by the call to <code>finalize</code>.
+            boost::container::flat_set<storm::expressions::Variable> writtenGlobalVariables;
         };
         
     }

src/storm/storage/jani/TemplateEdgeDestination.cpp

@@ -27,5 +27,20 @@ namespace storm {
             return assignments.remove(assignment);
         }
         
+        void TemplateEdgeDestination::addAssignment(Assignment const& assignment) {
+            assignments.add(assignment);
+        }
+        
+        bool TemplateEdgeDestination::hasAssignment(Assignment const& assignment) const {
+            return assignments.contains(assignment);
+        }
+        
+        bool TemplateEdgeDestination::hasTransientAssignment() const {
+            return assignments.hasTransientAssignment();
+        }
+        
+        bool TemplateEdgeDestination::usesAssignmentLevels() const {
+            return assignments.hasMultipleLevels();
+        }
     }
 }

src/storm/storage/jani/TemplateEdgeDestination.h

@@ -22,6 +22,7 @@ namespace storm {
             // Convenience methods to access the assignments.
             bool hasAssignment(Assignment const& assignment) const;
             bool removeAssignment(Assignment const& assignment);
+            void addAssignment(Assignment const& assignment);
             
             /*!
              * Retrieves whether this destination has transient assignments.

src/storm/storage/prism/ToJaniConverter.cpp

@@ -188,10 +188,10 @@ namespace storm {
                 }
                 
                 for (auto const& command : module.getCommands()) {
+                    std::shared_ptr<storm::jani::TemplateEdge> templateEdge = automaton.createTemplateEdge(command.getGuardExpression());
                     actionIndicesOfModule.insert(command.getActionIndex());
                     
                     boost::optional<storm::expressions::Expression> rateExpression;
-                    std::vector<storm::jani::EdgeDestination> destinations;
                     if (program.getModelType() == Program::ModelType::CTMC || program.getModelType() == Program::ModelType::CTMDP || (program.getModelType() == Program::ModelType::MA && command.isMarkovian())) {
                         for (auto const& update : command.getUpdates()) {
                             if (rateExpression) {
@@ -202,6 +202,7 @@ namespace storm {
                         }
                     }
                                         
+                    std::vector<std::pair<uint64_t, storm::expressions::Expression>> destinationLocationsAndProbabilities;
                     for (auto const& update : command.getUpdates()) {
                         std::vector<storm::jani::Assignment> assignments;
                         for (auto const& assignment : update.getAssignments()) {
@@ -209,18 +210,12 @@ namespace storm {
                         }
                         
                         if (rateExpression) {
-                            destinations.push_back(storm::jani::EdgeDestination(onlyLocationIndex, update.getLikelihoodExpression() / rateExpression.get(), assignments));
+                            destinationLocationsAndProbabilities.emplace_back(onlyLocationIndex, update.getLikelihoodExpression() / rateExpression.get());
                         } else {
-                            destinations.push_back(storm::jani::EdgeDestination(onlyLocationIndex, update.getLikelihoodExpression(), assignments));
+                            destinationLocationsAndProbabilities.emplace_back(onlyLocationIndex, update.getLikelihoodExpression());
                         }
-                    }
-                    
-                    // Create the edge object so we can add transient assignments.
-                    storm::jani::Edge newEdge;
-                    if (command.getActionName().empty()) {
-                        newEdge = storm::jani::Edge(onlyLocationIndex, storm::jani::Model::SILENT_ACTION_INDEX, rateExpression, command.getGuardExpression(), destinations);
-                    } else {
-                        newEdge = storm::jani::Edge(onlyLocationIndex, janiModel.getActionIndex(command.getActionName()), rateExpression, command.getGuardExpression(), destinations);
+                        
+                        templateEdge->addDestination(storm::jani::TemplateEdgeDestination(assignments));
                     }
                     
                     // Then add the transient assignments for the rewards. Note that we may do this only for the first
@@ -229,10 +224,18 @@ namespace storm {
                     auto transientEdgeAssignmentsToAdd = transientEdgeAssignments.find(janiModel.getActionIndex(command.getActionName()));
                     if (transientEdgeAssignmentsToAdd != transientEdgeAssignments.end()) {
                         for (auto const& assignment : transientEdgeAssignmentsToAdd->second) {
-                            newEdge.addTransientAssignment(assignment);
+                            templateEdge->addTransientAssignment(assignment);
                         }
                         transientEdgeAssignments.erase(transientEdgeAssignmentsToAdd);
                     }
+
+                    // Create the edge object.
+                    storm::jani::Edge newEdge;
+                    if (command.getActionName().empty()) {
+                        newEdge = storm::jani::Edge(onlyLocationIndex, storm::jani::Model::SILENT_ACTION_INDEX, rateExpression, templateEdge, destinationLocationsAndProbabilities);
+                    } else {
+                        newEdge = storm::jani::Edge(onlyLocationIndex, janiModel.getActionIndex(command.getActionName()), rateExpression, templateEdge, destinationLocationsAndProbabilities);
+                    }
                     
                     // Finally add the constructed edge.
                     automaton.addEdge(newEdge);

src/test/abstraction/PrismMenuGameTest.cpp

@@ -5,6 +5,7 @@
 
 #include "storm/parser/PrismParser.h"
 
+#include "storm/abstraction/MenuGameRefiner.h"
 #include "storm/abstraction/prism/PrismMenuGameAbstractor.h"
 
 #include "storm/storage/expressions/Expression.h"
@@ -25,9 +26,12 @@ TEST(PrismMenuGame, DieAbstractionTest_Cudd) {
     storm::expressions::ExpressionManager& manager = program.getManager();
     
     initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3));
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
-    
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::CUDD, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
+
     storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractor.abstract();
     
     EXPECT_EQ(26, game.getNumberOfTransitions());
@@ -43,7 +47,11 @@ TEST(PrismMenuGame, DieAbstractionTest_Sylvan) {
     
     initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3));
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::Sylvan, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
     
     storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractor.abstract();
     
@@ -53,22 +61,28 @@ TEST(PrismMenuGame, DieAbstractionTest_Sylvan) {
 }
 
 #ifdef STORM_HAVE_CARL
-TEST(PrismMenuGame, DieAbstractionTest_SylvanWithRationalFunction) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
+// Commented out due to incompatibility with new refiner functionality.
+// This functionality depends on some operators being available on the value type which are not there for rational functions.
+//TEST(PrismMenuGame, DieAbstractionTest_SylvanWithRationalFunction) {
+//    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
     
-    std::vector<storm::expressions::Expression> initialPredicates;
-    storm::expressions::ExpressionManager& manager = program.getManager();
+//    std::vector<storm::expressions::Expression> initialPredicates;
+//    storm::expressions::ExpressionManager& manager = program.getManager();
     
-    initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3));
+//    initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3));
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, storm::RationalFunction> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+//    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+
+//    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, storm::RationalFunction> abstractor(program, smtSolverFactory);
+//    storm::abstraction::MenuGameRefiner<storm::dd::DdType::Sylvan, storm::RationalFunction> refiner(abstractor, smtSolverFactory->create(manager));
+//    refiner.refine(initialPredicates);
     
-    storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, storm::RationalFunction> game = abstractor.abstract();
+//    storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, storm::RationalFunction> game = abstractor.abstract();
     
-    EXPECT_EQ(26, game.getNumberOfTransitions());
-    EXPECT_EQ(4, game.getNumberOfStates());
-    EXPECT_EQ(2, game.getBottomStates().getNonZeroCount());
-}
+//    EXPECT_EQ(26, game.getNumberOfTransitions());
+//    EXPECT_EQ(4, game.getNumberOfStates());
+//    EXPECT_EQ(2, game.getBottomStates().getNonZeroCount());
+//}
 #endif
 
 TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Cudd) {
@@ -79,9 +93,13 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Cudd) {
     
     initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3));
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
-    
-    ASSERT_NO_THROW(abstractor.refine({std::make_pair(manager.getVariableExpression("s") == manager.integer(7), true)}));
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::CUDD, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
+
+    ASSERT_NO_THROW(refiner.refine({manager.getVariableExpression("s") == manager.integer(7)}));
 
     storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractor.abstract();
     
@@ -98,9 +116,13 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Sylvan) {
     
     initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3));
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::Sylvan, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
     
-    ASSERT_NO_THROW(abstractor.refine({std::make_pair(manager.getVariableExpression("s") == manager.integer(7), true)}));
+    ASSERT_NO_THROW(refiner.refine({manager.getVariableExpression("s") == manager.integer(7)}));
     
     storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractor.abstract();
     
@@ -132,8 +154,12 @@ TEST(PrismMenuGame, DieFullAbstractionTest_Cudd) {
     initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(5));
     initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(6));
 
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
-    
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::CUDD, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
+
     storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractor.abstract();
     
     EXPECT_EQ(20, game.getNumberOfTransitions());
@@ -164,8 +190,12 @@ TEST(PrismMenuGame, DieFullAbstractionTest_Sylvan) {
     initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(5));
     initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(6));
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
-    
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::Sylvan, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
+
     storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractor.abstract();
     
     EXPECT_EQ(20, game.getNumberOfTransitions());
@@ -182,8 +212,12 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Cudd) {
     
     initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3));
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
-    
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::CUDD, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
+
     storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractor.abstract();
     
     EXPECT_EQ(31, game.getNumberOfTransitions());
@@ -200,8 +234,12 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Sylvan) {
     
     initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3));
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
-    
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::Sylvan, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
+
     storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractor.abstract();
     
     EXPECT_EQ(31, game.getNumberOfTransitions());
@@ -218,9 +256,13 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Cudd) {
     
     initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3));
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
-    
-    ASSERT_NO_THROW(abstractor.refine({std::make_pair(manager.getVariableExpression("observe0") + manager.getVariableExpression("observe1") + manager.getVariableExpression("observe2") + manager.getVariableExpression("observe3") + manager.getVariableExpression("observe4") <= manager.getVariableExpression("runCount"), true)}));
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::CUDD, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
+
+    ASSERT_NO_THROW(refiner.refine({manager.getVariableExpression("observe0") + manager.getVariableExpression("observe1") + manager.getVariableExpression("observe2") + manager.getVariableExpression("observe3") + manager.getVariableExpression("observe4") <= manager.getVariableExpression("runCount")}));
     
     storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractor.abstract();
     
@@ -238,9 +280,13 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Sylvan) {
     
     initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3));
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
-    
-    ASSERT_NO_THROW(abstractor.refine({std::make_pair(manager.getVariableExpression("observe0") + manager.getVariableExpression("observe1") + manager.getVariableExpression("observe2") + manager.getVariableExpression("observe3") + manager.getVariableExpression("observe4") <= manager.getVariableExpression("runCount"), true)}));
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::Sylvan, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
+
+    ASSERT_NO_THROW(refiner.refine({manager.getVariableExpression("observe0") + manager.getVariableExpression("observe1") + manager.getVariableExpression("observe2") + manager.getVariableExpression("observe3") + manager.getVariableExpression("observe4") <= manager.getVariableExpression("runCount")}));
     
     storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractor.abstract();
     
@@ -312,8 +358,12 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest_Cudd) {
     initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(3));
     initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(4));
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
-    
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::CUDD, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
+
     storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractor.abstract();
     
     EXPECT_EQ(15113, game.getNumberOfTransitions());
@@ -384,7 +434,11 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest_Sylvan) {
     initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(3));
     initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(4));
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+    
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::Sylvan, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
     
     storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractor.abstract();
     
@@ -404,8 +458,12 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Cudd) {
     initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(3));
     initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0));
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
-    
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::CUDD, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
+
     storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractor.abstract();
     
     EXPECT_EQ(90, game.getNumberOfTransitions());
@@ -424,7 +482,11 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) {
     initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(3));
     initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0));
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::Sylvan, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
     
     storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractor.abstract();
     
@@ -444,9 +506,13 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) {
     initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(3));
     initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0));
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
-    
-    ASSERT_NO_THROW(abstractor.refine({std::make_pair(manager.getVariableExpression("d1") + manager.getVariableExpression("d2") == manager.integer(7), true)}));
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::CUDD, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
+
+    ASSERT_NO_THROW(refiner.refine({manager.getVariableExpression("d1") + manager.getVariableExpression("d2") == manager.integer(7)}));
 
     storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractor.abstract();
 
@@ -466,9 +532,13 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) {
     initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(3));
     initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0));
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
-    
-    ASSERT_NO_THROW(abstractor.refine({std::make_pair(manager.getVariableExpression("d1") + manager.getVariableExpression("d2") == manager.integer(7), true)}));
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::CUDD, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
+
+    ASSERT_NO_THROW(refiner.refine({manager.getVariableExpression("d1") + manager.getVariableExpression("d2") == manager.integer(7)}));
     
     storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractor.abstract();
     
@@ -519,8 +589,12 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Cudd) {
     initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(5));
     initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(6));
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
-    
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::CUDD, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
+
     storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractor.abstract();
     
     EXPECT_EQ(436, game.getNumberOfTransitions());
@@ -570,8 +644,12 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Sylvan) {
     initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(5));
     initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(6));
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
-    
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::Sylvan, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
+
     storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractor.abstract();
     
     EXPECT_EQ(436, game.getNumberOfTransitions());
@@ -591,11 +669,15 @@ TEST(PrismMenuGame, WlanAbstractionTest_Cudd) {
     initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0));
     initialPredicates.push_back(manager.getVariableExpression("c1") == manager.getVariableExpression("c2"));
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
-    
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::CUDD, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
+
     storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractor.abstract();
     
-    EXPECT_EQ(1379, game.getNumberOfTransitions());
+    EXPECT_EQ(1507, game.getNumberOfTransitions());
     EXPECT_EQ(12, game.getNumberOfStates());
     EXPECT_EQ(8, game.getBottomStates().getNonZeroCount());
 }
@@ -612,11 +694,15 @@ TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) {
     initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0));
     initialPredicates.push_back(manager.getVariableExpression("c1") == manager.getVariableExpression("c2"));
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
-    
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::Sylvan, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
+
     storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractor.abstract();
     
-    EXPECT_EQ(1379, game.getNumberOfTransitions());
+    EXPECT_EQ(1507, game.getNumberOfTransitions());
     EXPECT_EQ(12, game.getNumberOfStates());
     EXPECT_EQ(8, game.getBottomStates().getNonZeroCount());
 }
@@ -633,13 +719,17 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) {
     initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0));
     initialPredicates.push_back(manager.getVariableExpression("c1") == manager.getVariableExpression("c2"));
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::CUDD, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
     
-    ASSERT_NO_THROW(abstractor.refine({std::make_pair(manager.getVariableExpression("backoff1") < manager.integer(7), true)}));
+    ASSERT_NO_THROW(refiner.refine({manager.getVariableExpression("backoff1") < manager.integer(7)}));
 
     storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractor.abstract();
 
-    EXPECT_EQ(2744, game.getNumberOfTransitions());
+    EXPECT_EQ(3000, game.getNumberOfTransitions());
     EXPECT_EQ(24, game.getNumberOfStates());
     EXPECT_EQ(16, game.getBottomStates().getNonZeroCount());
 }
@@ -656,13 +746,17 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) {
     initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0));
     initialPredicates.push_back(manager.getVariableExpression("c1") == manager.getVariableExpression("c2"));
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::Sylvan, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
     
-    ASSERT_NO_THROW(abstractor.refine({std::make_pair(manager.getVariableExpression("backoff1") < manager.integer(7), true)}));
+    ASSERT_NO_THROW(refiner.refine({manager.getVariableExpression("backoff1") < manager.integer(7)}));
     
     storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractor.abstract();
     
-    EXPECT_EQ(2744, game.getNumberOfTransitions());
+    EXPECT_EQ(3000, game.getNumberOfTransitions());
     EXPECT_EQ(24, game.getNumberOfStates());
     EXPECT_EQ(16, game.getBottomStates().getNonZeroCount());
 }
@@ -777,8 +871,12 @@ TEST(PrismMenuGame, WlanFullAbstractionTest_Cudd) {
     initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(0));
     initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(1));
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
-    
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::CUDD, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
+
     storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractor.abstract();
     
     EXPECT_EQ(9503, game.getNumberOfTransitions());
@@ -896,8 +994,12 @@ TEST(PrismMenuGame, WlanFullAbstractionTest_Sylvan) {
     initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(0));
     initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(1));
     
-    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
-    
+    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
+
+    storm::abstraction::prism::PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double> abstractor(program, smtSolverFactory);
+    storm::abstraction::MenuGameRefiner<storm::dd::DdType::Sylvan, double> refiner(abstractor, smtSolverFactory->create(manager));
+    refiner.refine(initialPredicates);
+
     storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractor.abstract();
     
     EXPECT_EQ(9503, game.getNumberOfTransitions());