first version of symbolic bisimulation minimization

resources/3rdparty/CMakeLists.txt

@@ -383,6 +383,7 @@ ExternalProject_Add(
         LOG_CONFIGURE ON
         LOG_BUILD ON
         BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/sylvan/src/libsylvan${STATIC_EXT}
+        BUILD_ALWAYS
 )
 ExternalProject_Get_Property(sylvan source_dir)
 ExternalProject_Get_Property(sylvan binary_dir)

resources/3rdparty/sylvan/src/storm_wrapper.cpp

@@ -18,6 +18,8 @@
 
 #if defined(STORM_HAVE_GMP) && !defined(STORM_USE_CLN_EA)
 #define RATIONAL_NUMBER_THREAD_SAFE
+#else
+#warning "Rational numbers do not appear to be thread-safe. Use in sylvan will be protected by mutexes, performance might degrade."
 #endif
 
 // A mutex that is used to lock all operations accessing rational numbers as they are not necessarily thread-safe.

resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c

@@ -676,7 +676,7 @@ TASK_4(MTBDD, sylvan_storm_rational_function_equal_norm_d2, MTBDD, a, MTBDD, b,
     
     /* Check cache */
     MTBDD result;
-    if (cache_get3(CACHE_MTBDD_EQUAL_NORM_RF, a, b, svalue, &result)) {
+    if (cache_get3(CACHE_MTBDD_EQUAL_NORM_RF, a, b, (uint64_t)svalue, &result)) {
         sylvan_stats_count(MTBDD_EQUAL_NORM_CACHED);
         return result;
     }
@@ -700,7 +700,7 @@ TASK_4(MTBDD, sylvan_storm_rational_function_equal_norm_d2, MTBDD, a, MTBDD, b,
     if (result == mtbdd_false) *shortcircuit = 1;
     
     /* Store in cache */
-    if (cache_put3(CACHE_MTBDD_EQUAL_NORM_RF, a, b, svalue, result)) {
+    if (cache_put3(CACHE_MTBDD_EQUAL_NORM_RF, a, b, (uint64_t)svalue, result)) {
         sylvan_stats_count(MTBDD_EQUAL_NORM_CACHEDPUT);
     }
     
@@ -749,7 +749,7 @@ TASK_4(MTBDD, sylvan_storm_rational_function_equal_norm_rel_d2, MTBDD, a, MTBDD,
     
     /* Check cache */
     MTBDD result;
-    if (cache_get3(CACHE_MTBDD_EQUAL_NORM_REL_RF, a, b, svalue, &result)) {
+    if (cache_get3(CACHE_MTBDD_EQUAL_NORM_REL_RF, a, b, (uint64_t)svalue, &result)) {
         sylvan_stats_count(MTBDD_EQUAL_NORM_REL_CACHED);
         return result;
     }
@@ -773,7 +773,7 @@ TASK_4(MTBDD, sylvan_storm_rational_function_equal_norm_rel_d2, MTBDD, a, MTBDD,
     if (result == mtbdd_false) *shortcircuit = 1;
     
     /* Store in cache */
-    if (cache_put3(CACHE_MTBDD_EQUAL_NORM_REL_RF, a, b, svalue, result)) {
+    if (cache_put3(CACHE_MTBDD_EQUAL_NORM_REL_RF, a, b, (uint64_t)svalue, result)) {
         sylvan_stats_count(MTBDD_EQUAL_NORM_REL_CACHEDPUT);
     }
     

resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c

@@ -710,7 +710,7 @@ TASK_4(MTBDD, sylvan_storm_rational_number_equal_norm_d2, MTBDD, a, MTBDD, b, st
     
     /* Check cache */
     MTBDD result;
-    if (cache_get3(CACHE_MTBDD_EQUAL_NORM_RN, a, b, svalue, &result)) {
+    if (cache_get3(CACHE_MTBDD_EQUAL_NORM_RN, a, b, (uint64_t)svalue, &result)) {
         sylvan_stats_count(MTBDD_EQUAL_NORM_CACHED);
         return result;
     }
@@ -734,7 +734,7 @@ TASK_4(MTBDD, sylvan_storm_rational_number_equal_norm_d2, MTBDD, a, MTBDD, b, st
     if (result == mtbdd_false) *shortcircuit = 1;
     
     /* Store in cache */
-    if (cache_put3(CACHE_MTBDD_EQUAL_NORM_RN, a, b, svalue, result)) {
+    if (cache_put3(CACHE_MTBDD_EQUAL_NORM_RN, a, b, (uint64_t)svalue, result)) {
         sylvan_stats_count(MTBDD_EQUAL_NORM_CACHEDPUT);
     }
     
@@ -783,7 +783,7 @@ TASK_4(MTBDD, sylvan_storm_rational_number_equal_norm_rel_d2, MTBDD, a, MTBDD, b
     
     /* Check cache */
     MTBDD result;
-    if (cache_get3(CACHE_MTBDD_EQUAL_NORM_REL_RN, a, b, svalue, &result)) {
+    if (cache_get3(CACHE_MTBDD_EQUAL_NORM_REL_RN, a, b, (uint64_t)svalue, &result)) {
         sylvan_stats_count(MTBDD_EQUAL_NORM_REL_CACHED);
         return result;
     }
@@ -807,7 +807,7 @@ TASK_4(MTBDD, sylvan_storm_rational_number_equal_norm_rel_d2, MTBDD, a, MTBDD, b
     if (result == mtbdd_false) *shortcircuit = 1;
     
     /* Store in cache */
-    if (cache_put3(CACHE_MTBDD_EQUAL_NORM_REL_RN, a, b, svalue, result)) {
+    if (cache_put3(CACHE_MTBDD_EQUAL_NORM_REL_RN, a, b, (uint64_t)svalue, result)) {
         sylvan_stats_count(MTBDD_EQUAL_NORM_REL_CACHEDPUT);
     }
     

resources/examples/testfiles/dtmc/die.pm

@@ -24,9 +24,3 @@ rewards "coin_flips"
 endrewards
 
 label "one" = s=7&d=1;
-label "two" = s=7&d=2;
-label "three" = s=7&d=3;
-label "four" = s=7&d=4;
-label "five" = s=7&d=5;
-label "six" = s=7&d=6;
-label "done" = s=7;

src/storm/models/symbolic/Model.cpp

@@ -50,12 +50,7 @@ namespace storm {
             }
             
             template<storm::dd::DdType Type, typename ValueType>
-            storm::dd::DdManager<Type> const& Model<Type, ValueType>::getManager() const {
-                return *manager;
-            }
-            
-            template<storm::dd::DdType Type, typename ValueType>
-            storm::dd::DdManager<Type>& Model<Type, ValueType>::getManager() {
+            storm::dd::DdManager<Type>& Model<Type, ValueType>::getManager() const {
                 return *manager;
             }
                         
@@ -85,6 +80,12 @@ namespace storm {
                 return this->getStates(labelToExpressionMap.at(label));
             }
             
+            template<storm::dd::DdType Type, typename ValueType>
+            storm::expressions::Expression Model<Type, ValueType>::getExpression(std::string const& label) const {
+                STORM_LOG_THROW(labelToExpressionMap.find(label) != labelToExpressionMap.end(), storm::exceptions::IllegalArgumentException, "The label " << label << " is invalid for the labeling of the model.");
+                return labelToExpressionMap.at(label);
+            }
+            
             template<storm::dd::DdType Type, typename ValueType>
             storm::dd::Bdd<Type> Model<Type, ValueType>::getStates(storm::expressions::Expression const& expression) const {
                 if (expression.isTrue()) {

src/storm/models/symbolic/Model.h

@@ -9,6 +9,7 @@
 #include "storm/storage/expressions/Expression.h"
 #include "storm/storage/expressions/Variable.h"
 #include "storm/storage/dd/DdType.h"
+#include "storm/storage/dd/Bdd.h"
 #include "storm/models/ModelBase.h"
 #include "storm/utility/OsDetection.h"
 
@@ -24,9 +25,6 @@ namespace storm {
         template<storm::dd::DdType Type, typename ValueType>
         class Add;
         
-        template<storm::dd::DdType Type>
-        class Bdd;
-        
         template<storm::dd::DdType Type>
         class DdManager;
         
@@ -104,14 +102,7 @@ namespace storm {
                  *
                  * @return The manager responsible for the DDs that represent this model.
                  */
-                storm::dd::DdManager<Type> const& getManager() const;
-
-                /*!
-                 * Retrieves the manager responsible for the DDs that represent this model.
-                 *
-                 * @return The manager responsible for the DDs that represent this model.
-                 */
-                storm::dd::DdManager<Type>& getManager();
+                storm::dd::DdManager<Type>& getManager() const;
 
                 /*!
                  * Retrieves the manager responsible for the DDs that represent this model.
@@ -143,10 +134,18 @@ namespace storm {
                  * Returns the sets of states labeled with the given label.
                  *
                  * @param label The label for which to get the labeled states.
-                 * @return The set of states labeled with the requested label in the form of a bit vector.
+                 * @return The set of states labeled with the requested label.
                  */
                 virtual storm::dd::Bdd<Type> getStates(std::string const& label) const;
                 
+                /*!
+                 * Returns the expression for the given label.
+                 *
+                 * @param label The label for which to get the expression.
+                 * @return The expression characterizing the requested label.
+                 */
+                virtual storm::expressions::Expression getExpression(std::string const& label) const;
+                
                 /*!
                  * Returns the set of states labeled satisfying the given expression (that must be of boolean type).
                  *

src/storm/storage/dd/Add.cpp

@@ -812,6 +812,16 @@ namespace storm {
             return internalAdd.createOdd(this->getSortedVariableIndices());
         }
         
+        template<DdType LibraryType, typename ValueType>
+        InternalAdd<LibraryType, ValueType> const& Add<LibraryType, ValueType>::getInternalAdd() const {
+            return internalAdd;
+        }
+        
+        template<DdType LibraryType, typename ValueType>
+        InternalDdManager<LibraryType> const& Add<LibraryType, ValueType>::getInternalDdManager() const {
+            return internalAdd.getInternalDdManager();
+        }
+
         template<DdType LibraryType, typename ValueType>
         Add<LibraryType, ValueType>::operator InternalAdd<LibraryType, ValueType>() const {
             return internalAdd;

src/storm/storage/dd/Add.h

@@ -25,6 +25,11 @@ namespace storm {
         template<DdType LibraryType, typename ValueType>
         class AddIterator;
         
+        namespace bisimulation {
+            template<DdType LibraryType, typename ValueType>
+            class InternalSignatureRefiner;
+        }
+        
         template<DdType LibraryType, typename ValueType = double>
         class Add : public Dd<LibraryType> {
         public:
@@ -34,6 +39,8 @@ namespace storm {
             template<DdType LibraryTypePrime, typename ValueTypePrime>
             friend class Add;
 
+            friend class bisimulation::InternalSignatureRefiner<LibraryType, ValueType>;
+
             // Instantiate all copy/move constructors/assignments with the default implementation.
             Add() = default;
             Add(Add<LibraryType, ValueType> const& other) = default;
@@ -625,6 +632,16 @@ namespace storm {
              */
             Odd createOdd() const;
 
+            /*!
+             * Retrieves the internal ADD.
+             */
+            InternalAdd<LibraryType, ValueType> const& getInternalAdd() const;
+
+            /*!
+             * Retrieves the internal ADD.
+             */
+            InternalDdManager<LibraryType> const& getInternalDdManager() const;
+
         private:
             /*!
              * Creates an ADD from the given internal ADD.

src/storm/storage/dd/DdMetaVariable.cpp

@@ -49,6 +49,21 @@ namespace storm {
             return this->cube;
         }
         
+        template<DdType LibraryType>
+        uint64_t DdMetaVariable<LibraryType>::getHighestLevel() const {
+            uint64_t result = 0;
+            bool first = true;
+            for (auto const& v : ddVariables) {
+                if (first) {
+                    result = v.getLevel();
+                } else {
+                    result = std::max(result, v.getLevel());
+                }
+            }
+            
+            return result;
+        }
+        
         template<DdType LibraryType>
         void DdMetaVariable<LibraryType>::createCube() {
             STORM_LOG_ASSERT(!this->ddVariables.empty(), "The DD variables must not be empty.");

src/storm/storage/dd/DdMetaVariable.h

@@ -73,6 +73,11 @@ namespace storm {
              */
             Bdd<LibraryType> const& getCube() const;
             
+            /*!
+             * Retrieves the highest level of all DD variables belonging to this meta variable.
+             */
+            uint64_t getHighestLevel() const;
+            
         private:
             /*!
              * Creates an integer meta variable with the given name and range bounds.

src/storm/storage/dd/bisimulation/Partition.cpp

@@ -0,0 +1,123 @@
+#include "storm/storage/dd/bisimulation/Partition.h"
+
+#include "storm/storage/dd/DdManager.h"
+
+namespace storm {
+    namespace dd {
+        namespace bisimulation {
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            Partition<DdType, ValueType>::Partition(storm::dd::Add<DdType, ValueType> const& partitionAdd, storm::expressions::Variable const& blockVariable, uint64_t nextFreeBlockIndex) : partitionAdd(partitionAdd), blockVariable(blockVariable), nextFreeBlockIndex(nextFreeBlockIndex) {
+                // Intentionally left empty.
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            bool Partition<DdType, ValueType>::operator==(Partition<DdType, ValueType> const& other) {
+                return this->partitionAdd == other.partitionAdd && this->blockVariable == other.blockVariable && this->nextFreeBlockIndex == other.nextFreeBlockIndex;
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            Partition<DdType, ValueType> Partition<DdType, ValueType>::replacePartitionAdd(storm::dd::Add<DdType, ValueType> const& newPartitionAdd, uint64_t nextFreeBlockIndex) const {
+                return Partition<DdType, ValueType>(newPartitionAdd, blockVariable, nextFreeBlockIndex);
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            Partition<DdType, ValueType> Partition<DdType, ValueType>::create(storm::models::symbolic::Model<DdType, ValueType> const& model) {
+                return create(model, model.getLabels());
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            Partition<DdType, ValueType> Partition<DdType, ValueType>::create(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::string> const& labels) {
+                std::vector<storm::expressions::Expression> expressions;
+                for (auto const& label : labels) {
+                    expressions.push_back(model.getExpression(label));
+                }
+                return create(model, expressions);
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            Partition<DdType, ValueType> Partition<DdType, ValueType>::create(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<storm::expressions::Expression> const& expressions) {
+                storm::dd::DdManager<DdType>& manager = model.getManager();
+                
+                std::vector<storm::dd::Bdd<DdType>> stateSets;
+                for (auto const& expression : expressions) {
+                    stateSets.emplace_back(model.getStates(expression));
+                }
+                
+                storm::expressions::Variable blockVariable = createBlockVariable(manager, model.getReachableStates().getNonZeroCount());
+                std::pair<storm::dd::Add<DdType, ValueType>, uint64_t> partitionAddAndBlockCount = createPartitionAdd(manager, model, stateSets, blockVariable);
+                return Partition<DdType, ValueType>(partitionAddAndBlockCount.first, blockVariable, partitionAddAndBlockCount.second);
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            uint64_t Partition<DdType, ValueType>::getNumberOfBlocks() const {
+                return nextFreeBlockIndex;
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            storm::dd::Add<DdType, ValueType> const& Partition<DdType, ValueType>::getPartitionAdd() const {
+                return partitionAdd;
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            storm::expressions::Variable const& Partition<DdType, ValueType>::getBlockVariable() const {
+                return blockVariable;
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            uint64_t Partition<DdType, ValueType>::getNextFreeBlockIndex() const {
+                return nextFreeBlockIndex;
+            }
+            
+            template<storm::dd::DdType DdType>
+            void enumerateBlocksRec(std::vector<storm::dd::Bdd<DdType>> const& stateSets, storm::dd::Bdd<DdType> const& currentStateSet, uint64_t offset, storm::expressions::Variable const& blockVariable, std::function<void (storm::dd::Bdd<DdType> const&)> const& callback) {
+                if (currentStateSet.isZero()) {
+                    return;
+                }
+                if (offset == stateSets.size()) {
+                    callback(currentStateSet);
+                } else {
+                    enumerateBlocksRec(stateSets, currentStateSet && stateSets[offset], offset + 1, blockVariable, callback);
+                    enumerateBlocksRec(stateSets, currentStateSet && !stateSets[offset], offset + 1, blockVariable, callback);
+                }
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            std::pair<storm::dd::Add<DdType, ValueType>, uint64_t> Partition<DdType, ValueType>::createPartitionAdd(storm::dd::DdManager<DdType> const& manager, storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<storm::dd::Bdd<DdType>> const& stateSets, storm::expressions::Variable const& blockVariable) {
+                uint64_t blockCount = 0;
+                storm::dd::Add<DdType, ValueType> partitionAdd = manager.template getAddZero<ValueType>();
+                
+                // Enumerate all realizable blocks.
+                enumerateBlocksRec<DdType>(stateSets, model.getReachableStates(), 0, blockVariable, [&manager, &partitionAdd, &blockVariable, &blockCount](storm::dd::Bdd<DdType> const& stateSet) {
+                    stateSet.template toAdd<ValueType>().exportToDot("states_" + std::to_string(blockCount) + ".dot");
+                    partitionAdd += (stateSet && manager.getEncoding(blockVariable, blockCount)).template toAdd<ValueType>();
+                    blockCount++;
+                } );
+                
+                return std::make_pair(partitionAdd, blockCount);
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            storm::expressions::Variable Partition<DdType, ValueType>::createBlockVariable(storm::dd::DdManager<DdType>& manager, uint64_t numberOfStates) {
+                storm::expressions::Variable blockVariable;
+                if (manager.hasMetaVariable("blocks")) {
+                    int64_t counter = 0;
+                    while (manager.hasMetaVariable("block" + std::to_string(counter))) {
+                        ++counter;
+                    }
+                    blockVariable = manager.addMetaVariable("blocks" + std::to_string(counter), 0, numberOfStates, 1).front();
+                } else {
+                    blockVariable = manager.addMetaVariable("blocks", 0, numberOfStates, 1).front();
+                }
+                return blockVariable;
+            }
+            
+            template class Partition<storm::dd::DdType::CUDD, double>;
+
+            template class Partition<storm::dd::DdType::Sylvan, double>;
+            template class Partition<storm::dd::DdType::Sylvan, storm::RationalNumber>;
+            template class Partition<storm::dd::DdType::Sylvan, storm::RationalFunction>;
+
+        }
+    }
+}

src/storm/storage/dd/bisimulation/Partition.h

@@ -0,0 +1,73 @@
+#pragma once
+
+#include "storm/storage/dd/DdType.h"
+#include "storm/storage/dd/Add.h"
+
+#include "storm/models/symbolic/Model.h"
+
+namespace storm {
+    namespace dd {
+        namespace bisimulation {
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            class Partition {
+            public:
+                Partition() = default;
+                
+                /*!
+                 * Creates a new partition from the given data.
+                 *
+                 * @param partitionAdd An ADD that maps encoding over the state/row variables and the block variable to
+                 * one iff the state is in the block.
+                 * @param blockVariable The variable to use for the block encoding. Its range must be [0, x] where x is
+                 * the number of states in the partition.
+                 * @param nextFreeBlockIndex The next free block index. The existing blocks must be encoded with indices
+                 * between 0 and this number.
+                 */
+                Partition(storm::dd::Add<DdType, ValueType> const& partitionAdd, storm::expressions::Variable const& blockVariable, uint64_t nextFreeBlockIndex);
+                
+                bool operator==(Partition<DdType, ValueType> const& other);
+                
+                Partition<DdType, ValueType> replacePartitionAdd(storm::dd::Add<DdType, ValueType> const& newPartitionAdd, uint64_t nextFreeBlockIndex) const;
+                
+                /*!
+                 * Creates a partition from the given model that respects all labels.
+                 */
+                static Partition create(storm::models::symbolic::Model<DdType, ValueType> const& model);
+
+                /*!
+                 * Creates a partition from the given model that respects the given labels.
+                 */
+                static Partition create(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::string> const& labels);
+
+                /*!
+                 * Creates a partition from the given model that respects the given expressions.
+                 */
+                static Partition create(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<storm::expressions::Expression> const& expressions);
+
+                uint64_t getNumberOfBlocks() const;
+                
+                storm::dd::Add<DdType, ValueType> const& getPartitionAdd() const;
+                
+                storm::expressions::Variable const& getBlockVariable() const;
+                
+                uint64_t getNextFreeBlockIndex() const;
+                
+            private:
+                static std::pair<storm::dd::Add<DdType, ValueType>, uint64_t> createPartitionAdd(storm::dd::DdManager<DdType> const& manager, storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<storm::dd::Bdd<DdType>> const& stateSets, storm::expressions::Variable const& blockVariable);
+                
+                static storm::expressions::Variable createBlockVariable(storm::dd::DdManager<DdType>& manager, uint64_t numberOfStates);
+                
+                // The ADD representing the partition. The ADD is over the row variables of the model and the block variable.
+                storm::dd::Add<DdType, ValueType> partitionAdd;
+                
+                // The meta variable used to encode the block of each state in this partition.
+                storm::expressions::Variable blockVariable;
+                
+                // The next free block index.
+                uint64_t nextFreeBlockIndex;
+            };
+            
+        }
+    }
+}

src/storm/storage/dd/bisimulation/Signature.cpp

@@ -0,0 +1,25 @@
+#include "storm/storage/dd/bisimulation/Signature.h"
+
+namespace storm {
+    namespace dd {
+        namespace bisimulation {
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            Signature<DdType, ValueType>::Signature(storm::dd::Add<DdType, ValueType> const& signatureAdd) : signatureAdd(signatureAdd) {
+                // Intentionally left empty.
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            storm::dd::Add<DdType, ValueType> const& Signature<DdType, ValueType>::getSignatureAdd() const {
+                return signatureAdd;
+            }
+            
+            template class Signature<storm::dd::DdType::CUDD, double>;
+            
+            template class Signature<storm::dd::DdType::Sylvan, double>;
+            template class Signature<storm::dd::DdType::Sylvan, storm::RationalNumber>;
+            template class Signature<storm::dd::DdType::Sylvan, storm::RationalFunction>;
+
+        }
+    }
+}

src/storm/storage/dd/bisimulation/Signature.h

@@ -0,0 +1,24 @@
+#pragma once
+
+#include "storm/storage/dd/DdType.h"
+
+#include "storm/storage/dd/bisimulation/Partition.h"
+
+namespace storm {
+    namespace dd {
+        namespace bisimulation {
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            class Signature {
+            public:
+                Signature(storm::dd::Add<DdType, ValueType> const& signatureAdd);
+                
+                storm::dd::Add<DdType, ValueType> const& getSignatureAdd() const;
+                
+            private:
+                storm::dd::Add<DdType, ValueType> signatureAdd;
+            };
+            
+        }
+    }
+}

src/storm/storage/dd/bisimulation/SignatureRefiner.cpp

@@ -0,0 +1,329 @@
+#include "storm/storage/dd/bisimulation/SignatureRefiner.h"
+
+#include <unordered_map>
+
+#include "storm/storage/dd/DdManager.h"
+
+#include "storm/storage/dd/cudd/InternalCuddDdManager.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/NotImplementedException.h"
+
+#include "resources/3rdparty/sparsepp/sparsepp.h"
+
+namespace storm {
+    namespace dd {
+        namespace bisimulation {
+            
+            struct CuddPointerPairHash {
+                std::size_t operator()(std::pair<DdNode const*, DdNode const*> const& pair) const {
+                    std::size_t seed = std::hash<DdNode const*>()(pair.first);
+                    boost::hash_combine(seed, pair.second);
+                    return seed;
+                }
+            };
+            
+            struct SylvanMTBDDPairHash {
+                std::size_t operator()(std::pair<MTBDD, MTBDD> const& pair) const {
+                    std::size_t seed = std::hash<MTBDD>()(pair.first);
+                    boost::hash_combine(seed, pair.second);
+                    return seed;
+                }
+            };
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            class InternalSignatureRefiner;
+            
+            template<typename ValueType>
+            class InternalSignatureRefiner<storm::dd::DdType::CUDD, ValueType> {
+            public:
+                InternalSignatureRefiner(storm::dd::DdManager<storm::dd::DdType::CUDD> const& manager, storm::expressions::Variable const& blockVariable, uint64_t lastStateLevel) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), lastStateLevel(lastStateLevel), nextFreeBlockIndex(0), numberOfRefinements(0) {
+                    // Intentionally left empty.
+                }
+                
+                Partition<storm::dd::DdType::CUDD, ValueType> refine(Partition<storm::dd::DdType::CUDD, ValueType> const& oldPartition, Signature<storm::dd::DdType::CUDD, ValueType> const& signature) {
+                    storm::dd::Add<storm::dd::DdType::CUDD, ValueType> newPartitionAdd = refine(oldPartition, signature.getSignatureAdd());
+                    ++numberOfRefinements;
+                    return oldPartition.replacePartitionAdd(newPartitionAdd, nextFreeBlockIndex);
+                }
+                
+            private:
+                storm::dd::Add<storm::dd::DdType::CUDD, ValueType> refine(Partition<storm::dd::DdType::CUDD, ValueType> const& oldPartition, storm::dd::Add<storm::dd::DdType::CUDD, ValueType> const& signatureAdd) {
+                    // Clear the caches.
+                    signatureCache.clear();
+                    reuseBlocksCache.clear();
+                    nextFreeBlockIndex = oldPartition.getNextFreeBlockIndex();
+                    
+                    // Perform the actual recursive refinement step.
+                    DdNodePtr result = refine(oldPartition.getPartitionAdd().getInternalAdd().getCuddDdNode(), signatureAdd.getInternalAdd().getCuddDdNode());
+
+                    // Construct resulting ADD from the obtained node and the meta information.
+                    storm::dd::InternalAdd<storm::dd::DdType::CUDD, ValueType> internalNewPartitionAdd(&internalDdManager, cudd::ADD(internalDdManager.getCuddManager(), result));
+                    storm::dd::Add<storm::dd::DdType::CUDD, ValueType> newPartitionAdd(oldPartition.getPartitionAdd().getDdManager(), internalNewPartitionAdd, oldPartition.getPartitionAdd().getContainedMetaVariables());
+                    
+                    return newPartitionAdd;
+                }
+                
+                DdNodePtr refine(DdNode* partitionNode, DdNode* signatureNode) {
+                    ::DdManager* ddman = internalDdManager.getCuddManager().getManager();
+                    
+                    // Check the cache whether we have seen the same node before.
+                    auto sigCacheIt = signatureCache.find(std::make_pair(signatureNode, partitionNode));
+                    if (sigCacheIt != signatureCache.end()) {
+                        // If so, we return the corresponding result.
+                        return sigCacheIt->second;
+                    }
+                    
+                    // Determine the levels in the DDs.
+                    uint64_t partitionVariable = Cudd_NodeReadIndex(partitionNode);
+                    uint64_t signatureVariable = Cudd_NodeReadIndex(signatureNode);
+                    uint64_t partitionLevel = Cudd_ReadPerm(ddman, partitionVariable);
+                    uint64_t signatureLevel = Cudd_ReadPerm(ddman, signatureVariable);
+                    uint64_t topLevel = std::min(partitionLevel, signatureLevel);
+                    uint64_t topVariable = topLevel == partitionLevel ? partitionVariable : signatureVariable;
+                    
+                    // Check whether the top variable is still within the state encoding.
+                    if (topLevel <= lastStateLevel) {
+                        // Determine subresults by recursive descent.
+                        DdNodePtr thenResult;
+                        DdNodePtr elseResult;
+                        if (partitionLevel < signatureLevel) {
+                            thenResult = refine(Cudd_T(partitionNode), signatureNode);
+                            Cudd_Ref(thenResult);
+                            elseResult = refine(Cudd_E(partitionNode), signatureNode);
+                            Cudd_Ref(elseResult);
+                        } else if (partitionLevel > signatureLevel) {
+                            thenResult = refine(partitionNode, Cudd_T(signatureNode));
+                            Cudd_Ref(thenResult);
+                            elseResult = refine(partitionNode, Cudd_E(signatureNode));
+                            Cudd_Ref(elseResult);
+                        } else {
+                            thenResult = refine(Cudd_T(partitionNode), Cudd_T(signatureNode));
+                            Cudd_Ref(thenResult);
+                            elseResult = refine(Cudd_E(partitionNode), Cudd_E(signatureNode));
+                            Cudd_Ref(elseResult);
+                        }
+                        
+                        if (thenResult == elseResult) {
+                            Cudd_Deref(thenResult);
+                            Cudd_Deref(elseResult);
+                            return thenResult;
+                        }
+                        
+                        // Get the node to connect the subresults.
+                        DdNode* var = Cudd_addIthVar(ddman, topVariable);
+                        Cudd_Ref(var);
+                        DdNode* result = Cudd_addIte(ddman, var, thenResult, elseResult);
+                        Cudd_Ref(result);
+                        Cudd_RecursiveDeref(ddman, var);
+                        Cudd_Deref(thenResult);
+                        Cudd_Deref(elseResult);
+                        
+                        // Store the result in the cache.
+                        signatureCache[std::make_pair(signatureNode, partitionNode)] = result;
+                        
+                        Cudd_Deref(result);
+                        return result;
+                    } else {
+                        
+                        // If we are not within the state encoding any more, we hit the signature itself.
+                        
+                        // If we arrived at the constant zero node, then this was an illegal state encoding (we require
+                        // all states to be non-deadlock).
+                        if (signatureNode == Cudd_ReadZero(ddman)) {
+                            return signatureNode;
+                        }
+                        
+                        // If this is the first time (in this traversal) that we encounter this signature, we check
+                        // whether we can assign the old block number to it.
+                        auto reuseCacheIt = reuseBlocksCache.find(partitionNode);
+                        if (reuseCacheIt == reuseBlocksCache.end()) {
+                            reuseBlocksCache.emplace(partitionNode, true);
+                            signatureCache[std::make_pair(signatureNode, partitionNode)] = partitionNode;
+                            return partitionNode;
+                        } else {
+                            DdNode* result;
+                            {
+                                storm::dd::Add<storm::dd::DdType::CUDD, ValueType> blockEncoding = manager.getEncoding(blockVariable, nextFreeBlockIndex).template toAdd<ValueType>();
+                                ++nextFreeBlockIndex;
+                                result = blockEncoding.getInternalAdd().getCuddDdNode();
+                                Cudd_Ref(result);
+                            }
+                            signatureCache[std::make_pair(signatureNode, partitionNode)] = result;
+                            Cudd_Deref(result);
+                            return result;
+                        }
+                    }
+                }
+                
+                storm::dd::DdManager<storm::dd::DdType::CUDD> const& manager;
+                storm::dd::InternalDdManager<storm::dd::DdType::CUDD> const& internalDdManager;
+                storm::expressions::Variable const& blockVariable;
+                
+                // The last level that belongs to the state encoding in the DDs.
+                uint64_t lastStateLevel;
+                
+                // The current number of blocks of the new partition.
+                uint64_t nextFreeBlockIndex;
+                
+                // The number of completed refinements.
+                uint64_t numberOfRefinements;
+                
+                // The cache used to identify states with identical signature.
+                spp::sparse_hash_map<std::pair<DdNode const*, DdNode const*>, DdNode*, CuddPointerPairHash> signatureCache;
+                
+                // The cache used to identify which old block numbers have already been reused.
+                spp::sparse_hash_map<DdNode const*, bool> reuseBlocksCache;
+            };
+            
+            
+            template<typename ValueType>
+            class InternalSignatureRefiner<storm::dd::DdType::Sylvan, ValueType> {
+            public:
+                InternalSignatureRefiner(storm::dd::DdManager<storm::dd::DdType::Sylvan> const& manager, storm::expressions::Variable const& blockVariable, uint64_t lastStateLevel) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), lastStateLevel(lastStateLevel), nextFreeBlockIndex(0), numberOfRefinements(0) {
+                    // Intentionally left empty.
+                }
+                
+                Partition<storm::dd::DdType::Sylvan, ValueType> refine(Partition<storm::dd::DdType::Sylvan, ValueType> const& oldPartition, Signature<storm::dd::DdType::Sylvan, ValueType> const& signature) {
+                    storm::dd::Add<storm::dd::DdType::Sylvan, ValueType> newPartitionAdd = refine(oldPartition, signature.getSignatureAdd());
+                    ++numberOfRefinements;
+                    return oldPartition.replacePartitionAdd(newPartitionAdd, nextFreeBlockIndex);
+                }
+                
+            private:
+                storm::dd::Add<storm::dd::DdType::Sylvan, ValueType> refine(Partition<storm::dd::DdType::Sylvan, ValueType> const& oldPartition, storm::dd::Add<storm::dd::DdType::Sylvan, ValueType> const& signatureAdd) {
+                    // Clear the caches.
+                    signatureCache.clear();
+                    reuseBlocksCache.clear();
+                    nextFreeBlockIndex = oldPartition.getNextFreeBlockIndex();
+                    
+                    // Perform the actual recursive refinement step.
+                    MTBDD result = refine(oldPartition.getPartitionAdd().getInternalAdd().getSylvanMtbdd().GetMTBDD(), signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD());
+                    
+                    // Construct resulting ADD from the obtained node and the meta information.
+                    storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType> internalNewPartitionAdd(&internalDdManager, sylvan::Mtbdd(result));
+                    storm::dd::Add<storm::dd::DdType::Sylvan, ValueType> newPartitionAdd(oldPartition.getPartitionAdd().getDdManager(), internalNewPartitionAdd, oldPartition.getPartitionAdd().getContainedMetaVariables());
+                    
+                    return newPartitionAdd;
+                }
+                
+                MTBDD refine(MTBDD partitionNode, MTBDD signatureNode) {
+                    LACE_ME;
+                    
+                    // Check the cache whether we have seen the same node before.
+                    auto sigCacheIt = signatureCache.find(std::make_pair(signatureNode, partitionNode));
+                    if (sigCacheIt != signatureCache.end()) {
+                        // If so, we return the corresponding result.
+                        return sigCacheIt->second;
+                    }
+
+                    // Determine levels in the DDs.
+                    BDDVAR signatureVariable = mtbdd_isleaf(signatureNode) ? 0xffffffff : sylvan_var(signatureNode);
+                    BDDVAR partitionVariable = sylvan_var(partitionNode);
+                    BDDVAR topVariable = std::min(signatureVariable, partitionVariable);
+
+                    // Check whether the top variable is still within the state encoding.
+                    if (topVariable <= lastStateLevel) {
+                        // Determine subresults by recursive descent.
+                        MTBDD thenResult;
+                        MTBDD elseResult;
+                        if (partitionVariable < signatureVariable) {
+                            thenResult = refine(sylvan_high(partitionNode), signatureNode);
+                            elseResult = refine(sylvan_low(partitionNode), signatureNode);
+                        } else if (partitionVariable > signatureVariable) {
+                            thenResult = refine(partitionNode, sylvan_high(signatureNode));
+                            elseResult = refine(partitionNode, sylvan_low(signatureNode));
+                        } else {
+                            thenResult = refine(sylvan_high(partitionNode), sylvan_high(signatureNode));
+                            elseResult = refine(sylvan_low(partitionNode), sylvan_low(signatureNode));
+                        }
+                        
+                        if (thenResult == elseResult) {
+                            return thenResult;
+                        }
+                        
+                        // Get the node to connect the subresults.
+                        MTBDD result = mtbdd_ite(sylvan_ithvar(topVariable), thenResult, elseResult);
+                        
+                        // Store the result in the cache.
+                        signatureCache[std::make_pair(signatureNode, partitionNode)] = result;
+                        
+                        return result;
+                    } else {
+                        
+                        // If we are not within the state encoding any more, we hit the signature itself.
+
+                        // If we arrived at the constant zero node, then this was an illegal state encoding (we require
+                        // all states to be non-deadlock).
+                        if (mtbdd_iszero(signatureNode)) {
+                            return signatureNode;
+                        }
+                        
+                        // If this is the first time (in this traversal) that we encounter this signature, we check
+                        // whether we can assign the old block number to it.
+                        auto reuseCacheIt = reuseBlocksCache.find(partitionNode);
+                        if (reuseCacheIt == reuseBlocksCache.end()) {
+                            reuseBlocksCache.emplace(partitionNode, true);
+                            signatureCache[std::make_pair(signatureNode, partitionNode)] = partitionNode;
+                            return partitionNode;
+                        } else {
+                            MTBDD result;
+                            {
+                                storm::dd::Add<storm::dd::DdType::Sylvan, ValueType> blockEncoding = manager.getEncoding(blockVariable, nextFreeBlockIndex).template toAdd<ValueType>();
+                                ++nextFreeBlockIndex;
+                                result = blockEncoding.getInternalAdd().getSylvanMtbdd().GetMTBDD();
+                            }
+                            signatureCache[std::make_pair(signatureNode, partitionNode)] = result;
+                            return result;
+                        }
+                    }
+                }
+                
+                storm::dd::DdManager<storm::dd::DdType::Sylvan> const& manager;
+                storm::dd::InternalDdManager<storm::dd::DdType::Sylvan> const& internalDdManager;
+                storm::expressions::Variable const& blockVariable;
+                
+                // The last level that belongs to the state encoding in the DDs.
+                uint64_t lastStateLevel;
+                
+                // The current number of blocks of the new partition.
+                uint64_t nextFreeBlockIndex;
+                
+                // The number of completed refinements.
+                uint64_t numberOfRefinements;
+                
+                // The cache used to identify states with identical signature.
+                spp::sparse_hash_map<std::pair<MTBDD, MTBDD>, MTBDD, SylvanMTBDDPairHash> signatureCache;
+                
+                // The cache used to identify which old block numbers have already been reused.
+                spp::sparse_hash_map<MTBDD, bool> reuseBlocksCache;
+            };
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            SignatureRefiner<DdType, ValueType>::SignatureRefiner(storm::dd::DdManager<DdType> const& manager, storm::expressions::Variable const& blockVariable, std::set<storm::expressions::Variable> const& stateVariables) : manager(manager), stateVariables(stateVariables) {
+                uint64_t lastStateLevel = 0;
+                for (auto const& stateVariable : stateVariables) {
+                    lastStateLevel = std::max(lastStateLevel, manager.getMetaVariable(stateVariable).getHighestLevel());
+                }
+                
+                internalRefiner = std::make_unique<InternalSignatureRefiner<DdType, ValueType>>(manager, blockVariable, lastStateLevel);
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            SignatureRefiner<DdType, ValueType>::~SignatureRefiner() = default;
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            Partition<DdType, ValueType> SignatureRefiner<DdType, ValueType>::refine(Partition<DdType, ValueType> const& oldPartition, Signature<DdType, ValueType> const& signature) {
+                return internalRefiner->refine(oldPartition, signature);
+            }
+            
+            template class SignatureRefiner<storm::dd::DdType::CUDD, double>;
+            
+            template class SignatureRefiner<storm::dd::DdType::Sylvan, double>;
+            template class SignatureRefiner<storm::dd::DdType::Sylvan, storm::RationalNumber>;
+            template class SignatureRefiner<storm::dd::DdType::Sylvan, storm::RationalFunction>;
+            
+            
+        }
+    }
+}

src/storm/storage/dd/bisimulation/SignatureRefiner.h

@@ -0,0 +1,37 @@
+#pragma once
+
+#include "storm/storage/dd/DdType.h"
+
+#include "storm/storage/dd/bisimulation/Partition.h"
+#include "storm/storage/dd/bisimulation/Signature.h"
+
+namespace storm {
+    namespace dd {
+        namespace bisimulation {
+
+            template<storm::dd::DdType DdType, typename ValueType>
+            class InternalSignatureRefiner;
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            class SignatureRefiner {
+            public:
+                SignatureRefiner(storm::dd::DdManager<DdType> const& manager, storm::expressions::Variable const& blockVariable, std::set<storm::expressions::Variable> const& stateVariables);
+                
+                ~SignatureRefiner();
+                
+                Partition<DdType, ValueType> refine(Partition<DdType, ValueType> const& oldPartition, Signature<DdType, ValueType> const& signature);
+
+            private:
+                // The manager responsible for the DDs.
+                storm::dd::DdManager<DdType> const& manager;
+                
+                // The variables encodin the states.
+                std::set<storm::expressions::Variable> const& stateVariables;
+                
+                // The internal refiner.
+                std::unique_ptr<InternalSignatureRefiner<DdType, ValueType>> internalRefiner;
+            };
+            
+        }
+    }
+}

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

@@ -209,6 +209,8 @@ namespace storm {
                 summationAdds.push_back(ddVariable.toAdd<ValueType>().getCuddAdd());
             }
             
+            return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().TimesPlus(otherMatrix.getCuddAdd(), summationAdds));
+            return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Triangle(otherMatrix.getCuddAdd(), summationAdds));
             return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().MatrixMultiply(otherMatrix.getCuddAdd(), summationAdds));
         }
         
@@ -425,6 +427,11 @@ namespace storm {
             }
         }
 
+        template<typename ValueType>
+        InternalDdManager<DdType::CUDD> const& InternalAdd<DdType::CUDD, ValueType>::getInternalDdManager() const {
+            return *ddManager;
+        }
+        
         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);

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

@@ -39,11 +39,18 @@ namespace storm {
         template<DdType LibraryType, typename ValueType>
         class AddIterator;
 
+        namespace bisimulation {
+            template<DdType LibraryType, typename ValueType>
+            class InternalSignatureRefiner;
+        }
+        
         template<typename ValueType>
         class InternalAdd<DdType::CUDD, ValueType> {
         public:
             friend class InternalBdd<DdType::CUDD>;
             
+            friend class bisimulation::InternalSignatureRefiner<DdType::CUDD, ValueType>;
+            
             /*!
              * Creates an ADD that encapsulates the given CUDD ADD.
              *
@@ -576,6 +583,8 @@ namespace storm {
              */
             Odd createOdd(std::vector<uint_fast64_t> const& ddVariableIndices) const;
             
+            InternalDdManager<DdType::CUDD> const& getInternalDdManager() const;
+            
         private:
             /*!
              * Retrieves the CUDD ADD object associated with this ADD.

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

@@ -118,7 +118,6 @@ namespace storm {
              */
             uint_fast64_t getNumberOfDdVariables() const;
 
-        private:
             /*!
              * Retrieves the underlying CUDD manager.
              *
@@ -133,6 +132,7 @@ namespace storm {
              */
             cudd::Cudd const& getCuddManager() const;
 
+        private:
             // The manager responsible for the DDs created/modified with this DdManager.
             cudd::Cudd cuddManager;
             

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

@@ -828,6 +828,11 @@ namespace storm {
             }
         }
         
+        template<typename ValueType>
+        InternalDdManager<DdType::Sylvan> const& InternalAdd<DdType::Sylvan, ValueType>::getInternalDdManager() const {
+            return *ddManager;
+        }
+        
         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);

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

@@ -586,6 +586,15 @@ namespace storm {
              */
             Odd createOdd(std::vector<uint_fast64_t> const& ddVariableIndices) const;
             
+            InternalDdManager<DdType::Sylvan> const& getInternalDdManager() const;
+
+            /*!
+             * Retrieves the underlying sylvan MTBDD.
+             *
+             * @return The sylvan MTBDD.
+             */
+            sylvan::Mtbdd getSylvanMtbdd() const;
+
         private:
             /*!
              * Recursively builds the ODD from an ADD.
@@ -721,13 +730,6 @@ namespace storm {
              */
             static ValueType getValue(MTBDD const& node);
             
-            /*!
-             * Retrieves the underlying sylvan MTBDD.
-             *
-             * @return The sylvan MTBDD.
-             */
-            sylvan::Mtbdd getSylvanMtbdd() const;
-            
             // The manager responsible for this MTBDD.
             InternalDdManager<DdType::Sylvan> const* ddManager;
             

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

@@ -9,6 +9,7 @@
 #include "storm/utility/constants.h"
 #include "storm/utility/macros.h"
 #include "storm/exceptions/NotSupportedException.h"
+#include "storm/exceptions/InvalidSettingsException.h"
 
 #include "storm/utility/sylvan.h"
 
@@ -47,7 +48,11 @@ namespace storm {
                 // Compute the power of two that still fits within the total numbers to store.
                 uint_fast64_t powerOfTwo = findLargestPowerOfTwoFitting(totalNodesToStore);
                 
-                sylvan::Sylvan::initPackage(1ull << std::max(16ull, powerOfTwo > 24 ? powerOfTwo - 8 : 0ull), 1ull << (powerOfTwo - 1), 1ull << std::max(16ull, powerOfTwo > 24 ? powerOfTwo - 12 : 0ull), 1ull << (powerOfTwo - 1));
+                STORM_LOG_THROW(powerOfTwo >= 16, storm::exceptions::InvalidSettingsException, "Too little memory assigned to sylvan.");
+                
+                STORM_LOG_TRACE("Assigning " << (1ull << (powerOfTwo - 1)) << " slots to both sylvan's unique table and its cache.");
+                sylvan::Sylvan::initPackage(1ull << (powerOfTwo - 1), 1ull << (powerOfTwo - 1), 1ull << (powerOfTwo - 1), 1ull << (powerOfTwo - 1));
+                sylvan::Sylvan::setGranularity(3);
                 sylvan::Sylvan::initBdd();
                 sylvan::Sylvan::initMtbdd();
                 sylvan::Sylvan::initCustomMtbdd();

src/storm/utility/storm.h

@@ -54,6 +54,7 @@
 // Headers for model processing.
 #include "storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h"
 #include "storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h"
+#include "storm/storage/dd/BisimulationDecomposition.h"
 #include "storm/transformer/SymbolicToSparseTransformer.h"
 #include "storm/storage/ModelFormulasPair.h"
 #include "storm/storage/SymbolicModelDescription.h"
@@ -167,20 +168,30 @@ namespace storm {
     
     template<typename ValueType, storm::dd::DdType LibraryType = storm::dd::DdType::CUDD>
     std::shared_ptr<storm::models::symbolic::Model<LibraryType, ValueType>> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
+        std::shared_ptr<storm::models::symbolic::Model<LibraryType, ValueType>> result;
         if (model.isPrismProgram()) {
             typename storm::builder::DdPrismModelBuilder<LibraryType, ValueType>::Options options;
             options = typename storm::builder::DdPrismModelBuilder<LibraryType, ValueType>::Options(formulas);
             
             storm::builder::DdPrismModelBuilder<LibraryType, ValueType> builder;
-            return builder.build(model.asPrismProgram(), options);
+            result = builder.build(model.asPrismProgram(), options);
         } else {
             STORM_LOG_THROW(model.isJaniModel(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model for the given symbolic model description.");
             typename storm::builder::DdJaniModelBuilder<LibraryType, ValueType>::Options options;
             options = typename storm::builder::DdJaniModelBuilder<LibraryType, ValueType>::Options(formulas);
             
             storm::builder::DdJaniModelBuilder<LibraryType, ValueType> builder;
-            return builder.build(model.asJaniModel(), options);
+            result = builder.build(model.asJaniModel(), options);
         }
+        
+        if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isBisimulationSet()) {
+            storm::dd::BisimulationDecomposition<LibraryType, ValueType> decomposition(*result);
+            decomposition.compute();
+            
+            // TODO build quotient and return it.
+        }
+        
+        return result;
     }
     
     template<typename ModelType>
@@ -237,7 +248,6 @@ namespace storm {
         return performBisimulationMinimization<ModelType>(model, formulas , type);
     }
     
-    
     template<typename ModelType>
     std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
         storm::utility::Stopwatch preprocessingWatch(true);

src/test/storage/SymbolicBisimulationDecompositionTest.cpp

@@ -0,0 +1,27 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+#include "storm/parser/PrismParser.h"
+#include "storm/storage/SymbolicModelDescription.h"
+#include "storm/builder/DdPrismModelBuilder.h"
+#include "storm/models/symbolic/Dtmc.h"
+#include "storm/storage/dd/BisimulationDecomposition.h"
+
+TEST(SymbolicBisimulationDecompositionTest_Cudd, Die) {
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
+    
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD, double>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD, double>().build(program);
+    
+    storm::dd::BisimulationDecomposition<storm::dd::DdType::CUDD, double> decomposition(*model, storm::dd::bisimulation::Partition<storm::dd::DdType::CUDD, double>::create(*model, {"one"}));
+    decomposition.compute();
+}
+
+TEST(SymbolicBisimulationDecompositionTest_Cudd, Crowds) {
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
+    
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD, double>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD, double>().build(program);
+    
+    storm::dd::BisimulationDecomposition<storm::dd::DdType::CUDD, double> decomposition(*model, storm::dd::bisimulation::Partition<storm::dd::DdType::CUDD, double>::create(*model, {"observe0Greater1"}));
+    decomposition.compute();
+}