From 057f8798a697250974ec920b9b33e69b12bcf29f Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 17 May 2018 21:55:45 +0200
Subject: [PATCH] avoiding bottom state computation when possible

---
 src/storm/abstraction/MenuGameAbstractor.h              | 6 ++++++
 src/storm/abstraction/MenuGameRefiner.cpp               | 3 ++-
 src/storm/abstraction/jani/AutomatonAbstractor.cpp      | 7 +++++++
 src/storm/abstraction/jani/AutomatonAbstractor.h        | 2 ++
 src/storm/abstraction/jani/EdgeAbstractor.cpp           | 5 +++++
 src/storm/abstraction/jani/EdgeAbstractor.h             | 2 ++
 src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp   | 7 +++++++
 src/storm/abstraction/jani/JaniMenuGameAbstractor.h     | 2 ++
 src/storm/abstraction/prism/CommandAbstractor.cpp       | 5 +++++
 src/storm/abstraction/prism/CommandAbstractor.h         | 2 ++
 src/storm/abstraction/prism/ModuleAbstractor.cpp        | 7 +++++++
 src/storm/abstraction/prism/ModuleAbstractor.h          | 2 ++
 src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp | 7 +++++++
 src/storm/abstraction/prism/PrismMenuGameAbstractor.h   | 2 ++
 14 files changed, 58 insertions(+), 1 deletion(-)

diff --git a/src/storm/abstraction/MenuGameAbstractor.h b/src/storm/abstraction/MenuGameAbstractor.h
index 7e957e406..f55a7f236 100644
--- a/src/storm/abstraction/MenuGameAbstractor.h
+++ b/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;
             
diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp
index 1bbdefd6a..627466d4a 100644
--- a/src/storm/abstraction/MenuGameRefiner.cpp
+++ b/src/storm/abstraction/MenuGameRefiner.cpp
@@ -86,7 +86,8 @@ namespace storm {
                     }
                 }
                 performRefinement(createGlobalRefinement(preprocessPredicates(guards, RefinementPredicates::Source::InitialGuard)));
-
+                
+                this->abstractor.get().notifyGuardsArePredicates();
                 addedAllGuardsFlag = true;
             }
         }
diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.cpp b/src/storm/abstraction/jani/AutomatonAbstractor.cpp
index f5c8030da..b14b4db7b 100644
--- a/src/storm/abstraction/jani/AutomatonAbstractor.cpp
+++ b/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
diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.h b/src/storm/abstraction/jani/AutomatonAbstractor.h
index 658d154f4..9e800b756 100644
--- a/src/storm/abstraction/jani/AutomatonAbstractor.h
+++ b/src/storm/abstraction/jani/AutomatonAbstractor.h
@@ -122,6 +122,8 @@ namespace storm {
                  */
                 std::size_t getNumberOfEdges() const;
                 
+                void notifyGuardsArePredicates();
+                
             private:
                 /*!
                  * Retrieves the abstraction information.
diff --git a/src/storm/abstraction/jani/EdgeAbstractor.cpp b/src/storm/abstraction/jani/EdgeAbstractor.cpp
index ebd7b5839..2342a497f 100644
--- a/src/storm/abstraction/jani/EdgeAbstractor.cpp
+++ b/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
diff --git a/src/storm/abstraction/jani/EdgeAbstractor.h b/src/storm/abstraction/jani/EdgeAbstractor.h
index 22cc7c40d..7ba7445a5 100644
--- a/src/storm/abstraction/jani/EdgeAbstractor.h
+++ b/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
diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp
index 58d5e02f8..ffa590a57 100644
--- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp
+++ b/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>;
diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h
index 3a02583b4..916dbd7d6 100644
--- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h
+++ b/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;
                 
diff --git a/src/storm/abstraction/prism/CommandAbstractor.cpp b/src/storm/abstraction/prism/CommandAbstractor.cpp
index 1c632e4c9..cfd1bed60 100644
--- a/src/storm/abstraction/prism/CommandAbstractor.cpp
+++ b/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
diff --git a/src/storm/abstraction/prism/CommandAbstractor.h b/src/storm/abstraction/prism/CommandAbstractor.h
index cb448bad8..cb6146e73 100644
--- a/src/storm/abstraction/prism/CommandAbstractor.h
+++ b/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
diff --git a/src/storm/abstraction/prism/ModuleAbstractor.cpp b/src/storm/abstraction/prism/ModuleAbstractor.cpp
index e8dc2795e..09e1932cb 100644
--- a/src/storm/abstraction/prism/ModuleAbstractor.cpp
+++ b/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
diff --git a/src/storm/abstraction/prism/ModuleAbstractor.h b/src/storm/abstraction/prism/ModuleAbstractor.h
index a8d5c94cd..d5d2e9dc7 100644
--- a/src/storm/abstraction/prism/ModuleAbstractor.h
+++ b/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.
diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp
index 167f437b6..529ecffad 100644
--- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp
+++ b/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>;
diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h
index 21d64cd30..5815c915a 100644
--- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h
+++ b/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;