From c586213bc60bf7690acfc25a6dcadae381d67abb Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 1 Aug 2017 13:28:54 +0200 Subject: [PATCH] started on factoring out preservation information --- .../storage/dd/bisimulation/Partition.cpp | 65 +++------------- src/storm/storage/dd/bisimulation/Partition.h | 35 ++------- .../bisimulation/PreservationInformation.cpp | 74 ++++++++++++++++++- .../dd/bisimulation/PreservationInformation.h | 13 ++++ 4 files changed, 98 insertions(+), 89 deletions(-) diff --git a/src/storm/storage/dd/bisimulation/Partition.cpp b/src/storm/storage/dd/bisimulation/Partition.cpp index 7c434f653..187c235e1 100644 --- a/src/storm/storage/dd/bisimulation/Partition.cpp +++ b/src/storm/storage/dd/bisimulation/Partition.cpp @@ -20,12 +20,12 @@ namespace storm { namespace bisimulation { template - Partition::Partition(std::shared_ptr preservationInformation, storm::dd::Add const& partitionAdd, std::pair const& blockVariables, uint64_t nextFreeBlockIndex) : preservationInformation(preservationInformation), partition(partitionAdd), blockVariables(blockVariables), nextFreeBlockIndex(nextFreeBlockIndex) { + Partition::Partition(storm::dd::Add const& partitionAdd, std::pair const& blockVariables, uint64_t nextFreeBlockIndex) : partition(partitionAdd), blockVariables(blockVariables), nextFreeBlockIndex(nextFreeBlockIndex) { // Intentionally left empty. } template - Partition::Partition(std::shared_ptr preservationInformation, storm::dd::Bdd const& partitionBdd, std::pair const& blockVariables, uint64_t nextFreeBlockIndex) : preservationInformation(preservationInformation), partition(partitionBdd), blockVariables(blockVariables), nextFreeBlockIndex(nextFreeBlockIndex) { + Partition::Partition(storm::dd::Bdd const& partitionBdd, std::pair const& blockVariables, uint64_t nextFreeBlockIndex) : partition(partitionBdd), blockVariables(blockVariables), nextFreeBlockIndex(nextFreeBlockIndex) { // Intentionally left empty. } @@ -36,72 +36,27 @@ namespace storm { template Partition Partition::replacePartition(storm::dd::Add const& newPartitionAdd, uint64_t nextFreeBlockIndex) const { - return Partition(preservationInformation, newPartitionAdd, blockVariables, nextFreeBlockIndex); + return Partition(newPartitionAdd, blockVariables, nextFreeBlockIndex); } template Partition Partition::replacePartition(storm::dd::Bdd const& newPartitionBdd, uint64_t nextFreeBlockIndex) const { - return Partition(preservationInformation, newPartitionBdd, blockVariables, nextFreeBlockIndex); + return Partition(newPartitionBdd, blockVariables, nextFreeBlockIndex); } template - Partition Partition::create(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType) { - return create(model, model.getLabels(), bisimulationType); - } - - template - Partition Partition::create(storm::models::symbolic::Model const& model, std::vector const& labels, storm::storage::BisimulationType const& bisimulationType) { - std::shared_ptr preservationInformation = std::make_shared(); - std::vector expressions; - for (auto const& label : labels) { - preservationInformation->addLabel(label); - expressions.push_back(model.getExpression(label)); - } - return create(model, expressions, preservationInformation, bisimulationType); - } - - template - Partition Partition::create(storm::models::symbolic::Model const& model, std::vector const& expressions, storm::storage::BisimulationType const& bisimulationType) { - std::shared_ptr preservationInformation = std::make_shared(); - for (auto const& expression : expressions) { - preservationInformation->addExpression(expression); - } - return create(model, expressions, preservationInformation, bisimulationType); - } - - template - Partition Partition::create(storm::models::symbolic::Model const& model, std::vector> const& formulas, storm::storage::BisimulationType const& bisimulationType) { - if (formulas.empty()) { - return create(model, bisimulationType); - } - - std::shared_ptr preservationInformation = std::make_shared(); - std::set labels; - std::set expressions; - - for (auto const& formula : formulas) { - for (auto const& expressionFormula : formula->getAtomicExpressionFormulas()) { - expressions.insert(expressionFormula->getExpression()); - preservationInformation->addExpression(expressionFormula->getExpression()); - } - for (auto const& labelFormula : formula->getAtomicLabelFormulas()) { - std::string const& label = labelFormula->getLabel(); - STORM_LOG_THROW(model.hasLabel(label), storm::exceptions::InvalidPropertyException, "Property refers to illegal label '" << label << "'."); - preservationInformation->addLabel(label); - expressions.insert(model.getExpression(label)); - } - } + Partition Partition::create(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType, PreservationInformation const& preservationInformation) { std::vector expressionVector; - for (auto const& expression : expressions) { + for (auto const& expression : preservationInformation.getExpressions()) { expressionVector.emplace_back(expression); } - return create(model, expressionVector, preservationInformation, bisimulationType); + return create(model, expressionVector, bisimulationType); } template - Partition Partition::create(storm::models::symbolic::Model const& model, std::vector const& expressions, std::shared_ptr const& preservationInformation, storm::storage::BisimulationType const& bisimulationType) { + 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."); @@ -123,9 +78,9 @@ namespace storm { // Store the partition as an ADD only in the case of CUDD. if (DdType == storm::dd::DdType::CUDD) { - return Partition(preservationInformation, partitionBddAndBlockCount.first.template toAdd(), blockVariables, partitionBddAndBlockCount.second); + return Partition(partitionBddAndBlockCount.first.template toAdd(), blockVariables, partitionBddAndBlockCount.second); } else { - return Partition(preservationInformation, partitionBddAndBlockCount.first, blockVariables, partitionBddAndBlockCount.second); + return Partition(partitionBddAndBlockCount.first, blockVariables, partitionBddAndBlockCount.second); } } diff --git a/src/storm/storage/dd/bisimulation/Partition.h b/src/storm/storage/dd/bisimulation/Partition.h index 80d882645..59183a332 100644 --- a/src/storm/storage/dd/bisimulation/Partition.h +++ b/src/storm/storage/dd/bisimulation/Partition.h @@ -30,28 +30,9 @@ 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; - /*! - * Creates a partition from the given model that respects all labels. - */ - static Partition create(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType); - - /*! - * Creates a partition from the given model that respects the given labels. - */ - static Partition create(storm::models::symbolic::Model const& model, std::vector const& labels, storm::storage::BisimulationType const& bisimulationType); - - /*! - * Creates a partition from the given model that respects the given expressions. - */ - static Partition create(storm::models::symbolic::Model const& model, std::vector const& expressions, storm::storage::BisimulationType const& bisimulationType); - - /*! - * Creates a partition from the given model that preserves the given formulas. - */ - static Partition create(storm::models::symbolic::Model const& model, std::vector> const& formulas, storm::storage::BisimulationType const& bisimulationType); + static Partition create(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType, PreservationInformation const& preservationInformation); uint64_t getNumberOfStates() const; uint64_t getNumberOfBlocks() const; @@ -69,14 +50,11 @@ namespace storm { uint64_t getNodeCount() const; storm::dd::Bdd getStates() const; - - PreservationInformation const& getPreservationInformation() const; - + private: /*! * Creates a new partition from the given data. * - * @param preservationInformation Informatin about which labels/expressions this partition preserves. * @param partitionAdd An ADD that maps encoding over the state/row variables and the block variable to * 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 @@ -84,12 +62,11 @@ namespace storm { * @param nextFreeBlockIndex The next free block index. The existing blocks must be encoded with indices * between 0 and this number. */ - Partition(std::shared_ptr preservationInformation, storm::dd::Add const& partitionAdd, std::pair const& blockVariables, uint64_t nextFreeBlockIndex); + Partition(storm::dd::Add const& partitionAdd, std::pair const& blockVariables, uint64_t nextFreeBlockIndex); /*! * Creates a new partition from the given data. * - * @param preservationInformation Informatin about which labels/expressions this partition preserves. * @param partitionBdd A BDD that maps encoding over the state/row variables and the block variable to * 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 @@ -97,18 +74,16 @@ namespace storm { * @param nextFreeBlockIndex The next free block index. The existing blocks must be encoded with indices * between 0 and this number. */ - Partition(std::shared_ptr preservationInformation, storm::dd::Bdd const& partitionBdd, std::pair const& blockVariables, uint64_t nextFreeBlockIndex); + Partition(storm::dd::Bdd const& partitionBdd, std::pair const& blockVariables, uint64_t nextFreeBlockIndex); /*! * Creates a partition from the given model that respects the given expressions. */ - static Partition create(storm::models::symbolic::Model const& model, std::vector const& expressions, std::shared_ptr const& preservationInformation, storm::storage::BisimulationType const& bisimulationType); + static Partition create(storm::models::symbolic::Model const& model, std::vector const& expressions, storm::storage::BisimulationType const& bisimulationType); 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::dd::DdManager& manager, uint64_t numberOfDdVariables); - - std::shared_ptr preservationInformation; /// The DD representing the partition. The DD is over the row variables of the model and the block variable. boost::variant, storm::dd::Add> partition; diff --git a/src/storm/storage/dd/bisimulation/PreservationInformation.cpp b/src/storm/storage/dd/bisimulation/PreservationInformation.cpp index f6d25ff4d..363e88fdd 100644 --- a/src/storm/storage/dd/bisimulation/PreservationInformation.cpp +++ b/src/storm/storage/dd/bisimulation/PreservationInformation.cpp @@ -1,24 +1,90 @@ #include "storm/storage/dd/bisimulation/PreservationInformation.h" +#include "storm/logic/Formulas.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidPropertyException.h" + namespace storm { namespace dd { namespace bisimulation { - void PreservationInformation::addLabel(std::string const& label) { + template + PreservationInformation::PreservationInformation(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType) : PreservationInformation(model, model.getLabels(), bisimulationType) { + // Intentionally left empty. + } + + template + PreservationInformation::PreservationInformation(storm::models::symbolic::Model const& model, std::vector const& labels, storm::storage::BisimulationType const& bisimulationType) { + for (auto const& label : labels) { + this->addLabel(label); + this->addExpression(model.getExpression(label)); + } + } + + template + PreservationInformation::PreservationInformation(storm::models::symbolic::Model const& model, std::vector const& expressions, storm::storage::BisimulationType const& bisimulationType) { + 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& bisimulationType) { + if (formulas.empty()) { + // Default to respect all labels if no formulas are given. + for (auto const& label : model.getLabels()) { + this->addLabel(label); + this->addExpression(model.getExpression(label)); + } + } else { + std::set labels; + std::set expressions; + + for (auto const& formula : formulas) { + for (auto const& expressionFormula : formula->getAtomicExpressionFormulas()) { + this->addExpression(expressionFormula->getExpression()); + } + for (auto const& labelFormula : formula->getAtomicLabelFormulas()) { + this->addLabel(labelFormula->getLabel()); + std::string const& label = labelFormula->getLabel(); + STORM_LOG_THROW(model.hasLabel(label), storm::exceptions::InvalidPropertyException, "Property refers to illegal label '" << label << "'."); + this->addExpression(model.getExpression(label)); + } + } + + std::vector expressionVector; + for (auto const& expression : expressions) { + expressionVector.emplace_back(expression); + } + } + } + + template + void PreservationInformation::addLabel(std::string const& label) { labels.insert(label); } - void PreservationInformation::addExpression(storm::expressions::Expression const& expression) { + template + void PreservationInformation::addExpression(storm::expressions::Expression const& expression) { expressions.insert(expression); } - std::set const& PreservationInformation::getLabels() const { + template + std::set const& PreservationInformation::getLabels() const { return labels; } - std::set const& PreservationInformation::getExpressions() const { + template + std::set const& PreservationInformation::getExpressions() const { return expressions; } + + template class PreservationInformation; + + template class PreservationInformation; + template class PreservationInformation; + template class PreservationInformation; } } } diff --git a/src/storm/storage/dd/bisimulation/PreservationInformation.h b/src/storm/storage/dd/bisimulation/PreservationInformation.h index 1aa2620bd..a5bfbc3d1 100644 --- a/src/storm/storage/dd/bisimulation/PreservationInformation.h +++ b/src/storm/storage/dd/bisimulation/PreservationInformation.h @@ -2,6 +2,13 @@ #include #include +#include +#include + +#include "storm/models/symbolic/Model.h" +#include "storm/storage/bisimulation/BisimulationType.h" + +#include "storm/logic/Formula.h" #include "storm/storage/expressions/Expression.h" @@ -9,9 +16,15 @@ namespace storm { namespace dd { namespace bisimulation { + template class PreservationInformation { 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); void addLabel(std::string const& label); void addExpression(storm::expressions::Expression const& expression);