From c85e30dfd05cdfc8f688ab2cc1747320678b07e7 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 25 Oct 2017 15:35:20 +0200 Subject: [PATCH] added distance-aware initial partition to dd-based bisimulation --- src/storm-cli-utilities/model-handling.h | 22 ++-- .../modelchecker/AbstractModelChecker.cpp | 4 + .../SymbolicPropositionalModelChecker.cpp | 7 +- .../settings/modules/BisimulationSettings.cpp | 17 +++ .../settings/modules/BisimulationSettings.h | 8 ++ .../storage/dd/BisimulationDecomposition.cpp | 2 +- .../storage/dd/bisimulation/Partition.cpp | 119 ++++++++++++++++-- src/storm/storage/dd/bisimulation/Partition.h | 6 + 8 files changed, 164 insertions(+), 21 deletions(-) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index ef3102d46..f296cafa6 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -44,8 +44,11 @@ namespace storm { // The symbolic model description. boost::optional model; - // The properties to check. + // The original properties to check. std::vector properties; + + // The preprocessed properties to check (in case they needed amendment). + boost::optional> preprocessedProperties; }; void parseSymbolicModelDescription(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input) { @@ -129,7 +132,7 @@ namespace storm { for (auto const& property : output.properties) { amendedProperties.emplace_back(property.substituteLabels(labelRenaming)); } - output.properties = std::move(amendedProperties); + output.preprocessedProperties = std::move(amendedProperties); } } } @@ -474,7 +477,8 @@ namespace storm { }; template - void verifyProperties(std::vector const& properties, std::function(std::shared_ptr const& formula, std::shared_ptr const& states)> const& verificationCallback, std::function const&)> const& postprocessingCallback = PostprocessingIdentity()) { + void verifyProperties(SymbolicInput const& input, std::function(std::shared_ptr const& formula, std::shared_ptr const& states)> const& verificationCallback, std::function const&)> const& postprocessingCallback = PostprocessingIdentity()) { + auto const& properties = input.preprocessedProperties ? input.preprocessedProperties.get() : input.properties; for (auto const& property : properties) { printModelCheckingProperty(property); storm::utility::Stopwatch watch(true); @@ -488,7 +492,7 @@ namespace storm { template void verifyWithAbstractionRefinementEngine(SymbolicInput const& input) { STORM_LOG_ASSERT(input.model, "Expected symbolic model description."); - verifyProperties(input.properties, [&input] (std::shared_ptr const& formula, std::shared_ptr const& states) { + verifyProperties(input, [&input] (std::shared_ptr const& formula, std::shared_ptr const& states) { STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states."); return storm::api::verifyWithAbstractionRefinementEngine(input.model.get(), storm::api::createTask(formula, true)); }); @@ -498,7 +502,7 @@ namespace storm { void verifyWithExplorationEngine(SymbolicInput const& input) { STORM_LOG_ASSERT(input.model, "Expected symbolic model description."); STORM_LOG_THROW((std::is_same::value), storm::exceptions::NotSupportedException, "Exploration does not support other data-types than floating points."); - verifyProperties(input.properties, [&input] (std::shared_ptr const& formula, std::shared_ptr const& states) { + verifyProperties(input, [&input] (std::shared_ptr const& formula, std::shared_ptr const& states) { STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Exploration can only filter initial states."); return storm::api::verifyWithExplorationEngine(input.model.get(), storm::api::createTask(formula, true)); }); @@ -507,7 +511,7 @@ namespace storm { template void verifyWithSparseEngine(std::shared_ptr const& model, SymbolicInput const& input) { auto sparseModel = model->as>(); - verifyProperties(input.properties, + verifyProperties(input, [&sparseModel] (std::shared_ptr const& formula, std::shared_ptr const& states) { bool filterForInitialStates = states->isInitialFormula(); auto task = storm::api::createTask(formula, filterForInitialStates); @@ -528,7 +532,7 @@ namespace storm { template void verifyWithHybridEngine(std::shared_ptr const& model, SymbolicInput const& input) { - verifyProperties(input.properties, [&model] (std::shared_ptr const& formula, std::shared_ptr const& states) { + verifyProperties(input, [&model] (std::shared_ptr const& formula, std::shared_ptr const& states) { bool filterForInitialStates = states->isInitialFormula(); auto task = storm::api::createTask(formula, filterForInitialStates); @@ -550,7 +554,7 @@ namespace storm { template void verifyWithDdEngine(std::shared_ptr const& model, SymbolicInput const& input) { - verifyProperties(input.properties, [&model] (std::shared_ptr const& formula, std::shared_ptr const& states) { + verifyProperties(input, [&model] (std::shared_ptr const& formula, std::shared_ptr const& states) { bool filterForInitialStates = states->isInitialFormula(); auto task = storm::api::createTask(formula, filterForInitialStates); @@ -572,7 +576,7 @@ namespace storm { template void verifyWithAbstractionRefinementEngine(std::shared_ptr const& model, SymbolicInput const& input) { - verifyProperties(input.properties, [&model] (std::shared_ptr const& formula, std::shared_ptr const& states) { + verifyProperties(input, [&model] (std::shared_ptr const& formula, std::shared_ptr const& states) { STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states."); auto symbolicModel = model->as>(); return storm::api::verifyWithAbstractionRefinementEngine(symbolicModel, storm::api::createTask(formula, true)); diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp index 78f6e7d93..1a12a89b7 100644 --- a/src/storm/modelchecker/AbstractModelChecker.cpp +++ b/src/storm/modelchecker/AbstractModelChecker.cpp @@ -314,6 +314,10 @@ namespace storm { template class AbstractModelChecker>; #endif // DD + template class AbstractModelChecker>; + template class AbstractModelChecker>; + template class AbstractModelChecker>; + template class AbstractModelChecker>; template class AbstractModelChecker>; template class AbstractModelChecker>; template class AbstractModelChecker>; diff --git a/src/storm/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp b/src/storm/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp index d7e93d372..9b063e7ea 100644 --- a/src/storm/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp +++ b/src/storm/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp @@ -55,20 +55,21 @@ namespace storm { ModelType const& SymbolicPropositionalModelChecker::getModel() const { return model; } - // Explicitly instantiate the template class. - - + template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; + template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; + template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; + template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; diff --git a/src/storm/settings/modules/BisimulationSettings.cpp b/src/storm/settings/modules/BisimulationSettings.cpp index cea523793..d048a35ca 100644 --- a/src/storm/settings/modules/BisimulationSettings.cpp +++ b/src/storm/settings/modules/BisimulationSettings.cpp @@ -18,6 +18,7 @@ namespace storm { const std::string BisimulationSettings::quotientFormatOptionName = "quot"; const std::string BisimulationSettings::signatureModeOptionName = "sigmode"; const std::string BisimulationSettings::reuseOptionName = "reuse"; + const std::string BisimulationSettings::initialPartitionOptionName = "init"; BisimulationSettings::BisimulationSettings() : ModuleSettings(moduleName) { std::vector types = { "strong", "weak" }; @@ -36,6 +37,12 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(reuseModes)) .setDefaultValueString("blocks").build()) .build()); + + std::vector initialPartitionModes = {"regular", "finer"}; + this->addOption(storm::settings::OptionBuilder(moduleName, initialPartitionOptionName, true, "Sets which initial partition mode to use.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(initialPartitionModes)) + .setDefaultValueString("finer").build()) + .build()); } bool BisimulationSettings::isStrongBisimulationSet() const { @@ -84,6 +91,16 @@ namespace storm { return ReuseMode::BlockNumbers; } + BisimulationSettings::InitialPartitionMode BisimulationSettings::getInitialPartitionMode() const { + std::string initialPartitionModeAsString = this->getOption(initialPartitionOptionName).getArgumentByName("mode").getValueAsString(); + if (initialPartitionModeAsString == "regular") { + return InitialPartitionMode::Regular; + } else if (initialPartitionModeAsString == "finer") { + return InitialPartitionMode::Finer; + } + return InitialPartitionMode::Finer; + } + 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 917c1479a..ed1a15c6d 100644 --- a/src/storm/settings/modules/BisimulationSettings.h +++ b/src/storm/settings/modules/BisimulationSettings.h @@ -21,6 +21,8 @@ namespace storm { enum class ReuseMode { None, BlockNumbers }; + enum class InitialPartitionMode { Regular, Finer }; + /*! * Creates a new set of bisimulation settings. */ @@ -62,6 +64,11 @@ namespace storm { */ ReuseMode getReuseMode() const; + /*! + * Retrieves the initial partition mode. + */ + InitialPartitionMode getInitialPartitionMode() const; + virtual bool check() const override; // The name of the module. @@ -74,6 +81,7 @@ namespace storm { static const std::string quotientFormatOptionName; static const std::string signatureModeOptionName; static const std::string reuseOptionName; + static const std::string initialPartitionOptionName; }; } // namespace modules } // namespace settings diff --git a/src/storm/storage/dd/BisimulationDecomposition.cpp b/src/storm/storage/dd/BisimulationDecomposition.cpp index 5a1f0622e..8106243b7 100644 --- a/src/storm/storage/dd/BisimulationDecomposition.cpp +++ b/src/storm/storage/dd/BisimulationDecomposition.cpp @@ -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), 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, formulas))) { this->initialize(); } diff --git a/src/storm/storage/dd/bisimulation/Partition.cpp b/src/storm/storage/dd/bisimulation/Partition.cpp index 79a0d007a..46a265fd6 100644 --- a/src/storm/storage/dd/bisimulation/Partition.cpp +++ b/src/storm/storage/dd/bisimulation/Partition.cpp @@ -4,13 +4,17 @@ #include "storm/storage/dd/bisimulation/PreservationInformation.h" -#include "storm/logic/Formula.h" +#include "storm/logic/Formulas.h" #include "storm/logic/AtomicExpressionFormula.h" #include "storm/logic/AtomicLabelFormula.h" +#include "storm/logic/FragmentSpecification.h" #include "storm/models/symbolic/Mdp.h" #include "storm/models/symbolic/StandardRewardModel.h" +#include "storm/modelchecker/propositional/SymbolicPropositionalModelChecker.h" +#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" + #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/BisimulationSettings.h" @@ -52,6 +56,50 @@ namespace storm { return Partition(newPartitionBdd, blockVariables, numberOfBlocks, nextFreeBlockIndex); } + template + boost::optional, std::shared_ptr>> Partition::extractConstraintTargetFormulas(storm::logic::Formula const& formula) { + boost::optional, std::shared_ptr>> result; + if (formula.isProbabilityOperatorFormula()) { + return extractConstraintTargetFormulas(formula.asProbabilityOperatorFormula().getSubformula()); + } else if (formula.isRewardOperatorFormula()) { + return extractConstraintTargetFormulas(formula.asRewardOperatorFormula().getSubformula()); + } else if (formula.isUntilFormula()) { + storm::logic::UntilFormula const& untilFormula = formula.asUntilFormula(); + storm::logic::FragmentSpecification propositional = storm::logic::propositional(); + if (untilFormula.getLeftSubformula().isInFragment(propositional) && untilFormula.getRightSubformula().isInFragment(propositional)) { + result = std::pair, std::shared_ptr>(); + result.get().first = untilFormula.getLeftSubformula().asSharedPointer(); + result.get().second = untilFormula.getRightSubformula().asSharedPointer(); + } + } else if (formula.isEventuallyFormula()) { + storm::logic::EventuallyFormula const& eventuallyFormula = formula.asEventuallyFormula(); + storm::logic::FragmentSpecification propositional = storm::logic::propositional(); + if (eventuallyFormula.getSubformula().isInFragment(propositional)) { + result = std::pair, std::shared_ptr>(); + result.get().first = std::make_shared(true); + result.get().second = eventuallyFormula.getSubformula().asSharedPointer(); + } + } + return result; + } + + template + Partition Partition::create(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType, std::vector> const& formulas) { + + auto const& bisimulationSettings = storm::settings::getModule(); + + boost::optional, std::shared_ptr>> constraintTargetFormulas; + if (bisimulationSettings.getInitialPartitionMode() == storm::settings::modules::BisimulationSettings::InitialPartitionMode::Finer && formulas.size() == 1) { + constraintTargetFormulas = extractConstraintTargetFormulas(*formulas.front()); + } + + if (constraintTargetFormulas && bisimulationType == storm::storage::BisimulationType::Strong) { + return createDistanceBased(model, *constraintTargetFormulas.get().first, *constraintTargetFormulas.get().second); + } else { + return create(model, bisimulationType, PreservationInformation(model, formulas)); + } + } + template Partition Partition::create(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType, PreservationInformation const& preservationInformation) { @@ -64,15 +112,58 @@ namespace storm { } template - Partition Partition::create(storm::models::symbolic::Model const& model, std::vector const& expressions, storm::storage::BisimulationType const& bisimulationType) { - STORM_LOG_THROW(bisimulationType == storm::storage::BisimulationType::Strong, storm::exceptions::NotSupportedException, "Currently only strong bisimulation is supported."); + Partition Partition::createDistanceBased(storm::models::symbolic::Model const& model, storm::logic::Formula const& constraintFormula, storm::logic::Formula const& targetFormula) { + storm::modelchecker::SymbolicPropositionalModelChecker> propositionalChecker(model); + + std::unique_ptr subresult = propositionalChecker.check(constraintFormula); + storm::dd::Bdd constraintStates = subresult->asSymbolicQualitativeCheckResult().getTruthValuesVector(); + subresult = propositionalChecker.check(targetFormula); + storm::dd::Bdd targetStates = subresult->asSymbolicQualitativeCheckResult().getTruthValuesVector(); + + return createDistanceBased(model, constraintStates, targetStates); + } + + template + Partition Partition::createDistanceBased(storm::models::symbolic::Model const& model, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates) { + + STORM_LOG_TRACE("Creating distance-based partition."); + std::pair blockVariables = createBlockVariables(model); + + // Set up the construction. storm::dd::DdManager& manager = model.getManager(); + storm::dd::Bdd partitionBdd = manager.getBddZero(); + storm::dd::Bdd transitionMatrixBdd = model.getTransitionMatrix().notZero().existsAbstract(model.getNondeterminismVariables()); + storm::dd::Bdd coveredStates = manager.getBddZero(); + uint64_t blockCount = 0; + + // Backward BFS. + storm::dd::Bdd backwardFrontier = targetStates; + while (!backwardFrontier.isZero()) { + partitionBdd |= backwardFrontier && manager.getEncoding(blockVariables.first, blockCount++, false); + coveredStates |= backwardFrontier; + backwardFrontier = backwardFrontier.inverseRelationalProduct(transitionMatrixBdd, model.getRowVariables(), model.getColumnVariables()) && !coveredStates && constraintStates; + } + + // If there are states that cannot reach the target states (via only constraint states) at all, put them in one block. + if (coveredStates != model.getReachableStates()) { + partitionBdd |= (model.getReachableStates() && !coveredStates) && manager.getEncoding(blockVariables.first, blockCount++, false); + } - std::vector> stateSets; - for (auto const& expression : expressions) { - stateSets.emplace_back(model.getStates(expression)); + // Move the partition over to the primed variables. + partitionBdd = partitionBdd.swapVariables(model.getRowColumnMetaVariablePairs()); + + // 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); + } else { + return Partition(partitionBdd, blockVariables, blockCount, blockCount); } + } + + template + std::pair Partition::createBlockVariables(storm::models::symbolic::Model const& model) { + storm::dd::DdManager& manager = model.getManager(); uint64_t numberOfDdVariables = 0; for (auto const& metaVariable : model.getRowVariables()) { @@ -87,8 +178,20 @@ namespace storm { } } - std::pair blockVariables = createBlockVariables(manager, numberOfDdVariables); - std::pair, uint64_t> partitionBddAndBlockCount = createPartitionBdd(manager, model, stateSets, blockVariables.first); + return createBlockVariables(manager, numberOfDdVariables); + } + + template + Partition Partition::create(storm::models::symbolic::Model const& model, std::vector const& expressions, storm::storage::BisimulationType const& bisimulationType) { + STORM_LOG_THROW(bisimulationType == storm::storage::BisimulationType::Strong, storm::exceptions::NotSupportedException, "Currently only strong bisimulation is supported."); + + std::pair blockVariables = createBlockVariables(model); + + std::vector> stateSets; + for (auto const& expression : expressions) { + stateSets.emplace_back(model.getStates(expression)); + } + std::pair, uint64_t> partitionBddAndBlockCount = createPartitionBdd(model.getManager(), model, stateSets, blockVariables.first); // Store the partition as an ADD only in the case of CUDD. if (DdType == storm::dd::DdType::CUDD) { diff --git a/src/storm/storage/dd/bisimulation/Partition.h b/src/storm/storage/dd/bisimulation/Partition.h index 394d6dfa8..8b5f16365 100644 --- a/src/storm/storage/dd/bisimulation/Partition.h +++ b/src/storm/storage/dd/bisimulation/Partition.h @@ -35,6 +35,7 @@ namespace storm { 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 create(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType, std::vector> const& formulas); static Partition createTrivialChoicePartition(storm::models::symbolic::NondeterministicModel const& model, std::pair const& blockVariables); uint64_t getNumberOfStates() const; @@ -85,8 +86,13 @@ namespace storm { */ static Partition create(storm::models::symbolic::Model const& model, std::vector const& expressions, storm::storage::BisimulationType const& bisimulationType); + static Partition createDistanceBased(storm::models::symbolic::Model const& model, storm::logic::Formula const& constraintFormula, storm::logic::Formula const& targetFormula); + static Partition createDistanceBased(storm::models::symbolic::Model const& model, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates); + static boost::optional, std::shared_ptr>> extractConstraintTargetFormulas(storm::logic::Formula const& formula); + static std::pair, uint64_t> createPartitionBdd(storm::dd::DdManager const& manager, storm::models::symbolic::Model const& model, std::vector> const& stateSets, storm::expressions::Variable const& blockVariable); + static std::pair createBlockVariables(storm::models::symbolic::Model const& model); static std::pair createBlockVariables(storm::dd::DdManager& manager, uint64_t numberOfDdVariables); /// The DD representing the partition. The DD is over the row variables of the model and the block variable.