more work on explicit game solving

src/storm/abstraction/QualitativeGameResultMinMax.h → src/storm/abstraction/ExplicitQualitativeGameResultMinMax.h

@@ -7,11 +7,10 @@
 
 namespace storm {
     namespace abstraction {
-
-        template<storm::dd::DdType Type>
-        class QualitativeGameResultMinMax : public SymbolicQualitativeResultMinMax<Type> {
+        
+        class ExplicitQualitativeGameResultMinMax : public QualitativeResultMinMax {
         public:
-            QualitativeGameResultMinMax() = default;
+            ExplicitQualitativeGameResultMinMax() = default;
             
             virtual QualitativeResult<Type> const& getProb0(storm::OptimizationDirection const& dir) const override {
                 if (dir == storm::OptimizationDirection::Minimize) {
@@ -34,6 +33,7 @@ namespace storm {
             QualitativeGameResult<Type> prob0Max;
             QualitativeGameResult<Type> prob1Max;
         };
-
+        
     }
 }
+

src/storm/abstraction/ExplicitQualitativeResult.h

@@ -0,0 +1,25 @@
+#pragma once
+
+#include "storm/storage/dd/DdType.h"
+
+#include "storm/abstraction/QualitativeResult.h"
+
+namespace storm {
+    namespace storage {
+        class BitVector;
+    }
+    
+    namespace abstraction {
+        
+        class ExplicitQualitativeResult : public QualitativeResult {
+        public:
+            virtual ~ExplicitQualitativeResult() = default;
+            
+            virtual storm::storage::BitVector const& getStates() const = 0;
+        };
+        
+    }
+}
+
+
+

src/storm/abstraction/ExplicitQualitativeResultMinMax.cpp

@@ -0,0 +1,29 @@
+#include "storm/abstraction/ExplicitQualitativeResultMinMax.h"
+
+#include "storm/abstraction/ExplicitQualitativeResult.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        bool ExplicitQualitativeResultMinMax::isExplicit() const {
+            return true;
+        }
+        
+        ExplicitQualitativeResult const& ExplicitQualitativeResultMinMax::getProb0Min() const {
+            return getProb0(storm::OptimizationDirection::Minimize);
+        }
+        
+        ExplicitQualitativeResult const& ExplicitQualitativeResultMinMax::getProb1Min() const {
+            return getProb1(storm::OptimizationDirection::Minimize);
+        }
+        
+        ExplicitQualitativeResult const& ExplicitQualitativeResultMinMax::getProb0Max() const {
+            return getProb0(storm::OptimizationDirection::Maximize);
+        }
+        
+        ExplicitQualitativeResult const& ExplicitQualitativeResultMinMax::getProb1Max() const {
+            return getProb1(storm::OptimizationDirection::Maximize);
+        }
+        
+    }
+}

src/storm/abstraction/ExplicitQualitativeResultMinMax.h

@@ -0,0 +1,28 @@
+#pragma once
+
+#include "storm/solver/OptimizationDirection.h"
+
+#include "storm/abstraction/QualitativeResultMinMax.h"
+
+namespace storm {
+    namespace abstraction {
+        class ExplicitQualitativeResult;
+
+        class ExplicitQualitativeResultMinMax : public QualitativeResultMinMax {
+        public:
+            ExplicitQualitativeResultMinMax() = default;
+            
+            virtual bool isExplicit() const override;
+            
+            ExplicitQualitativeResult const& getProb0Min() const;
+            ExplicitQualitativeResult const& getProb1Min() const;
+            ExplicitQualitativeResult const& getProb0Max() const;
+            ExplicitQualitativeResult const& getProb1Max() const;
+            
+            virtual ExplicitQualitativeResult const& getProb0(storm::OptimizationDirection const& dir) const = 0;
+            virtual ExplicitQualitativeResult const& getProb1(storm::OptimizationDirection const& dir) const = 0;
+        };
+        
+    }
+}
+

src/storm/abstraction/QualitativeGameResult.h

@@ -1,24 +0,0 @@
-#pragma once
-
-#include "storm/utility/graph.h"
-#include "storm/abstraction/QualitativeResult.h"
-
-namespace storm {
-    namespace abstraction {
-        
-        template <storm::dd::DdType Type>
-        struct QualitativeGameResult : public storm::utility::graph::GameProb01Result<Type>, public QualitativeResult<Type> {
-            QualitativeGameResult() = default;
-            
-            QualitativeGameResult(storm::utility::graph::GameProb01Result<Type> const& prob01Result) : storm::utility::graph::GameProb01Result<Type>(prob01Result) {
-                // Intentionally left empty.
-            }
-            
-            virtual storm::dd::Bdd<Type> const& getStates() const override {
-                return this->getPlayer1States();
-            }
-            
-        };
-        
-    }
-}

src/storm/abstraction/QualitativeMdpResult.h

@@ -1,25 +0,0 @@
-#pragma once
-
-#include "storm/abstraction/QualitativeResult.h"
-
-namespace storm {
-    namespace abstraction {
-        
-        template <storm::dd::DdType Type>
-        struct QualitativeMdpResult : public QualitativeResult<Type> {
-            QualitativeMdpResult() = default;
-            
-            QualitativeMdpResult(storm::dd::Bdd<Type> const& states) : states(states) {
-                // Intentionally left empty.
-            }
-            
-            virtual storm::dd::Bdd<Type> const& getStates() const override {
-                return states;
-            }
-            
-            storm::dd::Bdd<Type> states;
-        };
-        
-    }
-}
-

src/storm/abstraction/QualitativeMdpResultMinMax.h

@@ -1,40 +0,0 @@
-#pragma once
-
-#include "storm/storage/dd/DdType.h"
-
-#include "storm/abstraction/SymbolicQualitativeResultMinMax.h"
-#include "storm/abstraction/QualitativeMdpResult.h"
-
-namespace storm {
-    namespace abstraction {
-        
-        template<storm::dd::DdType Type>
-        class QualitativeMdpResultMinMax : public SymbolicQualitativeResultMinMax<Type> {
-        public:
-            QualitativeMdpResultMinMax() = default;
-            
-            virtual QualitativeResult<Type> const& getProb0(storm::OptimizationDirection const& dir) const override {
-                if (dir == storm::OptimizationDirection::Minimize) {
-                    return prob0Min;
-                } else {
-                    return prob0Max;
-                }
-            }
-            
-            virtual QualitativeResult<Type> const& getProb1(storm::OptimizationDirection const& dir) const override {
-                if (dir == storm::OptimizationDirection::Minimize) {
-                    return prob1Min;
-                } else {
-                    return prob1Max;
-                }
-            }
-            
-            QualitativeMdpResult<Type> prob0Min;
-            QualitativeMdpResult<Type> prob1Min;
-            QualitativeMdpResult<Type> prob0Max;
-            QualitativeMdpResult<Type> prob1Max;
-        };
-        
-    }
-}
-

src/storm/abstraction/QualitativeResult.cpp

@@ -1,3 +1,36 @@
 #include "storm/abstraction/QualitativeResult.h"
 
+#include "storm/abstraction/SymbolicQualitativeResult.h"
+#include "storm/abstraction/ExplicitQualitativeResult.h"
 
+namespace storm {
+    namespace abstraction {
+        
+        bool QualitativeResult::isSymbolic() const {
+            return false;
+        }
+        
+        bool QualitativeResult::isExplicit() const {
+            return false;
+        }
+        
+        template<storm::dd::DdType Type>
+        SymbolicQualitativeResult<Type>& QualitativeResult::asSymbolicQualitativeResult() {
+            return static_cast<SymbolicQualitativeResult<Type>&>(*this);
+        }
+        
+        template<storm::dd::DdType Type>
+        SymbolicQualitativeResult<Type> const& QualitativeResult::asSymbolicQualitativeResult() const {
+            return static_cast<SymbolicQualitativeResult<Type> const&>(*this);
+        }
+        
+        ExplicitQualitativeResult& QualitativeResult::asExplicitQualitativeResult() {
+            return static_cast<ExplicitQualitativeResult&>(*this);
+        }
+        
+        ExplicitQualitativeResult const& QualitativeResult::asExplicitQualitativeResult() const {
+            return static_cast<ExplicitQualitativeResult const&>(*this);
+        }
+
+    }
+}

src/storm/abstraction/QualitativeResult.h

@@ -3,22 +3,29 @@
 #include "storm/storage/dd/DdType.h"
 
 namespace storm {
-    namespace dd {
-        template <storm::dd::DdType Type>
-        class Bdd;
-    }
-    
     namespace abstraction {
         
-        template <storm::dd::DdType Type>
+        template<storm::dd::DdType Type>
+        class SymbolicQualitativeResult;
+
+        class ExplicitQualitativeResult;
+        
         class QualitativeResult {
         public:
             virtual ~QualitativeResult() = default;
+            
+            virtual bool isSymbolic() const;
+            virtual bool isExplicit() const;
+            
+            template<storm::dd::DdType Type>
+            SymbolicQualitativeResult<Type>& asSymbolicQualitativeResult();
+            template<storm::dd::DdType Type>
+            SymbolicQualitativeResult<Type> const& asSymbolicQualitativeResult() const;
+
+            ExplicitQualitativeResult& asExplicitQualitativeResult();
+            ExplicitQualitativeResult const& asExplicitQualitativeResult() const;
 
-            virtual storm::dd::Bdd<Type> const& getStates() const = 0;
         };
         
     }
 }
-
-

src/storm/abstraction/QualitativeResultMinMax.cpp

@@ -8,7 +8,11 @@ namespace storm {
         bool QualitativeResultMinMax::isSymbolic() const {
             return false;
         }
-        
+
+        bool QualitativeResultMinMax::isExplicit() const {
+            return false;
+        }
+
         template<storm::dd::DdType Type>
         SymbolicQualitativeResultMinMax<Type> const& QualitativeResultMinMax::asSymbolicQualitativeResultMinMax() const {
             return static_cast<SymbolicQualitativeResultMinMax<Type> const&>(*this);

src/storm/abstraction/QualitativeResultMinMax.h

@@ -13,7 +13,8 @@ namespace storm {
             virtual ~QualitativeResultMinMax() = default;
 
             virtual bool isSymbolic() const;
-            
+            virtual bool isExplicit() const;
+
             template<storm::dd::DdType Type>
             SymbolicQualitativeResultMinMax<Type> const& asSymbolicQualitativeResultMinMax() const;
             

src/storm/abstraction/QuantitativeGameResult.h

@@ -1,61 +0,0 @@
-#pragma once
-
-#include "storm/storage/dd/DdType.h"
-#include "storm/storage/dd/Add.h"
-#include "storm/storage/dd/Bdd.h"
-
-namespace storm {
-    namespace abstraction {
-
-        template<storm::dd::DdType Type, typename ValueType>
-        struct QuantitativeGameResult {
-            QuantitativeGameResult() = default;
-
-            QuantitativeGameResult(storm::dd::Add<Type, ValueType> const& values) : values(values) {
-                // Intentionally left empty.
-            }
-            
-            QuantitativeGameResult(boost::optional<std::pair<ValueType, ValueType>> const& initialStatesRange, storm::dd::Add<Type, ValueType> const& values, boost::optional<storm::dd::Bdd<Type>> const& player1Strategy, boost::optional<storm::dd::Bdd<Type>> const& player2Strategy) : initialStatesRange(initialStatesRange), values(values), player1Strategy(player1Strategy), player2Strategy(player2Strategy) {
-                // Intentionally left empty.
-            }
-            
-            bool hasPlayer1Strategy() const {
-                return static_cast<bool>(player1Strategy);
-            }
-
-            storm::dd::Bdd<Type> const& getPlayer1Strategy() const {
-                return player1Strategy.get();
-            }
-
-            storm::dd::Bdd<Type>& getPlayer1Strategy() {
-                return player1Strategy.get();
-            }
-
-            bool hasPlayer2Strategy() const {
-                return static_cast<bool>(player2Strategy);
-            }
-
-            storm::dd::Bdd<Type> const& getPlayer2Strategy() const {
-                return player2Strategy.get();
-            }
-
-            storm::dd::Bdd<Type>& getPlayer2Strategy() {
-                return player2Strategy.get();
-            }
-
-            bool hasInitialStatesRange() const {
-                return static_cast<bool>(initialStatesRange);
-            }
-            
-            std::pair<ValueType, ValueType> const& getInitialStatesRange() const {
-                return initialStatesRange.get();
-            }
-
-            boost::optional<std::pair<ValueType, ValueType>> initialStatesRange;
-            storm::dd::Add<Type, ValueType> values;
-            boost::optional<storm::dd::Bdd<Type>> player1Strategy;
-            boost::optional<storm::dd::Bdd<Type>> player2Strategy;
-        };
-        
-    }
-}

src/storm/abstraction/QuantitativeGameResultMinMax.h

@@ -1,22 +0,0 @@
-#pragma once
-
-#include "storm/abstraction/QuantitativeGameResult.h"
-
-namespace storm {
-    namespace abstraction {
-     
-        template<storm::dd::DdType Type, typename ValueType>
-        class QuantitativeGameResultMinMax {
-        public:
-            QuantitativeGameResultMinMax() = default;
-            
-            QuantitativeGameResultMinMax(QuantitativeGameResult<Type, ValueType> const& min, QuantitativeGameResult<Type, ValueType> const& max) : min(min), max(max) {
-                // Intentionally left empty.
-            }
-            
-            QuantitativeGameResult<Type, ValueType> min;
-            QuantitativeGameResult<Type, ValueType> max;
-        };
-        
-    }
-}

src/storm/abstraction/SymbolicQualitativeGameResult.cpp

@@ -0,0 +1,19 @@
+#include "storm/abstraction/SymbolicQualitativeGameResult.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        template <storm::dd::DdType Type>
+        SymbolicQualitativeGameResult<Type>::SymbolicQualitativeGameResult(storm::utility::graph::SymbolicGameProb01Result<Type> const& prob01Result) : storm::utility::graph::SymbolicGameProb01Result<Type>(prob01Result) {
+            // Intentionally left empty.
+        }
+        
+        template <storm::dd::DdType Type>
+        storm::dd::Bdd<Type> const& SymbolicQualitativeGameResult<Type>::getStates() const {
+            return this->getPlayer1States();
+        }
+        
+        template class SymbolicQualitativeGameResult<storm::dd::DdType::CUDD>;
+        template class SymbolicQualitativeGameResult<storm::dd::DdType::Sylvan>;
+    }
+}

src/storm/abstraction/SymbolicQualitativeGameResult.h

@@ -0,0 +1,19 @@
+#pragma once
+
+#include "storm/utility/graph.h"
+#include "storm/abstraction/SymbolicQualitativeResult.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        template <storm::dd::DdType Type>
+        class SymbolicQualitativeGameResult : public storm::utility::graph::SymbolicGameProb01Result<Type>, public SymbolicQualitativeResult<Type> {
+            SymbolicQualitativeGameResult() = default;
+            
+            SymbolicQualitativeGameResult(storm::utility::graph::SymbolicGameProb01Result<Type> const& prob01Result);
+            
+            virtual storm::dd::Bdd<Type> const& getStates() const override;
+        };
+        
+    }
+}

src/storm/abstraction/SymbolicQualitativeGameResultMinMax.cpp

@@ -0,0 +1,29 @@
+#include "storm/abstraction/SymbolicQualitativeGameResultMinMax.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        template<storm::dd::DdType Type>
+        SymbolicQualitativeResult<Type> const& SymbolicQualitativeGameResultMinMax<Type>::getProb0(storm::OptimizationDirection const& dir) const {
+            if (dir == storm::OptimizationDirection::Minimize) {
+                return prob0Min;
+            } else {
+                return prob0Max;
+            }
+        }
+        
+        template<storm::dd::DdType Type>
+        SymbolicQualitativeResult<Type> const& SymbolicQualitativeGameResultMinMax<Type>::getProb1(storm::OptimizationDirection const& dir) const {
+            if (dir == storm::OptimizationDirection::Minimize) {
+                return prob1Min;
+            } else {
+                return prob1Max;
+            }
+        }
+        
+        template class SymbolicQualitativeResultMinMax<storm::dd::DdType::CUDD>;
+        template class SymbolicQualitativeResultMinMax<storm::dd::DdType::Sylvan>;
+
+    }
+}
+

src/storm/abstraction/SymbolicQualitativeGameResultMinMax.h

@@ -0,0 +1,25 @@
+#pragma once
+
+#include "storm/storage/dd/DdType.h"
+
+#include "storm/abstraction/SymbolicQualitativeResultMinMax.h"
+
+namespace storm {
+    namespace abstraction {
+
+        template<storm::dd::DdType Type>
+        class SymbolicQualitativeGameResultMinMax : public SymbolicQualitativeResultMinMax<Type> {
+        public:
+            SymbolicQualitativeGameResultMinMax() = default;
+            
+            virtual SymbolicQualitativeResult<Type> const& getProb0(storm::OptimizationDirection const& dir) const override;
+            virtual SymbolicQualitativeResult<Type> const& getProb1(storm::OptimizationDirection const& dir) const override;
+            
+            SymbolicQualitativeResult<Type> prob0Min;
+            SymbolicQualitativeResult<Type> prob1Min;
+            SymbolicQualitativeResult<Type> prob0Max;
+            SymbolicQualitativeResult<Type> prob1Max;
+        };
+
+    }
+}

src/storm/abstraction/SymbolicQualitativeMdpResult.cpp

@@ -0,0 +1,20 @@
+#include "storm/abstraction/SymbolicQualitativeMdpResult.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        template <storm::dd::DdType Type>
+        SymbolicQualitativeMdpResult<Type>::SymbolicQualitativeMdpResult(storm::dd::Bdd<Type> const& states) : states(states) {
+            // Intentionally left empty.
+        }
+            
+        template <storm::dd::DdType Type>
+        storm::dd::Bdd<Type> const& SymbolicQualitativeMdpResult<Type>::getStates() const {
+            return states;
+        }
+        
+        template class SymbolicQualitativeMdpResult<storm::dd::DdType::CUDD>;
+        template class SymbolicQualitativeMdpResult<storm::dd::DdType::Sylvan>;
+
+    }
+}

src/storm/abstraction/SymbolicQualitativeMdpResult.h

@@ -0,0 +1,23 @@
+#pragma once
+
+#include "storm/abstraction/SymbolicQualitativeResult.h"
+
+#include "storm/storage/dd/Bdd.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        template <storm::dd::DdType Type>
+        class SymbolicQualitativeMdpResult : public SymbolicQualitativeResult<Type> {
+            SymbolicQualitativeMdpResult() = default;
+            
+            SymbolicQualitativeMdpResult(storm::dd::Bdd<Type> const& states);
+            
+            virtual storm::dd::Bdd<Type> const& getStates() const override;
+            
+            storm::dd::Bdd<Type> states;
+        };
+        
+    }
+}
+

src/storm/abstraction/SymbolicQualitativeMdpResultMinMax.cpp

@@ -0,0 +1,29 @@
+#include "storm/abstraction/SymbolicQualitativeMdpResultMinMax.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        template<storm::dd::DdType Type>
+        SymbolicQualitativeResult<Type> const& SymbolicQualitativeMdpResultMinMax<Type>::getProb0(storm::OptimizationDirection const& dir) const {
+            if (dir == storm::OptimizationDirection::Minimize) {
+                return prob0Min;
+            } else {
+                return prob0Max;
+            }
+        }
+        
+        template<storm::dd::DdType Type>
+        SymbolicQualitativeResult<Type> const& SymbolicQualitativeMdpResultMinMax<Type>::getProb1(storm::OptimizationDirection const& dir) const {
+            if (dir == storm::OptimizationDirection::Minimize) {
+                return prob1Min;
+            } else {
+                return prob1Max;
+            }
+        }
+        
+        template class SymbolicQualitativeMdpResultMinMax<storm::dd::DdType::CUDD>;
+        template class SymbolicQualitativeMdpResultMinMax<storm::dd::DdType::Sylvan>;
+
+    }
+}
+

src/storm/abstraction/SymbolicQualitativeMdpResultMinMax.h

@@ -0,0 +1,27 @@
+#pragma once
+
+#include "storm/storage/dd/DdType.h"
+
+#include "storm/abstraction/SymbolicQualitativeResultMinMax.h"
+#include "storm/abstraction/SymbolicQualitativeMdpResult.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        template<storm::dd::DdType Type>
+        class SymbolicQualitativeMdpResultMinMax : public SymbolicQualitativeResultMinMax<Type> {
+        public:
+            SymbolicQualitativeMdpResultMinMax() = default;
+            
+            virtual SymbolicQualitativeResult<Type> const& getProb0(storm::OptimizationDirection const& dir) const override;
+            virtual SymbolicQualitativeResult<Type> const& getProb1(storm::OptimizationDirection const& dir) const override;
+            
+            SymbolicQualitativeMdpResult<Type> prob0Min;
+            SymbolicQualitativeMdpResult<Type> prob1Min;
+            SymbolicQualitativeMdpResult<Type> prob0Max;
+            SymbolicQualitativeMdpResult<Type> prob1Max;
+        };
+        
+    }
+}
+

src/storm/abstraction/SymbolicQualitativeResult.h

@@ -0,0 +1,26 @@
+#pragma once
+
+#include "storm/storage/dd/DdType.h"
+
+#include "storm/abstraction/QualitativeResult.h"
+
+namespace storm {
+    namespace dd {
+        template <storm::dd::DdType Type>
+        class Bdd;
+    }
+    
+    namespace abstraction {
+        
+        template <storm::dd::DdType Type>
+        class SymbolicQualitativeResult : public QualitativeResult {
+        public:
+            virtual ~SymbolicQualitativeResult() = default;
+
+            virtual storm::dd::Bdd<Type> const& getStates() const = 0;
+        };
+        
+    }
+}
+
+

src/storm/abstraction/SymbolicQualitativeResultMinMax.cpp

@@ -11,22 +11,22 @@ namespace storm {
         }
         
         template<storm::dd::DdType Type>
-        QualitativeResult<Type> const& SymbolicQualitativeResultMinMax<Type>::getProb0Min() const {
+        SymbolicQualitativeResult<Type> const& SymbolicQualitativeResultMinMax<Type>::getProb0Min() const {
             return getProb0(storm::OptimizationDirection::Minimize);
         }
         
         template<storm::dd::DdType Type>
-        QualitativeResult<Type> const& SymbolicQualitativeResultMinMax<Type>::getProb1Min() const {
+        SymbolicQualitativeResult<Type> const& SymbolicQualitativeResultMinMax<Type>::getProb1Min() const {
             return getProb1(storm::OptimizationDirection::Minimize);
         }
         
         template<storm::dd::DdType Type>
-        QualitativeResult<Type> const& SymbolicQualitativeResultMinMax<Type>::getProb0Max() const {
+        SymbolicQualitativeResult<Type> const& SymbolicQualitativeResultMinMax<Type>::getProb0Max() const {
             return getProb0(storm::OptimizationDirection::Maximize);
         }
         
         template<storm::dd::DdType Type>
-        QualitativeResult<Type> const& SymbolicQualitativeResultMinMax<Type>::getProb1Max() const {
+        SymbolicQualitativeResult<Type> const& SymbolicQualitativeResultMinMax<Type>::getProb1Max() const {
             return getProb1(storm::OptimizationDirection::Maximize);
         }
         

src/storm/abstraction/SymbolicQualitativeResultMinMax.h

@@ -14,7 +14,7 @@ namespace storm {
     
     namespace abstraction {
         template<storm::dd::DdType Type>
-        class QualitativeResult;
+        class SymbolicQualitativeResult;
         
         template<storm::dd::DdType Type>
         class SymbolicQualitativeResultMinMax : public QualitativeResultMinMax {
@@ -23,13 +23,13 @@ namespace storm {
             
             virtual bool isSymbolic() const override;
             
-            QualitativeResult<Type> const& getProb0Min() const;
-            QualitativeResult<Type> const& getProb1Min() const;
-            QualitativeResult<Type> const& getProb0Max() const;
-            QualitativeResult<Type> const& getProb1Max() const;
+            SymbolicQualitativeResult<Type> const& getProb0Min() const;
+            SymbolicQualitativeResult<Type> const& getProb1Min() const;
+            SymbolicQualitativeResult<Type> const& getProb0Max() const;
+            SymbolicQualitativeResult<Type> const& getProb1Max() const;
             
-            virtual QualitativeResult<Type> const& getProb0(storm::OptimizationDirection const& dir) const = 0;
-            virtual QualitativeResult<Type> const& getProb1(storm::OptimizationDirection const& dir) const = 0;
+            virtual SymbolicQualitativeResult<Type> const& getProb0(storm::OptimizationDirection const& dir) const = 0;
+            virtual SymbolicQualitativeResult<Type> const& getProb1(storm::OptimizationDirection const& dir) const = 0;
         };
     }
 }

src/storm/abstraction/SymbolicQuantitativeGameResult.cpp

@@ -0,0 +1,61 @@
+#include "storm/abstraction/SymbolicQuantitativeGameResult.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        SymbolicQuantitativeGameResult<Type, ValueType>::SymbolicQuantitativeGameResult(storm::dd::Add<Type, ValueType> const& values) : values(values) {
+            // Intentionally left empty.
+        }
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        SymbolicQuantitativeGameResult<Type, ValueType>::SymbolicQuantitativeGameResult(boost::optional<std::pair<ValueType, ValueType>> const& initialStatesRange, storm::dd::Add<Type, ValueType> const& values, boost::optional<storm::dd::Bdd<Type>> const& player1Strategy, boost::optional<storm::dd::Bdd<Type>> const& player2Strategy) : initialStatesRange(initialStatesRange), values(values), player1Strategy(player1Strategy), player2Strategy(player2Strategy) {
+            // Intentionally left empty.
+        }
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        bool SymbolicQuantitativeGameResult<Type, ValueType>::hasPlayer1Strategy() const {
+            return static_cast<bool>(player1Strategy);
+        }
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        storm::dd::Bdd<Type> const& SymbolicQuantitativeGameResult<Type, ValueType>::getPlayer1Strategy() const {
+            return player1Strategy.get();
+        }
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        storm::dd::Bdd<Type>& SymbolicQuantitativeGameResult<Type, ValueType>::getPlayer1Strategy() {
+            return player1Strategy.get();
+        }
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        bool SymbolicQuantitativeGameResult<Type, ValueType>::hasPlayer2Strategy() const {
+            return static_cast<bool>(player2Strategy);
+        }
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        storm::dd::Bdd<Type> const& SymbolicQuantitativeGameResult<Type, ValueType>::getPlayer2Strategy() const {
+            return player2Strategy.get();
+        }
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        storm::dd::Bdd<Type>& SymbolicQuantitativeGameResult<Type, ValueType>::getPlayer2Strategy() {
+            return player2Strategy.get();
+        }
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        bool SymbolicQuantitativeGameResult<Type, ValueType>::hasInitialStatesRange() const {
+            return static_cast<bool>(initialStatesRange);
+        }
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        std::pair<ValueType, ValueType> const& SymbolicQuantitativeGameResult<Type, ValueType>::getInitialStatesRange() const {
+            return initialStatesRange.get();
+        }
+        
+        template class SymbolicQuantitativeGameResult<storm::dd::DdType::CUDD, double>;
+        template class SymbolicQuantitativeGameResult<storm::dd::DdType::Sylvan, double>;
+
+    }
+}
+

src/storm/abstraction/SymbolicQuantitativeGameResult.h

@@ -0,0 +1,41 @@
+#pragma once
+
+#include "storm/storage/dd/DdType.h"
+#include "storm/storage/dd/Add.h"
+#include "storm/storage/dd/Bdd.h"
+
+namespace storm {
+    namespace abstraction {
+
+        template<storm::dd::DdType Type, typename ValueType>
+        class SymbolicQuantitativeGameResult {
+        public:
+            SymbolicQuantitativeGameResult() = default;
+
+            SymbolicQuantitativeGameResult(storm::dd::Add<Type, ValueType> const& values);
+            SymbolicQuantitativeGameResult(boost::optional<std::pair<ValueType, ValueType>> const& initialStatesRange, storm::dd::Add<Type, ValueType> const& values, boost::optional<storm::dd::Bdd<Type>> const& player1Strategy, boost::optional<storm::dd::Bdd<Type>> const& player2Strategy);
+            
+            bool hasPlayer1Strategy() const;
+
+            storm::dd::Bdd<Type> const& getPlayer1Strategy() const;
+
+            storm::dd::Bdd<Type>& getPlayer1Strategy();
+
+            bool hasPlayer2Strategy() const;
+
+            storm::dd::Bdd<Type> const& getPlayer2Strategy() const;
+
+            storm::dd::Bdd<Type>& getPlayer2Strategy();
+
+            bool hasInitialStatesRange() const;
+            
+            std::pair<ValueType, ValueType> const& getInitialStatesRange() const;
+
+            boost::optional<std::pair<ValueType, ValueType>> initialStatesRange;
+            storm::dd::Add<Type, ValueType> values;
+            boost::optional<storm::dd::Bdd<Type>> player1Strategy;
+            boost::optional<storm::dd::Bdd<Type>> player2Strategy;
+        };
+        
+    }
+}

src/storm/abstraction/SymbolicQuantitativeGameResultMinMax.cpp

@@ -0,0 +1,12 @@
+#include "storm/abstraction/SymbolicQuantitativeGameResultMinMax.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        SymbolicQuantitativeGameResultMinMax<Type, ValueType>::SymbolicQuantitativeGameResultMinMax(SymbolicQuantitativeGameResult<Type, ValueType> const& min, SymbolicQuantitativeGameResult<Type, ValueType> const& max) : min(min), max(max) {
+            // Intentionally left empty.
+        }
+            
+    }
+}

src/storm/abstraction/SymbolicQuantitativeGameResultMinMax.h

@@ -0,0 +1,20 @@
+#pragma once
+
+#include "storm/abstraction/SymbolicQuantitativeGameResult.h"
+
+namespace storm {
+    namespace abstraction {
+     
+        template<storm::dd::DdType Type, typename ValueType>
+        class SymbolicQuantitativeGameResultMinMax {
+        public:
+            SymbolicQuantitativeGameResultMinMax() = default;
+            
+            SymbolicQuantitativeGameResultMinMax(SymbolicQuantitativeGameResult<Type, ValueType> const& min, SymbolicQuantitativeGameResult<Type, ValueType> const& max);
+            
+            SymbolicQuantitativeGameResult<Type, ValueType> min;
+            SymbolicQuantitativeGameResult<Type, ValueType> max;
+        };
+        
+    }
+}

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -367,8 +367,7 @@ namespace storm {
                 auto abstractionEnd = std::chrono::high_resolution_clock::now();
                 STORM_LOG_DEBUG("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " (player 1) states, " << game.getNumberOfTransitions() << " transitions, " << game.getBottomStates().getNonZeroCount() << " bottom states (computed in " << std::chrono::duration_cast<std::chrono::milliseconds>(abstractionEnd - abstractionStart).count() << "ms).");
                 
-                // (2) Prepare transition matrix BDD and target state BDD for later use.
-                storm::dd::Bdd<Type> transitionMatrixBdd = game.getTransitionMatrix().toBdd();
+                // (2) Prepare initial, constraint and target state BDDs for later use.
                 storm::dd::Bdd<Type> initialStates = game.getInitialStates();
                 STORM_LOG_THROW(initialStates.getNonZeroCount() == 1 || checkTask.isBoundSet(), storm::exceptions::InvalidPropertyException, "Game-based abstraction refinement requires a bound on the formula for model with " << initialStates.getNonZeroCount() << " initial states.");
                 storm::dd::Bdd<Type> constraintStates = globalConstraintStates && game.getReachableStates();
@@ -383,117 +382,18 @@ namespace storm {
                 // game.getReachableStates().template toAdd<ValueType>().exportToDot("reach.dot");
                 // #endif
                 
-                // (3) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max).
-                auto qualitativeStart = std::chrono::high_resolution_clock::now();
-                QualitativeGameResultMinMax<Type> qualitativeResult = computeProb01States(previousQualitativeResult, game, player1Direction, transitionMatrixBdd, constraintStates, targetStates);
-                std::unique_ptr<CheckResult> result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, initialStates, qualitativeResult);
+                std::unique_ptr<CheckResult> result;
+                if (solveMode == storm::settings::modules::AbstractionSettings::SolveMode::Dd) {
+                    result = performSymbolicAbstractionSolutionStep(env, checkTask, game, player1Direction, initialStates, constraintStates, targetStates, refiner, previousQualitativeResult, previousMinQuantitativeResult);
+                } else {
+                    result = performExplicitAbstractionSolutionStep(env, checkTask, game, player1Direction, initialStates, constraintStates, targetStates, refiner);
+                }
+
                 if (result) {
                     printStatistics(*abstractor, game);
                     return result;
                 }
-                previousQualitativeResult = qualitativeResult;
-                auto qualitativeEnd = std::chrono::high_resolution_clock::now();
-                STORM_LOG_DEBUG("Qualitative computation completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(qualitativeEnd - qualitativeStart).count() << "ms.");
                 
-                // (4) compute the states for which we have to determine quantitative information.
-                storm::dd::Bdd<Type> maybeMin = !(qualitativeResult.prob0Min.getPlayer1States() || qualitativeResult.prob1Min.getPlayer1States()) && game.getReachableStates();
-                storm::dd::Bdd<Type> maybeMax = !(qualitativeResult.prob0Max.getPlayer1States() || qualitativeResult.prob1Max.getPlayer1States()) && game.getReachableStates();
-                
-                // (5) if the initial states are not maybe states, then we can refine at this point.
-                storm::dd::Bdd<Type> initialMaybeStates = (initialStates && maybeMin) || (initialStates && maybeMax);
-                bool qualitativeRefinement = false;
-                if (initialMaybeStates.isZero()) {
-                    // In this case, we know the result for the initial states for both player 2 minimizing and maximizing.
-                    STORM_LOG_TRACE("No initial state is a 'maybe' state.");
-                    
-                    STORM_LOG_DEBUG("Obtained qualitative bounds [0, 1] on the actual value for the initial states. Refining abstraction based on qualitative check.");
-                    
-                    // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1)
-                    // depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine.
-                    auto qualitativeRefinementStart = std::chrono::high_resolution_clock::now();
-                    qualitativeRefinement = refiner.refine(game, transitionMatrixBdd, qualitativeResult);
-                    auto qualitativeRefinementEnd = std::chrono::high_resolution_clock::now();
-                    STORM_LOG_DEBUG("Qualitative refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(qualitativeRefinementEnd - qualitativeRefinementStart).count() << "ms.");
-                } else if (initialMaybeStates == initialStates && checkTask.isQualitativeSet()) {
-                    // If all initial states are 'maybe' states and the property we needed to check is a qualitative one,
-                    // we can return the result here.
-                    return std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), ValueType(0.5));
-                }
-                
-                // (6) if we arrived at this point and no refinement was made, we need to compute the quantitative solution.
-                if (!qualitativeRefinement) {
-                    // At this point, we know that we cannot answer the query without further numeric computation.
-                    STORM_LOG_TRACE("Starting numerical solution step.");
-
-                    // Solve abstraction using the selected mode.
-                    if (solveMode == storm::settings::modules::AbstractionSettings::SolveMode::Dd) {
-                        STORM_LOG_TRACE("Using dd-based solving.");
-                        storm::dd::Add<Type, ValueType> initialStatesAdd = initialStates.template toAdd<ValueType>();
-                        
-                        auto quantitativeStart = std::chrono::high_resolution_clock::now();
-                        
-                        QuantitativeGameResultMinMax<Type, ValueType> quantitativeResult;
-                        
-                        // (7) Solve the min values and check whether we can give the answer already.
-                        quantitativeResult.min = computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin, reuseQuantitativeResults ? previousMinQuantitativeResult : boost::none);
-                        previousMinQuantitativeResult = quantitativeResult.min;
-                        result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.min.getInitialStatesRange());
-                        if (result) {
-                            printStatistics(*abstractor, game);
-                            return result;
-                        }
-                        
-                        // (8) Solve the max values and check whether we can give the answer already.
-                        quantitativeResult.max = computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, game, qualitativeResult, initialStatesAdd, maybeMax, boost::make_optional(quantitativeResult.min));
-                        result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.max.getInitialStatesRange());
-                        if (result) {
-                            printStatistics(*abstractor, game);
-                            return result;
-                        }
-                        
-                        auto quantitativeEnd = std::chrono::high_resolution_clock::now();
-                        STORM_LOG_DEBUG("Obtained quantitative bounds [" << quantitativeResult.min.getInitialStatesRange().first << ", " << quantitativeResult.max.getInitialStatesRange().second << "] on the actual value for the initial states in " << std::chrono::duration_cast<std::chrono::milliseconds>(quantitativeEnd - quantitativeStart).count() << "ms.");
-                        
-                        // (9) Check whether the lower and upper bounds are close enough to terminate with an answer.
-                        result = checkForResultAfterQuantitativeCheck<ValueType>(quantitativeResult.min.getInitialStatesRange().first, quantitativeResult.max.getInitialStatesRange().second, comparator);
-                        if (result) {
-                            printStatistics(*abstractor, game);
-                            return result;
-                        }
-                        
-                        // Make sure that all strategies are still valid strategies.
-                        STORM_LOG_ASSERT(quantitativeResult.min.getPlayer1Strategy().isZero() || quantitativeResult.min.getPlayer1Strategy().template toAdd<ValueType>().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for min is illegal.");
-                        STORM_LOG_ASSERT(quantitativeResult.max.getPlayer1Strategy().isZero() || quantitativeResult.max.getPlayer1Strategy().template toAdd<ValueType>().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for max is illegal.");
-                        STORM_LOG_ASSERT(quantitativeResult.min.getPlayer2Strategy().isZero() || quantitativeResult.min.getPlayer2Strategy().template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal.");
-                        STORM_LOG_ASSERT(quantitativeResult.max.getPlayer2Strategy().isZero() || quantitativeResult.max.getPlayer2Strategy().template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal.");
-                        
-                        auto quantitativeRefinementStart = std::chrono::high_resolution_clock::now();
-                        // (10) If we arrived at this point, it means that we have all qualitative and quantitative
-                        // information about the game, but we could not yet answer the query. In this case, we need to refine.
-                        refiner.refine(game, transitionMatrixBdd, quantitativeResult);
-                        auto quantitativeRefinementEnd = std::chrono::high_resolution_clock::now();
-                        STORM_LOG_DEBUG("Quantitative refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(quantitativeRefinementEnd - quantitativeRefinementStart).count() << "ms.");
-                    } else {
-                        STORM_LOG_TRACE("Using hybrid solving.");
-
-                        auto relevantStates = maybeMin || maybeMax || targetStates;
-                        auto relevantStatesAdd = relevantStates.template toAdd<ValueType>();
-                        storm::dd::Odd odd = relevantStates.createOdd();
-                        
-                        auto relevantStatesTransitionMatrix = game.getTransitionMatrix() * relevantStatesAdd * relevantStatesAdd.swapVariables(game.getRowColumnMetaVariablePairs());
-                        std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<uint64_t>> transitionMatrixLabeling = relevantStatesTransitionMatrix.toLabeledMatrix(game.getRowVariables(), game.getColumnVariables(), game.getNondeterminismVariables(), game.getPlayer1Variables(), odd, odd, true);
-                        auto const& transitionMatrix = transitionMatrixLabeling.first;
-                        auto const& labeling = transitionMatrixLabeling.second;
-                        
-                        std::cout << transitionMatrix << std::endl;
-                        for (auto const& e : labeling) {
-                            std::cout << e << std::endl;
-                        }
-                        
-                        exit(-1);
-                    }
-
-                }
                 auto iterationEnd = std::chrono::high_resolution_clock::now();
                 STORM_LOG_DEBUG("Iteration " << iterations << " took " << std::chrono::duration_cast<std::chrono::milliseconds>(iterationEnd - iterationStart).count() << "ms.");
             }
@@ -502,6 +402,141 @@ namespace storm {
             return nullptr;
         }
         
+        template<storm::dd::DdType Type, typename ModelType>
+        std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ModelType>::performSymbolicAbstractionSolutionStep(Environment const& env, CheckTask<storm::logic::Formula> const& checkTask, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates, storm::abstraction::MenuGameRefiner<Type, ValueType> const& refiner, boost::optional<QualitativeGameResultMinMax<Type>>& previousQualitativeResult, boost::optional<QuantitativeGameResult<Type, ValueType>>& previousMinQuantitativeResult) {
+
+            STORM_LOG_TRACE("Using dd-based solving.");
+
+            // Prepare transition matrix BDD.
+            storm::dd::Bdd<Type> transitionMatrixBdd = game.getTransitionMatrix().toBdd();
+            
+            // (1) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max).
+            auto qualitativeStart = std::chrono::high_resolution_clock::now();
+            QualitativeGameResultMinMax<Type> qualitativeResult = computeProb01States(previousQualitativeResult, game, player1Direction, transitionMatrixBdd, constraintStates, targetStates);
+            std::unique_ptr<CheckResult> result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, initialStates, qualitativeResult);
+            if (result) {
+                return result;
+            }
+            previousQualitativeResult = qualitativeResult;
+            auto qualitativeEnd = std::chrono::high_resolution_clock::now();
+            STORM_LOG_DEBUG("Qualitative computation completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(qualitativeEnd - qualitativeStart).count() << "ms.");
+            
+            // (2) compute the states for which we have to determine quantitative information.
+            storm::dd::Bdd<Type> maybeMin = !(qualitativeResult.prob0Min.getPlayer1States() || qualitativeResult.prob1Min.getPlayer1States()) && game.getReachableStates();
+            storm::dd::Bdd<Type> maybeMax = !(qualitativeResult.prob0Max.getPlayer1States() || qualitativeResult.prob1Max.getPlayer1States()) && game.getReachableStates();
+            
+            // (3) if the initial states are not maybe states, then we can refine at this point.
+            storm::dd::Bdd<Type> initialMaybeStates = (initialStates && maybeMin) || (initialStates && maybeMax);
+            bool qualitativeRefinement = false;
+            if (initialMaybeStates.isZero()) {
+                // In this case, we know the result for the initial states for both player 2 minimizing and maximizing.
+                STORM_LOG_TRACE("No initial state is a 'maybe' state.");
+                
+                STORM_LOG_DEBUG("Obtained qualitative bounds [0, 1] on the actual value for the initial states. Refining abstraction based on qualitative check.");
+                
+                // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1)
+                // depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine.
+                auto qualitativeRefinementStart = std::chrono::high_resolution_clock::now();
+                qualitativeRefinement = refiner.refine(game, transitionMatrixBdd, qualitativeResult);
+                auto qualitativeRefinementEnd = std::chrono::high_resolution_clock::now();
+                STORM_LOG_DEBUG("Qualitative refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(qualitativeRefinementEnd - qualitativeRefinementStart).count() << "ms.");
+            } else if (initialMaybeStates == initialStates && checkTask.isQualitativeSet()) {
+                // If all initial states are 'maybe' states and the property we needed to check is a qualitative one,
+                // we can return the result here.
+                return std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), ValueType(0.5));
+            }
+            
+            // (4) if we arrived at this point and no refinement was made, we need to compute the quantitative solution.
+            if (!qualitativeRefinement) {
+                // At this point, we know that we cannot answer the query without further numeric computation.
+                STORM_LOG_TRACE("Starting numerical solution step.");
+                
+                STORM_LOG_TRACE("Using dd-based solving.");
+                storm::dd::Add<Type, ValueType> initialStatesAdd = initialStates.template toAdd<ValueType>();
+                
+                auto quantitativeStart = std::chrono::high_resolution_clock::now();
+                
+                QuantitativeGameResultMinMax<Type, ValueType> quantitativeResult;
+                
+                // (7) Solve the min values and check whether we can give the answer already.
+                quantitativeResult.min = computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin, reuseQuantitativeResults ? previousMinQuantitativeResult : boost::none);
+                previousMinQuantitativeResult = quantitativeResult.min;
+                result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.min.getInitialStatesRange());
+                if (result) {
+                    return result;
+                }
+                
+                // (8) Solve the max values and check whether we can give the answer already.
+                quantitativeResult.max = computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, game, qualitativeResult, initialStatesAdd, maybeMax, boost::make_optional(quantitativeResult.min));
+                result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.max.getInitialStatesRange());
+                if (result) {
+                    return result;
+                }
+                
+                auto quantitativeEnd = std::chrono::high_resolution_clock::now();
+                STORM_LOG_DEBUG("Obtained quantitative bounds [" << quantitativeResult.min.getInitialStatesRange().first << ", " << quantitativeResult.max.getInitialStatesRange().second << "] on the actual value for the initial states in " << std::chrono::duration_cast<std::chrono::milliseconds>(quantitativeEnd - quantitativeStart).count() << "ms.");
+                
+                // (9) Check whether the lower and upper bounds are close enough to terminate with an answer.
+                result = checkForResultAfterQuantitativeCheck<ValueType>(quantitativeResult.min.getInitialStatesRange().first, quantitativeResult.max.getInitialStatesRange().second, comparator);
+                if (result) {
+                    return result;
+                }
+                
+                // Make sure that all strategies are still valid strategies.
+                STORM_LOG_ASSERT(quantitativeResult.min.getPlayer1Strategy().isZero() || quantitativeResult.min.getPlayer1Strategy().template toAdd<ValueType>().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for min is illegal.");
+                STORM_LOG_ASSERT(quantitativeResult.max.getPlayer1Strategy().isZero() || quantitativeResult.max.getPlayer1Strategy().template toAdd<ValueType>().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for max is illegal.");
+                STORM_LOG_ASSERT(quantitativeResult.min.getPlayer2Strategy().isZero() || quantitativeResult.min.getPlayer2Strategy().template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal.");
+                STORM_LOG_ASSERT(quantitativeResult.max.getPlayer2Strategy().isZero() || quantitativeResult.max.getPlayer2Strategy().template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal.");
+                
+                auto quantitativeRefinementStart = std::chrono::high_resolution_clock::now();
+                
+                // (10) If we arrived at this point, it means that we have all qualitative and quantitative
+                // information about the game, but we could not yet answer the query. In this case, we need to refine.
+                refiner.refine(game, transitionMatrixBdd, quantitativeResult);
+                auto quantitativeRefinementEnd = std::chrono::high_resolution_clock::now();
+                STORM_LOG_DEBUG("Quantitative refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(quantitativeRefinementEnd - quantitativeRefinementStart).count() << "ms.");
+            }
+            
+            // Return null to indicate no result has been found yet.
+            return nullptr;
+        }
+
+        template<storm::dd::DdType Type, typename ModelType>
+        std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ModelType>::performExplicitAbstractionSolutionStep(Environment const& env, CheckTask<storm::logic::Formula> const& checkTask, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& initialStatesBdd, storm::dd::Bdd<Type> const& constraintStatesBdd, storm::dd::Bdd<Type> const& targetStatesBdd, storm::abstraction::MenuGameRefiner<Type, ValueType> const& refiner) {
+            STORM_LOG_TRACE("Using hybrid solving.");
+
+            // (0) Start by transforming the necessary symbolic elements to explicit ones.
+            storm::dd::Odd odd = game.getReachableStates().createOdd();
+            
+            std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<uint64_t>> transitionMatrixAndLabeling = game.getTransitionMatrix().toLabeledMatrix(game.getRowVariables(), game.getColumnVariables(), game.getNondeterminismVariables(), game.getPlayer1Variables(), odd, odd, true);
+            auto const& transitionMatrix = transitionMatrixAndLabeling.first;
+            auto const& labeling = transitionMatrixAndLabeling.second;
+
+            storm::storage::BitVector initialStates = initialStatesBdd.toVector(odd);
+            storm::storage::BitVector constraintStates = constraintStatesBdd.toVector(odd);
+            storm::storage::BitVector targetStates = targetStatesBdd.toVector(odd);
+
+            // (1) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max).
+            auto qualitativeStart = std::chrono::high_resolution_clock::now();
+            ExplicitQualitativeGameResultMinMax qualitativeResult = computeProb01States(game, player1Direction, transitionMatrix, constraintStates, targetStates);
+            std::unique_ptr<CheckResult> result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, initialStates, qualitativeResult);
+            if (result) {
+                return result;
+            }
+            auto qualitativeEnd = std::chrono::high_resolution_clock::now();
+            STORM_LOG_DEBUG("Qualitative computation completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(qualitativeEnd - qualitativeStart).count() << "ms.");
+
+            
+            
+            std::cout << transitionMatrix << std::endl;
+            std::cout << labeling.size() << std::endl;
+            std::cout << initialStates << std::endl;
+            std::cout << constraintStates << std::endl;
+            std::cout << targetStates << std::endl;
+            
+            exit(-1);
+        }
+        
         template<storm::dd::DdType Type, typename ModelType>
         std::vector<storm::expressions::Expression> GameBasedMdpModelChecker<Type, ModelType>::getInitialPredicates(storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) {
             std::vector<storm::expressions::Expression> initialPredicates;

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h

@@ -27,6 +27,15 @@ namespace storm {
 
         template<storm::dd::DdType Type, typename ValueType>
         class MenuGameAbstractor;
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        class MenuGameRefiner;
+        
+        template<storm::dd::DdType Type>
+        class QualitativeGameResultMinMax;
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        struct QuantitativeGameResult;
     }
     
     namespace modelchecker {
@@ -59,6 +68,9 @@ namespace storm {
              */
             std::unique_ptr<CheckResult> performGameBasedAbstractionRefinement(Environment const& env, CheckTask<storm::logic::Formula> const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression);
             
+            std::unique_ptr<CheckResult> performSymbolicAbstractionSolutionStep(Environment const& env, CheckTask<storm::logic::Formula> const& checkTask, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates, storm::abstraction::MenuGameRefiner<Type, ValueType> const& refiner, boost::optional<QualitativeGameResultMinMax<Type>>& previousQualitativeResult, boost::optional<abstraction::QuantitativeGameResult<Type, ValueType>>& previousMinQuantitativeResult);
+            std::unique_ptr<CheckResult> performExplicitAbstractionSolutionStep(Environment const& env, CheckTask<storm::logic::Formula> const& checkTask, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates, storm::abstraction::MenuGameRefiner<Type, ValueType> const& refiner);
+
             /*!
              * Retrieves the initial predicates for the abstraction.
              */

src/storm/settings/modules/AbstractionSettings.cpp

@@ -44,7 +44,7 @@ namespace storm {
                                              .setDefaultValueString("all").build())
                                 .build());
 
-                std::vector<std::string> solveModes = {"dd", "hybrid"};
+                std::vector<std::string> solveModes = {"dd", "sparse"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, solveModeOptionName, true, "Sets how the abstractions are solved.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(solveModes))
                                              .setDefaultValueString("dd").build())
@@ -110,7 +110,7 @@ namespace storm {
                 if (solveModeAsString == "dd") {
                     return SolveMode::Dd;
                 }
-                return SolveMode::Hybrid;
+                return SolveMode::Sparse;
             }
             
             bool AbstractionSettings::isAddAllGuardsSet() const {

src/storm/settings/modules/AbstractionSettings.h

@@ -28,7 +28,7 @@ namespace storm {
                 };
                 
                 enum class SolveMode {
-                    Dd, Hybrid
+                    Dd, Sparse
                 };
                 
                 /*!

src/storm/storage/dd/Add.cpp

@@ -810,13 +810,11 @@ namespace storm {
                 }
                 
                 statesWithGroupEnabled[i] = groupNotZero.existsAbstract(columnMetaVariables).template toAdd<uint_fast64_t>();
-                statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus<uint_fast64_t>());
-                
                 if (buildLabeling) {
                     uint64_t currentLabel = groupLabels[i];
-                    std::cout << "current label is " << currentLabel << std::endl;
-                    // statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, labeling, [currentLabel] (uint_fast64_t a, uint_fast64_t l) { return currentLabel; });
+                    statesWithGroupEnabled[i].forEach(rowOdd, ddRowVariableIndices, [currentLabel, &rowGroupIndices, &labeling] (uint64_t const& offset, uint_fast64_t const& value) { labeling[rowGroupIndices[offset]] = currentLabel; });
                 }
+                statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus<uint_fast64_t>());
             }
             
             // Since we modified the rowGroupIndices, we need to restore the correct values.

src/storm/storage/dd/cudd/InternalCuddAdd.cpp

@@ -494,16 +494,24 @@ namespace storm {
         
         template<typename ValueType>
         void InternalAdd<DdType::CUDD, ValueType>::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const {
-            composeWithExplicitVectorRec(this->getCuddDdNode(), nullptr, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function);
+            forEachRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, [&function, &targetVector] (uint64_t const& offset, ValueType const& value) { targetVector[offset] = function(targetVector[offset], value); });
+        }
+        
+        template<typename ValueType>
+        void InternalAdd<DdType::CUDD, ValueType>::forEach(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::function<void (uint64_t const&, ValueType const&)> const& function) const {
+            forEachRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, function);
         }
         
         template<typename ValueType>
         void InternalAdd<DdType::CUDD, ValueType>::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<uint_fast64_t> const& offsets, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const {
-            composeWithExplicitVectorRec(this->getCuddDdNode(), &offsets, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function);
+            forEachRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, [&function, &targetVector, &offsets] (uint64_t const& offset, ValueType const& value) {
+                ValueType& targetValue = targetVector[offsets[offset]];
+                targetValue = function(targetValue, value);
+            });
         }
 
         template<typename ValueType>
-        void InternalAdd<DdType::CUDD, ValueType>::composeWithExplicitVectorRec(DdNode const* dd, std::vector<uint_fast64_t> const* offsets, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const {
+        void InternalAdd<DdType::CUDD, ValueType>::forEachRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::function<void (uint64_t const&, ValueType const&)> const& function) const {
             // For the empty DD, we do not need to add any entries.
             if (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) {
                 return;
@@ -511,24 +519,22 @@ namespace storm {
             
             // If we are at the maximal level, the value to be set is stored as a constant in the DD.
             if (currentLevel == maxLevel) {
-                ValueType& targetValue = targetVector[offsets != nullptr ? (*offsets)[currentOffset] : currentOffset];
-                targetValue = function(targetValue, storm::utility::convertNumber<ValueType>(Cudd_V(dd)));
+                function(currentOffset, storm::utility::convertNumber<ValueType>(Cudd_V(dd)));
             } else if (ddVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) {
                 // If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set
                 // and for the one in which it is not set.
-                composeWithExplicitVectorRec(dd, offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function);
-                composeWithExplicitVectorRec(dd, offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function);
+                forEachRec(dd, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, function);
+                forEachRec(dd, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, function);
             } else {
                 // Otherwise, we simply recursively call the function for both (different) cases.
-                composeWithExplicitVectorRec(Cudd_E_const(dd), offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function);
-                composeWithExplicitVectorRec(Cudd_T_const(dd), offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function);
+                forEachRec(Cudd_E_const(dd), currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, function);
+                forEachRec(Cudd_T_const(dd), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, function);
             }
         }
         
         template<typename ValueType>
         std::vector<uint64_t> InternalAdd<DdType::CUDD, ValueType>::decodeGroupLabels(std::vector<uint_fast64_t> const& ddGroupVariableIndices, storm::storage::BitVector const& ddLabelVariableIndices) const {
             std::vector<uint64_t> result;
-            std::cout << ddLabelVariableIndices << std::endl;
             decodeGroupLabelsRec(this->getCuddDdNode(), result, ddGroupVariableIndices, ddLabelVariableIndices, 0, ddGroupVariableIndices.size(), 0);
             return result;
         }
@@ -546,7 +552,6 @@ namespace storm {
                 uint64_t elseLabel = label;
                 uint64_t thenLabel = label;
 
-                std::cout << "currentLevel " << currentLevel << " is in labels? " << ddLabelVariableIndices.get(currentLevel) << std::endl;
                 if (ddLabelVariableIndices.get(currentLevel)) {
                     elseLabel <<= 1;
                     thenLabel = (thenLabel << 1) | 1;

src/storm/storage/dd/cudd/InternalCuddAdd.h

@@ -549,6 +549,18 @@ namespace storm {
              */
             void composeWithExplicitVector(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const;
             
+            /*!
+             * Composes the ADD with an explicit vector by performing a specified function between the entries of this
+             * ADD and the explicit vector.
+             *
+             * @param odd The ODD to use for the translation from symbolic to explicit positions.
+             * @param ddVariableIndices The indices of the DD variables present in this ADD.
+             * @param targetVector The explicit vector that is to be composed with the ADD. The results are written to
+             * this vector again.
+             * @param function The function to perform in the composition.
+             */
+            void forEach(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::function<void (uint64_t const&, ValueType const&)> const& function) const;
+            
             /*!
              * Composes the (row-grouped) ADD with an explicit vector by performing a specified function between the
              * entries of this ADD and the explicit vector.
@@ -646,18 +658,18 @@ namespace storm {
             
         private:
             /*!
-             * Performs a recursive step to perform the given function between the given DD-based vector and the given
-             * explicit vector.
+             * Performs a recursive step for forEach.
              *
-             * @param dd The DD to add to the explicit vector.
+             * @param dd The DD to traverse.
              * @param currentLevel The currently considered level in the DD.
              * @param maxLevel The number of levels that need to be considered.
              * @param currentOffset The current offset.
              * @param odd The ODD used for the translation.
              * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered.
-             * @param targetVector The vector to which the translated DD-based vector is to be added.
+             * @param function The callback invoked for every element. The first argument is the offset and the second
+             * is the value.
              */
-            void composeWithExplicitVectorRec(DdNode const* dd, std::vector<uint_fast64_t> const* offsets, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const;
+            void forEachRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::function<void (uint64_t const&, ValueType const&)> const& function) const;
             
             /*!
              * Splits the given matrix DD into the groups using the given group variables.

src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp

@@ -884,16 +884,24 @@ namespace storm {
         
         template<typename ValueType>
         void InternalAdd<DdType::Sylvan, ValueType>::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const {
-            composeWithExplicitVectorRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_hascomp(this->getSylvanMtbdd().GetMTBDD()), nullptr, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function);
+            forEachRec(this->getSylvanMtbdd().GetMTBDD(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, [&function, &targetVector] (uint64_t const& offset, ValueType const& value) { targetVector[offset] = function(targetVector[offset], value); });
         }
         
         template<typename ValueType>
         void InternalAdd<DdType::Sylvan, ValueType>::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<uint_fast64_t> const& offsets, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const {
-            composeWithExplicitVectorRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_hascomp(this->getSylvanMtbdd().GetMTBDD()), &offsets, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function);
+            forEachRec(this->getSylvanMtbdd().GetMTBDD(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices,  [&function, &targetVector, &offsets] (uint64_t const& offset, ValueType const& value) {
+                ValueType& targetValue = targetVector[offsets[offset]];
+                targetValue = function(targetValue, value);
+            });
         }
         
         template<typename ValueType>
-        void InternalAdd<DdType::Sylvan, ValueType>::composeWithExplicitVectorRec(MTBDD dd, bool negated, std::vector<uint_fast64_t> const* offsets, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const {
+        void InternalAdd<DdType::Sylvan, ValueType>::forEach(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::function<void (uint64_t const&, ValueType const&)> const& function) const {
+            forEachRec(this->getSylvanMtbdd().GetMTBDD(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, function);
+        }
+        
+        template<typename ValueType>
+        void InternalAdd<DdType::Sylvan, ValueType>::forEachRec(MTBDD dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::function<void (uint64_t const&, ValueType const&)> const& function) const {
             // For the empty DD, we do not need to add any entries.
             if (mtbdd_isleaf(dd) && mtbdd_iszero(dd)) {
                 return;
@@ -901,24 +909,19 @@ namespace storm {
             
             // If we are at the maximal level, the value to be set is stored as a constant in the DD.
             if (currentLevel == maxLevel) {
-                ValueType& targetValue = targetVector[offsets != nullptr ? (*offsets)[currentOffset] : currentOffset];
-                targetValue = function(targetValue, getValue(dd));
+                function(currentOffset, getValue(dd));
             } else if (mtbdd_isleaf(dd) || ddVariableIndices[currentLevel] < mtbdd_getvar(dd)) {
                 // If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set
                 // and for the one in which it is not set.
-                composeWithExplicitVectorRec(dd, negated, offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function);
-                composeWithExplicitVectorRec(dd, negated, offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function);
+                forEachRec(dd, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, function);
+                forEachRec(dd, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, function);
             } else {
                 // Otherwise, we simply recursively call the function for both (different) cases.
                 MTBDD thenNode = mtbdd_gethigh(dd);
                 MTBDD elseNode = mtbdd_getlow(dd);
                 
-                // Determine whether we have to evaluate the successors as if they were complemented.
-                bool elseComplemented = mtbdd_hascomp(elseNode) ^ negated;
-                bool thenComplemented = mtbdd_hascomp(thenNode) ^ negated;
-                
-                composeWithExplicitVectorRec(mtbdd_regular(elseNode), elseComplemented, offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function);
-                composeWithExplicitVectorRec(mtbdd_regular(thenNode), thenComplemented, offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function);
+                forEachRec(elseNode, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, function);
+                forEachRec(thenNode, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, function);
             }
         }
         

src/storm/storage/dd/sylvan/InternalSylvanAdd.h

@@ -553,6 +553,18 @@ namespace storm {
              */
             void composeWithExplicitVector(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<uint_fast64_t> const& offsets, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const;
             
+            /*!
+             * Composes the ADD with an explicit vector by performing a specified function between the entries of this
+             * ADD and the explicit vector.
+             *
+             * @param odd The ODD to use for the translation from symbolic to explicit positions.
+             * @param ddVariableIndices The indices of the DD variables present in this ADD.
+             * @param targetVector The explicit vector that is to be composed with the ADD. The results are written to
+             * this vector again.
+             * @param function The function to perform in the composition.
+             */
+            void forEach(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::function<void (uint64_t const&, ValueType const&)> const& function) const;
+            
             /*!
              * Splits the ADD into several ADDs that differ in the encoding of the given group variables (given via indices).
              *
@@ -647,19 +659,18 @@ namespace storm {
             static std::shared_ptr<Odd> createOddRec(BDD dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<BDD, std::shared_ptr<Odd>>>& uniqueTableForLevels);
             
             /*!
-             * Performs a recursive step to perform the given function between the given DD-based vector and the given
-             * explicit vector.
+             * Performs a recursive step for forEach.
              *
-             * @param dd The DD to add to the explicit vector.
-             * @param negated A flag indicating whether the DD node is to be interpreted as being negated.
+             * @param dd The DD to traverse.
              * @param currentLevel The currently considered level in the DD.
              * @param maxLevel The number of levels that need to be considered.
              * @param currentOffset The current offset.
              * @param odd The ODD used for the translation.
              * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered.
-             * @param targetVector The vector to which the translated DD-based vector is to be added.
+             * @param function The callback invoked for every element. The first argument is the offset and the second
+             * is the value.
              */
-            void composeWithExplicitVectorRec(MTBDD dd, bool negated, std::vector<uint_fast64_t> const* offsets, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const;
+            void forEachRec(MTBDD dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::function<void (uint64_t const&, ValueType const&)> const& function) const;
             
             /*!
              * Splits the given matrix DD into the labelings of the gropus using the given group variables.

src/storm/utility/graph.cpp

@@ -1084,7 +1084,7 @@ namespace storm {
             }
 
             template <storm::dd::DdType Type, typename ValueType>
-            GameProb01Result<Type> performProb0(storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy) {
+            SymbolicGameProb01Result<Type> performProb0(storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy) {
 
                 // The solution sets.
                 storm::dd::Bdd<Type> player1States = psiStates;
@@ -1147,11 +1147,11 @@ namespace storm {
                     player1StrategyBdd = onlyProb0Successors.existsAbstractRepresentative(model.getPlayer1Variables());
                 }
                 
-                return GameProb01Result<Type>(player1States, player2States, player1StrategyBdd, player2StrategyBdd);
+                return SymbolicGameProb01Result<Type>(player1States, player2States, player1StrategyBdd, player2StrategyBdd);
             }
             
             template <storm::dd::DdType Type, typename ValueType>
-            GameProb01Result<Type> performProb1(storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional<storm::dd::Bdd<Type>> const& player1Candidates) {
+            SymbolicGameProb01Result<Type> performProb1(storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional<storm::dd::Bdd<Type>> const& player1Candidates) {
                 
                 // Create the potential prob1 states of player 1.
                 storm::dd::Bdd<Type> maybePlayer1States = model.getReachableStates();
@@ -1284,7 +1284,7 @@ namespace storm {
                     }
                 }
                 
-                return GameProb01Result<Type>(maybePlayer1States, maybePlayer2States, player1StrategyBdd, player2StrategyBdd);
+                return SymbolicGameProb01Result<Type>(maybePlayer1States, maybePlayer2States, player1StrategyBdd, player2StrategyBdd);
             }
             
             template <typename T>
@@ -1568,9 +1568,9 @@ namespace storm {
 
             template std::pair<storm::dd::Bdd<storm::dd::DdType::CUDD>, storm::dd::Bdd<storm::dd::DdType::CUDD>> performProb01Min(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::CUDD, double> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates);
 
-            template GameProb01Result<storm::dd::DdType::CUDD> performProb0(storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD, double> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy);
+            template SymbolicGameProb01Result<storm::dd::DdType::CUDD> performProb0(storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD, double> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy);
             
-            template GameProb01Result<storm::dd::DdType::CUDD> performProb1(storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD, double> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional<storm::dd::Bdd<storm::dd::DdType::CUDD>> const& player1Candidates);
+            template SymbolicGameProb01Result<storm::dd::DdType::CUDD> performProb1(storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD, double> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional<storm::dd::Bdd<storm::dd::DdType::CUDD>> const& player1Candidates);
 
             // Instantiations for Sylvan (double).
             
@@ -1608,9 +1608,9 @@ namespace storm {
 
             template std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, storm::dd::Bdd<storm::dd::DdType::Sylvan>> performProb01Min(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
 
-            template GameProb01Result<storm::dd::DdType::Sylvan> performProb0(storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::Sylvan> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy);
+            template SymbolicGameProb01Result<storm::dd::DdType::Sylvan> performProb0(storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::Sylvan> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy);
 
-            template GameProb01Result<storm::dd::DdType::Sylvan> performProb1(storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::Sylvan> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional<storm::dd::Bdd<storm::dd::DdType::Sylvan>> const& player1Candidates);
+            template SymbolicGameProb01Result<storm::dd::DdType::Sylvan> performProb1(storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::Sylvan> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional<storm::dd::Bdd<storm::dd::DdType::Sylvan>> const& player1Candidates);
 
             // Instantiations for Sylvan (rational number).
             

src/storm/utility/graph.h

@@ -10,7 +10,9 @@
 #include "storm/storage/Scheduler.h"
 #include "storm/models/sparse/NondeterministicModel.h"
 #include "storm/models/sparse/DeterministicModel.h"
+
 #include "storm/storage/dd/DdType.h"
+#include "storm/storage/dd/Bdd.h"
 
 #include "storm/solver/OptimizationDirection.h"
 
@@ -542,9 +544,9 @@ namespace storm {
             std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> performProb01Min(storm::models::symbolic::NondeterministicModel<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates);
 
             template <storm::dd::DdType Type>
-            struct GameProb01Result {
-                GameProb01Result() = default;
-                GameProb01Result(storm::dd::Bdd<Type> const& player1States, storm::dd::Bdd<Type> const& player2States, boost::optional<storm::dd::Bdd<Type>> const& player1Strategy = boost::none, boost::optional<storm::dd::Bdd<Type>> const& player2Strategy = boost::none) : player1States(player1States), player2States(player2States), player1Strategy(player1Strategy), player2Strategy(player2Strategy) {
+            struct SymbolicGameProb01Result {
+                SymbolicGameProb01Result() = default;
+                SymbolicGameProb01Result(storm::dd::Bdd<Type> const& player1States, storm::dd::Bdd<Type> const& player2States, boost::optional<storm::dd::Bdd<Type>> const& player1Strategy = boost::none, boost::optional<storm::dd::Bdd<Type>> const& player2Strategy = boost::none) : player1States(player1States), player2States(player2States), player1Strategy(player1Strategy), player2Strategy(player2Strategy) {
                     // Intentionally left empty.
                 }
                 
@@ -597,7 +599,7 @@ namespace storm {
              * @param producePlayer2Strategy A flag indicating whether the strategy of player 2 shall be produced.
              */
             template <storm::dd::DdType Type, typename ValueType>
-            GameProb01Result<Type> performProb0(storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false);
+            SymbolicGameProb01Result<Type> performProb0(storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false);
             
             /*!
              * Computes the set of states that have probability 1 given the strategies of the two players.
@@ -611,7 +613,7 @@ namespace storm {
              * @param player1Candidates If given, this set constrains the candidates of player 1 states that are considered.
              */
             template <storm::dd::DdType Type, typename ValueType>
-            GameProb01Result<Type> performProb1(storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false, boost::optional<storm::dd::Bdd<Type>> const& player1Candidates = boost::none);
+            SymbolicGameProb01Result<Type> performProb1(storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false, boost::optional<storm::dd::Bdd<Type>> const& player1Candidates = boost::none);
             
             /*!
              * Performs a topological sort of the states of the system according to the given transitions.

src/test/storm/utility/GraphTest.cpp

@@ -227,7 +227,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) {
     // The target states are those states where !(s < 3).
     storm::dd::Bdd<storm::dd::DdType::CUDD> targetStates = !abstractor.getStates(initialPredicates[0]) && game.getReachableStates();
     
-    storm::utility::graph::GameProb01Result<storm::dd::DdType::CUDD> result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true);
+    storm::utility::graph::SymbolicGameProb01Result<storm::dd::DdType::CUDD> result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true);
     EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount());
     EXPECT_TRUE(result.hasPlayer1Strategy());
     EXPECT_TRUE(result.hasPlayer2Strategy());
@@ -366,7 +366,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) {
     // The target states are those states where s1 == 7 & s2 == 7 & d1 + d2 == 2.
     storm::dd::Bdd<storm::dd::DdType::CUDD> targetStates = abstractor.getStates(initialPredicates[7]) && abstractor.getStates(initialPredicates[22]) && abstractor.getStates(initialPredicates[9]) && abstractor.getStates(initialPredicates[24]) && game.getReachableStates();
     
-    storm::utility::graph::GameProb01Result<storm::dd::DdType::CUDD> result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true);
+    storm::utility::graph::SymbolicGameProb01Result<storm::dd::DdType::CUDD> result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true);
     EXPECT_EQ(153ull, result.getPlayer1States().getNonZeroCount());
     ASSERT_TRUE(result.hasPlayer1Strategy());
     ASSERT_TRUE(result.hasPlayer2Strategy());
@@ -538,7 +538,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameWlan) {
     // The target states are those states where col == 2.
     storm::dd::Bdd<storm::dd::DdType::CUDD> targetStates = abstractor.getStates(initialPredicates[2]) && game.getReachableStates();
     
-    storm::utility::graph::GameProb01Result<storm::dd::DdType::CUDD> result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true);
+    storm::utility::graph::SymbolicGameProb01Result<storm::dd::DdType::CUDD> result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true);
     EXPECT_EQ(2831ull, result.getPlayer1States().getNonZeroCount());
     EXPECT_TRUE(result.hasPlayer1Strategy());
     EXPECT_TRUE(result.hasPlayer2Strategy());