From 34b6593ed86f241466f0758ea07e484f6a033488 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 1 Mar 2018 22:09:06 +0100 Subject: [PATCH] overhauled output of dd-based bisimulation for benchmarking --- .../settings/modules/BisimulationSettings.cpp | 2 +- .../SymbolicNativeLinearEquationSolver.cpp | 2 +- .../storage/dd/BisimulationDecomposition.cpp | 47 +++++++++---------- .../storage/dd/BisimulationDecomposition.h | 2 +- .../NondeterministicModelPartitionRefiner.cpp | 11 ++++- .../storage/dd/bisimulation/Partition.cpp | 10 +++- .../dd/bisimulation/PartitionRefiner.cpp | 5 +- .../dd/bisimulation/QuotientExtractor.cpp | 20 ++++---- src/storm/utility/dd.cpp | 2 +- src/test/storm/storage/CuddDdTest.cpp | 6 +-- 10 files changed, 59 insertions(+), 48 deletions(-) diff --git a/src/storm/settings/modules/BisimulationSettings.cpp b/src/storm/settings/modules/BisimulationSettings.cpp index 491958105..56b3419e9 100644 --- a/src/storm/settings/modules/BisimulationSettings.cpp +++ b/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"; diff --git a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp index 4252b1483..7c25f0e35 100644 --- a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp @@ -88,7 +88,7 @@ namespace storm { storm::dd::Add lu = diagonal.ite(manager.template getAddZero(), this->A); storm::dd::Add diagonalAdd = diagonal.template toAdd(); storm::dd::Add diag = diagonalAdd.multiplyMatrix(this->A, this->columnMetaVariables); - + storm::dd::Add scaledLu = lu / diag; storm::dd::Add scaledB = b / diag; diff --git a/src/storm/storage/dd/BisimulationDecomposition.cpp b/src/storm/storage/dd/BisimulationDecomposition.cpp index 386653329..b19142b1d 100644 --- a/src/storm/storage/dd/BisimulationDecomposition.cpp +++ b/src/storm/storage/dd/BisimulationDecomposition.cpp @@ -57,14 +57,16 @@ namespace storm { template void BisimulationDecomposition::initialize() { auto const& generalSettings = storm::settings::getModule(); - 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(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 @@ -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(now - timeOfLastMessage).count(); - if (static_cast(durationSinceLastMessage) >= showProgressDelay) { - auto durationSinceStart = std::chrono::duration_cast(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(now - timeOfLastMessage).count(); + if (static_cast(durationSinceLastMessage) >= showProgressDelay * 1000 || verboseProgress) { + auto durationSinceStart = std::chrono::duration_cast(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(end - start).count() << "ms (" << iterations << " iterations)."); + STORM_LOG_INFO("Partition refinement completed in " << std::chrono::duration_cast(end - start).count() << "ms (" << iterations << " iterations)."); } template @@ -112,14 +111,12 @@ namespace storm { ++iterations; - if (showProgress) { - auto now = std::chrono::high_resolution_clock::now(); - auto durationSinceLastMessage = std::chrono::duration_cast(now - timeOfLastMessage).count(); - if (static_cast(durationSinceLastMessage) >= showProgressDelay) { - auto durationSinceStart = std::chrono::duration_cast(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(now - timeOfLastMessage).count(); + if (static_cast(durationSinceLastMessage) >= showProgressDelay || verboseProgress) { + auto durationSinceStart = std::chrono::duration_cast(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> BisimulationDecomposition::getQuotient() const { std::shared_ptr> quotient; if (this->refiner->getStatus() == Status::FixedPoint) { - STORM_LOG_TRACE("Starting full quotient extraction."); + STORM_LOG_INFO("Starting full quotient extraction."); QuotientExtractor 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>(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; } diff --git a/src/storm/storage/dd/BisimulationDecomposition.h b/src/storm/storage/dd/BisimulationDecomposition.h index 21ff7de2a..b5a088ca2 100644 --- a/src/storm/storage/dd/BisimulationDecomposition.h +++ b/src/storm/storage/dd/BisimulationDecomposition.h @@ -83,7 +83,7 @@ namespace storm { mutable std::unique_ptr> partialQuotientExtractor; // A flag indicating whether progress is reported. - bool showProgress; + bool verboseProgress; // The delay between progress reports. uint64_t showProgressDelay; diff --git a/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp index 67fd21e8c..1bf58a5ad 100644 --- a/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp @@ -42,12 +42,21 @@ namespace storm { } else { choicePartitionAsBdd = this->choicePartition.asAdd().notZero(); } - Signature stateSignature(choicePartitionAsBdd.existsAbstract(model.getNondeterminismVariables()).template toAdd()); + auto signatureStart = std::chrono::high_resolution_clock::now(); + Signature stateSignature(choicePartitionAsBdd.existsAbstract(model.getNondeterminismVariables()).template toAdd()); + 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 newStatePartition = this->internalRefine(stateSignature, this->stateSignatureRefiner, this->statePartition); + auto refinementEnd = std::chrono::high_resolution_clock::now(); + auto signatureTime = std::chrono::duration_cast(signatureEnd - signatureStart).count(); + auto refinementTime = std::chrono::duration_cast(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; diff --git a/src/storm/storage/dd/bisimulation/Partition.cpp b/src/storm/storage/dd/bisimulation/Partition.cpp index d3708c6a5..6ada72f6b 100644 --- a/src/storm/storage/dd/bisimulation/Partition.cpp +++ b/src/storm/storage/dd/bisimulation/Partition.cpp @@ -130,6 +130,8 @@ namespace storm { std::pair blockVariables = createBlockVariables(model); + auto start = std::chrono::high_resolution_clock::now(); + // Set up the construction. storm::dd::DdManager& manager = model.getManager(); storm::dd::Bdd 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(end - start).count() << "ms."); + // Store the partition as an ADD only in the case of CUDD. if (DdType == storm::dd::DdType::CUDD) { return Partition(partitionBdd.template toAdd(), 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, 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(end - start).count() << "ms."); + // Store the partition as an ADD only in the case of CUDD. if (DdType == storm::dd::DdType::CUDD) { return Partition(partitionBddAndBlockCount.first.template toAdd(), blockVariables, partitionBddAndBlockCount.second, partitionBddAndBlockCount.second); diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp index 476bd5285..94a6d3666 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp @@ -66,7 +66,7 @@ namespace storm { } auto totalTimeInRefinement = std::chrono::duration_cast(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 PartitionRefiner::internalRefine(Signature const& signature, SignatureRefiner& signatureRefiner, Partition 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::high_resolution_clock::now() - start).count(); - STORM_LOG_TRACE("Refinement " << refinements << " produced " << newPartition.getNumberOfBlocks() << " blocks and was completed in " << totalTimeInRefinement << "ms."); ++refinements; return newPartition; diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index e28c80aaa..593f1491a 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/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(end - start).count() << "ms."); + STORM_LOG_INFO("Quotient extraction completed in " << std::chrono::duration_cast(end - start).count() << "ms."); STORM_LOG_THROW(result, storm::exceptions::NotSupportedException, "Quotient could not be extracted."); @@ -856,7 +856,7 @@ namespace storm { InternalSparseQuotientExtractor sparseExtractor(model, partitionAsBdd, partition.getBlockVariable(), partition.getNumberOfBlocks(), representatives); storm::storage::SparseMatrix 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(end - start).count() << "ms."); + STORM_LOG_INFO("Quotient transition matrix extracted in " << std::chrono::duration_cast(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(end - start).count() << "ms."); + STORM_LOG_INFO("Quotient labels extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); start = std::chrono::high_resolution_clock::now(); std::unordered_map> quotientRewardModels; @@ -898,7 +898,7 @@ namespace storm { quotientRewardModels.emplace(rewardModelName, storm::models::sparse::StandardRewardModel(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(end - start).count() << "ms."); + STORM_LOG_INFO("Reward models extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); std::shared_ptr> 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(end - start).count() << "ms."); + STORM_LOG_INFO("Quotient labels extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); start = std::chrono::high_resolution_clock::now(); std::set blockAndRowVariables; @@ -1004,7 +1004,7 @@ namespace storm { } STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).equalModuloPrecision(quotientTransitionMatrix.notZero().existsAbstract(blockPrimeVariableSet).template toAdd(), storm::utility::convertNumber(1e-6)), "Illegal non-probabilistic matrix."); - STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); + STORM_LOG_INFO("Quotient transition matrix extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); storm::dd::Bdd quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero(); storm::dd::Bdd deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(blockPrimeVariableSet) && reachableStates; @@ -1027,7 +1027,7 @@ namespace storm { quotientRewardModels.emplace(rewardModelName, storm::models::symbolic::StandardRewardModel(quotientStateRewards, quotientStateActionRewards, boost::none)); } end = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Reward models extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); + STORM_LOG_INFO("Reward models extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); if (modelType == storm::models::ModelType::Dtmc) { return std::shared_ptr>(new storm::models::symbolic::Dtmc(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(end - start).count() << "ms."); + STORM_LOG_INFO("Quotient labels extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); start = std::chrono::high_resolution_clock::now(); std::set blockAndRowVariables; @@ -1113,7 +1113,7 @@ namespace storm { } STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(model.getColumnVariables()).equalModuloPrecision(quotientTransitionMatrix.notZero().existsAbstract(model.getColumnVariables()).template toAdd(), storm::utility::convertNumber(1e-6)), "Illegal probabilistic matrix."); - STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); + STORM_LOG_INFO("Quotient transition matrix extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); storm::dd::Bdd quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero(); storm::dd::Bdd deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(model.getColumnVariables()) && reachableStates; @@ -1136,7 +1136,7 @@ namespace storm { quotientRewardModels.emplace(rewardModelName, storm::models::symbolic::StandardRewardModel(quotientStateRewards, quotientStateActionRewards, boost::none)); } end = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Reward models extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); + STORM_LOG_INFO("Reward models extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); if (modelType == storm::models::ModelType::Dtmc) { return std::shared_ptr>(new storm::models::symbolic::Dtmc(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, quotientRewardModels)); diff --git a/src/storm/utility/dd.cpp b/src/storm/utility/dd.cpp index 47d15347e..626dc845f 100644 --- a/src/storm/utility/dd.cpp +++ b/src/storm/utility/dd.cpp @@ -47,7 +47,7 @@ namespace storm { template storm::dd::Bdd getRowColumnDiagonal(storm::dd::DdManager const& ddManager, std::vector> const& rowColumnMetaVariablePairs) { - return ddManager.getIdentity(rowColumnMetaVariablePairs); + return ddManager.getIdentity(rowColumnMetaVariablePairs, false); } template storm::dd::Bdd computeReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables); diff --git a/src/test/storm/storage/CuddDdTest.cpp b/src/test/storm/storage/CuddDdTest.cpp index bc6ffab10..c1ae09561 100644 --- a/src/test/storm/storage/CuddDdTest.cpp +++ b/src/test/storm/storage/CuddDdTest.cpp @@ -607,9 +607,9 @@ TEST(CuddDd, MultiplyMatrixTest2) { storm::dd::Add 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) {