avoiding bottom state computation when possible

src/storm/abstraction/MenuGameAbstractor.h

@@ -71,6 +71,12 @@ namespace storm {
             storm::expressions::Expression const& getTargetStateExpression() const;
             bool hasTargetStateExpression() const;
             
+            /*!
+             * Notifies the abstractor that the guards are predicates, which may be used to improve the bottom state
+             * computation.
+             */
+            virtual void notifyGuardsArePredicates() = 0;
+            
         protected:
             bool isRestrictToRelevantStatesSet() const;
             

src/storm/abstraction/MenuGameRefiner.cpp

@@ -86,7 +86,8 @@ namespace storm {
                     }
                 }
                 performRefinement(createGlobalRefinement(preprocessPredicates(guards, RefinementPredicates::Source::InitialGuard)));
-
+                
+                this->abstractor.get().notifyGuardsArePredicates();
                 addedAllGuardsFlag = true;
             }
         }

src/storm/abstraction/jani/AutomatonAbstractor.cpp

@@ -141,6 +141,13 @@ namespace storm {
                 return abstractionInformation.get();
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            void AutomatonAbstractor<DdType, ValueType>::notifyGuardsArePredicates() {
+                for (auto& edge : edges) {
+                    edge.notifyGuardIsPredicate();
+                }
+            }
+            
             template class AutomatonAbstractor<storm::dd::DdType::CUDD, double>;
             template class AutomatonAbstractor<storm::dd::DdType::Sylvan, double>;
 #ifdef STORM_HAVE_CARL

src/storm/abstraction/jani/AutomatonAbstractor.h

@@ -122,6 +122,8 @@ namespace storm {
                  */
                 std::size_t getNumberOfEdges() const;
                 
+                void notifyGuardsArePredicates();
+                
             private:
                 /*!
                  * Retrieves the abstraction information.

src/storm/abstraction/jani/EdgeAbstractor.cpp

@@ -722,6 +722,11 @@ namespace storm {
                 return abstractionInformation.get();
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            void EdgeAbstractor<DdType, ValueType>::notifyGuardIsPredicate() {
+                skipBottomStates = true;
+            }
+            
             template class EdgeAbstractor<storm::dd::DdType::CUDD, double>;
             template class EdgeAbstractor<storm::dd::DdType::Sylvan, double>;
 #ifdef STORM_HAVE_CARL

src/storm/abstraction/jani/EdgeAbstractor.h

@@ -121,6 +121,8 @@ namespace storm {
                  */
                 storm::jani::Edge const& getConcreteEdge() const;
                 
+                void notifyGuardIsPredicate();
+                
             private:
                 /*!
                  * Determines the relevant predicates for source as well as successor states wrt. to the given assignments

src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp

@@ -268,6 +268,13 @@ namespace storm {
             void JaniMenuGameAbstractor<DdType, ValueType>::addTerminalStates(storm::expressions::Expression const& expression) {
                 terminalStateExpressions.emplace_back(expression);
             }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            void JaniMenuGameAbstractor<DdType, ValueType>::notifyGuardsArePredicates() {
+                for (auto& automaton : automata) {
+                    automaton.notifyGuardsArePredicates();
+                }
+            }
                         
             // Explicitly instantiate the class.
             template class JaniMenuGameAbstractor<storm::dd::DdType::CUDD, double>;

src/storm/abstraction/jani/JaniMenuGameAbstractor.h

@@ -123,6 +123,8 @@ namespace storm {
                 
                 virtual void addTerminalStates(storm::expressions::Expression const& expression) override;
                 
+                virtual void notifyGuardsArePredicates() override;
+
             protected:
                 using MenuGameAbstractor<DdType, ValueType>::exportToDot;
                 

src/storm/abstraction/prism/CommandAbstractor.cpp

@@ -696,6 +696,11 @@ namespace storm {
                 return abstractionInformation.get();
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            void CommandAbstractor<DdType, ValueType>::notifyGuardIsPredicate() {
+                skipBottomStates = true;
+            }
+            
             template class CommandAbstractor<storm::dd::DdType::CUDD, double>;
             template class CommandAbstractor<storm::dd::DdType::Sylvan, double>;
 #ifdef STORM_HAVE_CARL

src/storm/abstraction/prism/CommandAbstractor.h

@@ -117,6 +117,8 @@ namespace storm {
                  */
                 storm::prism::Command const& getConcreteCommand() const;
                 
+                void notifyGuardIsPredicate();
+                
             private:
                 /*!
                  * Determines the relevant predicates for source as well as successor states wrt. to the given assignments

src/storm/abstraction/prism/ModuleAbstractor.cpp

@@ -119,6 +119,13 @@ namespace storm {
                 return abstractionInformation.get();
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            void ModuleAbstractor<DdType, ValueType>::notifyGuardsArePredicates() {
+                for (auto& command : commands) {
+                    command.notifyGuardIsPredicate();
+                }
+            }
+            
             template class ModuleAbstractor<storm::dd::DdType::CUDD, double>;
             template class ModuleAbstractor<storm::dd::DdType::Sylvan, double>;
 #ifdef STORM_HAVE_CARL

src/storm/abstraction/prism/ModuleAbstractor.h

@@ -113,6 +113,8 @@ namespace storm {
                  */
                 std::vector<CommandAbstractor<DdType, ValueType>>& getCommands();
 
+                void notifyGuardsArePredicates();
+                
             private:
                 /*!
                  * Retrieves the abstraction information.

src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -262,6 +262,13 @@ namespace storm {
                 terminalStateExpressions.emplace_back(expression);
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            void PrismMenuGameAbstractor<DdType, ValueType>::notifyGuardsArePredicates() {
+                for (auto& module : modules) {
+                    module.notifyGuardsArePredicates();
+                }
+            }
+            
             // 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

@@ -123,6 +123,8 @@ namespace storm {
                 
                 virtual void addTerminalStates(storm::expressions::Expression const& expression) override;
                 
+                virtual void notifyGuardsArePredicates() override;
+                
             protected:
                 using MenuGameAbstractor<DdType, ValueType>::exportToDot;