optimizations for game-based abstraction refinement

src/storm/abstraction/ExpressionTranslator.cpp

@@ -17,7 +17,8 @@ namespace storm {
         
         template <storm::dd::DdType DdType>
         ExpressionTranslator<DdType>::ExpressionTranslator(AbstractionInformation<DdType>& abstractionInformation, std::unique_ptr<storm::solver::SmtSolver>&& smtSolver) : abstractionInformation(abstractionInformation), equivalenceChecker(std::move(smtSolver)), locationVariables(abstractionInformation.getLocationExpressionVariables()), abstractedVariables(abstractionInformation.getAbstractedVariables()) {
-            // Intentionally left empty.
+            
+            equivalenceChecker.addConstraints(abstractionInformation.getConstraints());
         }
 
         template <storm::dd::DdType DdType>
@@ -51,6 +52,8 @@ namespace storm {
                 for (uint64_t predicateIndex = 0; predicateIndex < abstractionInformation.get().getNumberOfPredicates(); ++predicateIndex) {
                     if (equivalenceChecker.areEquivalent(abstractionInformation.get().getPredicateByIndex(predicateIndex), expression.toExpression())) {
                         return abstractionInformation.get().encodePredicateAsSource(predicateIndex);
+                    } else if (equivalenceChecker.areEquivalent(abstractionInformation.get().getPredicateByIndex(predicateIndex), !expression.toExpression())) {
+                        return !abstractionInformation.get().encodePredicateAsSource(predicateIndex);
                     }
                 }
 
@@ -108,6 +111,8 @@ namespace storm {
                 for (uint64_t predicateIndex = 0; predicateIndex < abstractionInformation.get().getNumberOfPredicates(); ++predicateIndex) {
                     if (equivalenceChecker.areEquivalent(abstractionInformation.get().getPredicateByIndex(predicateIndex), expression.toExpression())) {
                         return abstractionInformation.get().encodePredicateAsSource(predicateIndex);
+                    } else if (equivalenceChecker.areEquivalent(abstractionInformation.get().getPredicateByIndex(predicateIndex), !expression.toExpression())) {
+                        return !abstractionInformation.get().encodePredicateAsSource(predicateIndex);
                     }
                 }
                 
@@ -124,6 +129,8 @@ namespace storm {
                 for (uint64_t predicateIndex = 0; predicateIndex < abstractionInformation.get().getNumberOfPredicates(); ++predicateIndex) {
                     if (equivalenceChecker.areEquivalent(abstractionInformation.get().getPredicateByIndex(predicateIndex), expression.toExpression())) {
                         return abstractionInformation.get().encodePredicateAsSource(predicateIndex);
+                    } else if (equivalenceChecker.areEquivalent(abstractionInformation.get().getPredicateByIndex(predicateIndex), !expression.toExpression())) {
+                        return !abstractionInformation.get().encodePredicateAsSource(predicateIndex);
                     }
                 }
                 
@@ -154,6 +161,8 @@ namespace storm {
                 for (uint64_t predicateIndex = 0; predicateIndex < abstractionInformation.get().getNumberOfPredicates(); ++predicateIndex) {
                     if (equivalenceChecker.areEquivalent(abstractionInformation.get().getPredicateByIndex(predicateIndex), expression.toExpression())) {
                         return abstractionInformation.get().encodePredicateAsSource(predicateIndex);
+                    } else if (equivalenceChecker.areEquivalent(abstractionInformation.get().getPredicateByIndex(predicateIndex), !expression.toExpression())) {
+                        return !abstractionInformation.get().encodePredicateAsSource(predicateIndex);
                     }
                 }
                 

src/storm/abstraction/MenuGameAbstractor.h

@@ -51,6 +51,13 @@ namespace storm {
             /// Retrieves the number of predicates currently in use.
             virtual uint64_t getNumberOfPredicates() const = 0;
             
+            /*!
+             * Adds the expression to the ones characterizing terminal states, i.e. states whose transitions are not
+             * explored. For this to work, appropriate predicates must have been used to refine the abstraction,
+             * otherwise this will fail.
+             */
+            virtual void addTerminalStates(storm::expressions::Expression const& expression) = 0;
+            
         protected:
             void exportToDot(storm::abstraction::MenuGame<DdType, ValueType> const& currentGame, std::string const& filename, storm::dd::Bdd<DdType> const& highlightStatesBdd, storm::dd::Bdd<DdType> const& filter) const;
         };

src/storm/abstraction/MenuGameRefiner.cpp

@@ -59,6 +59,8 @@ namespace storm {
         template<storm::dd::DdType Type, typename ValueType>
         MenuGameRefiner<Type, ValueType>::MenuGameRefiner(MenuGameAbstractor<Type, ValueType>& abstractor, std::unique_ptr<storm::solver::SmtSolver>&& smtSolver) : abstractor(abstractor), useInterpolation(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isUseInterpolationSet()), splitAll(false), splitPredicates(false), addedAllGuardsFlag(false), pivotSelectionHeuristic(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPivotSelectionHeuristic()), splitter(), equivalenceChecker(std::move(smtSolver)) {
             
+            equivalenceChecker.addConstraints(abstractor.getAbstractionInformation().getConstraints());
+            
             AbstractionSettings::SplitMode splitMode = storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getSplitMode();
             splitAll = splitMode == AbstractionSettings::SplitMode::All;
             splitPredicates = splitMode == AbstractionSettings::SplitMode::NonGuard;
@@ -325,7 +327,7 @@ namespace storm {
                 }
                 for (auto const& otherPredicate : otherRefinementPredicates) {
                     for (uint64_t index = 0; index < possibleRefinementPredicates.size(); ++index) {
-                        if (equivalenceChecker.areEquivalent(otherPredicate, possibleRefinementPredicates[index])) {
+                        if (equivalenceChecker.areEquivalentModuloNegation(otherPredicate, possibleRefinementPredicates[index])) {
                             ++refinementPredicateIndexToCount[index];
                         }
                     }
@@ -726,13 +728,13 @@ namespace storm {
                         // set or in the set that is to be added.
                         bool addAtom = true;
                         for (auto const& oldPredicate : abstractionInformation.getPredicates()) {
-                            if (equivalenceChecker.areEquivalent(atom, oldPredicate)) {
+                            if (equivalenceChecker.areEquivalent(atom, oldPredicate) || equivalenceChecker.areEquivalent(atom, !oldPredicate)) {
                                 addAtom = false;
                                 break;
                             }
                         }
                         for (auto const& addedAtom : cleanedAtoms) {
-                            if (equivalenceChecker.areEquivalent(addedAtom, atom)) {
+                            if (equivalenceChecker.areEquivalent(addedAtom, atom) || equivalenceChecker.areEquivalent(addedAtom, !atom)) {
                                 addAtom = false;
                                 break;
                             }

src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp

@@ -154,8 +154,14 @@ namespace storm {
                 auto auxVariables = abstractionInformation.getAuxVariableSet(0, abstractionInformation.getAuxVariableCount());
                 variablesToAbstract.insert(auxVariables.begin(), auxVariables.end());
                 
+                // Compute which states are non-terminal.
+                storm::dd::Bdd<DdType> nonTerminalStates = this->abstractionInformation.getDdManager().getBddOne();
+                for (auto const& expression : this->terminalStateExpressions) {
+                    nonTerminalStates &= !this->getStates(expression);
+                }
+                
                 // Do a reachability analysis on the raw transition relation.
-                storm::dd::Bdd<DdType> transitionRelation = game.bdd.existsAbstract(variablesToAbstract);
+                storm::dd::Bdd<DdType> transitionRelation = nonTerminalStates && game.bdd.existsAbstract(variablesToAbstract);
                 storm::dd::Bdd<DdType> initialStates = initialLocationsBdd && initialStateAbstractor.getAbstractStates();
                 initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables());
                 storm::dd::Bdd<DdType> reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables());
@@ -213,6 +219,11 @@ namespace storm {
                 return abstractionInformation.getNumberOfPredicates();
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            void JaniMenuGameAbstractor<DdType, ValueType>::addTerminalStates(storm::expressions::Expression const& expression) {
+                terminalStateExpressions.emplace_back(expression);
+            }
+            
             // Explicitly instantiate the class.
             template class JaniMenuGameAbstractor<storm::dd::DdType::CUDD, double>;
             template class JaniMenuGameAbstractor<storm::dd::DdType::Sylvan, double>;

src/storm/abstraction/jani/JaniMenuGameAbstractor.h

@@ -111,6 +111,8 @@ namespace storm {
                 
                 virtual uint64_t getNumberOfPredicates() const override;
                 
+                virtual void addTerminalStates(storm::expressions::Expression const& expression) override;
+                
             protected:
                 using MenuGameAbstractor<DdType, ValueType>::exportToDot;
                 
@@ -159,6 +161,9 @@ namespace storm {
                 
                 // A flag storing whether a refinement was performed.
                 bool refinementPerformed;
+                
+                // A list of terminal state expressions.
+                std::vector<storm::expressions::Expression> terminalStateExpressions;
             };
         }
     }

src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -99,7 +99,7 @@ namespace storm {
             MenuGame<DdType, ValueType> PrismMenuGameAbstractor<DdType, ValueType>::abstract() {
                 if (refinementPerformed) {
                     currentGame = buildGame();
-                    refinementPerformed = true;
+                    refinementPerformed = false;
                 }
                 return *currentGame;
             }
@@ -147,8 +147,14 @@ namespace storm {
                 auto auxVariables = abstractionInformation.getAuxVariableSet(0, abstractionInformation.getAuxVariableCount());
                 variablesToAbstract.insert(auxVariables.begin(), auxVariables.end());
                 
+                // Compute which states are non-terminal.
+                storm::dd::Bdd<DdType> nonTerminalStates = this->abstractionInformation.getDdManager().getBddOne();
+                for (auto const& expression : this->terminalStateExpressions) {
+                    nonTerminalStates &= !this->getStates(expression);
+                }
+                
                 // Do a reachability analysis on the raw transition relation.
-                storm::dd::Bdd<DdType> transitionRelation = game.bdd.existsAbstract(variablesToAbstract);
+                storm::dd::Bdd<DdType> transitionRelation = nonTerminalStates && game.bdd.existsAbstract(variablesToAbstract);
                 storm::dd::Bdd<DdType> initialStates = initialStateAbstractor.getAbstractStates();
                 initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables());
                 storm::dd::Bdd<DdType> reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables());
@@ -208,6 +214,11 @@ namespace storm {
                 return abstractionInformation.getNumberOfPredicates();
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            void PrismMenuGameAbstractor<DdType, ValueType>::addTerminalStates(storm::expressions::Expression const& expression) {
+                terminalStateExpressions.emplace_back(expression);
+            }
+            
             // Explicitly instantiate the class.
             template class PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double>;
             template class PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double>;

src/storm/abstraction/prism/PrismMenuGameAbstractor.h

@@ -111,6 +111,8 @@ namespace storm {
 
                 virtual uint64_t getNumberOfPredicates() const override;
                 
+                virtual void addTerminalStates(storm::expressions::Expression const& expression) override;
+                
             protected:
                 using MenuGameAbstractor<DdType, ValueType>::exportToDot;
                 
@@ -156,6 +158,9 @@ namespace storm {
                 
                 // A flag storing whether a refinement was performed.
                 bool refinementPerformed;
+                
+                // A list of terminal state expressions.
+                std::vector<storm::expressions::Expression> terminalStateExpressions;
             };
         }
     }

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -342,6 +342,10 @@ namespace storm {
             } else {
                 abstractor = std::make_shared<storm::abstraction::jani::JaniMenuGameAbstractor<Type, ValueType>>(preprocessedModel.asJaniModel(), smtSolverFactory);
             }
+            if (!constraintExpression.isTrue()) {
+                abstractor->addTerminalStates(!constraintExpression);
+            }
+            abstractor->addTerminalStates(targetStateExpression);
             
             // Create a refiner that can be used to refine the abstraction when needed.
             storm::abstraction::MenuGameRefiner<Type, ValueType> refiner(*abstractor, smtSolverFactory->create(preprocessedModel.getManager()));

src/storm/storage/expressions/EquivalenceChecker.cpp

@@ -13,6 +13,12 @@ namespace storm {
             }
         }
         
+        void EquivalenceChecker::addConstraints(std::vector<storm::expressions::Expression> const& constraints) {
+            for (auto const& constraint : constraints) {
+                this->smtSolver->add(constraint);
+            }
+        }
+        
         bool EquivalenceChecker::areEquivalent(storm::expressions::Expression const& first, storm::expressions::Expression const& second) {
             this->smtSolver->push();
             this->smtSolver->add((first && !second) || (!first && second));
@@ -21,5 +27,9 @@ namespace storm {
             return equivalent;
         }
         
+        bool EquivalenceChecker::areEquivalentModuloNegation(storm::expressions::Expression const& first, storm::expressions::Expression const& second) {
+            return this->areEquivalent(first, second) || this->areEquivalent(first, !second);
+        }
+        
     }
 }

src/storm/storage/expressions/EquivalenceChecker.h

@@ -20,7 +20,10 @@ namespace storm {
              */
             EquivalenceChecker(std::unique_ptr<storm::solver::SmtSolver>&& smtSolver, boost::optional<storm::expressions::Expression> const& constraint = boost::none);
             
+            void addConstraints(std::vector<storm::expressions::Expression> const& constraints);
+            
             bool areEquivalent(storm::expressions::Expression const& first, storm::expressions::Expression const& second);
+            bool areEquivalentModuloNegation(storm::expressions::Expression const& first, storm::expressions::Expression const& second);
             
         private:
             std::unique_ptr<storm::solver::SmtSolver> smtSolver;