diff --git a/src/storm/models/sparse/ItemLabeling.cpp b/src/storm/models/sparse/ItemLabeling.cpp index 5f5ffc548..329c961c8 100644 --- a/src/storm/models/sparse/ItemLabeling.cpp +++ b/src/storm/models/sparse/ItemLabeling.cpp @@ -201,6 +201,10 @@ namespace storm { } } + std::size_t ItemLabeling::hash() const { + return 0; + } + std::ostream& operator<<(std::ostream& out, ItemLabeling const& labeling) { labeling.printLabelingInformationToStream(out); return out; diff --git a/src/storm/models/sparse/ItemLabeling.h b/src/storm/models/sparse/ItemLabeling.h index 7f6c9ce55..43a5b9f21 100644 --- a/src/storm/models/sparse/ItemLabeling.h +++ b/src/storm/models/sparse/ItemLabeling.h @@ -121,6 +121,9 @@ namespace storm { void permuteItems(std::vector const& inversePermutation); + + virtual std::size_t hash() const; + /*! * Prints information about the labeling to the specified stream. * diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index bd62c17f5..00d5d404d 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -298,6 +298,31 @@ namespace storm { this->printModelInformationHeaderToStream(out); this->printModelInformationFooterToStream(out); } + + template + std::size_t Model::hash() const { + + // if set, retrieves for each state the variable valuation that this state represents + boost::optional stateValuations; + + // if set, gives information about where each choice originates w.r.t. the input model description + boost::optional> choiceOrigins; + std::size_t seed = 0; + boost::hash_combine(seed,transitionMatrix.hash()); + boost::hash_combine(seed,stateLabeling.hash()); + for (auto const& rewModel : rewardModels) { + boost::hash_combine(seed,rewModel.second.hash()); + } + if(choiceLabeling) { + boost::hash_combine(seed,choiceLabeling->hash()); + } + if(stateValuations) { + boost::hash_combine(seed,stateValuations->hash()); + } + if(choiceOrigins) { + boost::hash_combine(seed,choiceOrigins.get()->hash()); + } + } template void Model::printModelInformationHeaderToStream(std::ostream& out) const { diff --git a/src/storm/models/sparse/Model.h b/src/storm/models/sparse/Model.h index c86a5924f..7c747f0a9 100644 --- a/src/storm/models/sparse/Model.h +++ b/src/storm/models/sparse/Model.h @@ -358,6 +358,8 @@ namespace storm { virtual bool hasParameters() const override; virtual bool isExact() const override; + + virtual std::size_t hash() const; protected: RewardModelType & rewardModel(std::string const& rewardModelName); diff --git a/src/storm/models/sparse/StandardRewardModel.cpp b/src/storm/models/sparse/StandardRewardModel.cpp index b017ae58a..f73704b89 100644 --- a/src/storm/models/sparse/StandardRewardModel.cpp +++ b/src/storm/models/sparse/StandardRewardModel.cpp @@ -399,6 +399,21 @@ namespace storm { return true; } + template + std::size_t StandardRewardModel::hash() const { + size_t seed = 0; + if(hasStateRewards()) { + boost::hash_combine(seed, boost::hash_range(optionalStateRewardVector->begin(), optionalStateRewardVector->end())); + } + if (hasStateActionRewards()) { + boost::hash_combine(seed, boost::hash_range(optionalStateActionRewardVector->begin(), optionalStateActionRewardVector->end())); + } + if (hasTransitionRewards()) { + boost::hash_combine(seed, optionalTransitionRewardMatrix->hash()); + } + return seed; + } + template std::ostream& operator<<(std::ostream& out, StandardRewardModel const& rewardModel) { out << std::boolalpha << "reward model [state reward: " diff --git a/src/storm/models/sparse/StandardRewardModel.h b/src/storm/models/sparse/StandardRewardModel.h index aedd7c535..e4b0c6636 100644 --- a/src/storm/models/sparse/StandardRewardModel.h +++ b/src/storm/models/sparse/StandardRewardModel.h @@ -313,6 +313,8 @@ namespace storm { * @param nrChoices The number of choices in the model */ bool isCompatible(uint_fast64_t nrStates, uint_fast64_t nrChoices) const; + + std::size_t hash() const; template friend std::ostream& operator<<(std::ostream& out, StandardRewardModel const& rewardModel); diff --git a/src/storm/storage/sparse/ChoiceOrigins.h b/src/storm/storage/sparse/ChoiceOrigins.h index afc85faf3..4c1be9d2b 100644 --- a/src/storm/storage/sparse/ChoiceOrigins.h +++ b/src/storm/storage/sparse/ChoiceOrigins.h @@ -93,6 +93,8 @@ namespace storm { storm::models::sparse::ChoiceLabeling toChoiceLabeling() const; + virtual std::size_t hash() const = 0; + protected: ChoiceOrigins(std::vector const& indexToIdentifierMapping); ChoiceOrigins(std::vector&& indexToIdentifierMapping); diff --git a/src/storm/storage/sparse/JaniChoiceOrigins.cpp b/src/storm/storage/sparse/JaniChoiceOrigins.cpp index 8063142a7..88243145b 100644 --- a/src/storm/storage/sparse/JaniChoiceOrigins.cpp +++ b/src/storm/storage/sparse/JaniChoiceOrigins.cpp @@ -79,6 +79,10 @@ namespace storm { this->identifierToJson.push_back(std::move(setJson)); } } + + std::size_t JaniChoiceOrigins::hash() const { + return 0; + } } } } diff --git a/src/storm/storage/sparse/JaniChoiceOrigins.h b/src/storm/storage/sparse/JaniChoiceOrigins.h index 5ee1aa69b..f5684f189 100644 --- a/src/storm/storage/sparse/JaniChoiceOrigins.h +++ b/src/storm/storage/sparse/JaniChoiceOrigins.h @@ -47,6 +47,8 @@ namespace storm { * The edges set is represented by a set of indices that encode an automaton index and its local edge index. */ EdgeIndexSet const& getEdgeIndexSet(uint_fast64_t choiceIndex) const; + + std::size_t hash() const override; private: /* diff --git a/src/storm/storage/sparse/PrismChoiceOrigins.cpp b/src/storm/storage/sparse/PrismChoiceOrigins.cpp index 5084b58d7..38018ced8 100644 --- a/src/storm/storage/sparse/PrismChoiceOrigins.cpp +++ b/src/storm/storage/sparse/PrismChoiceOrigins.cpp @@ -156,6 +156,10 @@ namespace storm { this->identifierToJson.push_back(std::move(setJson)); } } + + std::size_t PrismChoiceOrigins::hash() const { + return 0; + } } } } diff --git a/src/storm/storage/sparse/PrismChoiceOrigins.h b/src/storm/storage/sparse/PrismChoiceOrigins.h index 05567a644..233d7c4aa 100644 --- a/src/storm/storage/sparse/PrismChoiceOrigins.h +++ b/src/storm/storage/sparse/PrismChoiceOrigins.h @@ -51,6 +51,8 @@ namespace storm { */ CommandSet const& getCommandSet(uint_fast64_t choiceIndex) const; + std::size_t hash() const override; + protected: /* * Returns a copy of this object where the mapping of choice indices to origin identifiers is replaced by the given one. diff --git a/src/storm/storage/sparse/StateValuations.cpp b/src/storm/storage/sparse/StateValuations.cpp index b1d70b81b..0dbe726bf 100644 --- a/src/storm/storage/sparse/StateValuations.cpp +++ b/src/storm/storage/sparse/StateValuations.cpp @@ -182,6 +182,10 @@ namespace storm { uint_fast64_t StateValuations::getNumberOfStates() const { return valuations.size(); } + + std::size_t StateValuations::hash() const { + return 0; + } StateValuations StateValuations::selectStates(storm::storage::BitVector const& selectedStates) const { return StateValuations(variableToIndexMap, storm::utility::vector::filterVector(valuations, selectedStates)); diff --git a/src/storm/storage/sparse/StateValuations.h b/src/storm/storage/sparse/StateValuations.h index 43edda895..8626f89c0 100644 --- a/src/storm/storage/sparse/StateValuations.h +++ b/src/storm/storage/sparse/StateValuations.h @@ -75,7 +75,8 @@ namespace storm { * If an invalid state index is selected, the corresponding valuation will be empty. */ StateValuations selectStates(std::vector const& selectedStates) const; - + + virtual std::size_t hash() const; private: StateValuations(std::map const& variableToIndexMap, std::vector&& valuations);