diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index 5882fa4f3..89f854d6d 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -78,6 +78,14 @@ class AbstractDeterministicModel: public AbstractModel { virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const { return this->transitionMatrix.constColumnIteratorEnd(state); } + + /*! + * Calculates a hash over all values contained in this Model. + * @return size_t A Hash Value + */ + virtual std::size_t getHash() const override { + return AbstractModel::getHash(); + } virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const override { AbstractModel::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index bd3583739..f605218f8 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -4,6 +4,7 @@ #include "src/models/AtomicPropositionsLabeling.h" #include "src/storage/BitVector.h" #include "src/storage/SparseMatrix.h" +#include "src/utility/Hash.h" #include #include @@ -377,6 +378,23 @@ class AbstractModel: public std::enable_shared_from_this> { out << "-------------------------------------------------------------- " << std::endl; } + /*! + * Calculates a hash over all values contained in this Model. + * @return size_t A Hash Value + */ + virtual size_t getHash() const { + std::size_t result = 0; + boost::hash_combine(result, transitionMatrix.getHash()); + boost::hash_combine(result, stateLabeling.getHash()); + if (stateRewardVector) { + boost::hash_combine(result, storm::utility::Hash::getHash(stateRewardVector.get())); + } + if (transitionRewardMatrix) { + boost::hash_combine(result, transitionRewardMatrix.get().getHash()); + } + return result; + } + protected: /*! * Exports the model to the dot-format and prints the result to the given stream. diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index 763b87128..f5e631555 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -126,6 +126,17 @@ class AbstractNondeterministicModel: public AbstractModel { return this->transitionMatrix.constColumnIteratorEnd(nondeterministicChoiceIndices[state + 1] - 1); } + /*! + * Calculates a hash over all values contained in this Model. + * @return size_t A Hash Value + */ + virtual size_t getHash() const override { + std::size_t result = 0; + boost::hash_combine(result, AbstractModel::getHash()); + boost::hash_combine(result, storm::utility::Hash::getHash(nondeterministicChoiceIndices)); + return result; + } + virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const override { AbstractModel::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h index ced1cd235..5ea3cc95f 100644 --- a/src/models/AtomicPropositionsLabeling.h +++ b/src/models/AtomicPropositionsLabeling.h @@ -15,6 +15,8 @@ #include #include +#include "src/utility/Hash.h" + #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" @@ -234,6 +236,29 @@ public: return this->nameToLabelingMap; } + /*! + * Calculates a hash over all values contained in this Sparse Matrix. + * @return size_t A Hash Value + */ + std::size_t getHash() const { + std::size_t result = 0; + + boost::hash_combine(result, stateCount); + boost::hash_combine(result, apCountMax); + boost::hash_combine(result, apsCurrent); + + for (auto it = nameToLabelingMap.begin(); it != nameToLabelingMap.end(); ++it) { + boost::hash_combine(result, it->first); + boost::hash_combine(result, it->second); + } + + for (auto it = singleLabelings.begin(); it != singleLabelings.end(); ++it) { + boost::hash_combine(result, it->getHash()); + } + + return result; + } + private: /*! The number of states whose labels are to be stored by this object. */ diff --git a/src/models/Ctmc.h b/src/models/Ctmc.h index 9c70b7416..9d92a560e 100644 --- a/src/models/Ctmc.h +++ b/src/models/Ctmc.h @@ -72,6 +72,14 @@ public: storm::models::ModelType getType() const { return CTMC; } + + /*! + * Calculates a hash over all values contained in this Model. + * @return size_t A Hash Value + */ + virtual std::size_t getHash() const override { + return AbstractDeterministicModel::getHash(); + } }; } // namespace models diff --git a/src/models/Ctmdp.h b/src/models/Ctmdp.h index 64bb267ac..0dfd154b5 100644 --- a/src/models/Ctmdp.h +++ b/src/models/Ctmdp.h @@ -103,6 +103,14 @@ public: return CTMDP; } + /*! + * Calculates a hash over all values contained in this Model. + * @return size_t A Hash Value + */ + virtual std::size_t getHash() const override { + return AbstractNondeterministicModel::getHash(); + } + private: /*! diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 07dc213d8..6e675c3d2 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -109,6 +109,14 @@ public: return DTMC; } + /*! + * Calculates a hash over all values contained in this Model. + * @return size_t A Hash Value + */ + virtual std::size_t getHash() const override { + return AbstractDeterministicModel::getHash(); + } + private: /*! * @brief Perform some sanity checks. diff --git a/src/models/Mdp.h b/src/models/Mdp.h index 48a651e6d..5241a3d7d 100644 --- a/src/models/Mdp.h +++ b/src/models/Mdp.h @@ -105,6 +105,13 @@ public: return MDP; } + /*! + * Calculates a hash over all values contained in this Model. + * @return size_t A Hash Value + */ + virtual std::size_t getHash() const override { + return AbstractNondeterministicModel::getHash(); + } private: /*! diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index 376555e3e..e3750f9cb 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -11,6 +11,7 @@ #include "src/exceptions/OutOfRangeException.h" #include "src/utility/OsDetection.h" +#include "src/utility/Hash.h" #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" @@ -80,6 +81,7 @@ public: bool operator!=(const constIndexIterator& rhs) const { return currentIndex != rhs.currentIndex; } + private: /*! The bit vector to search for set bits. */ @@ -628,6 +630,23 @@ public: return result.str(); } + /*! + * Calculates a hash over all values contained in this Sparse Matrix. + * @return size_t A Hash Value + */ + std::size_t getHash() const { + std::size_t result = 0; + + boost::hash_combine(result, bucketCount); + boost::hash_combine(result, bitCount); + + for (uint_fast64_t i = 0; i < bucketCount; ++i) { + boost::hash_combine(result, bucketArray[i]); + } + + return result; + } + private: /*! diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 04fa0d4a7..e98ab9270 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -17,6 +17,7 @@ #include "src/storage/JacobiDecomposition.h" #include "src/utility/ConstTemplates.h" +#include "src/utility/Hash.h" #include "Eigen/Sparse" #include "gmm/gmm_matrix.h" @@ -1232,6 +1233,25 @@ public: return result.str(); } + /*! + * Calculates a hash over all values contained in this Sparse Matrix. + * @return size_t A Hash Value + */ + std::size_t getHash() const { + std::size_t result = 0; + + boost::hash_combine(result, rowCount); + boost::hash_combine(result, colCount); + boost::hash_combine(result, nonZeroEntryCount); + boost::hash_combine(result, currentSize); + boost::hash_combine(result, lastRow); + boost::hash_combine(result, storm::utility::Hash::getHash(valueStorage)); + boost::hash_combine(result, storm::utility::Hash::getHash(columnIndications)); + boost::hash_combine(result, storm::utility::Hash::getHash(rowIndications)); + + return result; + } + private: /*! diff --git a/src/utility/Hash.h b/src/utility/Hash.h new file mode 100644 index 000000000..fad0da738 --- /dev/null +++ b/src/utility/Hash.h @@ -0,0 +1,25 @@ +#ifndef STORM_UTILITY_HASH_H_ +#define STORM_UTILITY_HASH_H_ + +#include +#include +#include + +namespace storm { +namespace utility { + + template + class Hash { + public: + static std::size_t getHash(std::vector const& target) { + return boost::hash_range(target.begin(), target.end()); + } + private: + Hash() {} + ~Hash() {} + }; + +} +} + +#endif // STORM_UTILITY_HASH_H_ \ No newline at end of file