enabled different invalid block detection strategies

src/storm/abstraction/LocalExpressionInformation.cpp

@@ -23,7 +23,7 @@ namespace storm {
         }
         
         template <storm::dd::DdType DdType>
-        bool LocalExpressionInformation<DdType>::addExpression(uint_fast64_t globalExpressionIndex) {
+        std::map<uint64_t, uint64_t> 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.
@@ -47,12 +47,12 @@ namespace storm {
         }
         
         template <storm::dd::DdType DdType>
-        bool LocalExpressionInformation<DdType>::relate(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable) {
+        std::map<uint64_t, uint64_t> LocalExpressionInformation<DdType>::relate(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable) {
             return this->relate({firstVariable, secondVariable});
         }
         
         template <storm::dd::DdType DdType>
-        bool LocalExpressionInformation<DdType>::relate(std::set<storm::expressions::Variable> const& variables) {
+        std::map<uint64_t, uint64_t> 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) {
@@ -63,15 +63,20 @@ namespace storm {
             
             // If we found a single block only, there is nothing to do.
             if (blocksToMerge.size() == 1) {
-                return false;
+                std::map<uint64_t, uint64_t> identity;
+                for (uint64_t i = 0; i < getNumberOfBlocks(); ++i) {
+                    identity.emplace_hint(identity.end(), i, i);
+                }
+                return identity;
             }
             
-            this->mergeBlocks(blocksToMerge);
-            return true;
+            return this->mergeBlocks(blocksToMerge);
         }
         
         template <storm::dd::DdType DdType>
-        void LocalExpressionInformation<DdType>::mergeBlocks(std::set<uint_fast64_t> const& blocksToMerge) {
+        std::map<uint64_t, uint64_t> LocalExpressionInformation<DdType>::mergeBlocks(std::set<uint_fast64_t> const& blocksToMerge) {
+            std::map<uint64_t, uint64_t> oldToNewIndices;
+            
             // Merge all blocks into the block to keep.
             std::vector<std::set<storm::expressions::Variable>> newVariableBlocks;
             std::vector<std::set<uint_fast64_t>> newExpressionBlocks;
@@ -90,12 +95,14 @@ namespace storm {
                     for (auto const& variable : variableBlocks[blockIndex]) {
                         variableToBlockMapping[variable] = blockToKeep;
                     }
+                    oldToNewIndices[blockIndex] = blockToKeep;
                     
                     newVariableBlocks[blockToKeep].insert(variableBlocks[blockIndex].begin(), variableBlocks[blockIndex].end());
                     newExpressionBlocks[blockToKeep].insert(expressionBlocks[blockIndex].begin(), expressionBlocks[blockIndex].end());
                     ++blocksToMergeIt;
                 } else {
                     // Otherwise just move the current block to the new partition.
+                    oldToNewIndices[blockIndex] = newVariableBlocks.size();
                     
                     // Adjust the mapping for all variables of the old block.
                     for (auto const& variable : variableBlocks[blockIndex]) {
@@ -109,6 +116,8 @@ namespace storm {
             
             variableBlocks = std::move(newVariableBlocks);
             expressionBlocks = std::move(newExpressionBlocks);
+            
+            return oldToNewIndices;
         }
         
         template <storm::dd::DdType DdType>
@@ -172,6 +181,11 @@ namespace storm {
             return result;
         }
         
+        template <storm::dd::DdType DdType>
+        std::set<uint_fast64_t> const& LocalExpressionInformation<DdType>::getExpressionBlock(uint64_t index) const {
+            return expressionBlocks[index];
+        }
+        
         template <storm::dd::DdType DdType>
         std::ostream& operator<<(std::ostream& out, LocalExpressionInformation<DdType> const& partition) {
             std::vector<std::string> blocks;

src/storm/abstraction/LocalExpressionInformation.h

@@ -30,9 +30,9 @@ namespace storm {
              * Adds the expression and therefore indirectly may cause blocks of variables to be merged.
              *
              * @param globalExpressionIndex The global index of the expression.
-             * @return True iff the partition changed.
+             * @return A mapping from old block indices to the new ones (after possible merges).
              */
-            bool addExpression(uint_fast64_t globalExpressionIndex);
+            std::map<uint64_t, uint64_t> addExpression(uint_fast64_t globalExpressionIndex);
             
             /*!
              * Retrieves whether the two given variables are in the same block of the partition.
@@ -48,17 +48,17 @@ namespace storm {
              *
              * @param firstVariable The first variable.
              * @param secondVariable The second variable.
-             * @return True iff the partition changed.
+             * @return A mapping from old block indices to the new ones (after possible merges).
              */
-            bool relate(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable);
+            std::map<uint64_t, uint64_t> relate(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable);
             
             /*!
              * Places the given variables in the same block of the partition and performs the implied merges.
              *
              * @param variables The variables to relate.
-             * @return True iff the partition changed.
+             * @return A mapping from old block indices to the new ones (after possible merges).
              */
-            bool relate(std::set<storm::expressions::Variable> const& variables);
+            std::map<uint64_t, uint64_t> relate(std::set<storm::expressions::Variable> const& variables);
             
             /*!
              * Retrieves the block of related variables of the given variable.
@@ -123,6 +123,13 @@ namespace storm {
              */
             std::set<uint_fast64_t> getExpressionsUsingVariables(std::set<storm::expressions::Variable> const& variables) const;
             
+            /*!
+             * Retrieves the expression block with the given index.
+             *
+             * @return The requested expression block.
+             */
+            std::set<uint_fast64_t> const& getExpressionBlock(uint64_t index) const;
+            
             template<storm::dd::DdType DdTypePrime>
             friend std::ostream& operator<<(std::ostream& out, LocalExpressionInformation<DdTypePrime> const& partition);
             
@@ -131,8 +138,9 @@ namespace storm {
              * Merges the blocks with the given indices.
              *
              * @param blocksToMerge The indices of the blocks to merge.
+             * @return A mapping from old block indices to the new ones (after possible merges).
              */
-            void mergeBlocks(std::set<uint_fast64_t> const& blocksToMerge);
+            std::map<uint64_t, uint64_t> mergeBlocks(std::set<uint_fast64_t> const& blocksToMerge);
             
             // The set of variables relevant for this partition.
             std::set<storm::expressions::Variable> relevantVariables;

src/storm/abstraction/ValidBlockAbstractor.cpp

@@ -0,0 +1,136 @@
+#include "storm/abstraction/ValidBlockAbstractor.h"
+
+#include "storm/abstraction/AbstractionInformation.h"
+
+#include "storm/storage/dd/DdManager.h"
+
+#include "storm/utility/solver.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        template <storm::dd::DdType DdType>
+        ValidBlockAbstractor<DdType>::ValidBlockAbstractor(AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : abstractionInformation(abstractionInformation), localExpressionInformation(abstractionInformation), validBlocks(abstractionInformation.getDdManager().getBddOne()), checkForRecomputation(false) {
+            
+            uint64_t numberOfBlocks = localExpressionInformation.getNumberOfBlocks();
+            validBlocksForPredicateBlocks.resize(numberOfBlocks, abstractionInformation.getDdManager().getBddOne());
+            relevantVariablesAndPredicates.resize(numberOfBlocks);
+            decisionVariables.resize(numberOfBlocks);
+            
+            for (uint64_t i = 0; i < numberOfBlocks; ++i) {
+                smtSolvers.emplace_back(smtSolverFactory->create(abstractionInformation.getExpressionManager()));
+                for (auto const& constraint : abstractionInformation.getConstraints()) {
+                    smtSolvers.back()->add(constraint);
+                }
+            }
+        }
+        
+        template <storm::dd::DdType DdType>
+        storm::dd::Bdd<DdType> const& ValidBlockAbstractor<DdType>::getValidBlocks() {
+            if (checkForRecomputation) {
+                recomputeValidBlocks();
+            }
+            
+            return validBlocks;
+        }
+        
+        template <storm::dd::DdType DdType>
+        void ValidBlockAbstractor<DdType>::refine(std::vector<uint64_t> const& predicates) {
+            for (auto const& predicate : predicates) {
+                std::map<uint64_t, uint64_t> mergeInformation = localExpressionInformation.addExpression(predicate);
+                
+                // Perform the remapping caused by merges.
+                for (auto const& blockRemapping : mergeInformation) {
+                    if (blockRemapping.first == blockRemapping.second) {
+                        continue;
+                    }
+                    
+                    validBlocksForPredicateBlocks[blockRemapping.second] = validBlocksForPredicateBlocks[blockRemapping.first];
+                    smtSolvers[blockRemapping.second] = std::move(smtSolvers[blockRemapping.first]);
+                    relevantVariablesAndPredicates[blockRemapping.second] = std::move(relevantVariablesAndPredicates[blockRemapping.first]);
+                    decisionVariables[blockRemapping.second] = std::move(decisionVariables[blockRemapping.first]);
+                }
+                validBlocksForPredicateBlocks.resize(localExpressionInformation.getNumberOfBlocks());
+                smtSolvers.resize(localExpressionInformation.getNumberOfBlocks());
+                relevantVariablesAndPredicates.resize(localExpressionInformation.getNumberOfBlocks());
+                decisionVariables.resize(localExpressionInformation.getNumberOfBlocks());
+            }
+            checkForRecomputation = true;
+        }
+
+        template <storm::dd::DdType DdType>
+        void ValidBlockAbstractor<DdType>::recomputeValidBlocks() {
+            storm::dd::Bdd<DdType> newValidBlocks = abstractionInformation.get().getDdManager().getBddOne();
+            
+            for (uint64_t blockIndex = 0; blockIndex < localExpressionInformation.getNumberOfBlocks(); ++blockIndex) {
+                std::set<uint64_t> const& predicateBlock = localExpressionInformation.getExpressionBlock(blockIndex);
+                
+                // If the size of the block changed, we need to add the appropriate variables and recompute the solution.
+                if (relevantVariablesAndPredicates[blockIndex].size() < predicateBlock.size()) {
+                    recomputeValidBlockForPredicateBlock(blockIndex);
+                }
+                
+                newValidBlocks &= validBlocksForPredicateBlocks[blockIndex];
+            }
+            
+            validBlocks = newValidBlocks;
+        }
+        
+        template <storm::dd::DdType DdType>
+        void ValidBlockAbstractor<DdType>::recomputeValidBlockForPredicateBlock(uint64_t blockIndex) {
+            std::set<uint64_t> const& predicateBlock = localExpressionInformation.getExpressionBlock(blockIndex);
+            
+            std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newVariables = this->getAbstractionInformation().declareNewVariables(relevantVariablesAndPredicates[blockIndex], predicateBlock);
+            for (auto const& element : newVariables) {
+                smtSolvers[blockIndex]->add(storm::expressions::iff(element.first, this->getAbstractionInformation().getPredicateByIndex(element.second)));
+                decisionVariables[blockIndex].push_back(element.first);
+            }
+
+            relevantVariablesAndPredicates[blockIndex].insert(relevantVariablesAndPredicates[blockIndex].end(), newVariables.begin(), newVariables.end());
+            std::sort(relevantVariablesAndPredicates[blockIndex].begin(), relevantVariablesAndPredicates[blockIndex].end(),
+                      [] (std::pair<storm::expressions::Variable, uint_fast64_t> const& first, std::pair<storm::expressions::Variable, uint_fast64_t> const& second) {
+                          return first.second < second.second;
+                      });
+
+            // Use all-sat to enumerate all valid blocks for this predicate block.
+            storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddZero();
+            uint64_t numberOfSolutions = 0;
+            smtSolvers[blockIndex]->allSat(decisionVariables[blockIndex], [&result,this,&numberOfSolutions,blockIndex] (storm::solver::SmtSolver::ModelReference const& model) {
+                result |= getSourceStateBdd(model, blockIndex);
+                ++numberOfSolutions;
+                return true;
+            });
+
+            STORM_LOG_TRACE("Computed valid blocks for predicate block " << blockIndex << " (" << numberOfSolutions << " solutions enumerated).");
+            
+            validBlocksForPredicateBlocks[blockIndex] = result;
+        }
+        
+        template <storm::dd::DdType DdType>
+        AbstractionInformation<DdType> const& ValidBlockAbstractor<DdType>::getAbstractionInformation() const {
+            return abstractionInformation.get();
+        }
+        
+        template <storm::dd::DdType DdType>
+        storm::dd::Bdd<DdType> ValidBlockAbstractor<DdType>::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model, uint64_t blockIndex) const {
+            storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddOne();
+//            std::cout << "new model ----------------" << std::endl;
+            for (auto const& variableIndexPair : relevantVariablesAndPredicates[blockIndex]) {
+                if (model.getBooleanValue(variableIndexPair.first)) {
+//                    std::cout << this->getAbstractionInformation().getPredicateByIndex(variableIndexPair.second) << " is true" << std::endl;
+                    result &= this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second);
+                } else {
+//                    std::cout << this->getAbstractionInformation().getPredicateByIndex(variableIndexPair.second) << " is false" << std::endl;
+                    result &= !this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second);
+                }
+            }
+            
+            STORM_LOG_ASSERT(!result.isZero(), "Source must not be empty.");
+            return result;
+        }
+        
+        template class ValidBlockAbstractor<storm::dd::DdType::CUDD>;
+        template class ValidBlockAbstractor<storm::dd::DdType::Sylvan>;
+        
+    }
+}

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), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!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 allowInvalidSuccessors) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), allowInvalidSuccessors(allowInvalidSuccessors), 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());
@@ -154,9 +154,10 @@ namespace storm {
                     assignedVariables.insert(assignedVariable);
                 }
                 
-                auto const& predicatesRelatedToAssignedVariable = localExpressionInformation.getRelatedExpressions(assignedVariables);
-                
-                result.first.insert(predicatesRelatedToAssignedVariable.begin(), predicatesRelatedToAssignedVariable.end());
+                if (!allowInvalidSuccessors) {
+                    auto const& predicatesRelatedToAssignedVariable = localExpressionInformation.getRelatedExpressions(assignedVariables);
+                    result.first.insert(predicatesRelatedToAssignedVariable.begin(), predicatesRelatedToAssignedVariable.end());
+                }
                 
                 return result;
             }
@@ -198,6 +199,7 @@ namespace storm {
                 // Determine and add new relevant source predicates.
                 std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newSourceVariables = this->getAbstractionInformation().declareNewVariables(relevantPredicatesAndVariables.first, newRelevantPredicates.first);
                 for (auto const& element : newSourceVariables) {
+                    allRelevantPredicates.insert(element.second);
                     smtSolver->add(storm::expressions::iff(element.first, this->getAbstractionInformation().getPredicateByIndex(element.second)));
                     decisionVariables.push_back(element.first);
                 }
@@ -210,6 +212,7 @@ namespace storm {
                 for (uint_fast64_t index = 0; index < command.get().getNumberOfUpdates(); ++index) {
                     std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newSuccessorVariables = this->getAbstractionInformation().declareNewVariables(relevantPredicatesAndVariables.second[index], newRelevantPredicates.second[index]);
                     for (auto const& element : newSuccessorVariables) {
+                        allRelevantPredicates.insert(element.second);
                         smtSolver->add(storm::expressions::iff(element.first, this->getAbstractionInformation().getPredicateByIndex(element.second).substitute(command.get().getUpdate(index).getAsVariableToExpressionMap())));
                         decisionVariables.push_back(element.first);
                     }
@@ -271,22 +274,34 @@ namespace storm {
             template <storm::dd::DdType DdType, typename ValueType>
             storm::dd::Bdd<DdType> CommandAbstractor<DdType, ValueType>::computeMissingUpdateIdentities() const {
                 storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddZero();
+                
                 for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) {
                     // Compute the identities that are missing for this update.
-                    auto firstIt = relevantPredicatesAndVariables.first.begin();
-                    auto firstIte = relevantPredicatesAndVariables.first.end();
-                    auto secondIt = relevantPredicatesAndVariables.second[updateIndex].begin();
-                    auto secondIte = relevantPredicatesAndVariables.second[updateIndex].end();
+                    auto updateRelevantIt = relevantPredicatesAndVariables.second[updateIndex].begin();
+                    auto updateRelevantIte = relevantPredicatesAndVariables.second[updateIndex].end();
                     
-                    // Go through all relevant source predicates. This is guaranteed to be a superset of the set of
-                    // relevant successor predicates for any update.
                     storm::dd::Bdd<DdType> updateIdentity = this->getAbstractionInformation().getDdManager().getBddOne();
-                    for (; firstIt != firstIte; ++firstIt) {
-                        // If the predicates do not match, there is a predicate missing, so we need to add its identity.
-                        if (secondIt == secondIte || firstIt->second != secondIt->second) {
-                            updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(firstIt->second);
-                        } else if (secondIt != secondIte) {
-                            ++secondIt;
+                    if (allowInvalidSuccessors) {
+                        for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) {
+                            if (updateRelevantIt == updateRelevantIte || updateRelevantIt->second != predicateIndex) {
+                                updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex);
+                            } else {
+                                ++updateRelevantIt;
+                            }
+                        }
+                    } else {
+                        auto sourceRelevantIt = relevantPredicatesAndVariables.first.begin();
+                        auto sourceRelevantIte = relevantPredicatesAndVariables.first.end();
+                        
+                        // Go through all relevant source predicates. This is guaranteed to be a superset of the set of
+                        // relevant successor predicates for any update.
+                        for (; sourceRelevantIt != sourceRelevantIte; ++sourceRelevantIt) {
+                            // If the predicates do not match, there is a predicate missing, so we need to add its identity.
+                            if (updateRelevantIt == updateRelevantIte || sourceRelevantIt->second != updateRelevantIt->second) {
+                                updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(sourceRelevantIt->second);
+                            } else {
+                                ++updateRelevantIt;
+                            }
                         }
                     }
                     
@@ -297,17 +312,32 @@ namespace storm {
             
             template <storm::dd::DdType DdType, typename ValueType>
             storm::dd::Bdd<DdType> CommandAbstractor<DdType, ValueType>::computeMissingGlobalIdentities() const {
-                auto relevantIt = relevantPredicatesAndVariables.first.begin();
-                auto relevantIte = relevantPredicatesAndVariables.first.end();
-                
                 storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddOne();
-                for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) {
-                    if (relevantIt == relevantIte || relevantIt->second != predicateIndex) {
-                        result &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex);
-                    } else {
-                        ++relevantIt;
+
+                if (allowInvalidSuccessors) {
+                    auto allRelevantIt = allRelevantPredicates.cbegin();
+                    auto allRelevantIte = allRelevantPredicates.cend();
+                    
+                    for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) {
+                        if (allRelevantIt == allRelevantIte || *allRelevantIt != predicateIndex) {
+                            result &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex);
+                        } else {
+                            ++allRelevantIt;
+                        }
+                    }
+                } else {
+                    auto relevantIt = relevantPredicatesAndVariables.first.begin();
+                    auto relevantIte = relevantPredicatesAndVariables.first.end();
+                    
+                    for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) {
+                        if (relevantIt == relevantIte || relevantIt->second != predicateIndex) {
+                            result &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex);
+                        } else {
+                            ++relevantIt;
+                        }
                     }
                 }
+                
                 return result;
             }
 

src/storm/abstraction/prism/CommandAbstractor.h

@@ -57,9 +57,9 @@ namespace storm {
                  * @param command The concrete command for which to build the abstraction.
                  * @param abstractionInformation An object holding information about the abstraction such as predicates and BDDs.
                  * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
-                 * @param guardIsPredicate A flag indicating whether the guard of the command was added as a predicate.
+                 * @param allowInvalidSuccessors A flag indicating whether it is allowed to enumerate invalid successors.
                  */
-                CommandAbstractor(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool guardIsPredicate = false);
+                CommandAbstractor(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool allowInvalidSuccessors);
                                
                 /*!
                  * Refines the abstract command with the given predicates.
@@ -220,6 +220,9 @@ namespace storm {
                 // The currently relevant source/successor predicates and the corresponding variables.
                 std::pair<std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>>, std::vector<std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>>>> relevantPredicatesAndVariables;
                 
+                // The set of all relevant predicates.
+                std::set<uint64_t> allRelevantPredicates;
+                
                 // The most recent result of a call to computeDd. If nothing has changed regarding the relevant
                 // predicates, this result may be reused.
                 GameBddResult<DdType> cachedDd;
@@ -227,6 +230,11 @@ namespace storm {
                 // All relevant decision variables over which to perform AllSat.
                 std::vector<storm::expressions::Variable> decisionVariables;
                 
+                // A flag indicating whether it is allowed to enumerate invalid successors. Invalid successors may be
+                // enumerated if the predicates that are (indirectly) related to an assignment variable are not
+                // considered as source predicates.
+                bool allowInvalidSuccessors;
+                
                 // A flag indicating whether the guard of the command was added as a predicate. If this is true, there
                 // is no need to compute bottom states.
                 bool skipBottomStates;

src/storm/abstraction/prism/ModuleAbstractor.cpp

@@ -9,6 +9,8 @@
 
 #include "storm/storage/prism/Module.h"
 
+#include "storm/settings/SettingsManager.h"
+
 #include "storm-config.h"
 #include "storm/adapters/CarlAdapter.h"
 
@@ -18,12 +20,19 @@ namespace storm {
     namespace abstraction {
         namespace prism {
             
+            using storm::settings::modules::AbstractionSettings;
+            
             template <storm::dd::DdType DdType, typename ValueType>
-            ModuleAbstractor<DdType, ValueType>::ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool allGuardsAdded) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) {
+            ModuleAbstractor<DdType, ValueType>::ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) {
+                
+                bool allowInvalidSuccessorsInCommands = false;
+                if (invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::None || invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::Global) {
+                    allowInvalidSuccessorsInCommands = true;
+                }
                 
                 // For each concrete command, we create an abstract counterpart.
                 for (auto const& command : module.getCommands()) {
-                    commands.emplace_back(command, abstractionInformation, smtSolverFactory, allGuardsAdded);
+                    commands.emplace_back(command, abstractionInformation, smtSolverFactory, allowInvalidSuccessorsInCommands);
                 }
             }
             

src/storm/abstraction/prism/ModuleAbstractor.h

@@ -4,6 +4,8 @@
 
 #include "storm/abstraction/prism/CommandAbstractor.h"
 
+#include "storm/settings/modules/AbstractionSettings.h"
+
 #include "storm/storage/expressions/Expression.h"
 
 #include "storm/utility/solver.h"
@@ -34,9 +36,8 @@ namespace storm {
                  * @param module The concrete module for which to build the abstraction.
                  * @param abstractionInformation An object holding information about the abstraction such as predicates and BDDs.
                  * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
-                 * @param allGuardsAdded A flag indicating whether all guards of the program were added.
                  */
-                ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), bool allGuardsAdded = false);
+                ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy = storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy::Command);
                 
                 ModuleAbstractor(ModuleAbstractor const&) = default;
                 ModuleAbstractor& operator=(ModuleAbstractor const&) = default;

src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -12,6 +12,8 @@
 
 #include "storm/models/symbolic/StandardRewardModel.h"
 
+#include "storm/settings/SettingsManager.h"
+
 #include "storm/utility/dd.h"
 #include "storm/utility/macros.h"
 #include "storm/utility/solver.h"
@@ -28,10 +30,12 @@ namespace storm {
             
 #undef LOCAL_DEBUG
             
+            using storm::settings::modules::AbstractionSettings;
+            
             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(), program.getAllExpressionVariables(), smtSolverFactory->create(program.getManager())), modules(), initialStateAbstractor(abstractionInformation, {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), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(false), invalidBlockDetectionStrategy(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getInvalidBlockDetectionStrategy()) {
                 
                 // 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.
@@ -62,7 +66,7 @@ namespace storm {
                 
                 // For each module of the concrete program, we create an abstract counterpart.
                 for (auto const& module : program.getModules()) {
-                    this->modules.emplace_back(module, abstractionInformation, this->smtSolverFactory);
+                    this->modules.emplace_back(module, abstractionInformation, this->smtSolverFactory, invalidBlockDetectionStrategy);
                 }
                 
                 // Retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later.
@@ -85,6 +89,9 @@ namespace storm {
                 
                 // Refine initial state abstractor.
                 initialStateAbstractor.refine(predicateIndices);
+                
+                // Refine the valid blocks.
+                validBlockAbstractor.refine(predicateIndices);
 
                 refinementPerformed |= !command.getPredicates().empty();
             }
@@ -134,6 +141,20 @@ namespace storm {
                 // As long as there is only one module, we only build its game representation.
                 GameBddResult<DdType> game = modules.front().abstract();
                 
+                if (invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::Global) {
+                    storm::dd::Bdd<DdType> validBlocks = validBlockAbstractor.getValidBlocks();
+                    
+                    // Cut away all invalid blocks for both source and targets.
+                    storm::dd::Bdd<DdType> newGameBdd = game.bdd;
+                    newGameBdd &= validBlocks;
+                    newGameBdd &= validBlocks.swapVariables(abstractionInformation.getExtendedSourceSuccessorVariablePairs());
+                    
+                    if (newGameBdd != game.bdd) {
+                        STORM_LOG_TRACE("Global invalid block detection reduced the number of transitions from " << game.bdd.getNonZeroCount() << " to " << newGameBdd.getNonZeroCount() << ".");
+                        game.bdd = newGameBdd;
+                    }
+                }
+                
                 // Construct a set of all unnecessary variables, so we can abstract from it.
                 std::set<storm::expressions::Variable> variablesToAbstract(abstractionInformation.getPlayer1VariableSet(abstractionInformation.getPlayer1VariableCount()));
                 auto player2Variables = abstractionInformation.getPlayer2VariableSet(game.numberOfPlayer2Variables);

src/storm/abstraction/prism/PrismMenuGameAbstractor.h

@@ -6,12 +6,15 @@
 #include "storm/abstraction/AbstractionInformation.h"
 #include "storm/abstraction/MenuGame.h"
 #include "storm/abstraction/RefinementCommand.h"
+#include "storm/abstraction/ValidBlockAbstractor.h"
 #include "storm/abstraction/prism/ModuleAbstractor.h"
 
 #include "storm/storage/dd/Add.h"
 
 #include "storm/storage/expressions/Expression.h"
 
+#include "storm/settings/modules/AbstractionSettings.h"
+
 namespace storm {
     namespace utility {
         namespace solver {
@@ -144,6 +147,9 @@ namespace storm {
                 
                 // A state-set abstractor used to determine the initial states of the abstraction.
                 StateSetAbstractor<DdType, ValueType> initialStateAbstractor;
+                
+                // An object that is used to compute the valid blocks.
+                ValidBlockAbstractor<DdType> validBlockAbstractor;
                                 
                 // An ADD characterizing the probabilities of commands and their updates.
                 storm::dd::Add<DdType, ValueType> commandUpdateProbabilitiesAdd;
@@ -153,6 +159,9 @@ namespace storm {
                 
                 // A flag storing whether a refinement was performed.
                 bool refinementPerformed;
+                
+                // The strategy to use for detecting invalid blocks.
+                storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy;
             };
         }
     }

src/storm/settings/modules/AbstractionSettings.cpp

@@ -19,6 +19,7 @@ namespace storm {
             const std::string AbstractionSettings::splitAllOptionName = "split-all";
             const std::string AbstractionSettings::precisionOptionName = "precision";
             const std::string AbstractionSettings::pivotHeuristicOptionName = "pivot-heuristic";
+            const std::string AbstractionSettings::invalidBlockStrategyOptionName = "invalid-blocks";
 
             AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, addAllGuardsOptionName, true, "Sets whether all guards are added as initial predicates.").build());
@@ -31,6 +32,10 @@ namespace storm {
                 std::vector<std::string> pivotHeuristic = {"nearest-max-dev", "most-prob-path", "max-weighted-dev"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, pivotHeuristicOptionName, true, "Sets the pivot selection heuristic.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an available heuristic. Available are: 'nearest-max-dev', 'most-prob-path' and 'max-weighted-dev'.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(pivotHeuristic)).setDefaultValueString("max-weighted-dev").build()).build());
+
+                std::vector<std::string> invalidBlockStrategies = {"none", "command", "global"};
+                this->addOption(storm::settings::OptionBuilder(moduleName, invalidBlockStrategyOptionName, true, "Sets the strategy to detect invalid blocks.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an available strategy. Available are: 'none', 'command' and 'global'.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(invalidBlockStrategies)).setDefaultValueString("command").build()).build());
             }
             
             bool AbstractionSettings::isAddAllGuardsSet() const {
@@ -72,6 +77,18 @@ namespace storm {
                 }
                 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown pivot selection heuristic '" << heuristicName << "'.");
             }
+            
+            AbstractionSettings::InvalidBlockDetectionStrategy AbstractionSettings::getInvalidBlockDetectionStrategy() const {
+                std::string strategyName = this->getOption(invalidBlockStrategyOptionName).getArgumentByName("name").getValueAsString();
+                if (strategyName == "none") {
+                    return AbstractionSettings::InvalidBlockDetectionStrategy::None;
+                } else if (strategyName == "command") {
+                    return AbstractionSettings::InvalidBlockDetectionStrategy::Command;
+                } else if (strategyName == "global") {
+                    return AbstractionSettings::InvalidBlockDetectionStrategy::Global;
+                }
+                STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown invalid block detection strategy '" << strategyName << "'.");
+            }
         }
     }
 }

src/storm/settings/modules/AbstractionSettings.h

@@ -15,6 +15,10 @@ namespace storm {
                     NearestMaximalDeviation, MostProbablePath, MaxWeightedDeviation
                 };
                 
+                enum class InvalidBlockDetectionStrategy {
+                    None, Command, Global
+                };
+                
                 /*!
                  * Creates a new set of abstraction settings.
                  */
@@ -75,6 +79,13 @@ namespace storm {
                  * @return The selected heuristic.
                  */
                 PivotSelectionHeuristic getPivotSelectionHeuristic() const;
+                
+                /*!
+                 * Retrieves the strategy to use for invalid block detection.
+                 *
+                 * @return The strategy to use
+                 */
+                InvalidBlockDetectionStrategy getInvalidBlockDetectionStrategy() const;
 
                 const static std::string moduleName;
                 
@@ -88,6 +99,7 @@ namespace storm {
                 const static std::string splitAllOptionName;
                 const static std::string precisionOptionName;
                 const static std::string pivotHeuristicOptionName;
+                const static std::string invalidBlockStrategyOptionName;
             };
             
         }