From 03ad4c27833cac122cccd52b6fca26ffb72e6110 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 19 Apr 2017 18:24:47 +0200 Subject: [PATCH] first version of symbolic bisimulation minimization --- resources/3rdparty/CMakeLists.txt | 1 + .../3rdparty/sylvan/src/storm_wrapper.cpp | 2 + .../src/sylvan_storm_rational_function.c | 8 +- .../sylvan/src/sylvan_storm_rational_number.c | 8 +- resources/examples/testfiles/dtmc/die.pm | 6 - src/storm/models/symbolic/Model.cpp | 15 +- src/storm/models/symbolic/Model.h | 23 +- src/storm/storage/dd/Add.cpp | 10 + src/storm/storage/dd/Add.h | 21 +- src/storm/storage/dd/DdMetaVariable.cpp | 15 + src/storm/storage/dd/DdMetaVariable.h | 5 + .../storage/dd/bisimulation/Partition.cpp | 123 +++++++ src/storm/storage/dd/bisimulation/Partition.h | 73 ++++ .../storage/dd/bisimulation/Signature.cpp | 25 ++ src/storm/storage/dd/bisimulation/Signature.h | 24 ++ .../dd/bisimulation/SignatureRefiner.cpp | 329 ++++++++++++++++++ .../dd/bisimulation/SignatureRefiner.h | 37 ++ src/storm/storage/dd/cudd/InternalCuddAdd.cpp | 7 + src/storm/storage/dd/cudd/InternalCuddAdd.h | 9 + .../storage/dd/cudd/InternalCuddDdManager.h | 6 +- .../storage/dd/sylvan/InternalSylvanAdd.cpp | 5 + .../storage/dd/sylvan/InternalSylvanAdd.h | 16 +- .../dd/sylvan/InternalSylvanDdManager.cpp | 7 +- src/storm/utility/storm.h | 16 +- .../SymbolicBisimulationDecompositionTest.cpp | 27 ++ 25 files changed, 769 insertions(+), 49 deletions(-) create mode 100644 src/storm/storage/dd/bisimulation/Partition.cpp create mode 100644 src/storm/storage/dd/bisimulation/Partition.h create mode 100644 src/storm/storage/dd/bisimulation/Signature.cpp create mode 100644 src/storm/storage/dd/bisimulation/Signature.h create mode 100644 src/storm/storage/dd/bisimulation/SignatureRefiner.cpp create mode 100644 src/storm/storage/dd/bisimulation/SignatureRefiner.h create mode 100644 src/test/storage/SymbolicBisimulationDecompositionTest.cpp diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index b62cfb3d0..97a4b4e74 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -383,6 +383,7 @@ ExternalProject_Add( LOG_CONFIGURE ON LOG_BUILD ON BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/sylvan/src/libsylvan${STATIC_EXT} + BUILD_ALWAYS ) ExternalProject_Get_Property(sylvan source_dir) ExternalProject_Get_Property(sylvan binary_dir) diff --git a/resources/3rdparty/sylvan/src/storm_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_wrapper.cpp index edb31fda1..fe8ed9a91 100644 --- a/resources/3rdparty/sylvan/src/storm_wrapper.cpp +++ b/resources/3rdparty/sylvan/src/storm_wrapper.cpp @@ -18,6 +18,8 @@ #if defined(STORM_HAVE_GMP) && !defined(STORM_USE_CLN_EA) #define RATIONAL_NUMBER_THREAD_SAFE +#else +#warning "Rational numbers do not appear to be thread-safe. Use in sylvan will be protected by mutexes, performance might degrade." #endif // A mutex that is used to lock all operations accessing rational numbers as they are not necessarily thread-safe. diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c index 8cf8a5b88..bf24f2bd1 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c @@ -676,7 +676,7 @@ TASK_4(MTBDD, sylvan_storm_rational_function_equal_norm_d2, MTBDD, a, MTBDD, b, /* Check cache */ MTBDD result; - if (cache_get3(CACHE_MTBDD_EQUAL_NORM_RF, a, b, svalue, &result)) { + if (cache_get3(CACHE_MTBDD_EQUAL_NORM_RF, a, b, (uint64_t)svalue, &result)) { sylvan_stats_count(MTBDD_EQUAL_NORM_CACHED); return result; } @@ -700,7 +700,7 @@ TASK_4(MTBDD, sylvan_storm_rational_function_equal_norm_d2, MTBDD, a, MTBDD, b, if (result == mtbdd_false) *shortcircuit = 1; /* Store in cache */ - if (cache_put3(CACHE_MTBDD_EQUAL_NORM_RF, a, b, svalue, result)) { + if (cache_put3(CACHE_MTBDD_EQUAL_NORM_RF, a, b, (uint64_t)svalue, result)) { sylvan_stats_count(MTBDD_EQUAL_NORM_CACHEDPUT); } @@ -749,7 +749,7 @@ TASK_4(MTBDD, sylvan_storm_rational_function_equal_norm_rel_d2, MTBDD, a, MTBDD, /* Check cache */ MTBDD result; - if (cache_get3(CACHE_MTBDD_EQUAL_NORM_REL_RF, a, b, svalue, &result)) { + if (cache_get3(CACHE_MTBDD_EQUAL_NORM_REL_RF, a, b, (uint64_t)svalue, &result)) { sylvan_stats_count(MTBDD_EQUAL_NORM_REL_CACHED); return result; } @@ -773,7 +773,7 @@ TASK_4(MTBDD, sylvan_storm_rational_function_equal_norm_rel_d2, MTBDD, a, MTBDD, if (result == mtbdd_false) *shortcircuit = 1; /* Store in cache */ - if (cache_put3(CACHE_MTBDD_EQUAL_NORM_REL_RF, a, b, svalue, result)) { + if (cache_put3(CACHE_MTBDD_EQUAL_NORM_REL_RF, a, b, (uint64_t)svalue, result)) { sylvan_stats_count(MTBDD_EQUAL_NORM_REL_CACHEDPUT); } diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c index 692a6f607..7bb207a5b 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c @@ -710,7 +710,7 @@ TASK_4(MTBDD, sylvan_storm_rational_number_equal_norm_d2, MTBDD, a, MTBDD, b, st /* Check cache */ MTBDD result; - if (cache_get3(CACHE_MTBDD_EQUAL_NORM_RN, a, b, svalue, &result)) { + if (cache_get3(CACHE_MTBDD_EQUAL_NORM_RN, a, b, (uint64_t)svalue, &result)) { sylvan_stats_count(MTBDD_EQUAL_NORM_CACHED); return result; } @@ -734,7 +734,7 @@ TASK_4(MTBDD, sylvan_storm_rational_number_equal_norm_d2, MTBDD, a, MTBDD, b, st if (result == mtbdd_false) *shortcircuit = 1; /* Store in cache */ - if (cache_put3(CACHE_MTBDD_EQUAL_NORM_RN, a, b, svalue, result)) { + if (cache_put3(CACHE_MTBDD_EQUAL_NORM_RN, a, b, (uint64_t)svalue, result)) { sylvan_stats_count(MTBDD_EQUAL_NORM_CACHEDPUT); } @@ -783,7 +783,7 @@ TASK_4(MTBDD, sylvan_storm_rational_number_equal_norm_rel_d2, MTBDD, a, MTBDD, b /* Check cache */ MTBDD result; - if (cache_get3(CACHE_MTBDD_EQUAL_NORM_REL_RN, a, b, svalue, &result)) { + if (cache_get3(CACHE_MTBDD_EQUAL_NORM_REL_RN, a, b, (uint64_t)svalue, &result)) { sylvan_stats_count(MTBDD_EQUAL_NORM_REL_CACHED); return result; } @@ -807,7 +807,7 @@ TASK_4(MTBDD, sylvan_storm_rational_number_equal_norm_rel_d2, MTBDD, a, MTBDD, b if (result == mtbdd_false) *shortcircuit = 1; /* Store in cache */ - if (cache_put3(CACHE_MTBDD_EQUAL_NORM_REL_RN, a, b, svalue, result)) { + if (cache_put3(CACHE_MTBDD_EQUAL_NORM_REL_RN, a, b, (uint64_t)svalue, result)) { sylvan_stats_count(MTBDD_EQUAL_NORM_REL_CACHEDPUT); } diff --git a/resources/examples/testfiles/dtmc/die.pm b/resources/examples/testfiles/dtmc/die.pm index af0797cff..5b7eb8e36 100644 --- a/resources/examples/testfiles/dtmc/die.pm +++ b/resources/examples/testfiles/dtmc/die.pm @@ -24,9 +24,3 @@ rewards "coin_flips" endrewards label "one" = s=7&d=1; -label "two" = s=7&d=2; -label "three" = s=7&d=3; -label "four" = s=7&d=4; -label "five" = s=7&d=5; -label "six" = s=7&d=6; -label "done" = s=7; diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp index c2ca3650e..94b185b15 100644 --- a/src/storm/models/symbolic/Model.cpp +++ b/src/storm/models/symbolic/Model.cpp @@ -50,15 +50,10 @@ namespace storm { } template - storm::dd::DdManager const& Model::getManager() const { + storm::dd::DdManager& Model::getManager() const { return *manager; } - - template - storm::dd::DdManager& Model::getManager() { - return *manager; - } - + template std::shared_ptr> const& Model::getManagerAsSharedPointer() const { return manager; @@ -85,6 +80,12 @@ namespace storm { return this->getStates(labelToExpressionMap.at(label)); } + template + storm::expressions::Expression Model::getExpression(std::string const& label) const { + STORM_LOG_THROW(labelToExpressionMap.find(label) != labelToExpressionMap.end(), storm::exceptions::IllegalArgumentException, "The label " << label << " is invalid for the labeling of the model."); + return labelToExpressionMap.at(label); + } + template storm::dd::Bdd Model::getStates(storm::expressions::Expression const& expression) const { if (expression.isTrue()) { diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h index 5c9382831..fa7d683ff 100644 --- a/src/storm/models/symbolic/Model.h +++ b/src/storm/models/symbolic/Model.h @@ -9,6 +9,7 @@ #include "storm/storage/expressions/Expression.h" #include "storm/storage/expressions/Variable.h" #include "storm/storage/dd/DdType.h" +#include "storm/storage/dd/Bdd.h" #include "storm/models/ModelBase.h" #include "storm/utility/OsDetection.h" @@ -24,9 +25,6 @@ namespace storm { template class Add; - template - class Bdd; - template class DdManager; @@ -104,14 +102,7 @@ namespace storm { * * @return The manager responsible for the DDs that represent this model. */ - storm::dd::DdManager const& getManager() const; - - /*! - * Retrieves the manager responsible for the DDs that represent this model. - * - * @return The manager responsible for the DDs that represent this model. - */ - storm::dd::DdManager& getManager(); + storm::dd::DdManager& getManager() const; /*! * Retrieves the manager responsible for the DDs that represent this model. @@ -143,10 +134,18 @@ namespace storm { * Returns the sets of states labeled with the given label. * * @param label The label for which to get the labeled states. - * @return The set of states labeled with the requested label in the form of a bit vector. + * @return The set of states labeled with the requested label. */ virtual storm::dd::Bdd getStates(std::string const& label) const; + /*! + * Returns the expression for the given label. + * + * @param label The label for which to get the expression. + * @return The expression characterizing the requested label. + */ + virtual storm::expressions::Expression getExpression(std::string const& label) const; + /*! * Returns the set of states labeled satisfying the given expression (that must be of boolean type). * diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index a3d374d23..6e00de3ec 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -811,6 +811,16 @@ namespace storm { Odd Add::createOdd() const { return internalAdd.createOdd(this->getSortedVariableIndices()); } + + template + InternalAdd const& Add::getInternalAdd() const { + return internalAdd; + } + + template + InternalDdManager const& Add::getInternalDdManager() const { + return internalAdd.getInternalDdManager(); + } template Add::operator InternalAdd() const { diff --git a/src/storm/storage/dd/Add.h b/src/storm/storage/dd/Add.h index 86f443ce3..d7a757eff 100644 --- a/src/storm/storage/dd/Add.h +++ b/src/storm/storage/dd/Add.h @@ -25,6 +25,11 @@ namespace storm { template class AddIterator; + namespace bisimulation { + template + class InternalSignatureRefiner; + } + template class Add : public Dd { public: @@ -33,7 +38,9 @@ namespace storm { template friend class Add; - + + friend class bisimulation::InternalSignatureRefiner; + // Instantiate all copy/move constructors/assignments with the default implementation. Add() = default; Add(Add const& other) = default; @@ -624,7 +631,17 @@ namespace storm { * @return The corresponding ODD. */ Odd createOdd() const; - + + /*! + * Retrieves the internal ADD. + */ + InternalAdd const& getInternalAdd() const; + + /*! + * Retrieves the internal ADD. + */ + InternalDdManager const& getInternalDdManager() const; + private: /*! * Creates an ADD from the given internal ADD. diff --git a/src/storm/storage/dd/DdMetaVariable.cpp b/src/storm/storage/dd/DdMetaVariable.cpp index 620e7311e..440612d7c 100644 --- a/src/storm/storage/dd/DdMetaVariable.cpp +++ b/src/storm/storage/dd/DdMetaVariable.cpp @@ -49,6 +49,21 @@ namespace storm { return this->cube; } + template + uint64_t DdMetaVariable::getHighestLevel() const { + uint64_t result = 0; + bool first = true; + for (auto const& v : ddVariables) { + if (first) { + result = v.getLevel(); + } else { + result = std::max(result, v.getLevel()); + } + } + + return result; + } + template void DdMetaVariable::createCube() { STORM_LOG_ASSERT(!this->ddVariables.empty(), "The DD variables must not be empty."); diff --git a/src/storm/storage/dd/DdMetaVariable.h b/src/storm/storage/dd/DdMetaVariable.h index c596b612a..9b9b736ed 100644 --- a/src/storm/storage/dd/DdMetaVariable.h +++ b/src/storm/storage/dd/DdMetaVariable.h @@ -73,6 +73,11 @@ namespace storm { */ Bdd const& getCube() const; + /*! + * Retrieves the highest level of all DD variables belonging to this meta variable. + */ + uint64_t getHighestLevel() const; + private: /*! * Creates an integer meta variable with the given name and range bounds. diff --git a/src/storm/storage/dd/bisimulation/Partition.cpp b/src/storm/storage/dd/bisimulation/Partition.cpp new file mode 100644 index 000000000..6ba1c2ca9 --- /dev/null +++ b/src/storm/storage/dd/bisimulation/Partition.cpp @@ -0,0 +1,123 @@ +#include "storm/storage/dd/bisimulation/Partition.h" + +#include "storm/storage/dd/DdManager.h" + +namespace storm { + namespace dd { + namespace bisimulation { + + template + Partition::Partition(storm::dd::Add const& partitionAdd, storm::expressions::Variable const& blockVariable, uint64_t nextFreeBlockIndex) : partitionAdd(partitionAdd), blockVariable(blockVariable), nextFreeBlockIndex(nextFreeBlockIndex) { + // Intentionally left empty. + } + + template + bool Partition::operator==(Partition const& other) { + return this->partitionAdd == other.partitionAdd && this->blockVariable == other.blockVariable && this->nextFreeBlockIndex == other.nextFreeBlockIndex; + } + + template + Partition Partition::replacePartitionAdd(storm::dd::Add const& newPartitionAdd, uint64_t nextFreeBlockIndex) const { + return Partition(newPartitionAdd, blockVariable, nextFreeBlockIndex); + } + + template + Partition Partition::create(storm::models::symbolic::Model const& model) { + return create(model, model.getLabels()); + } + + template + Partition Partition::create(storm::models::symbolic::Model const& model, std::vector const& labels) { + std::vector expressions; + for (auto const& label : labels) { + expressions.push_back(model.getExpression(label)); + } + return create(model, expressions); + } + + template + Partition Partition::create(storm::models::symbolic::Model const& model, std::vector const& expressions) { + storm::dd::DdManager& manager = model.getManager(); + + std::vector> stateSets; + for (auto const& expression : expressions) { + stateSets.emplace_back(model.getStates(expression)); + } + + storm::expressions::Variable blockVariable = createBlockVariable(manager, model.getReachableStates().getNonZeroCount()); + std::pair, uint64_t> partitionAddAndBlockCount = createPartitionAdd(manager, model, stateSets, blockVariable); + return Partition(partitionAddAndBlockCount.first, blockVariable, partitionAddAndBlockCount.second); + } + + template + uint64_t Partition::getNumberOfBlocks() const { + return nextFreeBlockIndex; + } + + template + storm::dd::Add const& Partition::getPartitionAdd() const { + return partitionAdd; + } + + template + storm::expressions::Variable const& Partition::getBlockVariable() const { + return blockVariable; + } + + template + uint64_t Partition::getNextFreeBlockIndex() const { + return nextFreeBlockIndex; + } + + template + void enumerateBlocksRec(std::vector> const& stateSets, storm::dd::Bdd const& currentStateSet, uint64_t offset, storm::expressions::Variable const& blockVariable, std::function const&)> const& callback) { + if (currentStateSet.isZero()) { + return; + } + if (offset == stateSets.size()) { + callback(currentStateSet); + } else { + enumerateBlocksRec(stateSets, currentStateSet && stateSets[offset], offset + 1, blockVariable, callback); + enumerateBlocksRec(stateSets, currentStateSet && !stateSets[offset], offset + 1, blockVariable, callback); + } + } + + template + std::pair, uint64_t> Partition::createPartitionAdd(storm::dd::DdManager const& manager, storm::models::symbolic::Model const& model, std::vector> const& stateSets, storm::expressions::Variable const& blockVariable) { + uint64_t blockCount = 0; + storm::dd::Add partitionAdd = manager.template getAddZero(); + + // Enumerate all realizable blocks. + enumerateBlocksRec(stateSets, model.getReachableStates(), 0, blockVariable, [&manager, &partitionAdd, &blockVariable, &blockCount](storm::dd::Bdd const& stateSet) { + stateSet.template toAdd().exportToDot("states_" + std::to_string(blockCount) + ".dot"); + partitionAdd += (stateSet && manager.getEncoding(blockVariable, blockCount)).template toAdd(); + blockCount++; + } ); + + return std::make_pair(partitionAdd, blockCount); + } + + template + storm::expressions::Variable Partition::createBlockVariable(storm::dd::DdManager& manager, uint64_t numberOfStates) { + storm::expressions::Variable blockVariable; + if (manager.hasMetaVariable("blocks")) { + int64_t counter = 0; + while (manager.hasMetaVariable("block" + std::to_string(counter))) { + ++counter; + } + blockVariable = manager.addMetaVariable("blocks" + std::to_string(counter), 0, numberOfStates, 1).front(); + } else { + blockVariable = manager.addMetaVariable("blocks", 0, numberOfStates, 1).front(); + } + return blockVariable; + } + + template class Partition; + + template class Partition; + template class Partition; + template class Partition; + + } + } +} diff --git a/src/storm/storage/dd/bisimulation/Partition.h b/src/storm/storage/dd/bisimulation/Partition.h new file mode 100644 index 000000000..647acf996 --- /dev/null +++ b/src/storm/storage/dd/bisimulation/Partition.h @@ -0,0 +1,73 @@ +#pragma once + +#include "storm/storage/dd/DdType.h" +#include "storm/storage/dd/Add.h" + +#include "storm/models/symbolic/Model.h" + +namespace storm { + namespace dd { + namespace bisimulation { + + template + class Partition { + public: + Partition() = default; + + /*! + * Creates a new partition from the given data. + * + * @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 blockVariable The variable to use for the block encoding. Its range must be [0, x] where x is + * 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. + */ + Partition(storm::dd::Add const& partitionAdd, storm::expressions::Variable const& blockVariable, uint64_t nextFreeBlockIndex); + + bool operator==(Partition const& other); + + Partition replacePartitionAdd(storm::dd::Add const& newPartitionAdd, uint64_t nextFreeBlockIndex) const; + + /*! + * Creates a partition from the given model that respects all labels. + */ + static Partition create(storm::models::symbolic::Model const& model); + + /*! + * 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); + + /*! + * 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); + + uint64_t getNumberOfBlocks() const; + + storm::dd::Add const& getPartitionAdd() const; + + storm::expressions::Variable const& getBlockVariable() const; + + uint64_t getNextFreeBlockIndex() const; + + private: + static std::pair, uint64_t> createPartitionAdd(storm::dd::DdManager const& manager, storm::models::symbolic::Model const& model, std::vector> const& stateSets, storm::expressions::Variable const& blockVariable); + + static storm::expressions::Variable createBlockVariable(storm::dd::DdManager& manager, uint64_t numberOfStates); + + // The ADD representing the partition. The ADD is over the row variables of the model and the block variable. + storm::dd::Add partitionAdd; + + // The meta variable used to encode the block of each state in this partition. + storm::expressions::Variable blockVariable; + + // The next free block index. + uint64_t nextFreeBlockIndex; + }; + + } + } +} diff --git a/src/storm/storage/dd/bisimulation/Signature.cpp b/src/storm/storage/dd/bisimulation/Signature.cpp new file mode 100644 index 000000000..e4a06feab --- /dev/null +++ b/src/storm/storage/dd/bisimulation/Signature.cpp @@ -0,0 +1,25 @@ +#include "storm/storage/dd/bisimulation/Signature.h" + +namespace storm { + namespace dd { + namespace bisimulation { + + template + Signature::Signature(storm::dd::Add const& signatureAdd) : signatureAdd(signatureAdd) { + // Intentionally left empty. + } + + template + storm::dd::Add const& Signature::getSignatureAdd() const { + return signatureAdd; + } + + template class Signature; + + template class Signature; + template class Signature; + template class Signature; + + } + } +} diff --git a/src/storm/storage/dd/bisimulation/Signature.h b/src/storm/storage/dd/bisimulation/Signature.h new file mode 100644 index 000000000..437839d54 --- /dev/null +++ b/src/storm/storage/dd/bisimulation/Signature.h @@ -0,0 +1,24 @@ +#pragma once + +#include "storm/storage/dd/DdType.h" + +#include "storm/storage/dd/bisimulation/Partition.h" + +namespace storm { + namespace dd { + namespace bisimulation { + + template + class Signature { + public: + Signature(storm::dd::Add const& signatureAdd); + + storm::dd::Add const& getSignatureAdd() const; + + private: + storm::dd::Add signatureAdd; + }; + + } + } +} diff --git a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp new file mode 100644 index 000000000..2ac0dd22c --- /dev/null +++ b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp @@ -0,0 +1,329 @@ +#include "storm/storage/dd/bisimulation/SignatureRefiner.h" + +#include + +#include "storm/storage/dd/DdManager.h" + +#include "storm/storage/dd/cudd/InternalCuddDdManager.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/NotImplementedException.h" + +#include "resources/3rdparty/sparsepp/sparsepp.h" + +namespace storm { + namespace dd { + namespace bisimulation { + + struct CuddPointerPairHash { + std::size_t operator()(std::pair const& pair) const { + std::size_t seed = std::hash()(pair.first); + boost::hash_combine(seed, pair.second); + return seed; + } + }; + + struct SylvanMTBDDPairHash { + std::size_t operator()(std::pair const& pair) const { + std::size_t seed = std::hash()(pair.first); + boost::hash_combine(seed, pair.second); + return seed; + } + }; + + template + class InternalSignatureRefiner; + + template + class InternalSignatureRefiner { + public: + InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, uint64_t lastStateLevel) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), lastStateLevel(lastStateLevel), nextFreeBlockIndex(0), numberOfRefinements(0) { + // Intentionally left empty. + } + + Partition refine(Partition const& oldPartition, Signature const& signature) { + storm::dd::Add newPartitionAdd = refine(oldPartition, signature.getSignatureAdd()); + ++numberOfRefinements; + return oldPartition.replacePartitionAdd(newPartitionAdd, nextFreeBlockIndex); + } + + private: + storm::dd::Add refine(Partition const& oldPartition, storm::dd::Add const& signatureAdd) { + // Clear the caches. + signatureCache.clear(); + reuseBlocksCache.clear(); + nextFreeBlockIndex = oldPartition.getNextFreeBlockIndex(); + + // Perform the actual recursive refinement step. + DdNodePtr result = refine(oldPartition.getPartitionAdd().getInternalAdd().getCuddDdNode(), signatureAdd.getInternalAdd().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.getPartitionAdd().getDdManager(), internalNewPartitionAdd, oldPartition.getPartitionAdd().getContainedMetaVariables()); + + return newPartitionAdd; + } + + DdNodePtr refine(DdNode* partitionNode, DdNode* signatureNode) { + ::DdManager* ddman = internalDdManager.getCuddManager().getManager(); + + // Check the cache whether we have seen the same node before. + auto sigCacheIt = signatureCache.find(std::make_pair(signatureNode, partitionNode)); + if (sigCacheIt != signatureCache.end()) { + // If so, we return the corresponding result. + return sigCacheIt->second; + } + + // Determine the levels in the DDs. + uint64_t partitionVariable = Cudd_NodeReadIndex(partitionNode); + uint64_t signatureVariable = Cudd_NodeReadIndex(signatureNode); + uint64_t partitionLevel = Cudd_ReadPerm(ddman, partitionVariable); + uint64_t signatureLevel = Cudd_ReadPerm(ddman, signatureVariable); + uint64_t topLevel = std::min(partitionLevel, signatureLevel); + uint64_t topVariable = topLevel == partitionLevel ? partitionVariable : signatureVariable; + + // Check whether the top variable is still within the state encoding. + if (topLevel <= lastStateLevel) { + // Determine subresults by recursive descent. + DdNodePtr thenResult; + DdNodePtr elseResult; + if (partitionLevel < signatureLevel) { + thenResult = refine(Cudd_T(partitionNode), signatureNode); + Cudd_Ref(thenResult); + elseResult = refine(Cudd_E(partitionNode), signatureNode); + Cudd_Ref(elseResult); + } else if (partitionLevel > signatureLevel) { + thenResult = refine(partitionNode, Cudd_T(signatureNode)); + Cudd_Ref(thenResult); + elseResult = refine(partitionNode, Cudd_E(signatureNode)); + Cudd_Ref(elseResult); + } else { + thenResult = refine(Cudd_T(partitionNode), Cudd_T(signatureNode)); + Cudd_Ref(thenResult); + elseResult = refine(Cudd_E(partitionNode), Cudd_E(signatureNode)); + Cudd_Ref(elseResult); + } + + if (thenResult == elseResult) { + Cudd_Deref(thenResult); + Cudd_Deref(elseResult); + return thenResult; + } + + // Get the node to connect the subresults. + DdNode* var = Cudd_addIthVar(ddman, topVariable); + Cudd_Ref(var); + DdNode* result = Cudd_addIte(ddman, var, thenResult, elseResult); + Cudd_Ref(result); + Cudd_RecursiveDeref(ddman, var); + Cudd_Deref(thenResult); + Cudd_Deref(elseResult); + + // Store the result in the cache. + signatureCache[std::make_pair(signatureNode, partitionNode)] = result; + + Cudd_Deref(result); + return result; + } else { + + // If we are not within the state encoding any more, we hit the signature itself. + + // 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; + } + + // If this is the first time (in this traversal) that we encounter this signature, we check + // whether we can assign the old block number to it. + auto reuseCacheIt = reuseBlocksCache.find(partitionNode); + if (reuseCacheIt == reuseBlocksCache.end()) { + reuseBlocksCache.emplace(partitionNode, true); + signatureCache[std::make_pair(signatureNode, partitionNode)] = partitionNode; + return partitionNode; + } else { + DdNode* result; + { + storm::dd::Add blockEncoding = manager.getEncoding(blockVariable, nextFreeBlockIndex).template toAdd(); + ++nextFreeBlockIndex; + result = blockEncoding.getInternalAdd().getCuddDdNode(); + Cudd_Ref(result); + } + signatureCache[std::make_pair(signatureNode, partitionNode)] = result; + Cudd_Deref(result); + return result; + } + } + } + + storm::dd::DdManager const& manager; + storm::dd::InternalDdManager const& internalDdManager; + storm::expressions::Variable const& blockVariable; + + // The last level that belongs to the state encoding in the DDs. + uint64_t lastStateLevel; + + // The current number of blocks of the new partition. + uint64_t nextFreeBlockIndex; + + // The number of completed refinements. + uint64_t numberOfRefinements; + + // The cache used to identify states with identical signature. + spp::sparse_hash_map, DdNode*, CuddPointerPairHash> signatureCache; + + // The cache used to identify which old block numbers have already been reused. + spp::sparse_hash_map reuseBlocksCache; + }; + + + template + class InternalSignatureRefiner { + public: + InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, uint64_t lastStateLevel) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), lastStateLevel(lastStateLevel), nextFreeBlockIndex(0), numberOfRefinements(0) { + // Intentionally left empty. + } + + Partition refine(Partition const& oldPartition, Signature const& signature) { + storm::dd::Add newPartitionAdd = refine(oldPartition, signature.getSignatureAdd()); + ++numberOfRefinements; + return oldPartition.replacePartitionAdd(newPartitionAdd, nextFreeBlockIndex); + } + + private: + storm::dd::Add refine(Partition const& oldPartition, storm::dd::Add const& signatureAdd) { + // Clear the caches. + signatureCache.clear(); + reuseBlocksCache.clear(); + nextFreeBlockIndex = oldPartition.getNextFreeBlockIndex(); + + // Perform the actual recursive refinement step. + MTBDD result = refine(oldPartition.getPartitionAdd().getInternalAdd().getSylvanMtbdd().GetMTBDD(), signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD()); + + // Construct resulting ADD from the obtained node and the meta information. + storm::dd::InternalAdd internalNewPartitionAdd(&internalDdManager, sylvan::Mtbdd(result)); + storm::dd::Add newPartitionAdd(oldPartition.getPartitionAdd().getDdManager(), internalNewPartitionAdd, oldPartition.getPartitionAdd().getContainedMetaVariables()); + + return newPartitionAdd; + } + + MTBDD refine(MTBDD partitionNode, MTBDD signatureNode) { + LACE_ME; + + // Check the cache whether we have seen the same node before. + auto sigCacheIt = signatureCache.find(std::make_pair(signatureNode, partitionNode)); + if (sigCacheIt != signatureCache.end()) { + // If so, we return the corresponding result. + return sigCacheIt->second; + } + + // Determine levels in the DDs. + BDDVAR signatureVariable = mtbdd_isleaf(signatureNode) ? 0xffffffff : sylvan_var(signatureNode); + BDDVAR partitionVariable = sylvan_var(partitionNode); + BDDVAR topVariable = std::min(signatureVariable, partitionVariable); + + // Check whether the top variable is still within the state encoding. + if (topVariable <= lastStateLevel) { + // Determine subresults by recursive descent. + MTBDD thenResult; + MTBDD elseResult; + if (partitionVariable < signatureVariable) { + thenResult = refine(sylvan_high(partitionNode), signatureNode); + elseResult = refine(sylvan_low(partitionNode), signatureNode); + } else if (partitionVariable > signatureVariable) { + thenResult = refine(partitionNode, sylvan_high(signatureNode)); + elseResult = refine(partitionNode, sylvan_low(signatureNode)); + } else { + thenResult = refine(sylvan_high(partitionNode), sylvan_high(signatureNode)); + elseResult = refine(sylvan_low(partitionNode), sylvan_low(signatureNode)); + } + + if (thenResult == elseResult) { + return thenResult; + } + + // Get the node to connect the subresults. + MTBDD result = mtbdd_ite(sylvan_ithvar(topVariable), thenResult, elseResult); + + // Store the result in the cache. + signatureCache[std::make_pair(signatureNode, partitionNode)] = result; + + return result; + } else { + + // If we are not within the state encoding any more, we hit the signature itself. + + // 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 signatureNode; + } + + // If this is the first time (in this traversal) that we encounter this signature, we check + // whether we can assign the old block number to it. + auto reuseCacheIt = reuseBlocksCache.find(partitionNode); + if (reuseCacheIt == reuseBlocksCache.end()) { + reuseBlocksCache.emplace(partitionNode, true); + signatureCache[std::make_pair(signatureNode, partitionNode)] = partitionNode; + return partitionNode; + } else { + MTBDD result; + { + storm::dd::Add blockEncoding = manager.getEncoding(blockVariable, nextFreeBlockIndex).template toAdd(); + ++nextFreeBlockIndex; + result = blockEncoding.getInternalAdd().getSylvanMtbdd().GetMTBDD(); + } + signatureCache[std::make_pair(signatureNode, partitionNode)] = result; + return result; + } + } + } + + storm::dd::DdManager const& manager; + storm::dd::InternalDdManager const& internalDdManager; + storm::expressions::Variable const& blockVariable; + + // The last level that belongs to the state encoding in the DDs. + uint64_t lastStateLevel; + + // The current number of blocks of the new partition. + uint64_t nextFreeBlockIndex; + + // The number of completed refinements. + uint64_t numberOfRefinements; + + // The cache used to identify states with identical signature. + spp::sparse_hash_map, MTBDD, SylvanMTBDDPairHash> signatureCache; + + // The cache used to identify which old block numbers have already been reused. + spp::sparse_hash_map reuseBlocksCache; + }; + + template + SignatureRefiner::SignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables) : manager(manager), stateVariables(stateVariables) { + uint64_t lastStateLevel = 0; + for (auto const& stateVariable : stateVariables) { + lastStateLevel = std::max(lastStateLevel, manager.getMetaVariable(stateVariable).getHighestLevel()); + } + + internalRefiner = std::make_unique>(manager, blockVariable, lastStateLevel); + } + + template + SignatureRefiner::~SignatureRefiner() = default; + + template + Partition SignatureRefiner::refine(Partition const& oldPartition, Signature const& signature) { + return internalRefiner->refine(oldPartition, signature); + } + + template class SignatureRefiner; + + template class SignatureRefiner; + template class SignatureRefiner; + template class SignatureRefiner; + + + } + } +} diff --git a/src/storm/storage/dd/bisimulation/SignatureRefiner.h b/src/storm/storage/dd/bisimulation/SignatureRefiner.h new file mode 100644 index 000000000..32532dc62 --- /dev/null +++ b/src/storm/storage/dd/bisimulation/SignatureRefiner.h @@ -0,0 +1,37 @@ +#pragma once + +#include "storm/storage/dd/DdType.h" + +#include "storm/storage/dd/bisimulation/Partition.h" +#include "storm/storage/dd/bisimulation/Signature.h" + +namespace storm { + namespace dd { + namespace bisimulation { + + template + class InternalSignatureRefiner; + + template + class SignatureRefiner { + public: + SignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables); + + ~SignatureRefiner(); + + Partition refine(Partition const& oldPartition, Signature const& signature); + + private: + // The manager responsible for the DDs. + storm::dd::DdManager const& manager; + + // The variables encodin the states. + std::set const& stateVariables; + + // The internal refiner. + std::unique_ptr> internalRefiner; + }; + + } + } +} diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp index d02222df0..142381d36 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp @@ -209,6 +209,8 @@ namespace storm { summationAdds.push_back(ddVariable.toAdd().getCuddAdd()); } + return InternalAdd(ddManager, this->getCuddAdd().TimesPlus(otherMatrix.getCuddAdd(), summationAdds)); + return InternalAdd(ddManager, this->getCuddAdd().Triangle(otherMatrix.getCuddAdd(), summationAdds)); return InternalAdd(ddManager, this->getCuddAdd().MatrixMultiply(otherMatrix.getCuddAdd(), summationAdds)); } @@ -425,6 +427,11 @@ namespace storm { } } + template + InternalDdManager const& InternalAdd::getInternalDdManager() const { + return *ddManager; + } + template void InternalAdd::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const { composeWithExplicitVectorRec(this->getCuddDdNode(), nullptr, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function); diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.h b/src/storm/storage/dd/cudd/InternalCuddAdd.h index 360a7b0f9..2218e3f62 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.h @@ -38,12 +38,19 @@ namespace storm { template class AddIterator; + + namespace bisimulation { + template + class InternalSignatureRefiner; + } template class InternalAdd { public: friend class InternalBdd; + friend class bisimulation::InternalSignatureRefiner; + /*! * Creates an ADD that encapsulates the given CUDD ADD. * @@ -576,6 +583,8 @@ namespace storm { */ Odd createOdd(std::vector const& ddVariableIndices) const; + InternalDdManager const& getInternalDdManager() const; + private: /*! * Retrieves the CUDD ADD object associated with this ADD. diff --git a/src/storm/storage/dd/cudd/InternalCuddDdManager.h b/src/storm/storage/dd/cudd/InternalCuddDdManager.h index 17d715206..404f577bf 100644 --- a/src/storm/storage/dd/cudd/InternalCuddDdManager.h +++ b/src/storm/storage/dd/cudd/InternalCuddDdManager.h @@ -118,21 +118,21 @@ namespace storm { */ uint_fast64_t getNumberOfDdVariables() const; - private: /*! * Retrieves the underlying CUDD manager. * * @return The underlying CUDD manager. */ cudd::Cudd& getCuddManager(); - + /*! * Retrieves the underlying CUDD manager. * * @return The underlying CUDD manager. */ cudd::Cudd const& getCuddManager() const; - + + private: // The manager responsible for the DDs created/modified with this DdManager. cudd::Cudd cuddManager; diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index dfa171eef..052fc2925 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -828,6 +828,11 @@ namespace storm { } } + template + InternalDdManager const& InternalAdd::getInternalDdManager() const { + return *ddManager; + } + template void InternalAdd::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const { composeWithExplicitVectorRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_hascomp(this->getSylvanMtbdd().GetMTBDD()), nullptr, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function); diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h index 13b96d25a..d719462ea 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h @@ -586,6 +586,15 @@ namespace storm { */ Odd createOdd(std::vector const& ddVariableIndices) const; + InternalDdManager const& getInternalDdManager() const; + + /*! + * Retrieves the underlying sylvan MTBDD. + * + * @return The sylvan MTBDD. + */ + sylvan::Mtbdd getSylvanMtbdd() const; + private: /*! * Recursively builds the ODD from an ADD. @@ -721,13 +730,6 @@ namespace storm { */ static ValueType getValue(MTBDD const& node); - /*! - * Retrieves the underlying sylvan MTBDD. - * - * @return The sylvan MTBDD. - */ - sylvan::Mtbdd getSylvanMtbdd() const; - // The manager responsible for this MTBDD. InternalDdManager const* ddManager; diff --git a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp index c026fbb1f..38644c856 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp @@ -9,6 +9,7 @@ #include "storm/utility/constants.h" #include "storm/utility/macros.h" #include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/InvalidSettingsException.h" #include "storm/utility/sylvan.h" @@ -47,7 +48,11 @@ namespace storm { // Compute the power of two that still fits within the total numbers to store. uint_fast64_t powerOfTwo = findLargestPowerOfTwoFitting(totalNodesToStore); - sylvan::Sylvan::initPackage(1ull << std::max(16ull, powerOfTwo > 24 ? powerOfTwo - 8 : 0ull), 1ull << (powerOfTwo - 1), 1ull << std::max(16ull, powerOfTwo > 24 ? powerOfTwo - 12 : 0ull), 1ull << (powerOfTwo - 1)); + STORM_LOG_THROW(powerOfTwo >= 16, storm::exceptions::InvalidSettingsException, "Too little memory assigned to sylvan."); + + STORM_LOG_TRACE("Assigning " << (1ull << (powerOfTwo - 1)) << " slots to both sylvan's unique table and its cache."); + sylvan::Sylvan::initPackage(1ull << (powerOfTwo - 1), 1ull << (powerOfTwo - 1), 1ull << (powerOfTwo - 1), 1ull << (powerOfTwo - 1)); + sylvan::Sylvan::setGranularity(3); sylvan::Sylvan::initBdd(); sylvan::Sylvan::initMtbdd(); sylvan::Sylvan::initCustomMtbdd(); diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index 407c0b40c..af63624de 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -54,6 +54,7 @@ // Headers for model processing. #include "storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h" #include "storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h" +#include "storm/storage/dd/BisimulationDecomposition.h" #include "storm/transformer/SymbolicToSparseTransformer.h" #include "storm/storage/ModelFormulasPair.h" #include "storm/storage/SymbolicModelDescription.h" @@ -167,20 +168,30 @@ namespace storm { template std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas) { + std::shared_ptr> result; if (model.isPrismProgram()) { typename storm::builder::DdPrismModelBuilder::Options options; options = typename storm::builder::DdPrismModelBuilder::Options(formulas); storm::builder::DdPrismModelBuilder builder; - return builder.build(model.asPrismProgram(), options); + result = builder.build(model.asPrismProgram(), options); } else { STORM_LOG_THROW(model.isJaniModel(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model for the given symbolic model description."); typename storm::builder::DdJaniModelBuilder::Options options; options = typename storm::builder::DdJaniModelBuilder::Options(formulas); storm::builder::DdJaniModelBuilder builder; - return builder.build(model.asJaniModel(), options); + result = builder.build(model.asJaniModel(), options); } + + if (storm::settings::getModule().isBisimulationSet()) { + storm::dd::BisimulationDecomposition decomposition(*result); + decomposition.compute(); + + // TODO build quotient and return it. + } + + return result; } template @@ -237,7 +248,6 @@ namespace storm { return performBisimulationMinimization(model, formulas , type); } - template std::shared_ptr preprocessModel(std::shared_ptr model, std::vector> const& formulas) { storm::utility::Stopwatch preprocessingWatch(true); diff --git a/src/test/storage/SymbolicBisimulationDecompositionTest.cpp b/src/test/storage/SymbolicBisimulationDecompositionTest.cpp new file mode 100644 index 000000000..4948f7906 --- /dev/null +++ b/src/test/storage/SymbolicBisimulationDecompositionTest.cpp @@ -0,0 +1,27 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "storm/parser/PrismParser.h" +#include "storm/storage/SymbolicModelDescription.h" +#include "storm/builder/DdPrismModelBuilder.h" +#include "storm/models/symbolic/Dtmc.h" +#include "storm/storage/dd/BisimulationDecomposition.h" + +TEST(SymbolicBisimulationDecompositionTest_Cudd, Die) { + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); + + storm::dd::BisimulationDecomposition decomposition(*model, storm::dd::bisimulation::Partition::create(*model, {"one"})); + decomposition.compute(); +} + +TEST(SymbolicBisimulationDecompositionTest_Cudd, Crowds) { + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); + + storm::dd::BisimulationDecomposition decomposition(*model, storm::dd::bisimulation::Partition::create(*model, {"observe0Greater1"})); + decomposition.compute(); +}