fixes here and there

src/storm/abstraction/AbstractionInformation.cpp

@@ -14,7 +14,7 @@ namespace storm {
     namespace abstraction {
 
         template<storm::dd::DdType DdType>
-        AbstractionInformation<DdType>::AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::unique_ptr<storm::solver::SmtSolver>&& smtSolver, std::shared_ptr<storm::dd::DdManager<DdType>> ddManager) : expressionManager(expressionManager), equivalenceChecker(std::move(smtSolver)), ddManager(ddManager), allPredicateIdentities(ddManager->getBddOne()) {
+        AbstractionInformation<DdType>::AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::set<storm::expressions::Variable> const& allVariables, std::unique_ptr<storm::solver::SmtSolver>&& smtSolver, std::shared_ptr<storm::dd::DdManager<DdType>> ddManager) : expressionManager(expressionManager), equivalenceChecker(std::move(smtSolver)), variables(allVariables), ddManager(ddManager), allPredicateIdentities(ddManager->getBddOne()), expressionToBddMap() {
             // Intentionally left empty.
         }
         
@@ -45,6 +45,7 @@ namespace storm {
             for (uint64_t index = 0; index < predicates.size(); ++index) {
                 auto const& oldPredicate = predicates[index];
                 if (equivalenceChecker.areEquivalent(oldPredicate, predicate)) {
+                    expressionToBddMap[predicate] = expressionToBddMap.at(oldPredicate);
                     return index;
                 }
             }
@@ -70,6 +71,8 @@ namespace storm {
             orderedSourceVariables.push_back(newMetaVariable.first);
             orderedSuccessorVariables.push_back(newMetaVariable.second);
             ddVariableIndexToPredicateIndexMap[predicateIdentities.back().getIndex()] = predicateIndex;
+            expressionToBddMap[predicate] = predicateBdds[predicateIndex].first && !bottomStateBdds.first;
+
             return predicateIndex;
         }
 
@@ -311,14 +314,8 @@ namespace storm {
         }
         
         template<storm::dd::DdType DdType>
-        std::map<storm::expressions::Expression, storm::dd::Bdd<DdType>> AbstractionInformation<DdType>::getPredicateToBddMap() const {
-            std::map<storm::expressions::Expression, storm::dd::Bdd<DdType>> result;
-            
-            for (uint_fast64_t index = 0; index < predicates.size(); ++index) {
-                result[predicates[index]] = predicateBdds[index].first && !bottomStateBdds.first;
-            }
-            
-            return result;
+        std::map<storm::expressions::Expression, storm::dd::Bdd<DdType>> const& AbstractionInformation<DdType>::getPredicateToBddMap() const {
+            return expressionToBddMap;
         }
         
         template<storm::dd::DdType DdType>
@@ -446,8 +443,8 @@ namespace storm {
         }
         
         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;
+        std::map<uint_fast64_t, std::pair<storm::storage::BitVector, double>> 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>();
             for (auto const& successorValuePair : lowerChoiceAsAdd) {
@@ -461,7 +458,7 @@ namespace storm {
                     }
                 }
                 
-                result[updateIndex] = successor;
+                result[updateIndex] = std::make_pair(successor, successorValuePair.second);
             }
             return result;
         }

src/storm/abstraction/AbstractionInformation.h

@@ -34,10 +34,11 @@ namespace storm {
              * Creates a new abstraction information object.
              *
              * @param expressionManager The manager responsible for all variables and expressions during the abstraction process.
+             * @param allVariables All expression variables that can appear in predicates known to this object.
              * @param smtSolver An SMT solver that is used to detect equivalent predicates.
              * @param ddManager The manager responsible for the DDs.
              */
-            AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::unique_ptr<storm::solver::SmtSolver>&& smtSolver, std::shared_ptr<storm::dd::DdManager<DdType>> ddManager = std::make_shared<storm::dd::DdManager<DdType>>());
+            AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::set<storm::expressions::Variable> const& allVariables, std::unique_ptr<storm::solver::SmtSolver>&& smtSolver, std::shared_ptr<storm::dd::DdManager<DdType>> ddManager = std::make_shared<storm::dd::DdManager<DdType>>());
 
             /*!
              * Adds the given variable.
@@ -372,7 +373,7 @@ namespace storm {
              *
              * @return A mapping from predicates to their representing BDDs.
              */
-            std::map<storm::expressions::Expression, storm::dd::Bdd<DdType>> getPredicateToBddMap() const;
+            std::map<storm::expressions::Expression, storm::dd::Bdd<DdType>> const& getPredicateToBddMap() const;
             
             /*!
              * Retrieves the meta variables pairs for all predicates.
@@ -455,7 +456,7 @@ namespace storm {
             /*!
              * 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;
+            std::map<uint_fast64_t, std::pair<storm::storage::BitVector, double>> 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
@@ -564,6 +565,9 @@ namespace storm {
             
             /// The BDDs associated with the meta variables encoding auxiliary information.
             std::vector<storm::dd::Bdd<DdType>> auxVariableBdds;
+            
+            /// A mapping from expressions to the corresponding BDDs.
+            std::map<storm::expressions::Expression, storm::dd::Bdd<DdType>> expressionToBddMap;
         };
         
     }

src/storm/abstraction/LocalExpressionInformation.cpp

@@ -1,5 +1,7 @@
 #include "storm/abstraction/LocalExpressionInformation.h"
 
+#include "storm/abstraction/AbstractionInformation.h"
+
 #include <boost/algorithm/string/join.hpp>
 
 #include "storm/utility/macros.h"
@@ -7,7 +9,8 @@
 namespace storm {
     namespace abstraction {
         
-        LocalExpressionInformation::LocalExpressionInformation(std::set<storm::expressions::Variable> const& relevantVariables, std::vector<std::pair<storm::expressions::Expression, uint_fast64_t>> const& expressionIndexPairs) : relevantVariables(relevantVariables), expressionBlocks(relevantVariables.size()) {
+        template <storm::dd::DdType DdType>
+        LocalExpressionInformation<DdType>::LocalExpressionInformation(AbstractionInformation<DdType> const& abstractionInformation) : relevantVariables(abstractionInformation.getVariables()), expressionBlocks(relevantVariables.size()), abstractionInformation(abstractionInformation) {
             // Assign each variable to a new block.
             uint_fast64_t currentBlock = 0;
             variableBlocks.resize(relevantVariables.size());
@@ -17,40 +20,39 @@ namespace storm {
                 variableBlocks[currentBlock].insert(variable);
                 ++currentBlock;
             }
-            
-            // Add all expressions, which might relate some variables.
-            for (auto const& expressionIndexPair : expressionIndexPairs) {
-                this->addExpression(expressionIndexPair.first, expressionIndexPair.second);
-            }
         }
         
-        bool LocalExpressionInformation::addExpression(storm::expressions::Expression const& expression, uint_fast64_t globalExpressionIndex) {
+        template <storm::dd::DdType DdType>
+        bool LocalExpressionInformation<DdType>::addExpression(uint_fast64_t globalExpressionIndex) {
+            storm::expressions::Expression const& expression = abstractionInformation.get().getPredicateByIndex(globalExpressionIndex);
+            
             // Register the expression for all variables that appear in it.
             std::set<storm::expressions::Variable> expressionVariables = expression.getVariables();
             for (auto const& variable : expressionVariables) {
-                variableToExpressionsMapping[variable].insert(this->expressions.size());
+                variableToExpressionsMapping[variable].insert(globalExpressionIndex);
             }
             
             // Add the expression to the block of the first variable. When relating the variables, the blocks will
             // get merged (if necessary).
             STORM_LOG_ASSERT(!expressionVariables.empty(), "Found no variables in expression.");
-            expressionBlocks[getBlockIndexOfVariable(*expressionVariables.begin())].insert(this->expressions.size());
+            expressionBlocks[getBlockIndexOfVariable(*expressionVariables.begin())].insert(globalExpressionIndex);
             
             // Add expression and relate all the appearing variables.
-            this->globalToLocalIndexMapping[globalExpressionIndex] = this->expressions.size();
-            this->expressions.push_back(expression);
             return this->relate(expressionVariables);
         }
         
-        bool LocalExpressionInformation::areRelated(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable) {
+        template <storm::dd::DdType DdType>
+        bool LocalExpressionInformation<DdType>::areRelated(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable) {
             return getBlockIndexOfVariable(firstVariable) == getBlockIndexOfVariable(secondVariable);
         }
         
-        bool LocalExpressionInformation::relate(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable) {
+        template <storm::dd::DdType DdType>
+        bool LocalExpressionInformation<DdType>::relate(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable) {
             return this->relate({firstVariable, secondVariable});
         }
         
-        bool LocalExpressionInformation::relate(std::set<storm::expressions::Variable> const& variables) {
+        template <storm::dd::DdType DdType>
+        bool LocalExpressionInformation<DdType>::relate(std::set<storm::expressions::Variable> const& variables) {
             // Determine all blocks that need to be merged.
             std::set<uint_fast64_t> blocksToMerge;
             for (auto const& variable : variables) {
@@ -68,7 +70,8 @@ namespace storm {
             return true;
         }
         
-        void LocalExpressionInformation::mergeBlocks(std::set<uint_fast64_t> const& blocksToMerge) {
+        template <storm::dd::DdType DdType>
+        void LocalExpressionInformation<DdType>::mergeBlocks(std::set<uint_fast64_t> const& blocksToMerge) {
             // Merge all blocks into the block to keep.
             std::vector<std::set<storm::expressions::Variable>> newVariableBlocks;
             std::vector<std::set<uint_fast64_t>> newExpressionBlocks;
@@ -108,28 +111,34 @@ namespace storm {
             expressionBlocks = std::move(newExpressionBlocks);
         }
         
-        std::set<storm::expressions::Variable> const& LocalExpressionInformation::getBlockOfVariable(storm::expressions::Variable const& variable) const {
+        template <storm::dd::DdType DdType>
+        std::set<storm::expressions::Variable> const& LocalExpressionInformation<DdType>::getBlockOfVariable(storm::expressions::Variable const& variable) const {
             return variableBlocks[getBlockIndexOfVariable(variable)];
         }
         
-        uint_fast64_t LocalExpressionInformation::getNumberOfBlocks() const {
+        template <storm::dd::DdType DdType>
+        uint_fast64_t LocalExpressionInformation<DdType>::getNumberOfBlocks() const {
             return this->variableBlocks.size();
         }
         
-        std::set<storm::expressions::Variable> const& LocalExpressionInformation::getVariableBlockWithIndex(uint_fast64_t blockIndex) const {
+        template <storm::dd::DdType DdType>
+        std::set<storm::expressions::Variable> const& LocalExpressionInformation<DdType>::getVariableBlockWithIndex(uint_fast64_t blockIndex) const {
             return this->variableBlocks[blockIndex];
         }
         
-        uint_fast64_t LocalExpressionInformation::getBlockIndexOfVariable(storm::expressions::Variable const& variable) const {
+        template <storm::dd::DdType DdType>
+        uint_fast64_t LocalExpressionInformation<DdType>::getBlockIndexOfVariable(storm::expressions::Variable const& variable) const {
             STORM_LOG_ASSERT(this->relevantVariables.find(variable) != this->relevantVariables.end(), "Illegal variable '" << variable.getName() << "' for partition.");
             return this->variableToBlockMapping.find(variable)->second;
         }
         
-        std::set<uint_fast64_t> const& LocalExpressionInformation::getRelatedExpressions(storm::expressions::Variable const& variable) const {
+        template <storm::dd::DdType DdType>
+        std::set<uint_fast64_t> const& LocalExpressionInformation<DdType>::getRelatedExpressions(storm::expressions::Variable const& variable) const {
             return this->expressionBlocks[getBlockIndexOfVariable(variable)];
         }
         
-        std::set<uint_fast64_t> LocalExpressionInformation::getRelatedExpressions(std::set<storm::expressions::Variable> const& variables) const {
+        template <storm::dd::DdType DdType>
+        std::set<uint_fast64_t> LocalExpressionInformation<DdType>::getRelatedExpressions(std::set<storm::expressions::Variable> const& variables) const {
             // Start by determining the indices of all expression blocks that are related to any of the variables.
             std::set<uint_fast64_t> relatedExpressionBlockIndices;
             for (auto const& variable : variables) {
@@ -144,12 +153,14 @@ namespace storm {
             return result;
         }
         
-        std::set<uint_fast64_t> const& LocalExpressionInformation::getExpressionsUsingVariable(storm::expressions::Variable const& variable) const {
+        template <storm::dd::DdType DdType>
+        std::set<uint_fast64_t> const& LocalExpressionInformation<DdType>::getExpressionsUsingVariable(storm::expressions::Variable const& variable) const {
             STORM_LOG_ASSERT(this->relevantVariables.find(variable) != this->relevantVariables.end(), "Illegal variable '" << variable.getName() << "' for partition.");
             return this->variableToExpressionsMapping.find(variable)->second;
         }
         
-        std::set<uint_fast64_t> LocalExpressionInformation::getExpressionsUsingVariables(std::set<storm::expressions::Variable> const& variables) const {
+        template <storm::dd::DdType DdType>
+        std::set<uint_fast64_t> LocalExpressionInformation<DdType>::getExpressionsUsingVariables(std::set<storm::expressions::Variable> const& variables) const {
             std::set<uint_fast64_t> result;
             
             for (auto const& variable : variables) {
@@ -161,11 +172,8 @@ namespace storm {
             return result;
         }
         
-        storm::expressions::Expression const& LocalExpressionInformation::getExpression(uint_fast64_t expressionIndex) const {
-            return this->expressions[expressionIndex];
-        }
-        
-        std::ostream& operator<<(std::ostream& out, LocalExpressionInformation const& partition) {
+        template <storm::dd::DdType DdType>
+        std::ostream& operator<<(std::ostream& out, LocalExpressionInformation<DdType> const& partition) {
             std::vector<std::string> blocks;
             for (uint_fast64_t index = 0; index < partition.variableBlocks.size(); ++index) {
                 auto const& variableBlock = partition.variableBlocks[index];
@@ -177,9 +185,9 @@ namespace storm {
                 }
                 
                 std::vector<std::string> expressionsInBlock;
-                for (auto const& expression : expressionBlock) {
+                for (auto const& expressionIndex : expressionBlock) {
                     std::stringstream stream;
-                    stream << partition.expressions[expression];
+                    stream << partition.abstractionInformation.get().getPredicateByIndex(expressionIndex);
                     expressionsInBlock.push_back(stream.str());
                 }
                 
@@ -191,6 +199,11 @@ namespace storm {
             out << "}";
             return out;
         }
-        
+     
+        template class LocalExpressionInformation<storm::dd::DdType::CUDD>;
+        template class LocalExpressionInformation<storm::dd::DdType::Sylvan>;
+
+        template std::ostream& operator<<(std::ostream& out, LocalExpressionInformation<storm::dd::DdType::CUDD> const& partition);
+        template std::ostream& operator<<(std::ostream& out, LocalExpressionInformation<storm::dd::DdType::Sylvan> const& partition);
     }
 }

src/storm/abstraction/LocalExpressionInformation.h

@@ -8,27 +8,31 @@
 #include "storm/storage/expressions/Variable.h"
 #include "storm/storage/expressions/Expression.h"
 
+#include "storm/storage/dd/DdType.h"
+
 namespace storm {
     namespace abstraction {
         
+        template <storm::dd::DdType DdType>
+        class AbstractionInformation;
+        
+        template <storm::dd::DdType DdType>
         class LocalExpressionInformation {
         public:
             /*!
              * Constructs a new variable partition.
              *
-             * @param relevantVariables The variables of this partition.
-             * @param expressionIndexPairs The (initial) pairs of expressions and their global indices.
+             * @param abstractionInformation The object storing global information about the abstraction.
              */
-            LocalExpressionInformation(std::set<storm::expressions::Variable> const& relevantVariables, std::vector<std::pair<storm::expressions::Expression, uint_fast64_t>> const& expressionIndexPairs = {});
+            LocalExpressionInformation(AbstractionInformation<DdType> const& abstractionInformation);
             
             /*!
              * Adds the expression and therefore indirectly may cause blocks of variables to be merged.
              *
-             * @param expression The expression to add.
              * @param globalExpressionIndex The global index of the expression.
              * @return True iff the partition changed.
              */
-            bool addExpression(storm::expressions::Expression const& expression, uint_fast64_t globalExpressionIndex);
+            bool addExpression(uint_fast64_t globalExpressionIndex);
             
             /*!
              * Retrieves whether the two given variables are in the same block of the partition.
@@ -119,15 +123,8 @@ namespace storm {
              */
             std::set<uint_fast64_t> getExpressionsUsingVariables(std::set<storm::expressions::Variable> const& variables) const;
             
-            /*!
-             * Retrieves the expression with the given index.
-             *
-             * @param expressionIndex The index of the expression to retrieve.
-             * @return The corresponding expression.
-             */
-            storm::expressions::Expression const& getExpression(uint_fast64_t expressionIndex) const;
-            
-            friend std::ostream& operator<<(std::ostream& out, LocalExpressionInformation const& partition);
+            template<storm::dd::DdType DdTypePrime>
+            friend std::ostream& operator<<(std::ostream& out, LocalExpressionInformation<DdTypePrime> const& partition);
             
         private:
             /*!
@@ -152,14 +149,12 @@ namespace storm {
             // A mapping from variables to the indices of all expressions they appear in.
             std::unordered_map<storm::expressions::Variable, std::set<uint_fast64_t>> variableToExpressionsMapping;
             
-            // A mapping from global expression indices to local ones.
-            std::unordered_map<uint_fast64_t, uint_fast64_t> globalToLocalIndexMapping;
-            
-            // The vector of all expressions.
-            std::vector<storm::expressions::Expression> expressions;
+            // The object storing the abstraction information.
+            std::reference_wrapper<AbstractionInformation<DdType> const> abstractionInformation;
         };
         
-        std::ostream& operator<<(std::ostream& out, LocalExpressionInformation const& partition);
+        template<storm::dd::DdType DdType>
+        std::ostream& operator<<(std::ostream& out, LocalExpressionInformation<DdType> const& partition);
         
     }
 }

src/storm/abstraction/MenuGameRefiner.cpp

@@ -195,30 +195,85 @@ namespace storm {
                 STORM_LOG_TRACE("No bottom state successor. Deriving a new predicate using weakest precondition.");
                 
                 // Decode both choices to explicit mappings.
-                std::map<uint_fast64_t, storm::storage::BitVector> lowerChoiceUpdateToSuccessorMapping = abstractionInformation.decodeChoiceToUpdateSuccessorMapping(lowerChoice);
-                std::map<uint_fast64_t, storm::storage::BitVector> upperChoiceUpdateToSuccessorMapping = abstractionInformation.decodeChoiceToUpdateSuccessorMapping(upperChoice);
+                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);
                 STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode (" << lowerChoiceUpdateToSuccessorMapping.size() << " vs. " << upperChoiceUpdateToSuccessorMapping.size() << ").");
                 
-                // Now go through the mappings and find points of deviation. Currently, we take the first deviation.
-                auto lowerIt = lowerChoiceUpdateToSuccessorMapping.begin();
-                auto lowerIte = lowerChoiceUpdateToSuccessorMapping.end();
-                auto upperIt = upperChoiceUpdateToSuccessorMapping.begin();
-                for (; lowerIt != lowerIte; ++lowerIt, ++upperIt) {
-                    STORM_LOG_ASSERT(lowerIt->first == upperIt->first, "Update indices mismatch.");
-                    uint_fast64_t updateIndex = lowerIt->first;
-                    bool deviates = lowerIt->second != upperIt->second;
+                // First, sort updates according to probability mass.
+                std::vector<std::pair<uint64_t, ValueType>> updateIndicesAndMasses;
+                for (auto const& entry : lowerChoiceUpdateToSuccessorMapping) {
+                    updateIndicesAndMasses.emplace_back(entry.first, entry.second.second);
+                }
+                std::sort(updateIndicesAndMasses.begin(), updateIndicesAndMasses.end(), [] (std::pair<uint64_t, ValueType> const& a, std::pair<uint64_t, ValueType> const& b) { return a.second > b.second; });
+                
+                // Now find the update with the highest probability mass among all deviating updates. More specifically,
+                // we determine the set of predicate indices for which there is a deviation.
+                std::set<uint64_t> deviationPredicates;
+                uint64_t orderedUpdateIndex = 0;
+                std::vector<storm::expressions::Expression> possibleRefinementPredicates;
+                for (; orderedUpdateIndex < updateIndicesAndMasses.size(); ++orderedUpdateIndex) {
+                    storm::storage::BitVector const& lower = lowerChoiceUpdateToSuccessorMapping.at(updateIndicesAndMasses[orderedUpdateIndex].first).first;
+                    storm::storage::BitVector const& upper = upperChoiceUpdateToSuccessorMapping.at(updateIndicesAndMasses[orderedUpdateIndex].first).first;
+                    
+                    bool deviates = lower != upper;
                     if (deviates) {
-                        for (uint_fast64_t predicateIndex = 0; predicateIndex < lowerIt->second.size(); ++predicateIndex) {
-                            if (lowerIt->second.get(predicateIndex) != upperIt->second.get(predicateIndex)) {
-                                // Now we know the point of the deviation (command, update, predicate).
-                                newPredicate = abstractionInformation.getPredicateByIndex(predicateIndex).substitute(abstractor.get().getVariableUpdates(player1Index, updateIndex)).simplify();
-                                break;
+                        std::map<storm::expressions::Variable, storm::expressions::Expression> variableUpdates = abstractor.get().getVariableUpdates(player1Index, updateIndicesAndMasses[orderedUpdateIndex].first);
+
+                        for (uint64_t predicateIndex = 0; predicateIndex < lower.size(); ++predicateIndex) {
+                            if (lower[predicateIndex] != upper[predicateIndex]) {
+                                possibleRefinementPredicates.push_back(abstractionInformation.getPredicateByIndex(predicateIndex).substitute(variableUpdates).simplify());
+                            }
+                        }
+                        ++orderedUpdateIndex;
+                        break;
+                    }
+                }
+                
+                STORM_LOG_ASSERT(!possibleRefinementPredicates.empty(), "Expected refinement predicates.");
+                
+                // Since we can choose any of the deviation predicates to perform the split, we go through the remaining
+                // updates and build all deviation predicates. We can then check whether any of the possible refinement
+                // predicates also eliminates another deviation.
+                std::vector<storm::expressions::Expression> otherRefinementPredicates;
+                for (; orderedUpdateIndex < updateIndicesAndMasses.size(); ++orderedUpdateIndex) {
+                    storm::storage::BitVector const& lower = lowerChoiceUpdateToSuccessorMapping.at(updateIndicesAndMasses[orderedUpdateIndex].first).first;
+                    storm::storage::BitVector const& upper = upperChoiceUpdateToSuccessorMapping.at(updateIndicesAndMasses[orderedUpdateIndex].first).first;
+                    
+                    bool deviates = lower != upper;
+                    if (deviates) {
+                        std::map<storm::expressions::Variable, storm::expressions::Expression> newVariableUpdates = abstractor.get().getVariableUpdates(player1Index, updateIndicesAndMasses[orderedUpdateIndex].first);
+                        for (uint64_t predicateIndex = 0; predicateIndex < lower.size(); ++predicateIndex) {
+                            if (lower[predicateIndex] != upper[predicateIndex]) {
+                                otherRefinementPredicates.push_back(abstractionInformation.getPredicateByIndex(predicateIndex).substitute(newVariableUpdates).simplify());
                             }
                         }
                     }
                 }
+                
+                // Finally, go through the refinement predicates and see how many deviations they cover.
+                std::vector<uint64_t> refinementPredicateIndexToCount(possibleRefinementPredicates.size(), 0);
+                for (uint64_t index = 0; index < possibleRefinementPredicates.size(); ++index) {
+                    refinementPredicateIndexToCount[index] = 1;
+                }
+                for (auto const& otherPredicate : otherRefinementPredicates) {
+                    for (uint64_t index = 0; index < possibleRefinementPredicates.size(); ++index) {
+                        if (equivalenceChecker.areEquivalent(otherPredicate, possibleRefinementPredicates[index])) {
+                            ++refinementPredicateIndexToCount[index];
+                        }
+                    }
+                }
+
+                // Find predicate that covers the most deviations.
+                uint64_t chosenPredicateIndex = 0;
+                for (uint64_t index = 0; index < possibleRefinementPredicates.size(); ++index) {
+                    if (refinementPredicateIndexToCount[index] > refinementPredicateIndexToCount[chosenPredicateIndex]) {
+                        chosenPredicateIndex = index;
+                    }
+                }
+                newPredicate = possibleRefinementPredicates[chosenPredicateIndex];
+
                 STORM_LOG_ASSERT(newPredicate.isInitialized(), "Could not derive new predicate as there is no deviation.");
-                STORM_LOG_DEBUG("Derived new predicate (based on weakest-precondition): " << newPredicate);
+                STORM_LOG_DEBUG("Derived new predicate (based on weakest-precondition): " << newPredicate << ", (equivalent to " << (refinementPredicateIndexToCount[chosenPredicateIndex] - 1) << " other refinement predicates)");
             }
             
             return RefinementPredicates(fromGuard ? RefinementPredicates::Source::Guard : RefinementPredicates::Source::WeakestPrecondition, {newPredicate});
@@ -240,14 +295,16 @@ namespace storm {
             // Then constrain these states by the requirement that for either the lower or upper player 1 choice the player 2 choices must be different and
             // that the difference is not because of a missing strategy in either case.
             
-            // Start with constructing the player 2 states that have a prob 0 (min) and prob 1 (max) strategy.
+            // Start with constructing the player 2 states that have a min and a max strategy.
             storm::dd::Bdd<Type> constraint = minPlayer2Strategy.existsAbstract(game.getPlayer2Variables()) && maxPlayer2Strategy.existsAbstract(game.getPlayer2Variables());
             
             // Now construct all player 2 choices that actually exist and differ in the min and max case.
             constraint &= minPlayer2Strategy.exclusiveOr(maxPlayer2Strategy);
+            minPlayer2Strategy.exclusiveOr(maxPlayer2Strategy).template toAdd<ValueType>().exportToDot("pl2diff.dot");
+            constraint.template toAdd<ValueType>().exportToDot("constraint.dot");
             
             // Then restrict the pivot states by requiring existing and different player 2 choices.
-            result.pivotStates &= ((minPlayer1Strategy && maxPlayer1Strategy) && constraint).existsAbstract(game.getNondeterminismVariables());
+            result.pivotStates &= ((minPlayer1Strategy || maxPlayer1Strategy) && constraint).existsAbstract(game.getNondeterminismVariables());
             
             return result;
         }

src/storm/abstraction/MenuGameRefiner.h

@@ -62,7 +62,9 @@ namespace storm {
             MenuGameRefiner(MenuGameAbstractor<Type, ValueType>& abstractor, std::unique_ptr<storm::solver::SmtSolver>&& smtSolver);
             
             /*!
-             * Refines the abstractor with the given set of predicates.
+             * Refines the abstractor with the given predicates.
+             *
+             * @param predicates The predicates to use for refinement.
              */
             void refine(std::vector<storm::expressions::Expression> const& predicates) const;
             

src/storm/abstraction/StateSetAbstractor.cpp

@@ -14,7 +14,7 @@ namespace storm {
     namespace abstraction {
         
         template <storm::dd::DdType DdType, typename ValueType>
-        StateSetAbstractor<DdType, ValueType>::StateSetAbstractor(AbstractionInformation<DdType>& abstractionInformation, std::set<storm::expressions::Variable> const& allVariables, std::vector<storm::expressions::Expression> const& statePredicates, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), localExpressionInformation(allVariables), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(abstractionInformation.getDdManager().getBddOne()), constraint(abstractionInformation.getDdManager().getBddOne()) {
+        StateSetAbstractor<DdType, ValueType>::StateSetAbstractor(AbstractionInformation<DdType>& abstractionInformation, std::vector<storm::expressions::Expression> const& statePredicates, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), localExpressionInformation(abstractionInformation), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(abstractionInformation.getDdManager().getBddOne()), constraint(abstractionInformation.getDdManager().getBddOne()) {
             
             // Assert all state predicates.
             for (auto const& predicate : statePredicates) {
@@ -44,7 +44,7 @@ namespace storm {
         void StateSetAbstractor<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& newPredicates) {
             // Make the partition aware of the new predicates, which may make more predicates relevant to the abstraction.
             for (auto const& predicateIndex : newPredicates) {
-                localExpressionInformation.addExpression(this->getAbstractionInformation().getPredicateByIndex(predicateIndex), predicateIndex);
+                localExpressionInformation.addExpression(predicateIndex);
             }
             needsRecomputation = true;
         }

src/storm/abstraction/StateSetAbstractor.h

@@ -47,12 +47,11 @@ namespace storm {
              * Creates a state set abstractor.
              *
              * @param abstractionInformation An object storing information about the abstraction such as predicates and BDDs.
-             * @param allVariables All variables that appear in the predicates.
              * @param statePredicates A set of predicates that have to hold in the concrete states this abstractor is
              * supposed to abstract.
              * @param smtSolverFactory A factory that can create new SMT solvers.
              */
-            StateSetAbstractor(AbstractionInformation<DdType>& abstractionInformation, std::set<storm::expressions::Variable> const& allVariables, std::vector<storm::expressions::Expression> const& statePredicates, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
+            StateSetAbstractor(AbstractionInformation<DdType>& abstractionInformation, std::vector<storm::expressions::Expression> const& statePredicates, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
             
             /*!
              * Refines the abstractor by making the given predicates new abstract predicates.
@@ -135,7 +134,7 @@ namespace storm {
             std::reference_wrapper<AbstractionInformation<DdType>> abstractionInformation;
             
             // The local expression-related information.
-            LocalExpressionInformation localExpressionInformation;
+            LocalExpressionInformation<DdType> localExpressionInformation;
             
             // The set of relevant predicates and the corresponding decision variables.
             std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> relevantPredicatesAndVariables;

src/storm/abstraction/prism/CommandAbstractor.cpp

@@ -23,7 +23,7 @@ namespace storm {
     namespace abstraction {
         namespace prism {
             template <storm::dd::DdType DdType, typename ValueType>
-            CommandAbstractor<DdType, ValueType>::CommandAbstractor(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool guardIsPredicate) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation.getVariables()), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, abstractionInformation.getExpressionVariables(), {!command.getGuardExpression()}, smtSolverFactory) {
+            CommandAbstractor<DdType, ValueType>::CommandAbstractor(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool guardIsPredicate) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!command.getGuardExpression()}, smtSolverFactory) {
 
                 // Make the second component of relevant predicates have the right size.
                 relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates());
@@ -42,7 +42,7 @@ namespace storm {
             void CommandAbstractor<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& predicates) {
                 // Add all predicates to the variable partition.
                 for (auto predicateIndex : predicates) {
-                    localExpressionInformation.addExpression(this->getAbstractionInformation().getPredicateByIndex(predicateIndex), predicateIndex);
+                    localExpressionInformation.addExpression(predicateIndex);
                 }
                 
                 STORM_LOG_TRACE("Current variable partition is: " << localExpressionInformation);

src/storm/abstraction/prism/CommandAbstractor.h

@@ -212,7 +212,7 @@ namespace storm {
                 std::reference_wrapper<storm::prism::Command const> command;
                 
                 // The local expression-related information.
-                LocalExpressionInformation localExpressionInformation;
+                LocalExpressionInformation<DdType> localExpressionInformation;
                 
                 // The evaluator used to translate the probability expressions.
                 storm::expressions::ExpressionEvaluator<ValueType> evaluator;

src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -31,16 +31,13 @@ namespace storm {
             template <storm::dd::DdType DdType, typename ValueType>
             PrismMenuGameAbstractor<DdType, ValueType>::PrismMenuGameAbstractor(storm::prism::Program const& program,
                                                                 std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory)
-            : program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager(), smtSolverFactory->create(program.getManager())), modules(), initialStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), {program.getInitialStatesExpression()}, this->smtSolverFactory), currentGame(nullptr), refinementPerformed(false) {
+            : program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager(), program.getAllExpressionVariables(), smtSolverFactory->create(program.getManager())), modules(), initialStateAbstractor(abstractionInformation, {program.getInitialStatesExpression()}, this->smtSolverFactory), currentGame(nullptr), refinementPerformed(false) {
                 
                 // For now, we assume that there is a single module. If the program has more than one module, it needs
                 // to be flattened before the procedure.
                 STORM_LOG_THROW(program.getNumberOfModules() == 1, storm::exceptions::WrongFormatException, "Cannot create abstract program from program containing too many modules.");
                 
-                // Add all variables and range expressions to the information object.
-                for (auto const& variable : this->program.get().getAllExpressionVariables()) {
-                    abstractionInformation.addExpressionVariable(variable);
-                }
+                // Add all variables range expressions to the information object.
                 for (auto const& range : this->program.get().getAllRangeExpressions()) {
                     abstractionInformation.addConstraint(range);
                     initialStateAbstractor.constrain(range);
@@ -162,11 +159,8 @@ namespace storm {
                 
                 // Compute bottom states and the appropriate transitions if necessary.
                 BottomStateResult<DdType> bottomStateResult(abstractionInformation.getDdManager().getBddZero(), abstractionInformation.getDdManager().getBddZero());
-                bool hasBottomStates = false;
-                if (!addedAllGuards) {
-                    bottomStateResult = modules.front().getBottomStateTransitions(reachableStates, game.numberOfPlayer2Variables);
-                    hasBottomStates = !bottomStateResult.states.isZero();
-                }
+                bottomStateResult = modules.front().getBottomStateTransitions(reachableStates, game.numberOfPlayer2Variables);
+                bool hasBottomStates = !bottomStateResult.states.isZero();
                 
                 // Construct the transition matrix by cutting away the transitions of unreachable states.
                 storm::dd::Add<DdType, ValueType> transitionMatrix = (game.bdd && reachableStates).template toAdd<ValueType>();

src/storm/abstraction/prism/PrismMenuGameAbstractor.h

@@ -145,9 +145,6 @@ namespace storm {
                 // A state-set abstractor used to determine the initial states of the abstraction.
                 StateSetAbstractor<DdType, ValueType> initialStateAbstractor;
                                 
-                // A flag that stores whether all guards were added (which is relevant for determining the bottom states).
-                bool addedAllGuards;
-                
                 // An ADD characterizing the probabilities of commands and their updates.
                 storm::dd::Add<DdType, ValueType> commandUpdateProbabilitiesAdd;
                 

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -18,6 +18,10 @@
 
 #include "storm/solver/SymbolicGameSolver.h"
 
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/CoreSettings.h"
+#include "storm/settings/modules/AbstractionSettings.h"
+
 #include "storm/utility/solver.h"
 #include "storm/utility/prism.h"
 #include "storm/utility/macros.h"
@@ -37,7 +41,7 @@ namespace storm {
         using storm::abstraction::QuantitativeResultMinMax;
         
         template<storm::dd::DdType Type, typename ModelType>
-        GameBasedMdpModelChecker<Type, ModelType>::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolverFactory(smtSolverFactory) {
+        GameBasedMdpModelChecker<Type, ModelType>::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPrecision()) {
             STORM_LOG_THROW(model.isPrismProgram(), storm::exceptions::NotSupportedException, "Currently only PRISM models are supported by the game-based model checker.");
             storm::prism::Program const& originalProgram = model.asPrismProgram();
             STORM_LOG_THROW(originalProgram.getModelType() == storm::prism::Program::ModelType::DTMC || originalProgram.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/MDPs are supported by the game-based model checker.");
@@ -165,11 +169,11 @@ namespace storm {
         }
         
         template<typename ValueType>
-        std::unique_ptr<CheckResult> checkForResultAfterQuantitativeCheck(CheckTask<storm::logic::Formula> const& checkTask, ValueType const& minValue, ValueType const& maxValue) {
+        std::unique_ptr<CheckResult> checkForResultAfterQuantitativeCheck(CheckTask<storm::logic::Formula> const& checkTask, ValueType const& minValue, ValueType const& maxValue, storm::utility::ConstantsComparator<ValueType> const& comparator) {
             std::unique_ptr<CheckResult> result;
 
             // If the lower and upper bounds are close enough, we can return the result.
-            if (maxValue - minValue < storm::utility::convertNumber<ValueType>(1e-3)) {
+            if (comparator.isEqual(minValue, maxValue)) {
                 result = std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), (minValue + maxValue) / ValueType(2));
             }
 
@@ -304,7 +308,7 @@ namespace storm {
                 }
                 
                 // #ifdef LOCAL_DEBUG
-                abstractor.exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne());
+                // abstractor.exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne());
                 // #endif
                 
                 // (3) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max).
@@ -312,6 +316,7 @@ namespace storm {
                 QualitativeResultMinMax<Type> qualitativeResult;
                 std::unique_ptr<CheckResult> result = computeProb01States(checkTask, qualitativeResult, game, player1Direction, transitionMatrixBdd, initialStates, constraintStates, targetStates);
                 if (result) {
+                    printStatistics(abstractor, game);
                     return result;
                 }
                 auto qualitativeEnd = std::chrono::high_resolution_clock::now();
@@ -330,6 +335,7 @@ namespace storm {
                     
                     result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, initialStates, qualitativeResult);
                     if (result) {
+                        printStatistics(abstractor, game);
                         return result;
                     } else {
                         STORM_LOG_DEBUG("Obtained qualitative bounds [0, 1] on the actual value for the initial states.");
@@ -355,6 +361,7 @@ namespace storm {
                     quantitativeResult.min = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin);
                     result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.min.initialStateValue);
                     if (result) {
+                        printStatistics(abstractor, game);
                         return result;
                     }
                     
@@ -362,6 +369,7 @@ namespace storm {
                     quantitativeResult.max = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Maximize, game, qualitativeResult, initialStatesAdd, maybeMax, boost::make_optional(quantitativeResult.min));
                     result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.max.initialStateValue);
                     if (result) {
+                        printStatistics(abstractor, game);
                         return result;
                     }
 
@@ -369,8 +377,9 @@ namespace storm {
                     STORM_LOG_DEBUG("Obtained quantitative bounds [" << quantitativeResult.min.initialStateValue << ", " << quantitativeResult.max.initialStateValue << "] on the actual value for the initial states in " << std::chrono::duration_cast<std::chrono::milliseconds>(quantitativeEnd - quantitativeStart).count() << "ms.");
 
                     // (9) Check whether the lower and upper bounds are close enough to terminate with an answer.
-                    result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, quantitativeResult.min.initialStateValue, quantitativeResult.max.initialStateValue);
+                    result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, quantitativeResult.min.initialStateValue, quantitativeResult.max.initialStateValue, comparator);
                     if (result) {
+                        printStatistics(abstractor, game);
                         return result;
                     }
 
@@ -420,15 +429,10 @@ namespace storm {
             qualitativeResult.prob0Min = computeProb01States(true, player1Direction, storm::OptimizationDirection::Minimize, game, transitionMatrixBdd, constraintStates, targetStates);
             qualitativeResult.prob1Min = computeProb01States(false, player1Direction, storm::OptimizationDirection::Minimize, game, transitionMatrixBdd, constraintStates, targetStates);
             std::unique_ptr<CheckResult> result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, storm::OptimizationDirection::Minimize, initialStates, qualitativeResult.prob0Min.getPlayer1States(), qualitativeResult.prob1Min.getPlayer1States());
-            if (result) {
-                return result;
-            }
-            
-            qualitativeResult.prob0Max = computeProb01States(true, player1Direction, storm::OptimizationDirection::Maximize, game, transitionMatrixBdd, constraintStates, targetStates);
-            qualitativeResult.prob1Max = computeProb01States(false, player1Direction, storm::OptimizationDirection::Maximize, game, transitionMatrixBdd, constraintStates, targetStates);
-            result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, storm::OptimizationDirection::Maximize, initialStates, qualitativeResult.prob0Max.getPlayer1States(), qualitativeResult.prob1Max.getPlayer1States());
-            if (result) {
-                return result;
+            if (!result) {
+                qualitativeResult.prob0Max = computeProb01States(true, player1Direction, storm::OptimizationDirection::Maximize, game, transitionMatrixBdd, constraintStates, targetStates);
+                qualitativeResult.prob1Max = computeProb01States(false, player1Direction, storm::OptimizationDirection::Maximize, game, transitionMatrixBdd, constraintStates, targetStates);
+                result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, storm::OptimizationDirection::Maximize, initialStates, qualitativeResult.prob0Max.getPlayer1States(), qualitativeResult.prob1Max.getPlayer1States());
             }
             return result;
         }
@@ -454,6 +458,19 @@ namespace storm {
             return result;
         }
         
+        template<storm::dd::DdType Type, typename ModelType>
+        void GameBasedMdpModelChecker<Type, ModelType>::printStatistics(storm::abstraction::MenuGameAbstractor<Type, ValueType> const& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game) const {
+            if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
+                storm::abstraction::AbstractionInformation<Type> const& abstractionInformation = abstractor.getAbstractionInformation();
+
+                std::cout << std::endl;
+                std::cout << "Statistics:" << std::endl;
+                std::cout << "    * player 1 states (final game): " << game.getReachableStates().getNonZeroCount() << std::endl;
+                std::cout << "    * transitions (final game): " << game.getTransitionMatrix().getNonZeroCount() << std::endl;
+                std::cout << "    * predicates used in abstraction: " << abstractionInformation.getNumberOfPredicates() << std::endl;
+            }
+        }
+        
         template<storm::dd::DdType Type, typename ModelType>
         storm::expressions::Expression GameBasedMdpModelChecker<Type, ModelType>::getExpression(storm::logic::Formula const& formula) {
             STORM_LOG_THROW(formula.isBooleanLiteralFormula() || formula.isAtomicExpressionFormula() || formula.isAtomicLabelFormula(), storm::exceptions::InvalidPropertyException, "The target states have to be given as label or an expression.");

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h

@@ -14,6 +14,7 @@
 
 #include "storm/logic/Bound.h"
 
+#include "storm/utility/ConstantsComparator.h"
 #include "storm/utility/solver.h"
 #include "storm/utility/graph.h"
 
@@ -21,6 +22,9 @@ namespace storm {
     namespace abstraction {
         template<storm::dd::DdType Type, typename ValueType>
         class MenuGame;
+
+        template<storm::dd::DdType Type, typename ValueType>
+        class MenuGameAbstractor;
     }
     
     namespace modelchecker {
@@ -70,6 +74,8 @@ namespace storm {
             std::unique_ptr<CheckResult> computeProb01States(CheckTask<storm::logic::Formula> const& checkTask, QualitativeResultMinMax<Type>& qualitativeResult, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates);
             QualitativeResult<Type> computeProb01States(bool prob0, storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates);
             
+            void printStatistics(storm::abstraction::MenuGameAbstractor<Type, ValueType> const& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game) const;
+            
             /*
              * Retrieves the expression characterized by the formula. The formula needs to be propositional.
              */
@@ -81,6 +87,9 @@ namespace storm {
             
             /// A factory that is used for creating SMT solvers when needed.
             std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
+            
+            /// A comparator that can be used for detecting convergence.
+            storm::utility::ConstantsComparator<ValueType> comparator;
         };
     }
 }

src/storm/settings/modules/AbstractionSettings.cpp

@@ -2,6 +2,8 @@
 
 #include "storm/settings/Option.h"
 #include "storm/settings/OptionBuilder.h"
+#include "storm/settings/ArgumentBuilder.h"
+#include "storm/settings/Argument.h"
 
 namespace storm {
     namespace settings {
@@ -15,7 +17,8 @@ namespace storm {
             const std::string AbstractionSettings::useInterpolationOptionName = "interpolation";
             const std::string AbstractionSettings::splitInterpolantsOptionName = "split-interpolants";
             const std::string AbstractionSettings::splitAllOptionName = "split-all";
-            
+            const std::string AbstractionSettings::precisionOptionName = "precision";
+
             AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, addAllGuardsOptionName, true, "Sets whether all guards are added as initial predicates.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, splitPredicatesOptionName, true, "Sets whether the predicates are split into atoms before they are added.").build());
@@ -23,6 +26,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, splitGuardsOptionName, true, "Sets whether the guards are split into atoms before they are added.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, splitAllOptionName, true, "Sets whether all predicates are split into atoms before they are added.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, useInterpolationOptionName, true, "Sets whether interpolation is to be used to eliminate spurious pivot blocks.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for detecting convergence.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-03).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
             }
             
             bool AbstractionSettings::isAddAllGuardsSet() const {
@@ -49,6 +53,9 @@ namespace storm {
                 return this->getOption(useInterpolationOptionName).getHasOptionBeenSet();
             }
             
+            double AbstractionSettings::getPrecision() const {
+                return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
+            }
         }
     }
 }

src/storm/settings/modules/AbstractionSettings.h

@@ -57,6 +57,13 @@ namespace storm {
                  * @return True iff the option was set.
                  */
                 bool isUseInterpolationSet() const;
+                
+                /*!
+                 * Retrieves the precision that is used for detecting convergence.
+                 *
+                 * @return The precision to use for detecting convergence.
+                 */
+                double getPrecision() const;
 
                 const static std::string moduleName;
                 
@@ -68,6 +75,7 @@ namespace storm {
                 const static std::string useInterpolationOptionName;
                 const static std::string splitInterpolantsOptionName;
                 const static std::string splitAllOptionName;
+                const static std::string precisionOptionName;
             };
             
         }