diff --git a/CMakeLists.txt b/CMakeLists.txt index e78152e06..f284dae11 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -181,9 +181,15 @@ elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang") set(STORM_COMPILER_ID "AppleClang") set(CMAKE_MACOSX_RPATH ON) elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU") + set(GCC ON) # using GCC if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 5.0) message(FATAL_ERROR "gcc version must be at least 5.0.") + elseif (CMAKE_CXX_COMPILER_VERSION VERSION_EQUAL 7.0 OR CMAKE_CXX_COMPILER_VERSION VERSION_GREATER 7.0) + if (STORM_USE_LTO) + set(STORM_USE_LTO OFF) + message(WARNING "Disabling link-time optimization, because of known incompatibility of LTO with gcc >= 7.") + endif() endif() set(STORM_COMPILER_GCC ON) diff --git a/src/storm/settings/modules/BisimulationSettings.cpp b/src/storm/settings/modules/BisimulationSettings.cpp index 8ed66dbdf..56b3419e9 100644 --- a/src/storm/settings/modules/BisimulationSettings.cpp +++ b/src/storm/settings/modules/BisimulationSettings.cpp @@ -15,6 +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 = "origvars"; const std::string BisimulationSettings::quotientFormatOptionName = "quot"; const std::string BisimulationSettings::signatureModeOptionName = "sigmode"; const std::string BisimulationSettings::reuseOptionName = "reuse"; @@ -29,6 +30,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, quotientFormatOptionName, true, "Sets the format in which the quotient is extracted (only applies to DD-based bisimulation).").addArgument(storm::settings::ArgumentBuilder::createStringArgument("format", "The format of the quotient.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(quotTypes)).setDefaultValueString("dd").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, representativeOptionName, false, "Sets whether to use representatives in the quotient rather than block numbers.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, originalVariablesOptionName, false, "Sets whether to use the original variables in the quotient rather than the block variables.").build()); std::vector signatureModes = { "eager", "lazy" }; this->addOption(storm::settings::OptionBuilder(moduleName, signatureModeOptionName, false, "Sets the signature computation mode.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(signatureModes)).setDefaultValueString("eager").build()).build()); @@ -78,6 +80,10 @@ namespace storm { return this->getOption(representativeOptionName).getHasOptionBeenSet(); } + bool BisimulationSettings::isUseOriginalVariablesSet() const { + return this->getOption(originalVariablesOptionName).getHasOptionBeenSet(); + } + storm::dd::bisimulation::SignatureMode BisimulationSettings::getSignatureMode() const { std::string modeAsString = this->getOption(signatureModeOptionName).getArgumentByName("mode").getValueAsString(); if (modeAsString == "eager") { diff --git a/src/storm/settings/modules/BisimulationSettings.h b/src/storm/settings/modules/BisimulationSettings.h index a482263bc..eb9627f68 100644 --- a/src/storm/settings/modules/BisimulationSettings.h +++ b/src/storm/settings/modules/BisimulationSettings.h @@ -56,6 +56,13 @@ namespace storm { */ bool isUseRepresentativesSet() const; + /*! + * Retrieves whether the extracted quotient model is supposed to use the same variables as the original + * model. + * NOTE: only applies to DD-based bisimulation. + */ + bool isUseOriginalVariablesSet() const; + /*! * Retrieves the mode to compute signatures. */ @@ -85,6 +92,7 @@ namespace storm { // Define the string names of the options as constants. static const std::string typeOptionName; static const std::string representativeOptionName; + static const std::string originalVariablesOptionName; static const std::string quotientFormatOptionName; static const std::string signatureModeOptionName; static const std::string reuseOptionName; 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/Add.cpp b/src/storm/storage/dd/Add.cpp index 635d16aed..9e91b2123 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -231,6 +231,46 @@ namespace storm { return Add(this->getDdManager(), internalAdd.swapVariables(fromBdds, toBdds), newContainedMetaVariables); } + template + Add Add::renameVariablesAbstract(std::set const& from, std::set const& to) const { + std::vector> fromBdds; + std::vector> toBdds; + + for (auto const& metaVariable : from) { + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename variable '" << metaVariable.getName() << "' that is not present."); + DdMetaVariable const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable); + for (auto const& ddVariable : ddMetaVariable.getDdVariables()) { + fromBdds.push_back(ddVariable.getInternalBdd()); + } + } + std::sort(fromBdds.begin(), fromBdds.end(), [] (InternalBdd const& a, InternalBdd const& b) { return a.getLevel() < b.getLevel(); } ); + for (auto const& metaVariable : to) { + STORM_LOG_THROW(!this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename to variable '" << metaVariable.getName() << "' that is already present."); + DdMetaVariable const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable); + for (auto const& ddVariable : ddMetaVariable.getDdVariables()) { + toBdds.push_back(ddVariable.getInternalBdd()); + } + } + std::sort(toBdds.begin(), toBdds.end(), [] (InternalBdd const& a, InternalBdd const& b) { return a.getLevel() < b.getLevel(); } ); + + std::set newContainedMetaVariables = to; + std::set_difference(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), from.begin(), from.end(), std::inserter(newContainedMetaVariables, newContainedMetaVariables.begin())); + + STORM_LOG_ASSERT(fromBdds.size() >= toBdds.size(), "Unable to perform rename-abstract with mismatching sizes."); + + if (fromBdds.size() == toBdds.size()) { + return Add(this->getDdManager(), internalAdd.permuteVariables(fromBdds, toBdds), newContainedMetaVariables); + } else { + InternalBdd cube = this->getDdManager().getBddOne().getInternalBdd(); + for (uint64_t index = toBdds.size(); index < fromBdds.size(); ++index) { + cube &= fromBdds[index]; + } + fromBdds.resize(toBdds.size()); + + return Add(this->getDdManager(), internalAdd.sumAbstract(cube).permuteVariables(fromBdds, toBdds), newContainedMetaVariables); + } + } + template Add Add::swapVariables(std::vector> const& metaVariablePairs) const { std::set newContainedMetaVariables; diff --git a/src/storm/storage/dd/Add.h b/src/storm/storage/dd/Add.h index c25b5a8c4..1a4a811d5 100644 --- a/src/storm/storage/dd/Add.h +++ b/src/storm/storage/dd/Add.h @@ -331,6 +331,20 @@ namespace storm { */ Add renameVariables(std::set const& from, std::set const& to) const; + /*! + * Renames the given meta variables in the ADD. The number of the underlying DD variables of the from meta + * variable set needs to be at least as large as the to meta variable set. If the amount of variables coincide, + * this operation coincides with renameVariables. Otherwise, it first abstracts from the superfluous variables + * and then performs the renaming. + * + * @param from The meta variables to be renamed. The current ADD needs to contain all these meta variables. + * @param to The meta variables that are the target of the renaming process. The current ADD must not contain + * any of these meta variables. + * @return The resulting ADD. + */ + Add renameVariablesAbstract(std::set const& from, std::set const& to) const; + + /*! * Swaps the given pairs of meta variables in the ADD. The pairs of meta variables must be guaranteed to have * the same number of underlying ADD variables. diff --git a/src/storm/storage/dd/Bdd.cpp b/src/storm/storage/dd/Bdd.cpp index 66c6d69a7..d17bbd3d4 100644 --- a/src/storm/storage/dd/Bdd.cpp +++ b/src/storm/storage/dd/Bdd.cpp @@ -319,6 +319,46 @@ namespace storm { return Bdd(this->getDdManager(), internalBdd.swapVariables(fromBdds, toBdds), newContainedMetaVariables); } + template + Bdd Bdd::renameVariablesAbstract(std::set const& from, std::set const& to) const { + std::vector> fromBdds; + std::vector> toBdds; + + for (auto const& metaVariable : from) { + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename variable '" << metaVariable.getName() << "' that is not present."); + DdMetaVariable const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable); + for (auto const& ddVariable : ddMetaVariable.getDdVariables()) { + fromBdds.push_back(ddVariable.getInternalBdd()); + } + } + std::sort(fromBdds.begin(), fromBdds.end(), [] (InternalBdd const& a, InternalBdd const& b) { return a.getLevel() < b.getLevel(); } ); + for (auto const& metaVariable : to) { + STORM_LOG_THROW(!this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename to variable '" << metaVariable.getName() << "' that is already present."); + DdMetaVariable const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable); + for (auto const& ddVariable : ddMetaVariable.getDdVariables()) { + toBdds.push_back(ddVariable.getInternalBdd()); + } + } + std::sort(toBdds.begin(), toBdds.end(), [] (InternalBdd const& a, InternalBdd const& b) { return a.getLevel() < b.getLevel(); } ); + + std::set newContainedMetaVariables = to; + std::set_difference(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), from.begin(), from.end(), std::inserter(newContainedMetaVariables, newContainedMetaVariables.begin())); + + STORM_LOG_ASSERT(fromBdds.size() >= toBdds.size(), "Unable to perform rename-abstract with mismatching sizes."); + + if (fromBdds.size() == toBdds.size()) { + return Bdd(this->getDdManager(), internalBdd.swapVariables(fromBdds, toBdds), newContainedMetaVariables); + } else { + InternalBdd cube = this->getDdManager().getBddOne().getInternalBdd(); + for (uint64_t index = toBdds.size(); index < fromBdds.size(); ++index) { + cube &= fromBdds[index]; + } + fromBdds.resize(toBdds.size()); + + return Bdd(this->getDdManager(), internalBdd.existsAbstract(cube).swapVariables(fromBdds, toBdds), newContainedMetaVariables); + } + } + template template Add Bdd::toAdd() const { diff --git a/src/storm/storage/dd/Bdd.h b/src/storm/storage/dd/Bdd.h index 41d6b2b86..c80e6a43b 100644 --- a/src/storm/storage/dd/Bdd.h +++ b/src/storm/storage/dd/Bdd.h @@ -285,6 +285,19 @@ namespace storm { */ Bdd renameVariables(std::set const& from, std::set const& to) const; + /*! + * Renames the given meta variables in the BDD. The number of the underlying DD variables of the from meta + * variable set needs to be at least as large as the to meta variable set. If the amount of variables coincide, + * this operation coincides with renameVariables. Otherwise, it first abstracts from the superfluous variables + * and then performs the renaming. + * + * @param from The meta variables to be renamed. The current ADD needs to contain all these meta variables. + * @param to The meta variables that are the target of the renaming process. The current ADD must not contain + * any of these meta variables. + * @return The resulting ADD. + */ + Bdd renameVariablesAbstract(std::set const& from, std::set const& to) const; + /*! * Retrieves whether this DD represents the constant one function. * diff --git a/src/storm/storage/dd/BisimulationDecomposition.cpp b/src/storm/storage/dd/BisimulationDecomposition.cpp index 386653329..682f5602d 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, signature: " << std::chrono::duration_cast(refiner->getTotalSignatureTime()).count() << "ms, refinement: " << std::chrono::duration_cast(refiner->getTotalRefinementTime()).count() << "ms)."); } 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..129c426c7 100644 --- a/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp @@ -42,12 +42,22 @@ namespace storm { } else { choicePartitionAsBdd = this->choicePartition.asAdd().notZero(); } + + auto signatureStart = std::chrono::high_resolution_clock::now(); Signature stateSignature(choicePartitionAsBdd.existsAbstract(model.getNondeterminismVariables()).template toAdd()); + auto signatureEnd = std::chrono::high_resolution_clock::now(); + this->totalSignatureTime += (signatureEnd - signatureStart); // 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..87af0987b 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp @@ -12,7 +12,7 @@ namespace storm { namespace bisimulation { template - PartitionRefiner::PartitionRefiner(storm::models::symbolic::Model const& model, Partition const& initialStatePartition) : status(Status::Initialized), refinements(0), statePartition(initialStatePartition), signatureComputer(model), signatureRefiner(model.getManager(), statePartition.getBlockVariable(), model.getRowAndNondeterminismVariables(), model.getColumnVariables(), !model.isNondeterministicModel(), model.getNondeterminismVariables()) { + PartitionRefiner::PartitionRefiner(storm::models::symbolic::Model const& model, Partition const& initialStatePartition) : status(Status::Initialized), refinements(0), statePartition(initialStatePartition), signatureComputer(model), signatureRefiner(model.getManager(), statePartition.getBlockVariable(), model.getRowAndNondeterminismVariables(), model.getColumnVariables(), !model.isNondeterministicModel(), model.getNondeterminismVariables()), totalSignatureTime(0), totalRefinementTime(0) { // Intentionally left empty. } @@ -50,7 +50,7 @@ namespace storm { auto signatureEnd = std::chrono::high_resolution_clock::now(); totalSignatureTime += (signatureEnd - signatureStart); STORM_LOG_TRACE("Signature " << refinements << "[" << index << "] DD has " << signature.getSignatureAdd().getNodeCount() << " nodes."); - + auto refinementStart = std::chrono::high_resolution_clock::now(); newPartition = signatureRefiner.refine(oldPartition, signature); auto refinementEnd = std::chrono::high_resolution_clock::now(); @@ -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,11 +78,11 @@ 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 refinementStart = 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."); - + auto refinementEnd = std::chrono::high_resolution_clock::now(); + totalRefinementTime += (refinementEnd - refinementStart); + ++refinements; return newPartition; } @@ -135,6 +135,16 @@ namespace storm { return status; } + template + std::chrono::high_resolution_clock::duration PartitionRefiner::getTotalSignatureTime() const { + return totalSignatureTime; + } + + template + std::chrono::high_resolution_clock::duration PartitionRefiner::getTotalRefinementTime() const { + return totalRefinementTime; + } + template class PartitionRefiner; template class PartitionRefiner; diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.h b/src/storm/storage/dd/bisimulation/PartitionRefiner.h index d4e59a207..4716a811a 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.h +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.h @@ -53,6 +53,9 @@ namespace storm { */ Status getStatus() const; + std::chrono::high_resolution_clock::duration getTotalSignatureTime() const; + std::chrono::high_resolution_clock::duration getTotalRefinementTime() const; + protected: Partition internalRefine(SignatureComputer& stateSignatureComputer, SignatureRefiner& signatureRefiner, Partition const& oldPartition, Partition const& targetPartition, SignatureMode const& mode = SignatureMode::Eager); Partition internalRefine(Signature const& signature, SignatureRefiner& signatureRefiner, Partition const& oldPartition); diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index 340b191fe..593f1491a 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -821,6 +821,7 @@ namespace storm { QuotientExtractor::QuotientExtractor() : useRepresentatives(false) { auto const& settings = storm::settings::getModule(); this->useRepresentatives = settings.isUseRepresentativesSet(); + this->useOriginalVariables = settings.isUseOriginalVariablesSet(); this->quotientFormat = settings.getQuotientFormat(); } @@ -834,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."); @@ -855,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()); @@ -877,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; @@ -897,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) { @@ -921,7 +922,12 @@ namespace storm { template std::shared_ptr> QuotientExtractor::extractDdQuotient(storm::models::symbolic::Model const& model, Partition const& partition, PreservationInformation const& preservationInformation) { - return extractQuotientUsingBlockVariables(model, partition, preservationInformation); + + if (this->useOriginalVariables) { + return extractQuotientUsingOriginalVariables(model, partition, preservationInformation); + } else { + return extractQuotientUsingBlockVariables(model, partition, preservationInformation); + } } template @@ -972,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; @@ -998,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; @@ -1021,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)); @@ -1036,6 +1042,115 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot extract quotient for this model type."); } } + + template + std::shared_ptr> QuotientExtractor::extractQuotientUsingOriginalVariables(storm::models::symbolic::Model const& model, Partition const& partition, PreservationInformation const& preservationInformation) { + auto modelType = model.getType(); + + if (modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Ctmc || modelType == storm::models::ModelType::Mdp || modelType == storm::models::ModelType::MarkovAutomaton) { + STORM_LOG_WARN_COND(!this->useRepresentatives, "Using representatives is unsupported for this extraction, falling back to regular extraction."); + + // Sanity checks. + STORM_LOG_ASSERT(partition.getNumberOfStates() == model.getNumberOfStates(), "Mismatching partition size."); + STORM_LOG_ASSERT(partition.getStates().renameVariables(model.getColumnVariables(), model.getRowVariables()) == model.getReachableStates(), "Mismatching partition."); + + std::set blockVariableSet = {partition.getBlockVariable()}; + std::set blockPrimeVariableSet = {partition.getPrimedBlockVariable()}; + std::vector> blockMetaVariablePairs = {std::make_pair(partition.getBlockVariable(), partition.getPrimedBlockVariable())}; + + storm::dd::Bdd partitionAsBdd = partition.storedAsBdd() ? partition.asBdd() : partition.asAdd().notZero(); + + auto start = std::chrono::high_resolution_clock::now(); + partitionAsBdd = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables()); + storm::dd::Bdd reachableStates = partitionAsBdd.existsAbstract(model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables()); + storm::dd::Bdd initialStates = (model.getInitialStates() && partitionAsBdd).existsAbstract(model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables()); + + std::map> preservedLabelBdds; + for (auto const& label : preservationInformation.getLabels()) { + preservedLabelBdds.emplace(label, (model.getStates(label) && partitionAsBdd).existsAbstract(model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables())); + } + for (auto const& expression : preservationInformation.getExpressions()) { + std::stringstream stream; + stream << expression; + std::string expressionAsString = stream.str(); + + auto it = preservedLabelBdds.find(expressionAsString); + if (it != preservedLabelBdds.end()) { + STORM_LOG_WARN("Duplicate label '" << expressionAsString << "', dropping second label definition."); + } else { + preservedLabelBdds.emplace(stream.str(), (model.getStates(expression) && partitionAsBdd).existsAbstract(model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables())); + } + } + auto end = std::chrono::high_resolution_clock::now(); + 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; + std::set_union(blockVariableSet.begin(), blockVariableSet.end(), model.getRowVariables().begin(), model.getRowVariables().end(), std::inserter(blockAndRowVariables, blockAndRowVariables.end())); + std::set blockPrimeAndColumnVariables; + std::set_union(blockPrimeVariableSet.begin(), blockPrimeVariableSet.end(), model.getColumnVariables().begin(), model.getColumnVariables().end(), std::inserter(blockPrimeAndColumnVariables, blockPrimeAndColumnVariables.end())); + storm::dd::Add partitionAsAdd = partitionAsBdd.template toAdd(); + storm::dd::Add quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(model.getRowVariables(), model.getColumnVariables()), model.getColumnVariables()).renameVariablesAbstract(blockVariableSet, model.getColumnVariables()); + + // Pick a representative from each block. + auto representatives = InternalRepresentativeComputer(partitionAsBdd, model.getRowVariables()).getRepresentatives(); + partitionAsBdd &= representatives; + partitionAsAdd = partitionAsBdd.template toAdd(); + + // Workaround for problem with CUDD. Matrix-Matrix multiplication yields other result than multiplication+sum-abstract... + if (DdType == storm::dd::DdType::CUDD) { + quotientTransitionMatrix = (quotientTransitionMatrix * partitionAsAdd).sumAbstract(model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables()); + } else { + quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables()); + } + end = std::chrono::high_resolution_clock::now(); + + // Check quotient matrix for sanity. + if (std::is_same::value) { + STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one()).isZero(), "Illegal entries in quotient matrix."); + } else { + STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one() + storm::utility::convertNumber(1e-6)).isZero(), "Illegal entries in quotient matrix."); + } + 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_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; + + start = std::chrono::high_resolution_clock::now(); + std::unordered_map> quotientRewardModels; + for (auto const& rewardModelName : preservationInformation.getRewardModelNames()) { + auto const& rewardModel = model.getRewardModel(rewardModelName); + + boost::optional> quotientStateRewards; + if (rewardModel.hasStateRewards()) { + quotientStateRewards = rewardModel.getStateRewardVector().multiplyMatrix(partitionAsAdd, model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables()); + } + + boost::optional> quotientStateActionRewards; + if (rewardModel.hasStateActionRewards()) { + quotientStateActionRewards = rewardModel.getStateActionRewardVector().multiplyMatrix(partitionAsAdd, model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables()); + } + + quotientRewardModels.emplace(rewardModelName, storm::models::symbolic::StandardRewardModel(quotientStateRewards, quotientStateActionRewards, boost::none)); + } + end = std::chrono::high_resolution_clock::now(); + 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)); + } else if (modelType == storm::models::ModelType::Ctmc) { + return std::shared_ptr>(new storm::models::symbolic::Ctmc(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, quotientRewardModels)); + } else if (modelType == storm::models::ModelType::Mdp) { + return std::shared_ptr>(new storm::models::symbolic::Mdp(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels)); + } else { + return std::shared_ptr>(new storm::models::symbolic::MarkovAutomaton(model.getManager().asSharedPointer(), model. template as>()->getMarkovianMarker(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels)); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot extract quotient for this model type."); + } + } template class QuotientExtractor; diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.h b/src/storm/storage/dd/bisimulation/QuotientExtractor.h index dcce31659..b75b27b08 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.h +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.h @@ -28,8 +28,10 @@ namespace storm { std::shared_ptr> extractDdQuotient(storm::models::symbolic::Model const& model, Partition const& partition, PreservationInformation const& preservationInformation); std::shared_ptr> extractQuotientUsingBlockVariables(storm::models::symbolic::Model const& model, Partition const& partition, PreservationInformation const& preservationInformation); - + std::shared_ptr> extractQuotientUsingOriginalVariables(storm::models::symbolic::Model const& model, Partition const& partition, PreservationInformation const& preservationInformation); + bool useRepresentatives; + bool useOriginalVariables; storm::settings::modules::BisimulationSettings::QuotientFormat quotientFormat; }; diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h index dc65e240a..5137caf15 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h @@ -319,7 +319,7 @@ namespace storm { * @return The resulting ADD. */ InternalAdd swapVariables(std::vector> const& from, std::vector> const& to) const; - + /*! * Permutes the given pairs of DD variables in the ADD. The pairs of meta variables have to be represented by * ADDs must have equal length. 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 499be2a12..c1ae09561 100644 --- a/src/test/storm/storage/CuddDdTest.cpp +++ b/src/test/storm/storage/CuddDdTest.cpp @@ -589,6 +589,29 @@ TEST(CuddDd, MultiplyMatrixTest) { EXPECT_TRUE(dd3 == dd2 * manager->template getConstant(2)); } +TEST(CuddDd, MultiplyMatrixTest2) { + std::shared_ptr> manager(new storm::dd::DdManager()); + std::pair x = manager->addMetaVariable("x", 0, 2); + std::pair b = manager->addMetaVariable("b", 0, 2); + + storm::dd::Add p = manager->getAddZero(); + p += (manager->getEncoding(x.first, 2, true) && manager->getEncoding(b.first, 0, true)).template toAdd(); + p += (manager->getEncoding(x.first, 0, true) && manager->getEncoding(b.first, 2, true)).template toAdd(); + + storm::dd::Add q = manager->getAddZero(); + q += (manager->getEncoding(x.first, 0, true) && manager->getEncoding(x.second, 0, true)).template toAdd() * manager->template getConstant(0.3); + q += (manager->getEncoding(x.first, 1, true) && manager->getEncoding(x.second, 0, true)).template toAdd() * manager->template getConstant(0.3); + q += (manager->getEncoding(x.first, 0, true) && manager->getEncoding(x.second, 2, true)).template toAdd() * manager->template getConstant(0.7); + q += (manager->getEncoding(x.first, 1, true) && manager->getEncoding(x.second, 2, true)).template toAdd() * manager->template getConstant(0.7); + q += (manager->getEncoding(x.first, 2, true) && manager->getEncoding(x.second, 0, true)).template toAdd() * manager->template getConstant(1); + + storm::dd::Add r = q.multiplyMatrix(p, {x.first}); + + ASSERT_EQ(12ull, r.getNodeCount()); + ASSERT_EQ(4ull, r.getLeafCount()); + ASSERT_EQ(3ull, r.getNonZeroCount()); +} + TEST(CuddDd, GetSetValueTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x = manager->addMetaVariable("x", 1, 9);