reworked refinement a bit in an attempt to prepare for MDPs

src/storm/storage/dd/BisimulationDecomposition.cpp

@@ -1,9 +1,11 @@
 #include "storm/storage/dd/BisimulationDecomposition.h"
 
-#include "storm/storage/dd/bisimulation/SignatureComputer.h"
-#include "storm/storage/dd/bisimulation/SignatureRefiner.h"
+#include "storm/storage/dd/bisimulation/PartitionRefiner.h"
+
 #include "storm/storage/dd/bisimulation/QuotientExtractor.h"
 
+#include "storm/models/symbolic/Model.h"
+
 #include "storm/utility/macros.h"
 #include "storm/exceptions/InvalidOperationException.h"
 #include "storm/exceptions/NotSupportedException.h"
@@ -24,80 +26,42 @@ namespace storm {
         }
         
         template <storm::dd::DdType DdType, typename ValueType>
-        BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& initialPartition) : model(model), currentPartition(initialPartition) {
+        BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& initialPartition) : model(model), refiner(std::make_unique<PartitionRefiner<DdType, ValueType>>(model, initialPartition)) {
             STORM_LOG_THROW(!model.hasRewardModel(), storm::exceptions::NotSupportedException, "Symbolic bisimulation currently does not support preserving rewards.");
         }
         
+        template <storm::dd::DdType DdType, typename ValueType>
+        BisimulationDecomposition<DdType, ValueType>::~BisimulationDecomposition() = default;
+        
         template <storm::dd::DdType DdType, typename ValueType>
         void BisimulationDecomposition<DdType, ValueType>::compute(bisimulation::SignatureMode const& mode) {
-            this->status = Status::InComputation;
-            auto start = std::chrono::high_resolution_clock::now();
-            std::chrono::high_resolution_clock::duration totalSignatureTime(0);
-            std::chrono::high_resolution_clock::duration totalRefinementTime(0);
+            STORM_LOG_ASSERT(refiner, "No suitable refiner.");
             
-            STORM_LOG_TRACE("Initial partition has " << currentPartition.getNumberOfBlocks() << " blocks.");
+            STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
 #ifndef NDEBUG
-            STORM_LOG_TRACE("Initial partition has " << currentPartition.getNodeCount() << " nodes.");
+            STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNodeCount() << " nodes.");
 #endif
-            
-            SignatureRefiner<DdType, ValueType> refiner(model.getManager(), currentPartition.getBlockVariable(), model.getRowVariables());
-            SignatureComputer<DdType, ValueType> signatureComputer(model, mode);
-            bool done = false;
+
+            auto start = std::chrono::high_resolution_clock::now();
             uint64_t iterations = 0;
-            while (!done) {
+            bool refined = true;
+            while (refined) {
+                refined = refiner->refine(mode);
                 ++iterations;
-                auto iterationStart = std::chrono::high_resolution_clock::now();
-
-                std::chrono::milliseconds::rep signatureTime = 0;
-                std::chrono::milliseconds::rep refinementTime = 0;
-                
-                Partition<DdType, ValueType> newPartition;
-                for (uint64_t index = 0, end = signatureComputer.getNumberOfSignatures(); index < end; ++index) {
-                    auto signatureStart = std::chrono::high_resolution_clock::now();
-                    Signature<DdType, ValueType> signature = signatureComputer.compute(currentPartition, index);
-                    auto signatureEnd = std::chrono::high_resolution_clock::now();
-                    totalSignatureTime += (signatureEnd - signatureStart);
-                    STORM_LOG_DEBUG("Signature " << iterations << "[" << index << "] DD has " << signature.getSignatureAdd().getNodeCount() << " nodes and partition DD has " << currentPartition.getNodeCount() << " nodes.");
-                    
-                    auto refinementStart = std::chrono::high_resolution_clock::now();
-                    newPartition = refiner.refine(currentPartition, signature);
-                    auto refinementEnd = std::chrono::high_resolution_clock::now();
-                    totalRefinementTime += (refinementEnd - refinementStart);
-
-                    signatureTime += std::chrono::duration_cast<std::chrono::milliseconds>(signatureEnd - signatureStart).count();
-                    refinementTime = std::chrono::duration_cast<std::chrono::milliseconds>(refinementEnd - refinementStart).count();
-                    
-                    // Potentially exit early in case we have refined the partition already. 
-                    if (newPartition.getNumberOfBlocks() > currentPartition.getNumberOfBlocks()) {
-                        break;
-                    }
-                }
-
-                auto iterationTime = std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::high_resolution_clock::now() - iterationStart).count();
-
-                STORM_LOG_DEBUG("Iteration " << iterations << " produced " << newPartition.getNumberOfBlocks() << " blocks and was completed in " << iterationTime << "ms (signature: " << signatureTime << "ms, refinement: " << refinementTime << "ms).");
-
-                if (currentPartition == newPartition) {
-                    done = true;
-                } else {
-                    currentPartition = newPartition;
-                }
+                STORM_LOG_TRACE("After iteration " << iterations << " partition has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
             }
-
-            this->status = Status::FixedPoint;
             auto end = std::chrono::high_resolution_clock::now();
-            auto totalSignatureTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(totalSignatureTime).count();
-            auto totalRefinementTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(totalRefinementTime).count();
-            STORM_LOG_DEBUG("Partition refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms (" << iterations << " iterations, signature: " << totalSignatureTimeInMilliseconds << "ms, refinement: " << totalRefinementTimeInMilliseconds << "ms).");
+            
+            STORM_LOG_DEBUG("Partition refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms (" << iterations << " iterations).");
         }
         
         template <storm::dd::DdType DdType, typename ValueType>
         std::shared_ptr<storm::models::Model<ValueType>> BisimulationDecomposition<DdType, ValueType>::getQuotient() const {
-            STORM_LOG_THROW(this->status == Status::FixedPoint, storm::exceptions::InvalidOperationException, "Cannot extract quotient, because bisimulation decomposition was not completed.");
+            STORM_LOG_THROW(this->refiner->getStatus() == Status::FixedPoint, storm::exceptions::InvalidOperationException, "Cannot extract quotient, because bisimulation decomposition was not completed.");
 
             STORM_LOG_TRACE("Starting quotient extraction.");
             QuotientExtractor<DdType, ValueType> extractor;
-            std::shared_ptr<storm::models::Model<ValueType>> quotient = extractor.extract(model, currentPartition);
+            std::shared_ptr<storm::models::Model<ValueType>> quotient = extractor.extract(model, refiner->getStatePartition());
             STORM_LOG_TRACE("Quotient extraction done.");
             
             return quotient;

src/storm/storage/dd/BisimulationDecomposition.h

@@ -5,27 +5,39 @@
 
 #include "storm/storage/dd/DdType.h"
 #include "storm/storage/bisimulation/BisimulationType.h"
-#include "storm/storage/dd/bisimulation/Partition.h"
 #include "storm/storage/dd/bisimulation/SignatureMode.h"
 
-#include "storm/models/symbolic/Model.h"
-
 #include "storm/logic/Formula.h"
 
 namespace storm {
+    namespace models {
+        template <typename ValueType>
+        class Model;
+        
+        namespace symbolic {
+            template <storm::dd::DdType DdType, typename ValueType>
+            class Model;
+        }
+    }
+    
     namespace dd {
+        namespace bisimulation {
+            template <storm::dd::DdType DdType, typename ValueType>
+            class Partition;
+
+            template <storm::dd::DdType DdType, typename ValueType>
+            class PartitionRefiner;
+        }
         
         template <storm::dd::DdType DdType, typename ValueType>
         class BisimulationDecomposition {
         public:
-            enum class Status {
-                Initialized, InComputation, FixedPoint
-            };
-            
             BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType);
             BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType);
             BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, bisimulation::Partition<DdType, ValueType> const& initialPartition);
             
+            ~BisimulationDecomposition();
+            
             /*!
              * Computes the decomposition.
              */
@@ -37,14 +49,11 @@ namespace storm {
             std::shared_ptr<storm::models::Model<ValueType>> getQuotient() const;
             
         private:
-            // The status of the computation.
-            Status status;
-            
             // The model for which to compute the bisimulation decomposition.
             storm::models::symbolic::Model<DdType, ValueType> const& model;
             
-            // The current partition in the partition refinement process. Initially set to the initial partition.
-            bisimulation::Partition<DdType, ValueType> currentPartition;
+            // The refiner to use.
+            std::unique_ptr<bisimulation::PartitionRefiner<DdType, ValueType>> refiner;
         };
         
     }

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

@@ -0,0 +1,78 @@
+#include "storm/storage/dd/bisimulation/PartitionRefiner.h"
+
+namespace storm {
+    namespace dd {
+        namespace bisimulation {
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            PartitionRefiner<DdType, ValueType>::PartitionRefiner(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& initialStatePartition) : status(Status::Initialized), refinements(0), statePartition(initialStatePartition), signatureComputer(model), signatureRefiner(model.getManager(), statePartition.getBlockVariable(), model.getRowVariables()) {
+                // Intentionally left empty.
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            bool PartitionRefiner<DdType, ValueType>::refine(bisimulation::SignatureMode const& mode) {
+                this->status = Status::InComputation;
+                
+                this->signatureComputer.setSignatureMode(mode);
+                auto start = std::chrono::high_resolution_clock::now();
+
+                std::chrono::milliseconds::rep signatureTime = 0;
+                std::chrono::milliseconds::rep refinementTime = 0;
+                
+                bool alreadyRefined = false;
+                uint64_t index = 0;
+                Partition<DdType, ValueType> newStatePartition;
+                auto signatureIterator = signatureComputer.compute(statePartition);
+                while (signatureIterator.hasNext() && !alreadyRefined) {
+                    auto signatureStart = std::chrono::high_resolution_clock::now();
+                    auto signature = signatureIterator.next();
+                    auto signatureEnd = std::chrono::high_resolution_clock::now();
+                    totalSignatureTime += (signatureEnd - signatureStart);
+                    STORM_LOG_DEBUG("Signature " << refinements << "[" << index << "] DD has " << signature.getSignatureAdd().getNodeCount() << " nodes.");
+                    
+                    auto refinementStart = std::chrono::high_resolution_clock::now();
+                    newStatePartition = signatureRefiner.refine(statePartition, signature);
+                    auto refinementEnd = std::chrono::high_resolution_clock::now();
+                    totalRefinementTime += (refinementEnd - refinementStart);
+
+                    signatureTime += std::chrono::duration_cast<std::chrono::milliseconds>(signatureEnd - signatureStart).count();
+                    refinementTime = std::chrono::duration_cast<std::chrono::milliseconds>(refinementEnd - refinementStart).count();
+                    
+                    // Potentially exit early in case we have refined the partition already.
+                    if (newStatePartition.getNumberOfBlocks() > statePartition.getNumberOfBlocks()) {
+                        alreadyRefined = true;
+                    }
+                }
+                
+                auto totalTimeInRefinement = std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::high_resolution_clock::now() - start).count();
+                ++refinements;
+                STORM_LOG_DEBUG("Refinement " << refinements << " produced " << newStatePartition.getNumberOfBlocks() << " blocks and was completed in " << totalTimeInRefinement << "ms (signature: " << signatureTime << "ms, refinement: " << refinementTime << "ms).");
+
+                if (statePartition == newStatePartition) {
+                    this->status = Status::FixedPoint;
+                    return false;
+                } else {
+                    this->statePartition = newStatePartition;
+                    return true;
+                }
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            Partition<DdType, ValueType> const& PartitionRefiner<DdType, ValueType>::getStatePartition() const {
+                return statePartition;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            Status PartitionRefiner<DdType, ValueType>::getStatus() const {
+                return status;
+            }
+            
+            template class PartitionRefiner<storm::dd::DdType::CUDD, double>;
+            
+            template class PartitionRefiner<storm::dd::DdType::Sylvan, double>;
+            template class PartitionRefiner<storm::dd::DdType::Sylvan, storm::RationalNumber>;
+            template class PartitionRefiner<storm::dd::DdType::Sylvan, storm::RationalFunction>;
+            
+        }
+    }
+}

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

@@ -11,6 +11,7 @@ namespace storm {
             template<storm::dd::DdType DdType, typename ValueType>
             class Signature {
             public:
+                Signature() = default;
                 Signature(storm::dd::Add<DdType, ValueType> const& signatureAdd);
                 
                 storm::dd::Add<DdType, ValueType> const& getSignatureAdd() const;

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

@@ -2,36 +2,71 @@
 
 #include "storm/storage/dd/DdManager.h"
 
+#include "storm/utility/macros.h"
+#include "storm/exceptions/OutOfRangeException.h"
+
 namespace storm {
     namespace dd {
         namespace bisimulation {
 
             template<storm::dd::DdType DdType, typename ValueType>
-            SignatureComputer<DdType, ValueType>::SignatureComputer(storm::models::symbolic::Model<DdType, ValueType> const& model, SignatureMode const& mode) : model(model), transitionMatrix(model.getTransitionMatrix()), mode(mode) {
+            SignatureIterator<DdType, ValueType>::SignatureIterator(SignatureComputer<DdType, ValueType> const& signatureComputer, Partition<DdType, ValueType> const& partition) : signatureComputer(signatureComputer), partition(partition), position(0) {
+                // Intentionally left empty.
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            bool SignatureIterator<DdType, ValueType>::hasNext() const {
+                if (signatureComputer.getSignatureMode() == SignatureMode::Eager) {
+                    return position < 1;
+                } else {
+                    return position < 2;
+                }
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            Signature<DdType, ValueType> SignatureIterator<DdType, ValueType>::next() {
+                auto mode = signatureComputer.getSignatureMode();
+                STORM_LOG_THROW((mode == SignatureMode::Eager && position < 1) || (mode == SignatureMode::Lazy && position < 2), storm::exceptions::OutOfRangeException, "Iterator is out of range.");
+                Signature<DdType, ValueType> result;
+                
+                if (mode == SignatureMode::Eager || position == 1) {
+                    result = signatureComputer.getFullSignature(partition);
+                } else if (position == 0) {
+                    result = signatureComputer.getQualitativeSignature(partition);
+                }
+                
+                ++position;
+                return result;
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            SignatureComputer<DdType, ValueType>::SignatureComputer(storm::models::symbolic::Model<DdType, ValueType> const& model, SignatureMode const& mode) : model(model), transitionMatrix(model.getTransitionMatrix()) {
                 if (DdType == storm::dd::DdType::Sylvan) {
                     this->transitionMatrix = this->transitionMatrix.notZero().ite(this->transitionMatrix, this->transitionMatrix.getDdManager().template getAddUndefined<ValueType>());
                 }
-                if (mode == SignatureMode::Lazy) {
+                this->setSignatureMode(mode);
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            SignatureIterator<DdType, ValueType> SignatureComputer<DdType, ValueType>::compute(Partition<DdType, ValueType> const& partition) {
+                return SignatureIterator<DdType, ValueType>(*this, partition);
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            void SignatureComputer<DdType, ValueType>::setSignatureMode(SignatureMode const& newMode) {
+                if (newMode == SignatureMode::Lazy && !transitionMatrix01) {
                     if (DdType == storm::dd::DdType::Sylvan) {
                         this->transitionMatrix01 = model.getQualitativeTransitionMatrix().ite(this->transitionMatrix.getDdManager().template getAddOne<ValueType>(), this->transitionMatrix.getDdManager().template getAddUndefined<ValueType>());
                     } else {
                         this->transitionMatrix01 = model.getQualitativeTransitionMatrix().template toAdd<ValueType>();
                     }
                 }
+                this->mode = newMode;
             }
             
             template<storm::dd::DdType DdType, typename ValueType>
-            uint64_t SignatureComputer<DdType, ValueType>::getNumberOfSignatures() const {
-                return this->mode == SignatureMode::Lazy ? 2 : 1;
-            }
-
-            template<storm::dd::DdType DdType, typename ValueType>
-            Signature<DdType, ValueType> SignatureComputer<DdType, ValueType>::compute(Partition<DdType, ValueType> const& partition, uint64_t index) {
-                if (mode == SignatureMode::Lazy && index == 1) {
-                    return getQualitativeSignature(partition);
-                } else {
-                    return getFullSignature(partition);
-                }
+            SignatureMode const& SignatureComputer<DdType, ValueType>::getSignatureMode() const {
+                return mode;
             }
             
             template<storm::dd::DdType DdType, typename ValueType>
@@ -45,15 +80,20 @@ namespace storm {
             
             template<storm::dd::DdType DdType, typename ValueType>
             Signature<DdType, ValueType> SignatureComputer<DdType, ValueType>::getQualitativeSignature(Partition<DdType, ValueType> const& partition) const {
+                STORM_LOG_ASSERT(this->transitionMatrix01, "Need qualitative transition matrix for this step.");
                 if (partition.storedAsBdd()) {
-                    return Signature<DdType, ValueType>(this->transitionMatrix01.multiplyMatrix(partition.asBdd(), model.getColumnVariables()));
+                    return Signature<DdType, ValueType>(this->transitionMatrix01.get().multiplyMatrix(partition.asBdd(), model.getColumnVariables()));
                 } else {
-                    return Signature<DdType, ValueType>(this->transitionMatrix01.multiplyMatrix(partition.asAdd(), model.getColumnVariables()));
+                    return Signature<DdType, ValueType>(this->transitionMatrix01.get().multiplyMatrix(partition.asAdd(), model.getColumnVariables()));
                 }
             }
+
+            template class SignatureIterator<storm::dd::DdType::CUDD, double>;
+            template class SignatureIterator<storm::dd::DdType::Sylvan, double>;
+            template class SignatureIterator<storm::dd::DdType::Sylvan, storm::RationalNumber>;
+            template class SignatureIterator<storm::dd::DdType::Sylvan, storm::RationalFunction>;
             
             template class SignatureComputer<storm::dd::DdType::CUDD, double>;
-
             template class SignatureComputer<storm::dd::DdType::Sylvan, double>;
             template class SignatureComputer<storm::dd::DdType::Sylvan, storm::RationalNumber>;
             template class SignatureComputer<storm::dd::DdType::Sylvan, storm::RationalFunction>;

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

@@ -1,5 +1,7 @@
 #pragma once
 
+#include <boost/optional.hpp>
+
 #include "storm/storage/dd/DdType.h"
 
 #include "storm/storage/dd/bisimulation/Signature.h"
@@ -11,21 +13,48 @@
 namespace storm {
     namespace dd {
         namespace bisimulation {
+
+            template<storm::dd::DdType DdType, typename ValueType>
+            class SignatureComputer;
             
+            template<storm::dd::DdType DdType, typename ValueType>
+            class SignatureIterator {
+            public:
+                SignatureIterator(SignatureComputer<DdType, ValueType> const& signatureComputer, Partition<DdType, ValueType> const& partition);
+
+                bool hasNext() const;
+                
+                Signature<DdType, ValueType> next();
+                
+            private:
+                // The signature computer to use.
+                SignatureComputer<DdType, ValueType> const& signatureComputer;
+                
+                // The current partition.
+                Partition<DdType, ValueType> const& partition;
+                
+                // The position in the enumeration.
+                uint64_t position;
+            };
+
             template<storm::dd::DdType DdType, typename ValueType>
             class SignatureComputer {
             public:
-                SignatureComputer(storm::models::symbolic::Model<DdType, ValueType> const& model, SignatureMode const& mode = SignatureMode::Eager);
+                friend class SignatureIterator<DdType, ValueType>;
                 
-                Signature<DdType, ValueType> compute(Partition<DdType, ValueType> const& partition, uint64_t index = 0);
+                SignatureComputer(storm::models::symbolic::Model<DdType, ValueType> const& model, SignatureMode const& mode = SignatureMode::Eager);
 
-                uint64_t getNumberOfSignatures() const;
+                void setSignatureMode(SignatureMode const& newMode);
+
+                SignatureIterator<DdType, ValueType> compute(Partition<DdType, ValueType> const& partition);
                 
             private:
                 Signature<DdType, ValueType> getFullSignature(Partition<DdType, ValueType> const& partition) const;
 
                 Signature<DdType, ValueType> getQualitativeSignature(Partition<DdType, ValueType> const& partition) const;
                 
+                SignatureMode const& getSignatureMode() const;
+                
                 storm::models::symbolic::Model<DdType, ValueType> const& model;
                 
                 // The transition matrix to use for the signature computation.
@@ -35,7 +64,7 @@ namespace storm {
                 SignatureMode mode;
                 
                 // Only used when using lazy signatures is enabled.
-                storm::dd::Add<DdType, ValueType> transitionMatrix01;
+                boost::optional<storm::dd::Add<DdType, ValueType>> transitionMatrix01;
             };
             
         }

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

@@ -0,0 +1,13 @@
+#pragma once
+
+namespace storm {
+    namespace dd {
+        namespace bisimulation {
+ 
+            enum class Status {
+                Initialized, InComputation, FixedPoint
+            };
+            
+        }
+    }
+}