started on debugging MDP bisimulation

src/storm/models/symbolic/Model.cpp

@@ -172,6 +172,16 @@ namespace storm {
                 return columnVariables;
             }
             
+            template<storm::dd::DdType Type, typename ValueType>
+            std::set<storm::expressions::Variable> Model<Type, ValueType>::getRowAndNondeterminismVariables() const {
+                return rowVariables;
+            }
+            
+            template<storm::dd::DdType Type, typename ValueType>
+            std::set<storm::expressions::Variable> Model<Type, ValueType>::getColumnAndNondeterminismVariables() const {
+                return columnVariables;
+            }
+            
             template<storm::dd::DdType Type, typename ValueType>
             std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& Model<Type, ValueType>::getRowColumnMetaVariablePairs() const {
                 return rowColumnMetaVariablePairs;

src/storm/models/symbolic/Model.h

@@ -221,6 +221,20 @@ namespace storm {
                  */
                 std::set<storm::expressions::Variable> const& getColumnVariables() const;
                 
+                /*!
+                 * Retrieves all meta variables used to encode rows and nondetermism.
+                 *
+                 * @return All meta variables used to encode rows and nondetermism.
+                 */
+                virtual std::set<storm::expressions::Variable> getRowAndNondeterminismVariables() const;
+
+                /*!
+                 * Retrieves all meta variables used to encode columns and nondetermism.
+                 *
+                 * @return All meta variables used to encode columns and nondetermism.
+                 */
+                virtual std::set<storm::expressions::Variable> getColumnAndNondeterminismVariables() const;
+
                 /*!
                  * Retrieves the pairs of row and column meta variables.
                  *

src/storm/models/symbolic/NondeterministicModel.cpp

@@ -62,6 +62,20 @@ namespace storm {
                 return nondeterminismVariables;
             }
             
+            template<storm::dd::DdType Type, typename ValueType>
+            std::set<storm::expressions::Variable> NondeterministicModel<Type, ValueType>::getRowAndNondeterminismVariables() const {
+                std::set<storm::expressions::Variable> result;
+                std::set_union(this->getRowVariables().begin(), this->getRowVariables().end(), this->getNondeterminismVariables().begin(), this->getNondeterminismVariables().end(), std::inserter(result, result.begin()));
+                return result;
+            }
+            
+            template<storm::dd::DdType Type, typename ValueType>
+            std::set<storm::expressions::Variable> NondeterministicModel<Type, ValueType>::getColumnAndNondeterminismVariables() const {
+                std::set<storm::expressions::Variable> result;
+                std::set_union(this->getColumnVariables().begin(), this->getColumnVariables().end(), this->getNondeterminismVariables().begin(), this->getNondeterminismVariables().end(), std::inserter(result, result.begin()));
+                return result;
+            }
+            
             template<storm::dd::DdType Type, typename ValueType>
             storm::dd::Bdd<Type> const& NondeterministicModel<Type, ValueType>::getIllegalMask() const {
                 return illegalMask;

src/storm/models/symbolic/NondeterministicModel.h

@@ -99,6 +99,9 @@ namespace storm {
                  */
                 std::set<storm::expressions::Variable> const& getNondeterminismVariables() const;
                 
+                virtual std::set<storm::expressions::Variable> getRowAndNondeterminismVariables() const override;
+                virtual std::set<storm::expressions::Variable> getColumnAndNondeterminismVariables() const override;
+
                 /*!
                  * Retrieves a BDD characterizing all illegal nondeterminism encodings in the model.
                  *

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

@@ -7,23 +7,36 @@ namespace storm {
         namespace bisimulation {
             
             template<storm::dd::DdType DdType, typename ValueType>
-            MdpPartitionRefiner<DdType, ValueType>::MdpPartitionRefiner(storm::models::symbolic::Mdp<DdType, ValueType> const& mdp, Partition<DdType, ValueType> const& initialStatePartition) : PartitionRefiner<DdType, ValueType>(mdp, initialStatePartition), choicePartition(Partition<DdType, ValueType>::createTrivialChoicePartition(mdp, initialStatePartition.getBlockVariables())) {
-                
-                // Initialize the choice signature refiner.
-                std::set<storm::expressions::Variable> choiceSignatureVariables;
-                std::set_union(mdp.getRowVariables().begin(), mdp.getRowVariables().end(), mdp.getNondeterminismVariables().begin(), mdp.getNondeterminismVariables().end(), std::inserter(choiceSignatureVariables, choiceSignatureVariables.begin()));
-                choiceSignatureRefiner = SignatureRefiner<DdType, ValueType>(mdp.getManager(), this->statePartition.getBlockVariable(), choiceSignatureVariables);
+            MdpPartitionRefiner<DdType, ValueType>::MdpPartitionRefiner(storm::models::symbolic::Mdp<DdType, ValueType> const& mdp, Partition<DdType, ValueType> const& initialStatePartition) : PartitionRefiner<DdType, ValueType>(mdp, initialStatePartition), choicePartition(Partition<DdType, ValueType>::createTrivialChoicePartition(mdp, initialStatePartition.getBlockVariables())), stateSignatureComputer(mdp.getQualitativeTransitionMatrix(false), mdp.getColumnAndNondeterminismVariables()), stateSignatureRefiner(mdp.getManager(), this->statePartition.getBlockVariable(), mdp.getRowVariables()) {
+                // Intentionally left empty.
             }
             
             template<storm::dd::DdType DdType, typename ValueType>
             bool MdpPartitionRefiner<DdType, ValueType>::refine(bisimulation::SignatureMode const& mode) {
-                Partition<DdType, ValueType> newChoicePartition = this->internalRefine(choiceSignatureRefiner, choicePartition, mode);
+                // In this procedure, we will
+                // (1) refine the partition of nondeterministic choices based on the state partition. For this, we use
+                // the signature computer/refiner of the superclass. These objects use the full transition matrix.
+                // (2) if the choice partition was in fact split, the state partition also needs to be refined.
+                // For this, we use the signature computer/refiner of this class.
+                
+                STORM_LOG_TRACE("Refining choice partition.");
+                Partition<DdType, ValueType> newChoicePartition = this->internalRefine(this->signatureComputer, this->signatureRefiner, choicePartition, this->statePartition, mode);
                 
                 if (newChoicePartition == choicePartition) {
                     this->status = Status::FixedPoint;
                     return false;
                 } else {
-                    return PartitionRefiner<DdType, ValueType>::refine(mode);
+                    // If the choice partition changed, refine the state partition. Use eager mode as abstracting from the probabilities is not worth doing.
+                    STORM_LOG_TRACE("Refining state partition.");
+                    Partition<DdType, ValueType> newStatePartition = this->internalRefine(this->stateSignatureComputer, this->stateSignatureRefiner, this->statePartition, this->choicePartition, SignatureMode::Eager);
+                    
+                    if (newStatePartition == this->statePartition) {
+                        this->status = Status::FixedPoint;
+                        return false;
+                    } else {
+                        this->statePartition = newStatePartition;
+                        return true;
+                    }
                 }
             }
             

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

@@ -34,9 +34,12 @@ namespace storm {
             private:
                 // The choice partition in the refinement process.
                 Partition<DdType, ValueType> choicePartition;
+
+                // The object used to compute the state signatures.
+                SignatureComputer<DdType, ValueType> stateSignatureComputer;
                 
-                // The object used to refine the choice partition based on the signatures.
-                SignatureRefiner<DdType, ValueType> choiceSignatureRefiner;
+                // The object used to refine the state partition based on the signatures.
+                SignatureRefiner<DdType, ValueType> stateSignatureRefiner;
             };
             
         }

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

@@ -5,13 +5,13 @@ namespace storm {
         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()) {
+            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.getRowAndNondeterminismVariables()) {
                 // Intentionally left empty.
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
             bool PartitionRefiner<DdType, ValueType>::refine(SignatureMode const& mode) {
-                Partition<DdType, ValueType> newStatePartition = this->internalRefine(signatureRefiner, statePartition, mode);
+                Partition<DdType, ValueType> newStatePartition = this->internalRefine(signatureComputer, signatureRefiner, statePartition, statePartition, mode);
                 if (statePartition == newStatePartition) {
                     this->status = Status::FixedPoint;
                     return false;
@@ -22,13 +22,13 @@ namespace storm {
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
-            Partition<DdType, ValueType> PartitionRefiner<DdType, ValueType>::internalRefine(SignatureRefiner<DdType, ValueType>& signatureRefiner, Partition<DdType, ValueType> const& oldPartition, SignatureMode const& mode) {
+            Partition<DdType, ValueType> PartitionRefiner<DdType, ValueType>::internalRefine(SignatureComputer<DdType, ValueType>& signatureComputer, SignatureRefiner<DdType, ValueType>& signatureRefiner, Partition<DdType, ValueType> const& oldPartition, Partition<DdType, ValueType> const& targetPartition, SignatureMode const& mode) {
                 auto start = std::chrono::high_resolution_clock::now();
                 
                 if (this->status != Status::FixedPoint) {
                     this->status = Status::InComputation;
                     
-                    this->signatureComputer.setSignatureMode(mode);
+                    signatureComputer.setSignatureMode(mode);
                     
                     std::chrono::milliseconds::rep signatureTime = 0;
                     std::chrono::milliseconds::rep refinementTime = 0;
@@ -36,7 +36,7 @@ namespace storm {
                     bool refined = false;
                     uint64_t index = 0;
                     Partition<DdType, ValueType> newPartition;
-                    auto signatureIterator = signatureComputer.compute(oldPartition);
+                    auto signatureIterator = signatureComputer.compute(targetPartition);
                     while (signatureIterator.hasNext() && !refined) {
                         auto signatureStart = std::chrono::high_resolution_clock::now();
                         auto signature = signatureIterator.next();
@@ -44,11 +44,18 @@ namespace storm {
                         totalSignatureTime += (signatureEnd - signatureStart);
                         STORM_LOG_DEBUG("Signature " << refinements << "[" << index << "] DD has " << signature.getSignatureAdd().getNodeCount() << " nodes.");
                         
+                        signature.getSignatureAdd().exportToDot("sig" + std::to_string(refinements) + ".dot");
+                        if (refinements == 1) {
+                            exit(-1);
+                        }
+                        
                         auto refinementStart = std::chrono::high_resolution_clock::now();
                         newPartition = signatureRefiner.refine(statePartition, signature);
                         auto refinementEnd = std::chrono::high_resolution_clock::now();
                         totalRefinementTime += (refinementEnd - refinementStart);
                         
+                        newPartition.asAdd().exportToDot("newpart" + std::to_string(refinements) + ".dot");
+                        
                         signatureTime += std::chrono::duration_cast<std::chrono::milliseconds>(signatureEnd - signatureStart).count();
                         refinementTime = std::chrono::duration_cast<std::chrono::milliseconds>(refinementEnd - refinementStart).count();
                         

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

@@ -41,7 +41,7 @@ namespace storm {
                 Status getStatus() const;
                 
             protected:
-                Partition<DdType, ValueType> internalRefine(SignatureRefiner<DdType, ValueType>& signatureRefiner, Partition<DdType, ValueType> const& oldPartition, SignatureMode const& mode = SignatureMode::Eager);
+                Partition<DdType, ValueType> internalRefine(SignatureComputer<DdType, ValueType>& stateSignatureComputer, SignatureRefiner<DdType, ValueType>& signatureRefiner, Partition<DdType, ValueType> const& oldPartition, Partition<DdType, ValueType> const& targetPartition, SignatureMode const& mode = SignatureMode::Eager);
                 
                 // The current status.
                 Status status;

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

@@ -40,11 +40,33 @@ namespace storm {
             }
             
             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()) {
+            SignatureComputer<DdType, ValueType>::SignatureComputer(storm::models::symbolic::Model<DdType, ValueType> const& model, SignatureMode const& mode) : SignatureComputer(model.getTransitionMatrix(), boost::none, model.getColumnVariables(), mode) {
+                // Intentionally left empty.
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            SignatureComputer<DdType, ValueType>::SignatureComputer(storm::dd::Add<DdType, ValueType> const& transitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, SignatureMode const& mode) : SignatureComputer(transitionMatrix, boost::none, columnVariables, mode) {
+                // Intentionally left empty.
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            SignatureComputer<DdType, ValueType>::SignatureComputer(storm::dd::Bdd<DdType> const& qualitativeTransitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, SignatureMode const& mode) : SignatureComputer(qualitativeTransitionMatrix.template toAdd<ValueType>(), boost::none, columnVariables, mode) {
+                // Intentionally left empty.
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            SignatureComputer<DdType, ValueType>::SignatureComputer(storm::dd::Add<DdType, ValueType> const& transitionMatrix, boost::optional<storm::dd::Bdd<DdType>> const& qualitativeTransitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, SignatureMode const& mode) : transitionMatrix(transitionMatrix), columnVariables(columnVariables), mode(mode) {
                 if (DdType == storm::dd::DdType::Sylvan) {
                     this->transitionMatrix = this->transitionMatrix.notZero().ite(this->transitionMatrix, this->transitionMatrix.getDdManager().template getAddUndefined<ValueType>());
                 }
-                this->setSignatureMode(mode);
+                
+                if (qualitativeTransitionMatrix) {
+                    if (DdType == storm::dd::DdType::Sylvan) {
+                        this->transitionMatrix01 = qualitativeTransitionMatrix.get().ite(this->transitionMatrix.getDdManager().template getAddOne<ValueType>(), this->transitionMatrix.getDdManager().template getAddUndefined<ValueType>());
+                    } else {
+                        this->transitionMatrix01 = qualitativeTransitionMatrix.get().template toAdd<ValueType>();
+                    }
+                }
             }
             
             template<storm::dd::DdType DdType, typename ValueType>
@@ -54,13 +76,6 @@ namespace storm {
             
             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;
             }
             
@@ -71,20 +86,37 @@ namespace storm {
             
             template<storm::dd::DdType DdType, typename ValueType>
             Signature<DdType, ValueType> SignatureComputer<DdType, ValueType>::getFullSignature(Partition<DdType, ValueType> const& partition) const {
+                this->transitionMatrix.exportToDot("trans.dot");
                 if (partition.storedAsBdd()) {
-                    return Signature<DdType, ValueType>(this->transitionMatrix.multiplyMatrix(partition.asBdd(), model.getColumnVariables()));
+                    return Signature<DdType, ValueType>(this->transitionMatrix.multiplyMatrix(partition.asBdd(), columnVariables));
                 } else {
-                    return Signature<DdType, ValueType>(this->transitionMatrix.multiplyMatrix(partition.asAdd(), model.getColumnVariables()));
+                    auto result = Signature<DdType, ValueType>(this->transitionMatrix.multiplyMatrix(partition.asAdd(), columnVariables));
+                    
+                    std::cout << "abstracting vars" << std::endl;
+                    for (auto const& v : columnVariables) {
+                        std::cout << v.getName() << std::endl;
+                    }
+                    std::cout << "----" << std::endl;
+                    result.getSignatureAdd().exportToDot("fullsig.dot");
+                    
+                    return result;
                 }
             }
             
             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 (this->mode == SignatureMode::Lazy && !transitionMatrix01) {
+                    if (DdType == storm::dd::DdType::Sylvan) {
+                        this->transitionMatrix01 = this->transitionMatrix.notZero().ite(this->transitionMatrix.getDdManager().template getAddOne<ValueType>(), this->transitionMatrix.getDdManager().template getAddUndefined<ValueType>());
+                    } else {
+                        this->transitionMatrix01 = this->transitionMatrix.notZero().template toAdd<ValueType>();
+                    }
+                }
+
                 if (partition.storedAsBdd()) {
-                    return Signature<DdType, ValueType>(this->transitionMatrix01.get().multiplyMatrix(partition.asBdd(), model.getColumnVariables()));
+                    return Signature<DdType, ValueType>(this->transitionMatrix01.get().multiplyMatrix(partition.asBdd(), columnVariables));
                 } else {
-                    return Signature<DdType, ValueType>(this->transitionMatrix01.get().multiplyMatrix(partition.asAdd(), model.getColumnVariables()));
+                    return Signature<DdType, ValueType>(this->transitionMatrix01.get().multiplyMatrix(partition.asAdd(), columnVariables));
                 }
             }
 

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

@@ -43,28 +43,32 @@ namespace storm {
                 friend class SignatureIterator<DdType, ValueType>;
                 
                 SignatureComputer(storm::models::symbolic::Model<DdType, ValueType> const& model, SignatureMode const& mode = SignatureMode::Eager);
+                SignatureComputer(storm::dd::Add<DdType, ValueType> const& transitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, SignatureMode const& mode = SignatureMode::Eager);
+                SignatureComputer(storm::dd::Bdd<DdType> const& qualitativeTransitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, SignatureMode const& mode = SignatureMode::Eager);
+                SignatureComputer(storm::dd::Add<DdType, ValueType> const& transitionMatrix, boost::optional<storm::dd::Bdd<DdType>> const& qualitativeTransitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, SignatureMode const& mode = SignatureMode::Eager);
 
                 void setSignatureMode(SignatureMode const& newMode);
 
                 SignatureIterator<DdType, ValueType> compute(Partition<DdType, ValueType> const& partition);
                 
             private:
+                /// Methods to compute the signatures.
                 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.
+                                
+                /// The transition matrix to use for the signature computation.
                 storm::dd::Add<DdType, ValueType> transitionMatrix;
+                
+                /// The set of variables from which to abstract when performing matrix-vector multiplication.
+                std::set<storm::expressions::Variable> columnVariables;
 
-                // The mode to use for signature computation.
+                /// The mode to use for signature computation.
                 SignatureMode mode;
                 
-                // Only used when using lazy signatures is enabled.
-                boost::optional<storm::dd::Add<DdType, ValueType>> transitionMatrix01;
+                /// Only used when using lazy signatures is enabled.
+                mutable boost::optional<storm::dd::Add<DdType, ValueType>> transitionMatrix01;
             };
             
         }