diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index b67fc9705..23f856c58 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -1240,7 +1240,7 @@ namespace storm { } stateActionRewardDd *= stateActionDd.get(); } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) { - // For CTMCs, we need to multiply the entries with the exit rate of the corresponding action. + // For DTMCs and CTMC, we need to multiply the entries with the multiplicity/exit rate of the corresponding action. stateActionRewardDd *= actionDd.transitionsDd.sumAbstract(generationInfo.columnMetaVariables); } diff --git a/src/storm/storage/dd/BisimulationDecomposition.cpp b/src/storm/storage/dd/BisimulationDecomposition.cpp index e34a7ddf8..57190ff23 100644 --- a/src/storm/storage/dd/BisimulationDecomposition.cpp +++ b/src/storm/storage/dd/BisimulationDecomposition.cpp @@ -29,17 +29,17 @@ namespace storm { template BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, bisimulationType), refiner(createRefiner(model, Partition::create(model, bisimulationType, preservationInformation))) { - // Intentionally left empty. + this->refineWrtRewardModels(); } template BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model, std::vector> const& formulas, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, formulas, bisimulationType), refiner(createRefiner(model, Partition::create(model, bisimulationType, preservationInformation))) { - // Intentionally left empty. + this->refineWrtRewardModels(); } template BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model, Partition const& initialPartition, bisimulation::PreservationInformation const& preservationInformation) : model(model), preservationInformation(preservationInformation), refiner(createRefiner(model, initialPartition)) { - STORM_LOG_THROW(!model.hasRewardModel(), storm::exceptions::NotSupportedException, "Symbolic bisimulation currently does not support preserving rewards."); + this->refineWrtRewardModels(); } template @@ -79,6 +79,14 @@ namespace storm { return quotient; } + template + void BisimulationDecomposition::refineWrtRewardModels() { + for (auto const& rewardModelName : this->preservationInformation.getRewardModelNames()) { + auto const& rewardModel = this->model.getRewardModel(rewardModelName); + refiner->refineWrtRewardModel(rewardModel); + } + } + template class BisimulationDecomposition; template class BisimulationDecomposition; diff --git a/src/storm/storage/dd/BisimulationDecomposition.h b/src/storm/storage/dd/BisimulationDecomposition.h index efc5a0a7f..66e562bea 100644 --- a/src/storm/storage/dd/BisimulationDecomposition.h +++ b/src/storm/storage/dd/BisimulationDecomposition.h @@ -50,6 +50,8 @@ namespace storm { std::shared_ptr> getQuotient() const; private: + void refineWrtRewardModels(); + // The model for which to compute the bisimulation decomposition. storm::models::symbolic::Model const& model; diff --git a/src/storm/storage/dd/Dd.cpp b/src/storm/storage/dd/Dd.cpp index f0619c633..52aaceac2 100644 --- a/src/storm/storage/dd/Dd.cpp +++ b/src/storm/storage/dd/Dd.cpp @@ -78,7 +78,7 @@ namespace storm { template std::set Dd::subtractMetaVariables(storm::dd::Dd const& first, storm::dd::Dd const& second) { bool includesAllMetaVariables = std::includes(first.getContainedMetaVariables().begin(), first.getContainedMetaVariables().end(), second.getContainedMetaVariables().begin(), second.getContainedMetaVariables().end()); - STORM_LOG_THROW(includesAllMetaVariables, storm::exceptions::InvalidArgumentException, "Cannot subtract meta variables that are not contained in the DD."); + STORM_LOG_WARN_COND(includesAllMetaVariables, "Subtracting from meta variables that are not contained in the DD."); std::set metaVariables; std::set_difference(first.getContainedMetaVariables().begin(), first.getContainedMetaVariables().end(), second.getContainedMetaVariables().begin(), second.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); return metaVariables; diff --git a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp index 5ce9fc504..80ef0761a 100644 --- a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp @@ -49,8 +49,14 @@ namespace storm { } template - bool MdpPartitionRefiner::refineWrtStateActionRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& stateActionRewards) { + bool MdpPartitionRefiner::refineWrtStateActionRewards(storm::dd::Add const& stateActionRewards) { Partition newChoicePartition = this->signatureRefiner.refine(this->choicePartition, Signature(stateActionRewards)); + if (newChoicePartition == this->choicePartition) { + return false; + } else { + this->choicePartition = newChoicePartition; + return true; + } } template class MdpPartitionRefiner; diff --git a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h index e5511e939..bafd9d97f 100644 --- a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h +++ b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h @@ -32,7 +32,7 @@ namespace storm { Partition const& getChoicePartition() const; private: - virtual bool refineWrtStateActionRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& stateActionRewards) override; + virtual bool refineWrtStateActionRewards(storm::dd::Add const& stateActionRewards) override; // The choice partition in the refinement process. Partition choicePartition; diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp index 422f4175b..2cf1cce76 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp @@ -73,20 +73,22 @@ namespace storm { } template - bool PartitionRefiner::refineWrtRewardModel(storm::models::symbolic::Model const& model, storm::models::symbolic::StandardRewardModel const& rewardModel) { - STORM_LOG_THROW(rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Symbolic bisimulation currently does not support transition rewards."); + bool PartitionRefiner::refineWrtRewardModel(storm::models::symbolic::StandardRewardModel const& rewardModel) { + STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Symbolic bisimulation currently does not support transition rewards."); + STORM_LOG_TRACE("Refining with respect to reward model."); bool result = false; - if (rewardModel.hasStateActionRewards()) { - result |= refineWrtStateActionRewards(model, rewardModel.getStateActionRewardVector()); - } if (rewardModel.hasStateRewards()) { - result |= refineWrtStateRewards(model, rewardModel.getStateActionRewardVector()); + result |= refineWrtStateRewards(rewardModel.getStateRewardVector()); + } + if (rewardModel.hasStateActionRewards()) { + result |= refineWrtStateRewards(rewardModel.getStateActionRewardVector()); } return result; } template - bool PartitionRefiner::refineWrtStateRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& stateRewards) { + bool PartitionRefiner::refineWrtStateRewards(storm::dd::Add const& stateRewards) { + STORM_LOG_TRACE("Refining with respect to state rewards."); Partition newPartition = signatureRefiner.refine(statePartition, Signature(stateRewards)); if (newPartition == statePartition) { return false; @@ -97,9 +99,10 @@ namespace storm { } template - bool PartitionRefiner::refineWrtStateActionRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& stateActionRewards) { + bool PartitionRefiner::refineWrtStateActionRewards(storm::dd::Add const& stateActionRewards) { + STORM_LOG_TRACE("Refining with respect to state-action rewards."); // By default, we treat state-action rewards just like state-rewards, which works for DTMCs and CTMCs. - return refineWrtStateRewards(model, stateActionRewards); + return refineWrtStateRewards(stateActionRewards); } template diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.h b/src/storm/storage/dd/bisimulation/PartitionRefiner.h index d8236d6e8..5ae860201 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.h +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.h @@ -36,7 +36,7 @@ namespace storm { * Refines the partition wrt. to the reward model. * @return True iff the partition is stable and no refinement was actually performed. */ - bool refineWrtRewardModel(storm::models::symbolic::Model const& model, storm::models::symbolic::StandardRewardModel const& rewardModel); + bool refineWrtRewardModel(storm::models::symbolic::StandardRewardModel const& rewardModel); /*! * Retrieves the current state partition in the refinement process. @@ -51,8 +51,8 @@ namespace storm { protected: Partition internalRefine(SignatureComputer& stateSignatureComputer, SignatureRefiner& signatureRefiner, Partition const& oldPartition, Partition const& targetPartition, SignatureMode const& mode = SignatureMode::Eager); - virtual bool refineWrtStateRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& stateRewards); - virtual bool refineWrtStateActionRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& stateActionRewards); + virtual bool refineWrtStateRewards(storm::dd::Add const& stateRewards); + virtual bool refineWrtStateActionRewards(storm::dd::Add const& stateActionRewards); // The current status. Status status;