diff --git a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp index d1ec80394..976006cf6 100644 --- a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp @@ -61,19 +61,17 @@ namespace storm { STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException, "The game-based abstraction refinement model checker can only compute the result for the initial states."); // Create the appropriate preservation information. - storm::dd::bisimulation::PreservationInformation preservationInformation(model, storm::storage::BisimulationType::Strong); - if (checkTask.isRewardModelSet()) { - if (checkTask.getRewardModel() != "" || model.hasRewardModel(checkTask.getRewardModel())) { - preservationInformation.addRewardModel(checkTask.getRewardModel()); - } else if (model.hasUniqueRewardModel()) { + storm::dd::bisimulation::PreservationInformation preservationInformation(model, {checkTask.getFormula().asSharedPointer()}); + if (rewards) { + if (!checkTask.isRewardModelSet() || model.hasUniqueRewardModel()) { preservationInformation.addRewardModel(model.getUniqueRewardModelName()); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Property refers to illegal reward model '" << checkTask.getRewardModel() << "'."); + } else if (checkTask.isRewardModelSet()) { + preservationInformation.addRewardModel(checkTask.getRewardModel()); } } // Create a bisimulation object that is used to obtain (partial) quotients. - storm::dd::BisimulationDecomposition bisimulation(this->model, {checkTask.getFormula().asSharedPointer()}, storm::storage::BisimulationType::Strong); + storm::dd::BisimulationDecomposition bisimulation(this->model, storm::storage::BisimulationType::Strong, preservationInformation); auto start = std::chrono::high_resolution_clock::now(); @@ -124,20 +122,17 @@ namespace storm { if (lowerBounds.getStates().getNonZeroCount() == 1 && upperBounds.getStates().getNonZeroCount() == 1) { STORM_LOG_TRACE("Obtained bounds [" << lowerBounds.getValueVector().getMax() << ", " << upperBounds.getValueVector().getMax() << "] on actual result."); } else { - STORM_LOG_TRACE("Largest difference over initial states is " << getLargestDifference(bounds) << "."); + storm::dd::Add diffs = upperBounds.getValueVector() - lowerBounds.getValueVector(); + storm::dd::Bdd maxDiffRepresentative = diffs.maxAbstractRepresentative(diffs.getContainedMetaVariables()); + + std::pair bounds; + bounds.first = (lowerBounds.getValueVector() * maxDiffRepresentative.template toAdd()).getMax(); + bounds.second = (upperBounds.getValueVector() * maxDiffRepresentative.template toAdd()).getMax(); + + STORM_LOG_TRACE("Largest interval over initial is [" << bounds.first << ", " << bounds.second << "], difference " << (bounds.second - bounds.first) << "."); } } - template - typename PartialBisimulationMdpModelChecker::ValueType PartialBisimulationMdpModelChecker::getLargestDifference(std::pair, std::unique_ptr> const& bounds) { - STORM_LOG_THROW(bounds.first->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result."); - storm::modelchecker::SymbolicQuantitativeCheckResult const& lowerBounds = bounds.first->asSymbolicQuantitativeCheckResult(); - STORM_LOG_THROW(bounds.second->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result."); - storm::modelchecker::SymbolicQuantitativeCheckResult const& upperBounds = bounds.second->asSymbolicQuantitativeCheckResult(); - - return (upperBounds.getValueVector() - lowerBounds.getValueVector()).getMax(); - } - template bool PartialBisimulationMdpModelChecker::checkBoundsSufficientlyClose(std::pair, std::unique_ptr> const& bounds) { STORM_LOG_THROW(bounds.first->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result."); @@ -174,15 +169,17 @@ namespace storm { } else { result.first = checker.computeProbabilities(newCheckTask); } + STORM_LOG_ASSERT(result.first, "Expected result."); result.first->asSymbolicQuantitativeCheckResult().getValueVector().exportToDot("lower_values" + std::to_string(i) + ".dot"); result.first->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotient.getReachableStates(), quotient.getInitialStates())); newCheckTask.setOptimizationDirection(storm::OptimizationDirection::Maximize); if (rewards) { - result.first = checker.computeRewards(storm::logic::RewardMeasureType::Expectation, newCheckTask); + result.second = checker.computeRewards(storm::logic::RewardMeasureType::Expectation, newCheckTask); } else { result.second = checker.computeProbabilities(newCheckTask); } + STORM_LOG_ASSERT(result.second, "Expected result."); result.first->asSymbolicQuantitativeCheckResult().getValueVector().exportToDot("upper_values" + std::to_string(i++) + ".dot"); result.second->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotient.getReachableStates(), quotient.getInitialStates())); diff --git a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h index dacdb4be5..3fa6f0c03 100644 --- a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h +++ b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h @@ -52,7 +52,6 @@ namespace storm { bool checkBoundsSufficientlyClose(std::pair, std::unique_ptr> const& bounds); std::unique_ptr getAverageOfBounds(std::pair, std::unique_ptr> const& bounds); void printBoundsInformation(std::pair, std::unique_ptr> const& bounds); - ValueType getLargestDifference(std::pair, std::unique_ptr> const& bounds); // Methods to compute bounds on the partial quotient. std::pair, std::unique_ptr> computeBoundsPartialQuotient(storm::models::symbolic::Mdp const& quotient, bool rewards, CheckTask const& checkTask); diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index fb68a1a0e..4835019d4 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -121,7 +121,7 @@ namespace storm { } AbstractionSettings::ReuseMode AbstractionSettings::getReuseMode() const { - std::string reuseModeAsString = this->getOption(splitModeOptionName).getArgumentByName("mode").getValueAsString(); + std::string reuseModeAsString = this->getOption(reuseResultsOptionName).getArgumentByName("mode").getValueAsString(); if (reuseModeAsString == "all") { return ReuseMode::All; } else if (reuseModeAsString == "none") { diff --git a/src/storm/settings/modules/BisimulationSettings.cpp b/src/storm/settings/modules/BisimulationSettings.cpp index 679daa54d..ee9c6165b 100644 --- a/src/storm/settings/modules/BisimulationSettings.cpp +++ b/src/storm/settings/modules/BisimulationSettings.cpp @@ -17,6 +17,7 @@ namespace storm { const std::string BisimulationSettings::representativeOptionName = "repr"; const std::string BisimulationSettings::quotientFormatOptionName = "quot"; const std::string BisimulationSettings::signatureModeOptionName = "sigmode"; + const std::string BisimulationSettings::reuseOptionName = "reuse"; BisimulationSettings::BisimulationSettings() : ModuleSettings(moduleName) { std::vector types = { "strong", "weak" }; @@ -29,6 +30,12 @@ namespace storm { 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()); + + std::vector reuseModes = {"all", "none", "blocks", "sig"}; + this->addOption(storm::settings::OptionBuilder(moduleName, reuseOptionName, true, "Sets whether to reuse all results.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(reuseModes)) + .setDefaultValueString("blocks").build()) + .build()); } bool BisimulationSettings::isStrongBisimulationSet() const { @@ -67,6 +74,20 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unknown signature mode '" << modeAsString << "."); } + BisimulationSettings::ReuseMode BisimulationSettings::getReuseMode() const { + std::string reuseModeAsString = this->getOption(reuseOptionName).getArgumentByName("mode").getValueAsString(); + if (reuseModeAsString == "all") { + return ReuseMode::All; + } else if (reuseModeAsString == "none") { + return ReuseMode::None; + } else if (reuseModeAsString == "blocks") { + return ReuseMode::BlockNumbers; + } else if (reuseModeAsString == "sig") { + return ReuseMode::SignatureResults; + } + return ReuseMode::All; + } + bool BisimulationSettings::check() const { bool optionsSet = this->getOption(typeOptionName).getHasOptionBeenSet(); STORM_LOG_WARN_COND(storm::settings::getModule().isBisimulationSet() || !optionsSet, "Bisimulation minimization is not selected, so setting options for bisimulation has no effect."); diff --git a/src/storm/settings/modules/BisimulationSettings.h b/src/storm/settings/modules/BisimulationSettings.h index 0d71baa86..e0678ea71 100644 --- a/src/storm/settings/modules/BisimulationSettings.h +++ b/src/storm/settings/modules/BisimulationSettings.h @@ -19,6 +19,8 @@ namespace storm { enum class QuotientFormat { Sparse, Dd }; + enum class ReuseMode { All, None, BlockNumbers, SignatureResults }; + /*! * Creates a new set of bisimulation settings. */ @@ -55,6 +57,11 @@ namespace storm { */ storm::dd::bisimulation::SignatureMode getSignatureMode() const; + /*! + * Retrieves the selected reuse mode. + */ + ReuseMode getReuseMode() const; + virtual bool check() const override; // The name of the module. @@ -66,6 +73,7 @@ namespace storm { static const std::string representativeOptionName; static const std::string quotientFormatOptionName; static const std::string signatureModeOptionName; + static const std::string reuseOptionName; }; } // namespace modules } // namespace settings diff --git a/src/storm/storage/dd/BisimulationDecomposition.cpp b/src/storm/storage/dd/BisimulationDecomposition.cpp index 2ee9088e0..5a1f0622e 100644 --- a/src/storm/storage/dd/BisimulationDecomposition.cpp +++ b/src/storm/storage/dd/BisimulationDecomposition.cpp @@ -32,7 +32,7 @@ namespace storm { } template - BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, bisimulationType), refiner(createRefiner(model, Partition::create(model, bisimulationType, preservationInformation))) { + BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model), refiner(createRefiner(model, Partition::create(model, bisimulationType, preservationInformation))) { this->initialize(); } @@ -42,7 +42,7 @@ namespace storm { } template - BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model, std::vector> const& formulas, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, formulas, bisimulationType), refiner(createRefiner(model, Partition::create(model, bisimulationType, preservationInformation))) { + BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model, std::vector> const& formulas, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, formulas), refiner(createRefiner(model, Partition::create(model, bisimulationType, preservationInformation))) { this->initialize(); } diff --git a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp index d6ee3b41e..c78bc8d78 100644 --- a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp @@ -23,7 +23,7 @@ namespace storm { STORM_LOG_TRACE("Refining choice partition."); Partition newChoicePartition = this->internalRefine(this->signatureComputer, this->signatureRefiner, this->choicePartition, this->statePartition, mode); - if (newChoicePartition == choicePartition) { + if (newChoicePartition.getNumberOfBlocks() == choicePartition.getNumberOfBlocks()) { this->status = Status::FixedPoint; return false; } else { diff --git a/src/storm/storage/dd/bisimulation/Partition.cpp b/src/storm/storage/dd/bisimulation/Partition.cpp index a923c199c..79a0d007a 100644 --- a/src/storm/storage/dd/bisimulation/Partition.cpp +++ b/src/storm/storage/dd/bisimulation/Partition.cpp @@ -28,28 +28,28 @@ namespace storm { } template - Partition::Partition(storm::dd::Add const& partitionAdd, std::pair const& blockVariables, uint64_t nextFreeBlockIndex) : partition(partitionAdd), blockVariables(blockVariables), nextFreeBlockIndex(nextFreeBlockIndex) { + Partition::Partition(storm::dd::Add const& partitionAdd, std::pair const& blockVariables, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex) : partition(partitionAdd), blockVariables(blockVariables), numberOfBlocks(numberOfBlocks), nextFreeBlockIndex(nextFreeBlockIndex) { // Intentionally left empty. } template - Partition::Partition(storm::dd::Bdd const& partitionBdd, std::pair const& blockVariables, uint64_t nextFreeBlockIndex) : partition(partitionBdd), blockVariables(blockVariables), nextFreeBlockIndex(nextFreeBlockIndex) { + Partition::Partition(storm::dd::Bdd const& partitionBdd, std::pair const& blockVariables, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex) : partition(partitionBdd), blockVariables(blockVariables), numberOfBlocks(numberOfBlocks), nextFreeBlockIndex(nextFreeBlockIndex) { // Intentionally left empty. } template bool Partition::operator==(Partition const& other) { - return this->partition == other.partition && this->blockVariables == other.blockVariables && this->nextFreeBlockIndex == other.nextFreeBlockIndex; + return this->partition == other.partition && this->blockVariables == other.blockVariables && this->numberOfBlocks == other.numberOfBlocks && this->nextFreeBlockIndex == other.nextFreeBlockIndex; } template - Partition Partition::replacePartition(storm::dd::Add const& newPartitionAdd, uint64_t nextFreeBlockIndex) const { - return Partition(newPartitionAdd, blockVariables, nextFreeBlockIndex); + Partition Partition::replacePartition(storm::dd::Add const& newPartitionAdd, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex) const { + return Partition(newPartitionAdd, blockVariables, numberOfBlocks, nextFreeBlockIndex); } template - Partition Partition::replacePartition(storm::dd::Bdd const& newPartitionBdd, uint64_t nextFreeBlockIndex) const { - return Partition(newPartitionBdd, blockVariables, nextFreeBlockIndex); + Partition Partition::replacePartition(storm::dd::Bdd const& newPartitionBdd, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex) const { + return Partition(newPartitionBdd, blockVariables, numberOfBlocks, nextFreeBlockIndex); } template @@ -92,9 +92,9 @@ namespace storm { // 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); + return Partition(partitionBddAndBlockCount.first.template toAdd(), blockVariables, partitionBddAndBlockCount.second, partitionBddAndBlockCount.second); } else { - return Partition(partitionBddAndBlockCount.first, blockVariables, partitionBddAndBlockCount.second); + return Partition(partitionBddAndBlockCount.first, blockVariables, partitionBddAndBlockCount.second, partitionBddAndBlockCount.second); } } @@ -104,9 +104,9 @@ namespace storm { // Store the partition as an ADD only in the case of CUDD. if (DdType == storm::dd::DdType::CUDD) { - return Partition(choicePartitionBdd.template toAdd(), blockVariables, 1); + return Partition(choicePartitionBdd.template toAdd(), blockVariables, 1, 1); } else { - return Partition(choicePartitionBdd, blockVariables, 1); + return Partition(choicePartitionBdd, blockVariables, 1, 1); } } @@ -126,7 +126,7 @@ namespace storm { template uint64_t Partition::getNumberOfBlocks() const { - return nextFreeBlockIndex; + return numberOfBlocks; } template diff --git a/src/storm/storage/dd/bisimulation/Partition.h b/src/storm/storage/dd/bisimulation/Partition.h index 3a620e681..394d6dfa8 100644 --- a/src/storm/storage/dd/bisimulation/Partition.h +++ b/src/storm/storage/dd/bisimulation/Partition.h @@ -31,8 +31,8 @@ namespace storm { bool operator==(Partition const& other); - Partition replacePartition(storm::dd::Add const& newPartitionAdd, uint64_t nextFreeBlockIndex) const; - Partition replacePartition(storm::dd::Bdd const& newPartitionBdd, uint64_t nextFreeBlockIndex) const; + Partition replacePartition(storm::dd::Add const& newPartitionAdd, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex) const; + Partition replacePartition(storm::dd::Bdd const& newPartitionBdd, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex) const; static Partition create(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType, PreservationInformation const& preservationInformation); static Partition createTrivialChoicePartition(storm::models::symbolic::NondeterministicModel const& model, std::pair const& blockVariables); @@ -63,10 +63,10 @@ namespace storm { * one iff the state is in the block. * @param blockVariables The variables to use for the block encoding. Its range must be [0, x] where x is * greater or equal than the number of states in the partition. - * @param nextFreeBlockIndex The next free block index. The existing blocks must be encoded with indices - * between 0 and this number. + * @param numberOfBlocks The number of blocks in this partition. + * @param nextFreeBlockIndex The next free block index. */ - Partition(storm::dd::Add const& partitionAdd, std::pair const& blockVariables, uint64_t nextFreeBlockIndex); + Partition(storm::dd::Add const& partitionAdd, std::pair const& blockVariables, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex); /*! * Creates a new partition from the given data. @@ -75,10 +75,10 @@ namespace storm { * true iff the state is in the block. * @param blockVariables The variables to use for the block encoding. Their range must be [0, x] where x is * greater or equal than the number of states in the partition. - * @param nextFreeBlockIndex The next free block index. The existing blocks must be encoded with indices - * between 0 and this number. + * @param numberOfBlocks The number of blocks in this partition. + * @param nextFreeBlockIndex The next free block index. */ - Partition(storm::dd::Bdd const& partitionBdd, std::pair const& blockVariables, uint64_t nextFreeBlockIndex); + Partition(storm::dd::Bdd const& partitionBdd, std::pair const& blockVariables, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex); /*! * Creates a partition from the given model that respects the given expressions. @@ -95,6 +95,9 @@ namespace storm { /// The meta variables used to encode the block of each state in this partition. std::pair blockVariables; + /// The number of blocks in this partition. + uint64_t numberOfBlocks; + /// The next free block index. uint64_t nextFreeBlockIndex; }; diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp index fdec559d8..9c1c36064 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp @@ -17,7 +17,7 @@ namespace storm { template bool PartitionRefiner::refine(SignatureMode const& mode) { Partition newStatePartition = this->internalRefine(signatureComputer, signatureRefiner, statePartition, statePartition, mode); - if (statePartition == newStatePartition) { + if (statePartition.getNumberOfBlocks() == newStatePartition.getNumberOfBlocks()) { this->status = Status::FixedPoint; return false; } else { diff --git a/src/storm/storage/dd/bisimulation/PreservationInformation.cpp b/src/storm/storage/dd/bisimulation/PreservationInformation.cpp index 0569df104..897c50fc7 100644 --- a/src/storm/storage/dd/bisimulation/PreservationInformation.cpp +++ b/src/storm/storage/dd/bisimulation/PreservationInformation.cpp @@ -12,12 +12,12 @@ namespace storm { namespace bisimulation { template - PreservationInformation::PreservationInformation(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType) : PreservationInformation(model, model.getLabels(), bisimulationType) { + PreservationInformation::PreservationInformation(storm::models::symbolic::Model const& model) : PreservationInformation(model, model.getLabels()) { // Intentionally left empty. } template - PreservationInformation::PreservationInformation(storm::models::symbolic::Model const& model, std::vector const& labels, storm::storage::BisimulationType const&) { + PreservationInformation::PreservationInformation(storm::models::symbolic::Model const& model, std::vector const& labels) { for (auto const& label : labels) { this->addLabel(label); this->addExpression(model.getExpression(label)); @@ -25,14 +25,14 @@ namespace storm { } template - PreservationInformation::PreservationInformation(storm::models::symbolic::Model const& model, std::vector const& expressions, storm::storage::BisimulationType const&) { + PreservationInformation::PreservationInformation(storm::models::symbolic::Model const& model, std::vector const& expressions) { for (auto const& e : expressions) { this->addExpression(e); } } template - PreservationInformation::PreservationInformation(storm::models::symbolic::Model const& model, std::vector> const& formulas, storm::storage::BisimulationType const&) { + PreservationInformation::PreservationInformation(storm::models::symbolic::Model const& model, std::vector> const& formulas) { if (formulas.empty()) { // Default to respect all labels if no formulas are given. for (auto const& label : model.getLabels()) { diff --git a/src/storm/storage/dd/bisimulation/PreservationInformation.h b/src/storm/storage/dd/bisimulation/PreservationInformation.h index 2286e9bc6..eec8a8e00 100644 --- a/src/storm/storage/dd/bisimulation/PreservationInformation.h +++ b/src/storm/storage/dd/bisimulation/PreservationInformation.h @@ -21,10 +21,10 @@ namespace storm { public: PreservationInformation() = default; - PreservationInformation(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType); - PreservationInformation(storm::models::symbolic::Model const& model, std::vector const& labels, storm::storage::BisimulationType const& bisimulationType); - PreservationInformation(storm::models::symbolic::Model const& model, std::vector const& expressions, storm::storage::BisimulationType const& bisimulationType); - PreservationInformation(storm::models::symbolic::Model const& model, std::vector> const& formulas, storm::storage::BisimulationType const& bisimulationType); + PreservationInformation(storm::models::symbolic::Model const& model); + PreservationInformation(storm::models::symbolic::Model const& model, std::vector const& labels); + PreservationInformation(storm::models::symbolic::Model const& model, std::vector const& expressions); + PreservationInformation(storm::models::symbolic::Model const& model, std::vector> const& formulas); void addLabel(std::string const& label); void addExpression(storm::expressions::Expression const& expression); diff --git a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp index eb16ecf57..510cafc45 100644 --- a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp @@ -36,6 +36,24 @@ namespace storm { template class InternalSignatureRefiner; + struct InternalSignatureRefinerOptions { + InternalSignatureRefinerOptions() : InternalSignatureRefinerOptions(true) { + // Intentionally left empty. + } + + InternalSignatureRefinerOptions(bool shiftStateVariables) : shiftStateVariables(shiftStateVariables) { + auto const& bisimulationSettings = storm::settings::getModule(); + storm::settings::modules::BisimulationSettings::ReuseMode reuseMode = bisimulationSettings.getReuseMode(); + + this->reuseBlockNumbers = reuseMode == storm::settings::modules::BisimulationSettings::ReuseMode::All || reuseMode == storm::settings::modules::BisimulationSettings::ReuseMode::BlockNumbers; + this->reuseSignatureResult = reuseMode == storm::settings::modules::BisimulationSettings::ReuseMode::All || reuseMode == storm::settings::modules::BisimulationSettings::ReuseMode::SignatureResults; + } + + bool shiftStateVariables; + bool reuseBlockNumbers; + bool reuseSignatureResult; + }; + class ReuseWrapper { public: ReuseWrapper() : ReuseWrapper(false) { @@ -61,7 +79,7 @@ namespace storm { template class InternalSignatureRefiner { public: - InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables, bool shiftStateVariables) : manager(manager), internalDdManager(manager.getInternalDdManager()), ddman(internalDdManager.getCuddManager().getManager()), blockVariable(blockVariable), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), shiftStateVariables(shiftStateVariables), nextFreeBlockIndex(0), numberOfRefinements(0), lastNumberOfVisitedNodes(10000), signatureCache(lastNumberOfVisitedNodes), reuseBlocksCache(lastNumberOfVisitedNodes) { + InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables, InternalSignatureRefinerOptions const& options = InternalSignatureRefinerOptions()) : manager(manager), internalDdManager(manager.getInternalDdManager()), ddman(internalDdManager.getCuddManager().getManager()), blockVariable(blockVariable), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), options(options), nextFreeBlockIndex(0), numberOfRefinements(0), lastNumberOfVisitedNodes(10000), signatureCache(lastNumberOfVisitedNodes), reuseBlocksCache(lastNumberOfVisitedNodes) { // Initialize precomputed data. auto const& ddMetaVariable = manager.getMetaVariable(blockVariable); @@ -72,30 +90,67 @@ namespace storm { } Partition refine(Partition const& oldPartition, Signature const& signature) { - storm::dd::Add newPartitionAdd = refine(oldPartition, signature.getSignatureAdd()); + storm::dd::Add newPartitionAdd; + if (options.reuseBlockNumbers && !options.reuseSignatureResult) { + newPartitionAdd = refineReuseBlockNumber(oldPartition, signature.getSignatureAdd()); + } else { + newPartitionAdd = refineReuseSignatureResults(oldPartition, signature.getSignatureAdd()); + } ++numberOfRefinements; - return oldPartition.replacePartition(newPartitionAdd, nextFreeBlockIndex); + + uint64_t numberOfBlocks = nextFreeBlockIndex; + if (options.reuseSignatureResult) { + std::set blockVariableSet = {blockVariable}; + std::set nonBlockExpressionVariables; + std::set_difference(oldPartition.asAdd().getContainedMetaVariables().begin(), oldPartition.asAdd().getContainedMetaVariables().end(), blockVariableSet.begin(), blockVariableSet.end(), std::inserter(nonBlockExpressionVariables, nonBlockExpressionVariables.begin())); + numberOfBlocks = newPartitionAdd.notZero().existsAbstract(nonBlockExpressionVariables).getNonZeroCount(); + } + + return oldPartition.replacePartition(newPartitionAdd, numberOfBlocks, nextFreeBlockIndex); } private: - storm::dd::Add refine(Partition const& oldPartition, storm::dd::Add const& signatureAdd) { - STORM_LOG_ASSERT(oldPartition.storedAsAdd(), "Expecting partition to be stored as ADD for CUDD."); - - // Clear the caches. + void clearCaches() { signatureCache.clear(); + signatureCache2.clear(); reuseBlocksCache.clear(); + } + + storm::dd::Add refineReuseBlockNumber(Partition const& oldPartition, storm::dd::Add const& signatureAdd) { + STORM_LOG_ASSERT(oldPartition.storedAsAdd(), "Expecting partition to be stored as ADD for CUDD."); + nextFreeBlockIndex = oldPartition.getNextFreeBlockIndex(); // Perform the actual recursive refinement step. - DdNodePtr result = refine(oldPartition.asAdd().getInternalAdd().getCuddDdNode(), signatureAdd.getInternalAdd().getCuddDdNode(), nondeterminismVariables.getInternalBdd().getCuddDdNode(), nonBlockVariables.getInternalBdd().getCuddDdNode()); + DdNodePtr result = refineReuseBlockNumber(oldPartition.asAdd().getInternalAdd().getCuddDdNode(), signatureAdd.getInternalAdd().getCuddDdNode(), nondeterminismVariables.getInternalBdd().getCuddDdNode(), nonBlockVariables.getInternalBdd().getCuddDdNode()); // Construct resulting ADD from the obtained node and the meta information. storm::dd::InternalAdd internalNewPartitionAdd(&internalDdManager, cudd::ADD(internalDdManager.getCuddManager(), result)); storm::dd::Add newPartitionAdd(oldPartition.asAdd().getDdManager(), internalNewPartitionAdd, oldPartition.asAdd().getContainedMetaVariables()); + clearCaches(); return newPartitionAdd; } + storm::dd::Add refineReuseSignatureResults(Partition const& oldPartition, storm::dd::Add const& signatureAdd) { + STORM_LOG_ASSERT(oldPartition.storedAsAdd(), "Expecting partition to be stored as ADD for CUDD."); + + nextFreeBlockIndex = options.reuseSignatureResult ? oldPartition.getNextFreeBlockIndex() : 0; + + // Perform the actual recursive refinement step. + DdNodePtr result = refineReuseSignatureResults(signatureAdd.getInternalAdd().getCuddDdNode(), nondeterminismVariables.getInternalBdd().getCuddDdNode(), nonBlockVariables.getInternalBdd().getCuddDdNode()); + + // Construct resulting ADD from the obtained node and the meta information. + storm::dd::InternalAdd internalNewPartitionAdd(&internalDdManager, cudd::ADD(internalDdManager.getCuddManager(), result)); + storm::dd::Add newPartitionAdd(oldPartition.asAdd().getDdManager(), internalNewPartitionAdd, oldPartition.asAdd().getContainedMetaVariables()); + + if (options.reuseSignatureResult) { + oldSignatureCache = signatureCache; + } + clearCaches(); + return newPartitionAdd; + } + DdNodePtr encodeBlock(uint64_t blockIndex) { for (auto const& blockDdVariableIndex : blockDdVariableIndices) { blockEncoding[blockDdVariableIndex] = blockIndex & 1 ? 1 : 0; @@ -110,7 +165,102 @@ namespace storm { return result; } - DdNodePtr refine(DdNode* partitionNode, DdNode* signatureNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode) { + DdNodePtr refineReuseSignatureResults(DdNode* signatureNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode) { + // If we arrived at the constant zero node, then this was an illegal state encoding (we require + // all states to be non-deadlock). + if (signatureNode == Cudd_ReadZero(ddman)) { + return signatureNode; + } + + // Check the cache whether we have seen the same node before. + auto it = signatureCache.find(signatureNode); + if (it != signatureCache.end()) { + // If so, we return the corresponding result. + return it->second; + } + + // If we are to reuse signature results, check the old cache. + if (options.reuseSignatureResult) { + it = oldSignatureCache.find(signatureNode); + if (it != oldSignatureCache.end()) { + // If so, we return the corresponding result. + return it->second; + } + } + + // If there are no more non-block variables, we hit the signature. + if (Cudd_IsConstant(nonBlockVariablesNode)) { + DdNode* result = encodeBlock(nextFreeBlockIndex++); + signatureCache[signatureNode] = result; + return result; + } else { + // If there are more variables that belong to the non-block part of the encoding, we need to recursively descend. + + bool skipped = true; + DdNode* signatureThen; + DdNode* signatureElse; + short offset; + bool isNondeterminismVariable = false; + while (skipped && !Cudd_IsConstant(nonBlockVariablesNode)) { + // Remember an offset that indicates whether the top variable is a nondeterminism variable or not. + offset = options.shiftStateVariables ? 1 : 0; + if (!Cudd_IsConstant(nondeterminismVariablesNode) && Cudd_NodeReadIndex(nondeterminismVariablesNode) == Cudd_NodeReadIndex(nonBlockVariablesNode)) { + offset = 0; + isNondeterminismVariable = true; + } + + if (Cudd_NodeReadIndex(signatureNode) == Cudd_NodeReadIndex(nonBlockVariablesNode)) { + signatureThen = Cudd_T(signatureNode); + signatureElse = Cudd_E(signatureNode); + skipped = false; + } else { + signatureThen = signatureElse = signatureNode; + } + + // If we skipped the next variable, we fast-forward. + if (skipped) { + // If the current variable is a nondeterminism variable, we need to advance both variable sets otherwise just the non-block variables. + nonBlockVariablesNode = Cudd_T(nonBlockVariablesNode); + if (isNondeterminismVariable) { + nondeterminismVariablesNode = Cudd_T(nondeterminismVariablesNode); + } + } + } + + // If there are no more non-block variables remaining, make a recursive call to enter the base case. + if (Cudd_IsConstant(nonBlockVariablesNode)) { + return refineReuseSignatureResults(signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode); + } + + DdNode* thenResult = refineReuseSignatureResults(signatureThen, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); + Cudd_Ref(thenResult); + DdNode* elseResult = refineReuseSignatureResults(signatureElse, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); + Cudd_Ref(elseResult); + + DdNode* result; + if (thenResult == elseResult) { + Cudd_Deref(thenResult); + Cudd_Deref(elseResult); + result = thenResult; + } else { + // Get the node to connect the subresults. + bool complemented = Cudd_IsComplement(thenResult); + result = cuddUniqueInter(ddman, Cudd_NodeReadIndex(nonBlockVariablesNode) + offset, Cudd_Regular(thenResult), complemented ? Cudd_Not(elseResult) : elseResult); + if (complemented) { + result = Cudd_Not(result); + } + Cudd_Deref(thenResult); + Cudd_Deref(elseResult); + } + + // Store the result in the cache. + signatureCache[signatureNode] = result; + + return result; + } + } + + DdNodePtr refineReuseBlockNumber(DdNode* partitionNode, DdNode* signatureNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode) { // If we arrived at the constant zero node, then this was an illegal state encoding (we require // all states to be non-deadlock). if (partitionNode == Cudd_ReadZero(ddman)) { @@ -119,8 +269,8 @@ namespace storm { // Check the cache whether we have seen the same node before. auto nodePair = std::make_pair(signatureNode, partitionNode); - auto it = signatureCache.find(nodePair); - if (it != signatureCache.end()) { + auto it = signatureCache2.find(nodePair); + if (it != signatureCache2.end()) { // If so, we return the corresponding result. return it->second; } @@ -132,11 +282,11 @@ namespace storm { auto& reuseEntry = reuseBlocksCache[partitionNode]; if (!reuseEntry.isReused()) { reuseEntry.setReused(); - signatureCache[nodePair] = partitionNode; + signatureCache2[nodePair] = partitionNode; return partitionNode; } else { DdNode* result = encodeBlock(nextFreeBlockIndex++); - signatureCache[nodePair] = result; + signatureCache2[nodePair] = result; return result; } } else { @@ -151,7 +301,7 @@ namespace storm { bool isNondeterminismVariable = false; while (skippedBoth && !Cudd_IsConstant(nonBlockVariablesNode)) { // Remember an offset that indicates whether the top variable is a nondeterminism variable or not. - offset = shiftStateVariables ? 1 : 0; + offset = options.shiftStateVariables ? 1 : 0; if (!Cudd_IsConstant(nondeterminismVariablesNode) && Cudd_NodeReadIndex(nondeterminismVariablesNode) == Cudd_NodeReadIndex(nonBlockVariablesNode)) { offset = 0; isNondeterminismVariable = true; @@ -185,12 +335,12 @@ namespace storm { // If there are no more non-block variables remaining, make a recursive call to enter the base case. if (Cudd_IsConstant(nonBlockVariablesNode)) { - return refine(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode); + return refineReuseBlockNumber(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode); } - DdNode* thenResult = refine(partitionThen, signatureThen, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); + DdNode* thenResult = refineReuseBlockNumber(partitionThen, signatureThen, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); Cudd_Ref(thenResult); - DdNode* elseResult = refine(partitionElse, signatureElse, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); + DdNode* elseResult = refineReuseBlockNumber(partitionElse, signatureElse, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); Cudd_Ref(elseResult); DdNode* result; @@ -210,7 +360,7 @@ namespace storm { } // Store the result in the cache. - signatureCache[nodePair] = result; + signatureCache2[nodePair] = result; return result; } @@ -224,9 +374,9 @@ namespace storm { // The cubes representing all non-block and all nondeterminism variables, respectively. storm::dd::Bdd nondeterminismVariables; storm::dd::Bdd nonBlockVariables; - - // A flag indicating whether we are to shift the state variables by one. - bool shiftStateVariables; + + // The provided options. + InternalSignatureRefinerOptions options; // The indices of the DD variables associated with the block variable. std::vector blockDdVariableIndices; @@ -244,7 +394,9 @@ namespace storm { uint64_t lastNumberOfVisitedNodes; // The cache used to identify states with identical signature. - spp::sparse_hash_map, DdNode*, CuddPointerPairHash> signatureCache; + spp::sparse_hash_map oldSignatureCache; + spp::sparse_hash_map signatureCache; + spp::sparse_hash_map, DdNode*, CuddPointerPairHash> signatureCache2; // The cache used to identify which old block numbers have already been reused. spp::sparse_hash_map reuseBlocksCache; @@ -253,64 +405,79 @@ namespace storm { template class InternalSignatureRefiner { public: - InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables, bool shiftStateVariables) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), shiftStateVariables(shiftStateVariables), numberOfBlockVariables(manager.getMetaVariable(blockVariable).getNumberOfDdVariables()), blockCube(manager.getMetaVariable(blockVariable).getCube()), nextFreeBlockIndex(0), numberOfRefinements(0), signatureCache() { + InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables, InternalSignatureRefinerOptions const& options) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), options(options), numberOfBlockVariables(manager.getMetaVariable(blockVariable).getNumberOfDdVariables()), blockCube(manager.getMetaVariable(blockVariable).getCube()), nextFreeBlockIndex(0), numberOfRefinements(0), signatureCache() { // Perform garbage collection to clean up stuff not needed anymore. LACE_ME; sylvan_gc(); } Partition refine(Partition const& oldPartition, Signature const& signature) { - storm::dd::Bdd newPartitionBdd = refine(oldPartition, signature.getSignatureAdd()); - return oldPartition.replacePartition(newPartitionBdd, nextFreeBlockIndex); + storm::dd::Bdd newPartitionBdd; + if (options.reuseBlockNumbers && !options.reuseSignatureResult) { + newPartitionBdd = refineReuseBlockNumber(oldPartition, signature.getSignatureAdd()); + } else { + newPartitionBdd = refineReuseSignatureResults(oldPartition, signature.getSignatureAdd()); + } + + auto start = std::chrono::high_resolution_clock::now(); + uint64_t numberOfBlocks = nextFreeBlockIndex; + if (options.reuseSignatureResult) { + std::set blockVariableSet = {blockVariable}; + std::set nonBlockExpressionVariables; + std::set_difference(oldPartition.asBdd().getContainedMetaVariables().begin(), oldPartition.asBdd().getContainedMetaVariables().end(), blockVariableSet.begin(), blockVariableSet.end(), std::inserter(nonBlockExpressionVariables, nonBlockExpressionVariables.begin())); + numberOfBlocks = newPartitionBdd.existsAbstract(nonBlockExpressionVariables).getNonZeroCount(); + } + auto end = std::chrono::high_resolution_clock::now(); + std::cout << "took " << std::chrono::duration_cast(end - start).count() << std::endl; + + return oldPartition.replacePartition(newPartitionBdd, numberOfBlocks, nextFreeBlockIndex); } private: - storm::dd::Bdd refine(Partition const& oldPartition, storm::dd::Add const& signatureAdd) { + void clearCaches() { + signatureCache.clear(); + signatureCache2.clear(); + reuseBlocksCache.clear(); + } + + storm::dd::Bdd refineReuseBlockNumber(Partition const& oldPartition, storm::dd::Add const& signatureAdd) { STORM_LOG_ASSERT(oldPartition.storedAsBdd(), "Expecting partition to be stored as BDD for Sylvan."); - - LACE_ME; // Set up next refinement. ++numberOfRefinements; - // Clear the caches. - std::size_t oldSize = signatureCache.size(); - signatureCache.clear(); - signatureCache.reserve(3 * oldSize); - reuseBlocksCache.clear(); - reuseBlocksCache.reserve(3 * oldPartition.getNumberOfBlocks()); nextFreeBlockIndex = oldPartition.getNextFreeBlockIndex(); - - // Clear performance counters. -// signatureCacheLookups = 0; -// signatureCacheHits = 0; -// numberOfVisitedNodes = 0; -// totalSignatureCacheLookupTime = std::chrono::high_resolution_clock::duration(0); -// totalSignatureCacheStoreTime = std::chrono::high_resolution_clock::duration(0); -// totalReuseBlocksLookupTime = std::chrono::high_resolution_clock::duration(0); -// totalLevelLookupTime = std::chrono::high_resolution_clock::duration(0); -// totalBlockEncodingTime = std::chrono::high_resolution_clock::duration(0); -// totalMakeNodeTime = std::chrono::high_resolution_clock::duration(0); // Perform the actual recursive refinement step. - BDD result = refine(oldPartition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD(), nondeterminismVariables.getInternalBdd().getSylvanBdd().GetBDD(), nonBlockVariables.getInternalBdd().getSylvanBdd().GetBDD()); + BDD result = refineReuseBlockNumber(oldPartition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD(), nondeterminismVariables.getInternalBdd().getSylvanBdd().GetBDD(), nonBlockVariables.getInternalBdd().getSylvanBdd().GetBDD()); // Construct resulting BDD from the obtained node and the meta information. storm::dd::InternalBdd internalNewPartitionBdd(&internalDdManager, sylvan::Bdd(result)); storm::dd::Bdd newPartitionBdd(oldPartition.asBdd().getDdManager(), internalNewPartitionBdd, oldPartition.asBdd().getContainedMetaVariables()); -// // Display some statistics. -// STORM_LOG_TRACE("Refinement visited " << numberOfVisitedNodes << " nodes."); -// STORM_LOG_TRACE("Current #nodes in table: " << llmsset_count_marked(nodes) << " of " << llmsset_get_size(nodes) << ", cache: " << cache_getused() << " of " << cache_getsize() << "."); -// STORM_LOG_TRACE("Signature cache hits: " << signatureCacheHits << ", misses: " << (signatureCacheLookups - signatureCacheHits) << "."); -// STORM_LOG_TRACE("Signature cache lookup time: " << std::chrono::duration_cast(totalSignatureCacheLookupTime).count() << "ms"); -// STORM_LOG_TRACE("Signature cache store time: " << std::chrono::duration_cast(totalSignatureCacheStoreTime).count() << "ms"); -// STORM_LOG_TRACE("Signature cache total time: " << std::chrono::duration_cast(totalSignatureCacheStoreTime + totalSignatureCacheLookupTime).count() << "ms"); -// STORM_LOG_TRACE("Reuse blocks lookup time: " << std::chrono::duration_cast(totalReuseBlocksLookupTime).count() << "ms"); -// STORM_LOG_TRACE("Level lookup time: " << std::chrono::duration_cast(totalLevelLookupTime).count() << "ms"); -// STORM_LOG_TRACE("Block encoding time: " << std::chrono::duration_cast(totalBlockEncodingTime).count() << "ms"); -// STORM_LOG_TRACE("Make node time: " << std::chrono::duration_cast(totalMakeNodeTime).count() << "ms"); + clearCaches(); + return newPartitionBdd; + } + + storm::dd::Bdd refineReuseSignatureResults(Partition const& oldPartition, storm::dd::Add const& signatureAdd) { + STORM_LOG_ASSERT(oldPartition.storedAsBdd(), "Expecting partition to be stored as BDD for Sylvan."); + + // Set up next refinement. + ++numberOfRefinements; + + nextFreeBlockIndex = options.reuseSignatureResult ? oldPartition.getNextFreeBlockIndex() : 0; + + // Perform the actual recursive refinement step. + BDD result = refineReuseSignatureResults(signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD(), nondeterminismVariables.getInternalBdd().getSylvanBdd().GetBDD(), nonBlockVariables.getInternalBdd().getSylvanBdd().GetBDD()); + + // Construct resulting BDD from the obtained node and the meta information. + storm::dd::InternalBdd internalNewPartitionBdd(&internalDdManager, sylvan::Bdd(result)); + storm::dd::Bdd newPartitionBdd(oldPartition.asBdd().getDdManager(), internalNewPartitionBdd, oldPartition.asBdd().getContainedMetaVariables()); + if (options.reuseSignatureResult) { + oldSignatureCache = signatureCache; + } + clearCaches(); return newPartitionBdd; } @@ -323,7 +490,101 @@ namespace storm { return sylvan_cube(blockCube.getInternalBdd().getSylvanBdd().GetBDD(), e.data()); } - BDD refine(BDD partitionNode, MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) { + BDD refineReuseSignatureResults(MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) { + LACE_ME; + + // If we arrived at the constant zero node, then this was an illegal state encoding (we require + // all states to be non-deadlock). + if (mtbdd_iszero(signatureNode)) { + return sylvan_false; + } + + // Check the cache whether we have seen the same node before. + auto it = signatureCache.find(signatureNode); + if (it != signatureCache.end()) { + // If so, we return the corresponding result. + return it->second; + } + + // If we are to reuse signature results, check the old cache. + if (options.reuseSignatureResult) { + it = oldSignatureCache.find(signatureNode); + if (it != oldSignatureCache.end()) { + // If so, we return the corresponding result. + return it->second; + } + } + + sylvan_gc_test(); + + // If there are no more non-block variables, we hit the signature. + if (sylvan_isconst(nonBlockVariablesNode)) { + BDD result = encodeBlock(nextFreeBlockIndex++); + signatureCache[signatureNode] = result; + return result; + } else { + // If there are more variables that belong to the non-block part of the encoding, we need to recursively descend. + + bool skipped = true; + MTBDD signatureThen; + MTBDD signatureElse; + short offset; + bool isNondeterminismVariable = false; + while (skipped && !sylvan_isconst(nonBlockVariablesNode)) { + // Remember an offset that indicates whether the top variable is a nondeterminism variable or not. + offset = options.shiftStateVariables ? 1 : 0; + if (!sylvan_isconst(nondeterminismVariablesNode) && sylvan_var(nondeterminismVariablesNode) == sylvan_var(nonBlockVariablesNode)) { + offset = 0; + isNondeterminismVariable = true; + } + + if (storm::dd::InternalAdd::matchesVariableIndex(signatureNode, sylvan_var(nonBlockVariablesNode))) { + signatureThen = sylvan_high(signatureNode); + signatureElse = sylvan_low(signatureNode); + skipped = false; + } else { + signatureThen = signatureElse = signatureNode; + } + + // If we skipped the next variable, we fast-forward. + if (skipped) { + // If the current variable is a nondeterminism variable, we need to advance both variable sets otherwise just the non-block variables. + nonBlockVariablesNode = sylvan_high(nonBlockVariablesNode); + if (isNondeterminismVariable) { + nondeterminismVariablesNode = sylvan_high(nondeterminismVariablesNode); + } + } + } + + // If there are no more non-block variables remaining, make a recursive call to enter the base case. + if (sylvan_isconst(nonBlockVariablesNode)) { + return refineReuseSignatureResults(signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode); + } + + BDD thenResult = refineReuseSignatureResults(signatureThen, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); + bdd_refs_push(thenResult); + BDD elseResult = refineReuseSignatureResults(signatureElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); + bdd_refs_push(elseResult); + + BDD result; + if (thenResult == elseResult) { + result = thenResult; + } else { + // Get the node to connect the subresults. + result = sylvan_makenode(sylvan_var(nonBlockVariablesNode) + offset, elseResult, thenResult); + } + + // Dispose of the intermediate results. + bdd_refs_pop(2); + + // Store the result in the cache. + signatureCache[signatureNode] = result; + + return result; + } + } + + BDD refineReuseBlockNumber(BDD partitionNode, MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) { LACE_ME; // If we arrived at the constant zero node, then this was an illegal state encoding (we require @@ -336,8 +597,8 @@ namespace storm { // Check the cache whether we have seen the same node before. auto nodePair = std::make_pair(signatureNode, partitionNode); - auto it = signatureCache.find(nodePair); - if (it != signatureCache.end()) { + auto it = signatureCache2.find(nodePair); + if (it != signatureCache2.end()) { // If so, we return the corresponding result. return it->second; } @@ -353,11 +614,11 @@ namespace storm { if (!reuseBlockEntry.isReused()) { reuseBlockEntry.setReused(); reuseBlocksCache.emplace(partitionNode, true); - signatureCache[nodePair] = partitionNode; + signatureCache2[nodePair] = partitionNode; return partitionNode; } else { BDD result = encodeBlock(nextFreeBlockIndex++); - signatureCache[nodePair] = result; + signatureCache2[nodePair] = result; return result; } } else { @@ -372,7 +633,7 @@ namespace storm { bool isNondeterminismVariable = false; while (skippedBoth && !sylvan_isconst(nonBlockVariablesNode)) { // Remember an offset that indicates whether the top variable is a nondeterminism variable or not. - offset = shiftStateVariables ? 1 : 0; + offset = options.shiftStateVariables ? 1 : 0; if (!sylvan_isconst(nondeterminismVariablesNode) && sylvan_var(nondeterminismVariablesNode) == sylvan_var(nonBlockVariablesNode)) { offset = 0; isNondeterminismVariable = true; @@ -406,12 +667,12 @@ namespace storm { // If there are no more non-block variables remaining, make a recursive call to enter the base case. if (sylvan_isconst(nonBlockVariablesNode)) { - return refine(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode); + return refineReuseBlockNumber(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode); } - BDD thenResult = refine(partitionThen, signatureThen, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); + BDD thenResult = refineReuseBlockNumber(partitionThen, signatureThen, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); bdd_refs_push(thenResult); - BDD elseResult = refine(partitionElse, signatureElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); + BDD elseResult = refineReuseBlockNumber(partitionElse, signatureElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); bdd_refs_push(elseResult); BDD result; @@ -426,7 +687,7 @@ namespace storm { bdd_refs_pop(2); // Store the result in the cache. - signatureCache[nodePair] = result; + signatureCache2[nodePair] = result; return result; } @@ -439,8 +700,9 @@ namespace storm { storm::dd::Bdd nondeterminismVariables; storm::dd::Bdd nonBlockVariables; - bool shiftStateVariables; - + // The provided options. + InternalSignatureRefinerOptions options; + uint64_t numberOfBlockVariables; storm::dd::Bdd blockCube; @@ -452,7 +714,9 @@ namespace storm { uint64_t numberOfRefinements; // The cache used to identify states with identical signature. - spp::sparse_hash_map, MTBDD, SylvanMTBDDPairHash> signatureCache; + spp::sparse_hash_map oldSignatureCache; + spp::sparse_hash_map signatureCache; + spp::sparse_hash_map, MTBDD, SylvanMTBDDPairHash> signatureCache2; // The cache used to identify which old block numbers have already been reused. spp::sparse_hash_map reuseBlocksCache; @@ -467,7 +731,6 @@ namespace storm { // std::chrono::high_resolution_clock::duration totalLevelLookupTime; // std::chrono::high_resolution_clock::duration totalBlockEncodingTime; // std::chrono::high_resolution_clock::duration totalMakeNodeTime; - }; template @@ -485,7 +748,7 @@ namespace storm { nonBlockVariablesCube &= cube; } - internalRefiner = std::make_unique>(manager, blockVariable, nondeterminismVariablesCube, nonBlockVariablesCube, shiftStateVariables); + internalRefiner = std::make_unique>(manager, blockVariable, nondeterminismVariablesCube, nonBlockVariablesCube, InternalSignatureRefinerOptions(shiftStateVariables)); } template