started to pull the rest of the refinement logic into refiner class, not working (or compiling) yet

src/storm/abstraction/AbstractionInformation.cpp

@@ -1,5 +1,7 @@
 #include "storm/abstraction/AbstractionInformation.h"
 
+#include "storm/storage/BitVector.h"
+
 #include "storm/storage/dd/DdManager.h"
 
 #include "storm/utility/macros.h"
@@ -394,6 +396,43 @@ namespace storm {
             return result;
         }
         
+        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;
+            
+            storm::dd::Add<DdType, double> lowerChoiceAsAdd = choice.template toAdd<double>();
+            for (auto const& successorValuePair : lowerChoiceAsAdd) {
+                uint_fast64_t updateIndex = this->decodeAux(successorValuePair.first, 0, this->getAuxVariableCount());
+                
+#ifdef LOCAL_DEBUG
+                std::cout << "update idx: " << updateIndex << std::endl;
+#endif
+                storm::storage::BitVector successor(this->getNumberOfPredicates());
+                for (uint_fast64_t index = 0; index < this->getOrderedSuccessorVariables().size(); ++index) {
+                    auto const& successorVariable = this->getOrderedSuccessorVariables()[index];
+#ifdef LOCAL_DEBUG
+                    std::cout << successorVariable.getName() << " has value";
+#endif
+                    if (successorValuePair.first.getBooleanValue(successorVariable)) {
+                        successor.set(index);
+#ifdef LOCAL_DEBUG
+                        std::cout << " true";
+#endif
+                    } else {
+#ifdef LOCAL_DEBUG
+                        std::cout << " false";
+#endif
+                    }
+#ifdef LOCAL_DEBUG
+                    std::cout << std::endl;
+#endif
+                }
+                
+                result[updateIndex] = successor;
+            }
+            return result;
+        }
+        
         template class AbstractionInformation<storm::dd::DdType::CUDD>;
         template class AbstractionInformation<storm::dd::DdType::Sylvan>;
     }

src/storm/abstraction/AbstractionInformation.h

@@ -426,6 +426,11 @@ namespace storm {
              */
             std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> declareNewVariables(std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> const& oldPredicates, std::set<uint_fast64_t> const& newPredicates) const;
             
+            /*!
+             * Decodes the choice in the form of a BDD over the source and
+             */
+            std::map<uint_fast64_t, storm::storage::BitVector> decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<DdType> const& choice) const;
+            
         private:
             /*!
              * Encodes the given index with the given number of variables from the given variables.

src/storm/abstraction/MenuGameAbstractor.h

@@ -11,12 +11,15 @@ namespace storm {
         class MenuGameAbstractor {
         public:
             /// Retrieves the abstraction.
-            virtual storm::abstraction::MenuGame<DdType, ValueType> abstract() = 0;
+            virtual MenuGame<DdType, ValueType> abstract() = 0;
+
+            /// Retrieves information about the abstraction.
+            virtual AbstractionInformation<DdType> const& getAbstractionInformation() const = 0;
             
             /// Methods to refine the abstraction.
             virtual void refine(std::vector<storm::expressions::Expression> const& predicates) = 0;
             virtual void refine(storm::dd::Bdd<DdType> const& pivotState, storm::dd::Bdd<DdType> const& player1Choice, storm::dd::Bdd<DdType> const& lowerChoice, storm::dd::Bdd<DdType> const& upperChoice) = 0;
-
+            
             /// Exports a representation of the current abstraction state in the dot format.
             virtual void exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStates, storm::dd::Bdd<DdType> const& filter) const = 0;
         };

src/storm/abstraction/MenuGameRefiner.cpp

@@ -8,7 +8,7 @@ namespace storm {
     namespace abstraction {
         
         template<storm::dd::DdType Type, typename ValueType>
-        MenuGameRefiner<Type, ValueType>::MenuGameRefiner(MenuGameAbstractor<Type, ValueType>& abstractor) : abstractor(abstractor) {
+        MenuGameRefiner<Type, ValueType>::MenuGameRefiner(MenuGameAbstractor<Type, ValueType>& abstractor, std::unique_ptr<storm::solver::SmtSolver>&& smtSolver) : abstractor(abstractor), splitter(), equivalenceChecker(std::move(smtSolver)) {
             // Intentionally left empty.
         }
         
@@ -47,6 +47,124 @@ namespace storm {
             return pivotState;
         }
         
+        template <storm::dd::DdType DdType, typename ValueType>
+        void refine(storm::dd::Bdd<DdType> const& pivotState, storm::dd::Bdd<DdType> const& player1Choice, storm::dd::Bdd<DdType> const& lowerChoice, storm::dd::Bdd<DdType> const& upperChoice) {
+            AbstractionInformation<DdType> const& abstractionInformation = abstractor.get().getAbstractionInformation();
+            
+            // Decode the index of the command chosen by player 1.
+            storm::dd::Add<DdType, ValueType> player1ChoiceAsAdd = player1Choice.template toAdd<ValueType>();
+            auto pl1It = player1ChoiceAsAdd.begin();
+            uint_fast64_t commandIndex = abstractionInformation.decodePlayer1Choice((*pl1It).first, abstractionInformation.getPlayer1VariableCount());
+#ifdef LOCAL_DEBUG
+            std::cout << "command index " << commandIndex << std::endl;
+            std::cout << program.get() << std::endl;
+            
+            for (auto stateValue : pivotState.template toAdd<ValueType>()) {
+                std::stringstream stateName;
+                stateName << "\tpl1_";
+                for (auto const& var : currentGame->getRowVariables()) {
+                    std::cout << "var " << var.getName() << std::endl;
+                    if (stateValue.first.getBooleanValue(var)) {
+                        stateName << "1";
+                    } else {
+                        stateName << "0";
+                    }
+                }
+                std::cout << "pivot is " << stateName.str() << std::endl;
+            }
+#endif
+            storm::abstraction::prism::AbstractCommand<DdType, ValueType>& abstractCommand = modules.front().getCommands()[commandIndex];
+            storm::prism::Command const& concreteCommand = abstractCommand.getConcreteCommand();
+#ifdef LOCAL_DEBUG
+            player1Choice.template toAdd<ValueType>().exportToDot("pl1choice_ref.dot");
+            std::cout << concreteCommand << std::endl;
+            
+            (currentGame->getTransitionMatrix() * player1Choice.template toAdd<ValueType>()).exportToDot("cuttrans.dot");
+#endif
+            
+            // Check whether there are bottom states in the game and whether one of the choices actually picks the
+            // bottom state as the successor.
+            bool buttomStateSuccessor = false;
+            if (!currentGame->getBottomStates().isZero()) {
+                buttomStateSuccessor = !((abstractionInformation.getBottomStateBdd(false, false) && lowerChoice) || (abstractionInformation.getBottomStateBdd(false, false) && upperChoice)).isZero();
+            }
+            
+            // If one of the choices picks the bottom state, the new predicate is based on the guard of the appropriate
+            // command (that is the player 1 choice).
+            if (buttomStateSuccessor) {
+                STORM_LOG_TRACE("One of the successors is a bottom state, taking a guard as a new predicate.");
+                abstractCommand.notifyGuardIsPredicate();
+                storm::expressions::Expression newPredicate = concreteCommand.getGuardExpression();
+                STORM_LOG_DEBUG("Derived new predicate: " << newPredicate);
+                this->refine({std::make_pair(newPredicate, true)});
+            } else {
+                STORM_LOG_TRACE("No bottom state successor. Deriving a new predicate using weakest precondition.");
+                
+#ifdef LOCAL_DEBUG
+                lowerChoice.template toAdd<ValueType>().exportToDot("lowerchoice_ref.dot");
+                upperChoice.template toAdd<ValueType>().exportToDot("upperchoice_ref.dot");
+#endif
+                
+                // Decode both choices to explicit mappings.
+#ifdef LOCAL_DEBUG
+                std::cout << "lower" << std::endl;
+#endif
+                std::map<uint_fast64_t, storm::storage::BitVector> lowerChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(lowerChoice);
+#ifdef LOCAL_DEBUG
+                std::cout << "upper" << std::endl;
+#endif
+                std::map<uint_fast64_t, storm::storage::BitVector> upperChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(upperChoice);
+                STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode (" << lowerChoiceUpdateToSuccessorMapping.size() << " vs. " << upperChoiceUpdateToSuccessorMapping.size() << ").");
+                
+#ifdef LOCAL_DEBUG
+                std::cout << "lower" << std::endl;
+                for (auto const& entry : lowerChoiceUpdateToSuccessorMapping) {
+                    std::cout << entry.first << " -> " << entry.second << std::endl;
+                }
+                std::cout << "upper" << std::endl;
+                for (auto const& entry : upperChoiceUpdateToSuccessorMapping) {
+                    std::cout << entry.first << " -> " << entry.second << std::endl;
+                }
+#endif
+                
+                // Now go through the mappings and find points of deviation. Currently, we take the first deviation.
+                storm::expressions::Expression newPredicate;
+                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;
+#ifdef LOCAL_DEBUG
+                    std::cout << "update idx " << updateIndex << std::endl;
+#endif
+                    bool deviates = lowerIt->second != upperIt->second;
+                    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).
+                                std::cout << "ref" << std::endl;
+                                std::cout << abstractionInformation.getPredicateByIndex(predicateIndex) << std::endl;
+                                std::cout << concreteCommand.getUpdate(updateIndex) << std::endl;
+                                newPredicate = abstractionInformation.getPredicateByIndex(predicateIndex).substitute(concreteCommand.getUpdate(updateIndex).getAsVariableToExpressionMap()).simplify();
+                                break;
+                            }
+                        }
+                    }
+                }
+                STORM_LOG_ASSERT(newPredicate.isInitialized(), "Could not derive new predicate as there is no deviation.");
+                
+                STORM_LOG_DEBUG("Derived new predicate: " << newPredicate);
+                
+                this->refine({std::make_pair(newPredicate, true)});
+            }
+            
+            STORM_LOG_TRACE("Current set of predicates:");
+            for (auto const& predicate : abstractionInformation.getPredicates()) {
+                STORM_LOG_TRACE(predicate);
+            }
+        }
+        
         template<storm::dd::DdType Type, typename ValueType>
         bool MenuGameRefiner<Type, ValueType>::refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QualitativeResultMinMax<Type> const& qualitativeResult) {
             STORM_LOG_TRACE("Trying refinement after qualitative check.");
@@ -202,6 +320,39 @@ namespace storm {
         }
 
         
+        template<storm::dd::DdType Type, typename ValueType>
+        bool MenuGameRefiner<Type, ValueType>::performRefinement(std::vector<storm::expressions::Expression> const& predicates) const {
+            for (auto const& predicate : predicates) {
+                storm::expressions::Expression const& predicate = predicateAllowSplitPair.first;
+                bool allowSplit = predicateAllowSplitPair.second;
+                STORM_LOG_THROW(predicate.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expecting a predicate of type bool.");
+                
+                if (allowSplit && splitPredicates) {
+                    // Split the predicates.
+                    std::vector<storm::expressions::Expression> atoms = splitter.split(predicate);
+                    
+                    // Check which of the atoms are redundant in the sense that they are equivalent to a predicate we already have.
+                    for (auto const& atom : atoms) {
+                        bool addAtom = true;
+                        for (auto const& oldPredicate : abstractionInformation.getPredicates()) {
+                            if (equivalenceChecker.areEquivalent(atom, oldPredicate)) {
+                                addAtom = false;
+                                break;
+                            }
+                        }
+                        
+                        if (addAtom) {
+                            uint_fast64_t newPredicateIndex = abstractionInformation.addPredicate(atom);
+                            newPredicateIndices.push_back(newPredicateIndex);
+                        }
+                    }
+                } else {
+                    uint_fast64_t newPredicateIndex = abstractionInformation.addPredicate(predicate);
+                    newPredicateIndices.push_back(newPredicateIndex);
+                }
+            }
+        }
+        
         template class MenuGameRefiner<storm::dd::DdType::CUDD, double>;
         template class MenuGameRefiner<storm::dd::DdType::Sylvan, double>;
         

src/storm/abstraction/MenuGameRefiner.h

@@ -2,14 +2,19 @@
 
 #include <functional>
 #include <vector>
+#include <memory>
 
 #include "storm/abstraction/QualitativeResultMinMax.h"
 #include "storm/abstraction/QuantitativeResultMinMax.h"
 
 #include "storm/storage/expressions/Expression.h"
+#include "storm/storage/expressions/PredicateSplitter.h"
+#include "storm/storage/expressions/EquivalenceChecker.h"
 
 #include "storm/storage/dd/DdType.h"
 
+#include "storm/utility/solver.h"
+
 namespace storm {
     namespace abstraction {
 
@@ -25,7 +30,7 @@ namespace storm {
             /*!
              * Creates a refiner for the provided abstractor.
              */
-            MenuGameRefiner(MenuGameAbstractor<Type, ValueType>& abstractor);
+            MenuGameRefiner(MenuGameAbstractor<Type, ValueType>& abstractor, std::unique_ptr<storm::solver::SmtSolver>&& smtSolver);
             
             /*!
              * Refines the abstractor with the given set of predicates.
@@ -37,18 +42,29 @@ namespace storm {
              *
              * @param True if predicates for refinement could be derived, false otherwise.
              */
-            bool refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QualitativeResultMinMax<Type> const& qualitativeResult);
+            bool refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QualitativeResultMinMax<Type> const& qualitativeResult) const;
             
             /*!
              * Refines the abstractor based on the quantitative result by trying to derive suitable predicates.
              *
              * @param True if predicates for refinement could be derived, false otherwise.
              */
-            bool refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QuantitativeResultMinMax<Type, ValueType> const& quantitativeResult);
+            bool refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QuantitativeResultMinMax<Type, ValueType> const& quantitativeResult) const;
             
         private:
+            /*!
+             * Takes the given predicates, preprocesses them and then refines the abstractor.
+             */
+            bool performRefinement(std::vector<storm::expressions::Expression> const& predicates) const;
+            
             /// The underlying abstractor to refine.
             std::reference_wrapper<MenuGameAbstractor<Type, ValueType>> abstractor;
+            
+            /// An object that can be used for splitting predicates.
+            storm::expressions::PredicateSplitter splitter;
+            
+            /// An object that can be used to determine whether predicates are equivalent.
+            storm::expressions::EquivalenceChecker equivalenceChecker;
         };
         
     }

src/storm/abstraction/prism/AbstractProgram.cpp

@@ -30,8 +30,8 @@ namespace storm {
             template <storm::dd::DdType DdType, typename ValueType>
             AbstractProgram<DdType, ValueType>::AbstractProgram(storm::prism::Program const& program,
                                                                 std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory,
-                                                                bool addAllGuards, bool splitPredicates)
-            : program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager()), modules(), initialStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), {program.getInitialStatesExpression()}, this->smtSolverFactory), splitPredicates(splitPredicates), splitter(), equivalenceChecker(smtSolverFactory->create(abstractionInformation.getExpressionManager()), abstractionInformation.getExpressionManager().boolean(true)), addedAllGuards(addAllGuards), currentGame(nullptr) {
+                                                                bool addAllGuards)
+            : program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager()), modules(), initialStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), {program.getInitialStatesExpression()}, this->smtSolverFactory), addedAllGuards(addAllGuards), currentGame(nullptr) {
                 
                 // For now, we assume that there is a single module. If the program has more than one module, it needs
                 // to be flattened before the procedure.
@@ -75,10 +75,10 @@ namespace storm {
                 commandUpdateProbabilitiesAdd = modules.front().getCommandUpdateProbabilitiesAdd();
                 
                 // Now that we have created all other DD variables, we create the DD variables for the predicates.
-                std::vector<std::pair<storm::expressions::Expression, bool>> initialPredicates;
+                std::vector<storm::expressions::Expression> initialPredicates;
                 if (addAllGuards) {
                     for (auto const& guard : allGuards) {
-                        initialPredicates.push_back(std::make_pair(guard, true));
+                        initialPredicates.push_back(guard);
                     }
                 }
                 
@@ -87,37 +87,12 @@ namespace storm {
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
-            void AbstractProgram<DdType, ValueType>::refine(std::vector<std::pair<storm::expressions::Expression, bool>> const& predicates) {
-                // Add the predicates to the global list of predicates.
+            void AbstractProgram<DdType, ValueType>::refine(std::vector<storm::expressions::Expression> const& predicates) {
+                // Add the predicates to the global list of predicates and gather their indices.
                 std::vector<uint_fast64_t> newPredicateIndices;
-                for (auto const& predicateAllowSplitPair : predicates) {
-                    storm::expressions::Expression const& predicate = predicateAllowSplitPair.first;
-                    bool allowSplit = predicateAllowSplitPair.second;
+                for (auto const& predicate : predicates) {
                     STORM_LOG_THROW(predicate.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expecting a predicate of type bool.");
-                    
-                    if (allowSplit && splitPredicates) {
-                        // Split the predicates.
-                        std::vector<storm::expressions::Expression> atoms = splitter.split(predicate);
-                        
-                        // Check which of the atoms are redundant in the sense that they are equivalent to a predicate we already have.
-                        for (auto const& atom : atoms) {
-                            bool addAtom = true;
-                            for (auto const& oldPredicate : abstractionInformation.getPredicates()) {
-                                if (equivalenceChecker.areEquivalent(atom, oldPredicate)) {
-                                    addAtom = false;
-                                    break;
-                                }
-                            }
-                            
-                            if (addAtom) {
-                                uint_fast64_t newPredicateIndex = abstractionInformation.addPredicate(atom);
-                                newPredicateIndices.push_back(newPredicateIndex);
-                            }
-                        }
-                    } else {
-                        uint_fast64_t newPredicateIndex = abstractionInformation.addPredicate(predicate);
-                        newPredicateIndices.push_back(newPredicateIndex);
-                    }
+                    newPredicateIndices.push_back(abstractionInformation.addPredicate(predicate));
                 }
                 
                 // Refine all abstract modules.
@@ -131,166 +106,18 @@ namespace storm {
                 // Finally, we rebuild the game.
                 currentGame = buildGame();
             }
-            
-            template <storm::dd::DdType DdType, typename ValueType>
-            std::map<uint_fast64_t, storm::storage::BitVector> AbstractProgram<DdType, ValueType>::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<DdType> const& choice) const {
-                std::map<uint_fast64_t, storm::storage::BitVector> result;
-                
-                storm::dd::Add<DdType, ValueType> lowerChoiceAsAdd = choice.template toAdd<ValueType>();
-                for (auto const& successorValuePair : lowerChoiceAsAdd) {
-                    uint_fast64_t updateIndex = abstractionInformation.decodeAux(successorValuePair.first, 0, currentGame->getProbabilisticBranchingVariables().size());
-                    
-#ifdef LOCAL_DEBUG
-                    std::cout << "update idx: " << updateIndex << std::endl;
-#endif
-                    storm::storage::BitVector successor(abstractionInformation.getNumberOfPredicates());
-                    for (uint_fast64_t index = 0; index < abstractionInformation.getOrderedSuccessorVariables().size(); ++index) {
-                        auto const& successorVariable = abstractionInformation.getOrderedSuccessorVariables()[index];
-#ifdef LOCAL_DEBUG
-                        std::cout << successorVariable.getName() << " has value";
-#endif
-                        if (successorValuePair.first.getBooleanValue(successorVariable)) {
-                            successor.set(index);
-#ifdef LOCAL_DEBUG
-                            std::cout << " true";
-#endif
-                        } else {
-#ifdef LOCAL_DEBUG
-                            std::cout << " false";
-#endif
-                        }
-#ifdef LOCAL_DEBUG
-                        std::cout << std::endl;
-#endif
-                    }
-                    
-                    result[updateIndex] = successor;
-                }
-                return result;
-            }
-            
-            template <storm::dd::DdType DdType, typename ValueType>
-            void AbstractProgram<DdType, ValueType>::refine(storm::dd::Bdd<DdType> const& pivotState, storm::dd::Bdd<DdType> const& player1Choice, storm::dd::Bdd<DdType> const& lowerChoice, storm::dd::Bdd<DdType> const& upperChoice) {
-                // Decode the index of the command chosen by player 1.
-                storm::dd::Add<DdType, ValueType> player1ChoiceAsAdd = player1Choice.template toAdd<ValueType>();
-                auto pl1It = player1ChoiceAsAdd.begin();
-                uint_fast64_t commandIndex = abstractionInformation.decodePlayer1Choice((*pl1It).first, abstractionInformation.getPlayer1VariableCount());
-#ifdef LOCAL_DEBUG
-                std::cout << "command index " << commandIndex << std::endl;
-                std::cout << program.get() << std::endl;
-                
-                for (auto stateValue : pivotState.template toAdd<ValueType>()) {
-                    std::stringstream stateName;
-                    stateName << "\tpl1_";
-                    for (auto const& var : currentGame->getRowVariables()) {
-                        std::cout << "var " << var.getName() << std::endl;
-                        if (stateValue.first.getBooleanValue(var)) {
-                            stateName << "1";
-                        } else {
-                            stateName << "0";
-                        }
-                    }
-                    std::cout << "pivot is " << stateName.str() << std::endl;
-                }
-#endif
-                storm::abstraction::prism::AbstractCommand<DdType, ValueType>& abstractCommand = modules.front().getCommands()[commandIndex];
-                storm::prism::Command const& concreteCommand = abstractCommand.getConcreteCommand();
-#ifdef LOCAL_DEBUG
-                player1Choice.template toAdd<ValueType>().exportToDot("pl1choice_ref.dot");
-                std::cout << concreteCommand << std::endl;
-                
-                (currentGame->getTransitionMatrix() * player1Choice.template toAdd<ValueType>()).exportToDot("cuttrans.dot");
-#endif
-                
-                // Check whether there are bottom states in the game and whether one of the choices actually picks the
-                // bottom state as the successor.
-                bool buttomStateSuccessor = false;
-                if (!currentGame->getBottomStates().isZero()) {
-                    buttomStateSuccessor = !((abstractionInformation.getBottomStateBdd(false, false) && lowerChoice) || (abstractionInformation.getBottomStateBdd(false, false) && upperChoice)).isZero();
-                }
-                
-                // If one of the choices picks the bottom state, the new predicate is based on the guard of the appropriate
-                // command (that is the player 1 choice).
-                if (buttomStateSuccessor) {
-                    STORM_LOG_TRACE("One of the successors is a bottom state, taking a guard as a new predicate.");
-                    abstractCommand.notifyGuardIsPredicate();
-                    storm::expressions::Expression newPredicate = concreteCommand.getGuardExpression();
-                    STORM_LOG_DEBUG("Derived new predicate: " << newPredicate);
-                    this->refine({std::make_pair(newPredicate, true)});
-                } else {
-                    STORM_LOG_TRACE("No bottom state successor. Deriving a new predicate using weakest precondition.");
-                    
-#ifdef LOCAL_DEBUG
-                    lowerChoice.template toAdd<ValueType>().exportToDot("lowerchoice_ref.dot");
-                    upperChoice.template toAdd<ValueType>().exportToDot("upperchoice_ref.dot");
-#endif
-                    
-                    // Decode both choices to explicit mappings.
-#ifdef LOCAL_DEBUG
-                    std::cout << "lower" << std::endl;
-#endif
-                    std::map<uint_fast64_t, storm::storage::BitVector> lowerChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(lowerChoice);
-#ifdef LOCAL_DEBUG
-                    std::cout << "upper" << std::endl;
-#endif
-                    std::map<uint_fast64_t, storm::storage::BitVector> upperChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(upperChoice);
-                    STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode (" << lowerChoiceUpdateToSuccessorMapping.size() << " vs. " << upperChoiceUpdateToSuccessorMapping.size() << ").");
-                    
-#ifdef LOCAL_DEBUG
-                    std::cout << "lower" << std::endl;
-                    for (auto const& entry : lowerChoiceUpdateToSuccessorMapping) {
-                        std::cout << entry.first << " -> " << entry.second << std::endl;
-                    }
-                    std::cout << "upper" << std::endl;
-                    for (auto const& entry : upperChoiceUpdateToSuccessorMapping) {
-                        std::cout << entry.first << " -> " << entry.second << std::endl;
-                    }
-#endif
-                    
-                    // Now go through the mappings and find points of deviation. Currently, we take the first deviation.
-                    storm::expressions::Expression newPredicate;
-                    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;
-#ifdef LOCAL_DEBUG
-                        std::cout << "update idx " << updateIndex << std::endl;
-#endif
-                        bool deviates = lowerIt->second != upperIt->second;
-                        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).
-                                    std::cout << "ref" << std::endl;
-                                    std::cout << abstractionInformation.getPredicateByIndex(predicateIndex) << std::endl;
-                                    std::cout << concreteCommand.getUpdate(updateIndex) << std::endl;
-                                    newPredicate = abstractionInformation.getPredicateByIndex(predicateIndex).substitute(concreteCommand.getUpdate(updateIndex).getAsVariableToExpressionMap()).simplify();
-                                    break;
-                                }
-                            }
-                        }
-                    }
-                    STORM_LOG_ASSERT(newPredicate.isInitialized(), "Could not derive new predicate as there is no deviation.");
-                    
-                    STORM_LOG_DEBUG("Derived new predicate: " << newPredicate);
-                    
-                    this->refine({std::make_pair(newPredicate, true)});
-                }
-                
-                STORM_LOG_TRACE("Current set of predicates:");
-                for (auto const& predicate : abstractionInformation.getPredicates()) {
-                    STORM_LOG_TRACE(predicate);
-                }
-            }
-            
+                                    
             template <storm::dd::DdType DdType, typename ValueType>
             MenuGame<DdType, ValueType> AbstractProgram<DdType, ValueType>::getAbstractGame() {
                 STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created.");
                 return *currentGame;
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            AbstractionInformation<DdType> const& AbstractProgram<DdType, ValueType>::getAbstractionInformation() const {
+                return abstractionInformation;
+            }
+            
             template <storm::dd::DdType DdType, typename ValueType>
             storm::dd::Bdd<DdType> AbstractProgram<DdType, ValueType>::getStates(storm::expressions::Expression const& predicate) {
                 STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created.");

src/storm/abstraction/prism/AbstractProgram.h

@@ -9,8 +9,6 @@
 #include "storm/storage/dd/Add.h"
 
 #include "storm/storage/expressions/Expression.h"
-#include "storm/storage/expressions/PredicateSplitter.h"
-#include "storm/storage/expressions/EquivalenceChecker.h"
 
 namespace storm {
     namespace utility {
@@ -44,9 +42,8 @@ namespace storm {
                  * @param program The concrete program for which to build the abstraction.
                  * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
                  * @param addAllGuards A flag that indicates whether all guards of the program should be added to the initial set of predicates.
-                 * @param splitPredicates A flag that indicates whether the predicates are to be split into atoms before being added.
                  */
-                AbstractProgram(storm::prism::Program const& program, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), bool addAllGuards = false, bool splitPredicates = false);
+                AbstractProgram(storm::prism::Program const& program, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), bool addAllGuards = false);
                 
                 AbstractProgram(AbstractProgram const&) = default;
                 AbstractProgram& operator=(AbstractProgram const&) = default;
@@ -60,6 +57,13 @@ namespace storm {
                  */
                 MenuGame<DdType, ValueType> getAbstractGame();
                 
+                /*!
+                 * Retrieves information about the abstraction.
+                 *
+                 * @return The abstraction information object.
+                 */
+                AbstractionInformation<DdType> const& getAbstractionInformation() const;
+                
                 /*!
                  * Retrieves the set of states (represented by a BDD) satisfying the given predicate, assuming that it
                  * was either given as an initial predicate or used as a refining predicate later.
@@ -74,18 +78,7 @@ namespace storm {
                  *
                  * @param predicates The new predicates.
                  */
-                void refine(std::vector<std::pair<storm::expressions::Expression, bool>> const& predicates);
-                
-                /*!
-                 * Refines the abstract program using the pivot state, and player 1 choice. The refinement guarantees that
-                 * the two provided choices are not possible from the same pivot state using the given player 1 choice.
-                 *
-                 * @param pivotState The pivot state on which to base the refinement.
-                 * @param player1Choice The player 1 choice that needs to be refined.
-                 * @param lowerChoice The first of the two choices on which to base the refinement.
-                 * @param upperChoice The first of the two choices on which to base the refinement.
-                 */
-                void refine(storm::dd::Bdd<DdType> const& pivotState, storm::dd::Bdd<DdType> const& player1Choice, storm::dd::Bdd<DdType> const& lowerChoice, storm::dd::Bdd<DdType> const& upperChoice);
+                void refine(std::vector<storm::expressions::Expression> const& predicates);
                 
                 /*!
                  * Exports the current state of the abstraction in the dot format to the given file.
@@ -126,16 +119,7 @@ namespace storm {
                 
                 // A state-set abstractor used to determine the initial states of the abstraction.
                 StateSetAbstractor<DdType, ValueType> initialStateAbstractor;
-                
-                // A flag indicating whether predicates are to be split into atoms or not.
-                bool splitPredicates;
-                
-                // An object that can be used for splitting predicates.
-                storm::expressions::PredicateSplitter splitter;
-                
-                // An object that can be used to determine whether predicates are equivalent.
-                storm::expressions::EquivalenceChecker equivalenceChecker;
-                
+                                
                 // A flag that stores whether all guards were added (which is relevant for determining the bottom states).
                 bool addedAllGuards;
                 

src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -19,6 +19,10 @@ namespace storm {
                 return abstractProgram.getAbstractGame();
             }
             
+            AbstractionInformation<DdType> const& PrismMenuGameAbstractor<DdType, ValueType>::getAbstractionInformation() const {
+                return abstractProgram.getAbstractionInformation();
+            }
+            
             template <storm::dd::DdType DdType, typename ValueType>
             void PrismMenuGameAbstractor<DdType, ValueType>::refine(std::vector<storm::expressions::Expression> const& predicates) {
                 std::vector<std::pair<storm::expressions::Expression, bool>> predicatesWithFlags;

src/storm/abstraction/prism/PrismMenuGameAbstractor.h

@@ -14,6 +14,8 @@ namespace storm {
                 PrismMenuGameAbstractor(storm::prism::Program const& program, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
                 
                 virtual storm::abstraction::MenuGame<DdType, ValueType> abstract() override;
+                virtual AbstractionInformation<DdType> const& getAbstractionInformation() const override;
+                
                 virtual void refine(std::vector<storm::expressions::Expression> const& predicates) override;
                 virtual void refine(storm::dd::Bdd<DdType> const& pivotState, storm::dd::Bdd<DdType> const& player1Choice, storm::dd::Bdd<DdType> const& lowerChoice, storm::dd::Bdd<DdType> const& upperChoice) override;
 

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -275,7 +275,7 @@ namespace storm {
             storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType> abstractor(preprocessedModel.asPrismProgram(), smtSolverFactory);
             
             // Create a refiner that can be used to refine the abstraction when needed.
-            storm::abstraction::MenuGameRefiner<Type, ValueType> refiner(abstractor);
+            storm::abstraction::MenuGameRefiner<Type, ValueType> refiner(abstractor, smtSolverFactory->create(preprocessedModel.getManager()));
             refiner.refine(initialPredicates);
             
             // Enter the main-loop of abstraction refinement.

src/storm/storage/expressions/EquivalenceChecker.cpp

@@ -7,8 +7,10 @@
 namespace storm {
     namespace expressions {
  
-        EquivalenceChecker::EquivalenceChecker(std::unique_ptr<storm::solver::SmtSolver>&& smtSolver, storm::expressions::Expression const& constraint) : smtSolver(std::move(smtSolver)) {
-            this->smtSolver->add(constraint);
+        EquivalenceChecker::EquivalenceChecker(std::unique_ptr<storm::solver::SmtSolver>&& smtSolver, boost::optional<storm::expressions::Expression> const& constraint) : smtSolver(std::move(smtSolver)) {
+            if (constraint) {
+                this->smtSolver->add(constraint.get());
+            }
         }
         
         bool EquivalenceChecker::areEquivalent(storm::expressions::Expression const& first, storm::expressions::Expression const& second) {

src/storm/storage/expressions/EquivalenceChecker.h

@@ -2,6 +2,8 @@
 
 #include <memory>
 
+#include <boost/optional.hpp>
+
 #include "storm/solver/SmtSolver.h"
 
 namespace storm {
@@ -16,7 +18,7 @@ namespace storm {
              * @param smtSolver The solver to use.
              * @param constraint An additional constraint. Must be satisfiable.
              */
-            EquivalenceChecker(std::unique_ptr<storm::solver::SmtSolver>&& smtSolver, storm::expressions::Expression const& constraint);
+            EquivalenceChecker(std::unique_ptr<storm::solver::SmtSolver>&& smtSolver, boost::optional<storm::expressions::Expression> const& constraint = boost::none);
             
             bool areEquivalent(storm::expressions::Expression const& first, storm::expressions::Expression const& second);