diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index b115e2551..76efcdb07 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -11,7 +11,11 @@ #include "src/storage/SparseMatrix.h" #include "src/storage/Scheduler.h" #include "src/storage/StronglyConnectedComponentDecomposition.h" +#include "src/utility/macros.h" #include "src/utility/Hash.h" +#include "src/utility/vector.h" + +#include "src/exceptions/InvalidOperationException.h" namespace storm { namespace models { @@ -329,6 +333,15 @@ class AbstractModel: public std::enable_shared_from_this> { return static_cast(choiceLabeling); } + void convertTransitionRewardsToStateRewards() { + STORM_LOG_THROW(this->hasTransitionRewards(), storm::exceptions::InvalidOperationException, "Cannot reduce non-existant transition rewards to state rewards."); + if (this->hasStateRewards()) { + storm::utility::vector::addVectorsInPlace(stateRewardVector.get(), transitionMatrix.getPointwiseProductRowSumVector(transitionRewardMatrix.get())); + } else { + this->stateRewardVector = transitionMatrix.getPointwiseProductRowSumVector(transitionRewardMatrix.get()); + } + } + /*! * Retrieves the size of the internal representation of the model in memory. * @return the size of the internal representation of the model in memory diff --git a/src/utility/cli.h b/src/utility/cli.h index de987e365..07fb2fbd5 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -288,6 +288,10 @@ namespace storm { STORM_LOG_THROW(model->getType() == storm::models::DTMC, storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs."); std::shared_ptr> dtmc = model->template as>(); + if (dtmc->hasTransitionRewards()) { + dtmc->convertTransitionRewardsToStateRewards(); + } + std::cout << "Performing bisimulation minimization... "; storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, boost::optional>(), true, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true); model = bisimulationDecomposition.getQuotient();