diff --git a/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp index 129c426c7..d047acfde 100644 --- a/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp @@ -73,6 +73,18 @@ namespace storm { return choicePartition; } + template + bool NondeterministicModelPartitionRefiner::refineWrtStateRewards(storm::dd::Add const& stateRewards) { + STORM_LOG_TRACE("Refining with respect to state rewards."); + Partition newStatePartition = this->stateSignatureRefiner.refine(this->statePartition, Signature(stateRewards)); + if (newStatePartition == this->statePartition) { + return false; + } else { + this->statePartition = newStatePartition; + return true; + } + } + template bool NondeterministicModelPartitionRefiner::refineWrtStateActionRewards(storm::dd::Add const& stateActionRewards) { STORM_LOG_TRACE("Refining with respect to state-action rewards."); diff --git a/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.h b/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.h index bf2717998..0dae7f90e 100644 --- a/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.h +++ b/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.h @@ -34,6 +34,8 @@ namespace storm { private: virtual bool refineWrtStateActionRewards(storm::dd::Add const& stateActionRewards) override; + virtual bool refineWrtStateRewards(storm::dd::Add const& stateRewards) override; + // The model to refine. storm::models::symbolic::NondeterministicModel const& model;