overhauled output of dd-based bisimulation for benchmarking

src/storm/settings/modules/BisimulationSettings.cpp

@@ -15,7 +15,7 @@ namespace storm {
             const std::string BisimulationSettings::moduleName = "bisimulation";
             const std::string BisimulationSettings::typeOptionName = "type";
             const std::string BisimulationSettings::representativeOptionName = "repr";
-            const std::string BisimulationSettings::originalVariablesOptionName = "origvar";
+            const std::string BisimulationSettings::originalVariablesOptionName = "origvars";
             const std::string BisimulationSettings::quotientFormatOptionName = "quot";
             const std::string BisimulationSettings::signatureModeOptionName = "sigmode";
             const std::string BisimulationSettings::reuseOptionName = "reuse";

src/storm/solver/SymbolicNativeLinearEquationSolver.cpp

@@ -88,7 +88,7 @@ namespace storm {
             storm::dd::Add<DdType, ValueType> lu = diagonal.ite(manager.template getAddZero<ValueType>(), this->A);
             storm::dd::Add<DdType, ValueType> diagonalAdd = diagonal.template toAdd<ValueType>();
             storm::dd::Add<DdType, ValueType> diag = diagonalAdd.multiplyMatrix(this->A, this->columnMetaVariables);
-            
+
             storm::dd::Add<DdType, ValueType> scaledLu = lu / diag;
             storm::dd::Add<DdType, ValueType> scaledB = b / diag;
             

src/storm/storage/dd/BisimulationDecomposition.cpp

@@ -57,14 +57,16 @@ namespace storm {
         template <storm::dd::DdType DdType, typename ValueType>
         void BisimulationDecomposition<DdType, ValueType>::initialize() {
             auto const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
-            showProgress = generalSettings.isVerboseSet();
+            verboseProgress = generalSettings.isVerboseSet();
             showProgressDelay = generalSettings.getShowProgressDelay();
+            
+            auto start = std::chrono::high_resolution_clock::now();
             this->refineWrtRewardModels();
+            auto end = std::chrono::high_resolution_clock::now();
+            STORM_LOG_INFO("Refining with respect to reward models took " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
             
-            STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
-#ifndef NDEBUG
+            STORM_LOG_INFO("Initial partition has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
             STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNodeCount() << " nodes.");
-#endif
         }
         
         template <storm::dd::DdType DdType, typename ValueType>
@@ -80,21 +82,18 @@ namespace storm {
                 refined = refiner->refine(mode);
 
                 ++iterations;
-                STORM_LOG_TRACE("After iteration " << iterations << " partition has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
                 
-                if (showProgress) {
-                    auto now = std::chrono::high_resolution_clock::now();
-                    auto durationSinceLastMessage = std::chrono::duration_cast<std::chrono::seconds>(now - timeOfLastMessage).count();
-                    if (static_cast<uint64_t>(durationSinceLastMessage) >= showProgressDelay) {
-                        auto durationSinceStart = std::chrono::duration_cast<std::chrono::seconds>(now - start).count();
-                        STORM_LOG_INFO("State partition after " << iterations << " iterations (" << durationSinceStart << "s) has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
-                        timeOfLastMessage = std::chrono::high_resolution_clock::now();
-                    }
+                auto now = std::chrono::high_resolution_clock::now();
+                auto durationSinceLastMessage = std::chrono::duration_cast<std::chrono::milliseconds>(now - timeOfLastMessage).count();
+                if (static_cast<uint64_t>(durationSinceLastMessage) >= showProgressDelay * 1000 || verboseProgress) {
+                    auto durationSinceStart = std::chrono::duration_cast<std::chrono::milliseconds>(now - start).count();
+                    STORM_LOG_INFO("State partition after " << iterations << " iterations (" << durationSinceStart << "ms) has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
+                    timeOfLastMessage = std::chrono::high_resolution_clock::now();
                 }
             }
             auto end = std::chrono::high_resolution_clock::now();
             
-            STORM_LOG_DEBUG("Partition refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms (" << iterations << " iterations).");
+            STORM_LOG_INFO("Partition refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms (" << iterations << " iterations).");
         }
 
         template <storm::dd::DdType DdType, typename ValueType>
@@ -112,14 +111,12 @@ namespace storm {
                 
                 ++iterations;
                 
-                if (showProgress) {
-                    auto now = std::chrono::high_resolution_clock::now();
-                    auto durationSinceLastMessage = std::chrono::duration_cast<std::chrono::seconds>(now - timeOfLastMessage).count();
-                    if (static_cast<uint64_t>(durationSinceLastMessage) >= showProgressDelay) {
-                        auto durationSinceStart = std::chrono::duration_cast<std::chrono::seconds>(now - start).count();
-                        STORM_LOG_INFO("State partition after " << iterations << " iterations (" << durationSinceStart << "ms) has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
-                        timeOfLastMessage = std::chrono::high_resolution_clock::now();
-                    }
+                auto now = std::chrono::high_resolution_clock::now();
+                auto durationSinceLastMessage = std::chrono::duration_cast<std::chrono::seconds>(now - timeOfLastMessage).count();
+                if (static_cast<uint64_t>(durationSinceLastMessage) >= showProgressDelay || verboseProgress) {
+                    auto durationSinceStart = std::chrono::duration_cast<std::chrono::seconds>(now - start).count();
+                    STORM_LOG_INFO("State partition after " << iterations << " iterations (" << durationSinceStart << "ms) has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
+                    timeOfLastMessage = std::chrono::high_resolution_clock::now();
                 }
             }
             
@@ -135,13 +132,13 @@ namespace storm {
         std::shared_ptr<storm::models::Model<ValueType>> BisimulationDecomposition<DdType, ValueType>::getQuotient() const {
             std::shared_ptr<storm::models::Model<ValueType>> quotient;
             if (this->refiner->getStatus() == Status::FixedPoint) {
-                STORM_LOG_TRACE("Starting full quotient extraction.");
+                STORM_LOG_INFO("Starting full quotient extraction.");
                 QuotientExtractor<DdType, ValueType> extractor;
                 quotient = extractor.extract(model, refiner->getStatePartition(), preservationInformation);
             } else {
                 STORM_LOG_THROW(model.getType() == storm::models::ModelType::Dtmc || model.getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidOperationException, "Can only extract partial quotient for discrete-time models.");
                 
-                STORM_LOG_TRACE("Starting partial quotient extraction.");
+                STORM_LOG_INFO("Starting partial quotient extraction.");
                 if (!partialQuotientExtractor) {
                     partialQuotientExtractor = std::make_unique<bisimulation::PartialQuotientExtractor<DdType, ValueType>>(model);
                 }
@@ -149,7 +146,7 @@ namespace storm {
                 quotient = partialQuotientExtractor->extract(refiner->getStatePartition(), preservationInformation);
             }
 
-            STORM_LOG_TRACE("Quotient extraction done.");
+            STORM_LOG_INFO("Quotient extraction done.");
             return quotient;
         }
         

src/storm/storage/dd/BisimulationDecomposition.h

@@ -83,7 +83,7 @@ namespace storm {
             mutable std::unique_ptr<bisimulation::PartialQuotientExtractor<DdType, ValueType>> partialQuotientExtractor;
             
             // A flag indicating whether progress is reported.
-            bool showProgress;
+            bool verboseProgress;
             
             // The delay between progress reports.
             uint64_t showProgressDelay;

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

@@ -42,12 +42,21 @@ namespace storm {
                     } else {
                         choicePartitionAsBdd = this->choicePartition.asAdd().notZero();
                     }
-                    Signature<DdType, ValueType> stateSignature(choicePartitionAsBdd.existsAbstract(model.getNondeterminismVariables()).template toAdd<ValueType>());
                     
+                    auto signatureStart = std::chrono::high_resolution_clock::now();
+                    Signature<DdType, ValueType> stateSignature(choicePartitionAsBdd.existsAbstract(model.getNondeterminismVariables()).template toAdd<ValueType>());
+                    auto signatureEnd = std::chrono::high_resolution_clock::now();
+
                     // If the choice partition changed, refine the state partition.
                     STORM_LOG_TRACE("Refining state partition.");
+                    auto refinementStart = std::chrono::high_resolution_clock::now();
                     Partition<DdType, ValueType> newStatePartition = this->internalRefine(stateSignature, this->stateSignatureRefiner, this->statePartition);
+                    auto refinementEnd = std::chrono::high_resolution_clock::now();
                     
+                    auto signatureTime = std::chrono::duration_cast<std::chrono::milliseconds>(signatureEnd - signatureStart).count();
+                    auto refinementTime = std::chrono::duration_cast<std::chrono::milliseconds>(refinementEnd - refinementStart).count();
+                    STORM_LOG_INFO("Refinement " << (this->refinements-1) << " produced " << newStatePartition.getNumberOfBlocks() << " blocks and was completed in " << (signatureTime + refinementTime) << "ms (signature: " << signatureTime << "ms, refinement: " << refinementTime << "ms).");
+
                     if (newStatePartition == this->statePartition) {
                         this->status = Status::FixedPoint;
                         return false;

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

@@ -130,6 +130,8 @@ namespace storm {
                 
                 std::pair<storm::expressions::Variable, storm::expressions::Variable> blockVariables = createBlockVariables(model);
 
+                auto start = std::chrono::high_resolution_clock::now();
+                
                 // Set up the construction.
                 storm::dd::DdManager<DdType>& manager = model.getManager();
                 storm::dd::Bdd<DdType> partitionBdd = manager.getBddZero();
@@ -153,6 +155,9 @@ namespace storm {
                 // Move the partition over to the primed variables.
                 partitionBdd = partitionBdd.swapVariables(model.getRowColumnMetaVariablePairs());
                 
+                auto end = std::chrono::high_resolution_clock::now();
+                STORM_LOG_INFO("Created distance and label-based initial partition in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+                
                 // Store the partition as an ADD only in the case of CUDD.
                 if (DdType == storm::dd::DdType::CUDD) {
                     return Partition<DdType, ValueType>(partitionBdd.template toAdd<ValueType>(), blockVariables, blockCount, blockCount);
@@ -191,8 +196,11 @@ namespace storm {
                 for (auto const& expression : expressions) {
                     stateSets.emplace_back(model.getStates(expression));
                 }
+                auto start = std::chrono::high_resolution_clock::now();
                 std::pair<storm::dd::Bdd<DdType>, uint64_t> partitionBddAndBlockCount = createPartitionBdd(model.getManager(), model, stateSets, blockVariables.first);
-                
+                auto end = std::chrono::high_resolution_clock::now();
+                STORM_LOG_INFO("Created label-based initial partition in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+
                 // Store the partition as an ADD only in the case of CUDD.
                 if (DdType == storm::dd::DdType::CUDD) {
                     return Partition<DdType, ValueType>(partitionBddAndBlockCount.first.template toAdd<ValueType>(), blockVariables, partitionBddAndBlockCount.second, partitionBddAndBlockCount.second);

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

@@ -66,7 +66,7 @@ namespace storm {
                     }
                     
                     auto totalTimeInRefinement = std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::high_resolution_clock::now() - start).count();
-                    STORM_LOG_TRACE("Refinement " << refinements << " produced " << newPartition.getNumberOfBlocks() << " blocks and was completed in " << totalTimeInRefinement << "ms (signature: " << signatureTime << "ms, refinement: " << refinementTime << "ms).");
+                    STORM_LOG_INFO("Refinement " << refinements << " produced " << newPartition.getNumberOfBlocks() << " blocks and was completed in " << totalTimeInRefinement << "ms (signature: " << signatureTime << "ms, refinement: " << refinementTime << "ms).");
                     ++refinements;
                     return newPartition;
                 } else {
@@ -78,10 +78,7 @@ namespace storm {
             Partition<DdType, ValueType> PartitionRefiner<DdType, ValueType>::internalRefine(Signature<DdType, ValueType> const& signature, SignatureRefiner<DdType, ValueType>& signatureRefiner, Partition<DdType, ValueType> const& oldPartition) {
 
                 STORM_LOG_TRACE("Signature " << refinements << " DD has " << signature.getSignatureAdd().getNodeCount() << " nodes.");
-                auto start = std::chrono::high_resolution_clock::now();
                 auto newPartition = signatureRefiner.refine(oldPartition, signature);
-                auto totalTimeInRefinement = std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::high_resolution_clock::now() - start).count();
-                STORM_LOG_TRACE("Refinement " << refinements << " produced " << newPartition.getNumberOfBlocks() << " blocks and was completed in " << totalTimeInRefinement << "ms.");
                 
                 ++refinements;
                 return newPartition;

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

@@ -835,7 +835,7 @@ namespace storm {
                     result = extractDdQuotient(model, partition, preservationInformation);
                 }
                 auto end = std::chrono::high_resolution_clock::now();
-                STORM_LOG_TRACE("Quotient extraction completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+                STORM_LOG_INFO("Quotient extraction completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
                 
                 STORM_LOG_THROW(result, storm::exceptions::NotSupportedException, "Quotient could not be extracted.");
                 
@@ -856,7 +856,7 @@ namespace storm {
                 InternalSparseQuotientExtractor<DdType, ValueType> sparseExtractor(model, partitionAsBdd, partition.getBlockVariable(), partition.getNumberOfBlocks(), representatives);
                 storm::storage::SparseMatrix<ValueType> quotientTransitionMatrix = sparseExtractor.extractTransitionMatrix(model.getTransitionMatrix());
                 auto end = std::chrono::high_resolution_clock::now();
-                STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+                STORM_LOG_INFO("Quotient transition matrix extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
 
                 start = std::chrono::high_resolution_clock::now();
                 storm::models::sparse::StateLabeling quotientStateLabeling(partition.getNumberOfBlocks());
@@ -878,7 +878,7 @@ namespace storm {
                     }
                 }
                 end = std::chrono::high_resolution_clock::now();
-                STORM_LOG_TRACE("Quotient labels extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+                STORM_LOG_INFO("Quotient labels extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
 
                 start = std::chrono::high_resolution_clock::now();
                 std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> quotientRewardModels;
@@ -898,7 +898,7 @@ namespace storm {
                     quotientRewardModels.emplace(rewardModelName, storm::models::sparse::StandardRewardModel<ValueType>(std::move(quotientStateRewards), std::move(quotientStateActionRewards), boost::none));
                 }
                 end = std::chrono::high_resolution_clock::now();
-                STORM_LOG_TRACE("Reward models extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+                STORM_LOG_INFO("Reward models extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
 
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> result;
                 if (model.getType() == storm::models::ModelType::Dtmc) {
@@ -978,7 +978,7 @@ namespace storm {
                         }
                     }
                     auto end = std::chrono::high_resolution_clock::now();
-                    STORM_LOG_TRACE("Quotient labels extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+                    STORM_LOG_INFO("Quotient labels extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
 
                     start = std::chrono::high_resolution_clock::now();
                     std::set<storm::expressions::Variable> blockAndRowVariables;
@@ -1004,7 +1004,7 @@ namespace storm {
                     }
                     STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).equalModuloPrecision(quotientTransitionMatrix.notZero().existsAbstract(blockPrimeVariableSet).template toAdd<ValueType>(), storm::utility::convertNumber<ValueType>(1e-6)), "Illegal non-probabilistic matrix.");
                     
-                    STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+                    STORM_LOG_INFO("Quotient transition matrix extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
 
                     storm::dd::Bdd<DdType> quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero();
                     storm::dd::Bdd<DdType> deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(blockPrimeVariableSet) && reachableStates;
@@ -1027,7 +1027,7 @@ namespace storm {
                         quotientRewardModels.emplace(rewardModelName, storm::models::symbolic::StandardRewardModel<DdType, ValueType>(quotientStateRewards, quotientStateActionRewards, boost::none));
                     }
                     end = std::chrono::high_resolution_clock::now();
-                    STORM_LOG_TRACE("Reward models extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+                    STORM_LOG_INFO("Reward models extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
 
                     if (modelType == storm::models::ModelType::Dtmc) {
                         return std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>>(new storm::models::symbolic::Dtmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, quotientRewardModels));
@@ -1082,7 +1082,7 @@ namespace storm {
                         }
                     }
                     auto end = std::chrono::high_resolution_clock::now();
-                    STORM_LOG_TRACE("Quotient labels extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+                    STORM_LOG_INFO("Quotient labels extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
                     
                     start = std::chrono::high_resolution_clock::now();
                     std::set<storm::expressions::Variable> blockAndRowVariables;
@@ -1113,7 +1113,7 @@ namespace storm {
                     }
                     STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(model.getColumnVariables()).equalModuloPrecision(quotientTransitionMatrix.notZero().existsAbstract(model.getColumnVariables()).template toAdd<ValueType>(), storm::utility::convertNumber<ValueType>(1e-6)), "Illegal probabilistic matrix.");
                     
-                    STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+                    STORM_LOG_INFO("Quotient transition matrix extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
                     
                     storm::dd::Bdd<DdType> quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero();
                     storm::dd::Bdd<DdType> deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(model.getColumnVariables()) && reachableStates;
@@ -1136,7 +1136,7 @@ namespace storm {
                         quotientRewardModels.emplace(rewardModelName, storm::models::symbolic::StandardRewardModel<DdType, ValueType>(quotientStateRewards, quotientStateActionRewards, boost::none));
                     }
                     end = std::chrono::high_resolution_clock::now();
-                    STORM_LOG_TRACE("Reward models extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+                    STORM_LOG_INFO("Reward models extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
                     
                     if (modelType == storm::models::ModelType::Dtmc) {
                         return std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>>(new storm::models::symbolic::Dtmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, quotientRewardModels));

src/storm/utility/dd.cpp

@@ -47,7 +47,7 @@ namespace storm {
             
             template <storm::dd::DdType Type>
             storm::dd::Bdd<Type> getRowColumnDiagonal(storm::dd::DdManager<Type> const& ddManager, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) {
-                return ddManager.getIdentity(rowColumnMetaVariablePairs);
+                return ddManager.getIdentity(rowColumnMetaVariablePairs, false);
             }
             
             template storm::dd::Bdd<storm::dd::DdType::CUDD> computeReachableStates(storm::dd::Bdd<storm::dd::DdType::CUDD> const& initialStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitions, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables);

src/test/storm/storage/CuddDdTest.cpp

@@ -607,9 +607,9 @@ TEST(CuddDd, MultiplyMatrixTest2) {
     
     storm::dd::Add<storm::dd::DdType::CUDD, double> r = q.multiplyMatrix(p, {x.first});
     
-    ASSERT_EQ(12, r.getNodeCount());
-    ASSERT_EQ(4, r.getLeafCount());
-    ASSERT_EQ(3, r.getNonZeroCount());
+    ASSERT_EQ(12ull, r.getNodeCount());
+    ASSERT_EQ(4ull, r.getLeafCount());
+    ASSERT_EQ(3ull, r.getNonZeroCount());
 }
 
 TEST(CuddDd, GetSetValueTest) {