sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

dd quotient extraction of reward models in dd bisimulation

tempestpy_adaptions
dehnert 7 years ago
parent
34e23f94fc
commit
722cb3109c
14 changed files with 120 additions and 34 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
  2. 7
      src/storm/models/sparse/Ctmc.cpp
  3. 2
      src/storm/models/sparse/Ctmc.h
  4. 7
      src/storm/models/sparse/DeterministicModel.cpp
  5. 2
      src/storm/models/sparse/DeterministicModel.h
  6. 6
      src/storm/models/sparse/Dtmc.cpp
  7. 1
      src/storm/models/sparse/Dtmc.h
  8. 41
      src/storm/models/sparse/StandardRewardModel.cpp
  9. 10
      src/storm/models/sparse/StandardRewardModel.h
  10. 7
      src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp
  11. 2
      src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h
  12. 33
      src/storm/storage/dd/bisimulation/PartitionRefiner.cpp
  13. 9
      src/storm/storage/dd/bisimulation/PartitionRefiner.h
  14. 23
      src/storm/storage/dd/bisimulation/QuotientExtractor.cpp

4
src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
View File

@ -264,7 +264,7 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> uniformizedMatrix = computeUniformizedMatrix(rateMatrix, storm::storage::BitVector(numberOfStates, true), uniformizationRate, exitRateVector);
// Compute the total state reward vector.
std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, exitRateVector, false);
std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, exitRateVector);
// Finally, compute the transient probabilities.
return computeTransientProbabilities<ValueType, true>(uniformizedMatrix, nullptr, timeBound, uniformizationRate, totalRewardVector, linearEquationSolverFactory);
@ -359,7 +359,7 @@ namespace storm {
// Only compute the result if the model has a state-based reward model.
STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
return computeLongRunAverageRewards(probabilityMatrix, rewardModel.getTotalRewardVector(probabilityMatrix, *exitRateVector, true), exitRateVector, linearEquationSolverFactory);
return computeLongRunAverageRewards(probabilityMatrix, rewardModel.getTotalRewardVector(probabilityMatrix, *exitRateVector), exitRateVector, linearEquationSolverFactory);
}
template <typename ValueType>

7
src/storm/models/sparse/Ctmc.cpp
View File

@ -72,6 +72,13 @@ namespace storm {
return exitRates;
}
template<typename ValueType, typename RewardModelType>
void Ctmc<ValueType, RewardModelType>::reduceToStateBasedRewards() {
for (auto& rewardModel : this->getRewardModels()) {
rewardModel.second.reduceToStateBasedRewards(this->getTransitionMatrix(), true, &exitRates);
}
}
template class Ctmc<double>;
#ifdef STORM_HAVE_CARL

2
src/storm/models/sparse/Ctmc.h
View File

@ -62,6 +62,8 @@ namespace storm {
*/
std::vector<ValueType>& getExitRateVector();
virtual void reduceToStateBasedRewards() override;
private:
/*!
* Computes the exit rate vector based on the given rate matrix.

7
src/storm/models/sparse/DeterministicModel.cpp
View File

@ -59,13 +59,6 @@ namespace storm {
}
}
template<typename ValueType, typename RewardModelType>
void DeterministicModel<ValueType, RewardModelType>::reduceToStateBasedRewards() {
for (auto& rewardModel : this->getRewardModels()) {
rewardModel.second.reduceToStateBasedRewards(this->getTransitionMatrix(), true);
}
}
template class DeterministicModel<double>;
#ifdef STORM_HAVE_CARL
template class DeterministicModel<storm::RationalNumber>;

2
src/storm/models/sparse/DeterministicModel.h
View File

@ -29,8 +29,6 @@ namespace storm {
DeterministicModel(DeterministicModel<ValueType, RewardModelType>&& other) = default;
DeterministicModel<ValueType, RewardModelType>& operator=(DeterministicModel<ValueType, RewardModelType>&& model) = default;
virtual void reduceToStateBasedRewards() override;
virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector<ValueType> const* firstValue = nullptr, std::vector<ValueType> const* secondValue = nullptr, std::vector<uint_fast64_t> const* stateColoring = nullptr, std::vector<std::string> const* colors = nullptr, std::vector<uint_fast64_t>* scheduler = nullptr, bool finalizeOutput = true) const override;
};

6
src/storm/models/sparse/Dtmc.cpp
View File

@ -35,6 +35,12 @@ namespace storm {
// Intentionally left empty
}
template<typename ValueType, typename RewardModelType>
void Dtmc<ValueType, RewardModelType>::reduceToStateBasedRewards() {
for (auto& rewardModel : this->getRewardModels()) {
rewardModel.second.reduceToStateBasedRewards(this->getTransitionMatrix(), true);
}
}
template class Dtmc<double>;

1
src/storm/models/sparse/Dtmc.h
View File

@ -50,6 +50,7 @@ namespace storm {
Dtmc(Dtmc<ValueType, RewardModelType>&& dtmc) = default;
Dtmc& operator=(Dtmc<ValueType, RewardModelType>&& dtmc) = default;
virtual void reduceToStateBasedRewards() override;
};

41
src/storm/models/sparse/StandardRewardModel.cpp
View File

@ -165,7 +165,7 @@ namespace storm {
template<typename ValueType>
template<typename MatrixValueType>
void StandardRewardModel<ValueType>::reduceToStateBasedRewards(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, bool reduceToStateRewards) {
void StandardRewardModel<ValueType>::reduceToStateBasedRewards(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, bool reduceToStateRewards, std::vector<MatrixValueType> const* weights) {
if (this->hasTransitionRewards()) {
if (this->hasStateActionRewards()) {
storm::utility::vector::addVectors<ValueType>(this->getStateActionRewardVector(), transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()), this->getStateActionRewardVector());
@ -177,10 +177,21 @@ namespace storm {
if (reduceToStateRewards && this->hasStateActionRewards()) {
STORM_LOG_THROW(transitionMatrix.getRowGroupCount() == this->getStateActionRewardVector().size(), storm::exceptions::InvalidOperationException, "The reduction to state rewards is only possible if the size of the action reward vector equals the number of states.");
if (this->hasStateRewards()) {
storm::utility::vector::addVectors<ValueType>(this->getStateActionRewardVector(), this->getStateRewardVector(), this->getStateRewardVector());
if (weights) {
if (this->hasStateRewards()) {
storm::utility::vector::applyPointwise<ValueType, MatrixValueType, ValueType>(this->getStateActionRewardVector(), *weights, this->getStateRewardVector(),
[] (ValueType const& sar, MatrixValueType const& w, ValueType const& sr) -> ValueType {
return sr + w * sar; });
} else {
this->optionalStateRewardVector = std::move(this->optionalStateActionRewardVector);
storm::utility::vector::applyPointwise<ValueType, MatrixValueType, ValueType>(this->optionalStateRewardVector.get(), *weights, this->optionalStateRewardVector.get(), [] (ValueType const& r, MatrixValueType const& w) { return w * r; } );
}
} else {
this->optionalStateRewardVector = std::move(this->optionalStateActionRewardVector);
if (this->hasStateRewards()) {
storm::utility::vector::addVectors<ValueType>(this->getStateActionRewardVector(), this->getStateRewardVector(), this->getStateRewardVector());
} else {
this->optionalStateRewardVector = std::move(this->optionalStateActionRewardVector);
}
}
this->optionalStateActionRewardVector = boost::none;
}
@ -201,7 +212,7 @@ namespace storm {
template<typename ValueType>
template<typename MatrixValueType>
std::vector<ValueType> StandardRewardModel<ValueType>::getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::vector<MatrixValueType> const& weights, bool scaleTransAndActions) const {
std::vector<ValueType> StandardRewardModel<ValueType>::getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::vector<MatrixValueType> const& weights) const {
std::vector<ValueType> result;
if (this->hasTransitionRewards()) {
result = transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix());
@ -382,13 +393,13 @@ namespace storm {
// Explicitly instantiate the class.
template std::vector<double> StandardRewardModel<double>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix) const;
template std::vector<double> StandardRewardModel<double>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::BitVector const& filter) const;
template std::vector<double> StandardRewardModel<double>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<double> const& weights, bool scaleTransAndActions) const;
template std::vector<double> StandardRewardModel<double>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<double> const& weights) const;
template std::vector<double> StandardRewardModel<double>::getTotalActionRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<double> const& stateRewardWeights) const;
template storm::storage::BitVector StandardRewardModel<double>::getStatesWithZeroReward(storm::storage::SparseMatrix<double> const& transitionMatrix) const;
template storm::storage::BitVector StandardRewardModel<double>::getChoicesWithZeroReward(storm::storage::SparseMatrix<double> const& transitionMatrix) const;
template double StandardRewardModel<double>::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix<double> const& transitionMatrix, double const& stateRewardWeight, double const& actionRewardWeight) const;
template void StandardRewardModel<double>::reduceToStateBasedRewards(storm::storage::SparseMatrix<double> const& transitionMatrix, bool reduceToStateRewards);
template void StandardRewardModel<double>::reduceToStateBasedRewards(storm::storage::SparseMatrix<double> const& transitionMatrix, bool reduceToStateRewards, std::vector<double> const* weights);
template void StandardRewardModel<double>::setStateActionReward(uint_fast64_t choiceIndex, double const & newValue);
template void StandardRewardModel<double>::setStateReward(uint_fast64_t state, double const & newValue);
template class StandardRewardModel<double>;
@ -396,9 +407,9 @@ namespace storm {
template std::vector<float> StandardRewardModel<float>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<float> const& transitionMatrix, storm::storage::BitVector const& filter) const;
template std::vector<float> StandardRewardModel<float>::getTotalRewardVector(storm::storage::SparseMatrix<float> const& transitionMatrix) const;
template std::vector<float> StandardRewardModel<float>::getTotalRewardVector(storm::storage::SparseMatrix<float> const& transitionMatrix, std::vector<float> const& weights, bool scaleTransAndActions) const;
template std::vector<float> StandardRewardModel<float>::getTotalRewardVector(storm::storage::SparseMatrix<float> const& transitionMatrix, std::vector<float> const& weights) const;
template std::vector<float> StandardRewardModel<float>::getTotalActionRewardVector(storm::storage::SparseMatrix<float> const& transitionMatrix, std::vector<float> const& stateRewardWeights) const;
template void StandardRewardModel<float>::reduceToStateBasedRewards(storm::storage::SparseMatrix<float> const& transitionMatrix, bool reduceToStateRewards);
template void StandardRewardModel<float>::reduceToStateBasedRewards(storm::storage::SparseMatrix<float> const& transitionMatrix, bool reduceToStateRewards, std::vector<float> const* weights);
template void StandardRewardModel<float>::setStateActionReward(uint_fast64_t choiceIndex, float const & newValue);
template void StandardRewardModel<float>::setStateReward(uint_fast64_t state, float const & newValue);
template class StandardRewardModel<float>;
@ -407,12 +418,12 @@ namespace storm {
#ifdef STORM_HAVE_CARL
template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::BitVector const& filter) const;
template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix) const;
template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<storm::RationalNumber> const& weights, bool scaleTransAndActions) const;
template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<storm::RationalNumber> const& weights) const;
template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalActionRewardVector(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<storm::RationalNumber> const& stateRewardWeights) const;
template storm::storage::BitVector StandardRewardModel<storm::RationalNumber>::getStatesWithZeroReward(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix) const;
template storm::storage::BitVector StandardRewardModel<storm::RationalNumber>::getChoicesWithZeroReward(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix) const;
template storm::RationalNumber StandardRewardModel<storm::RationalNumber>::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::RationalNumber const& stateRewardWeight, storm::RationalNumber const& actionRewardWeight) const;
template void StandardRewardModel<storm::RationalNumber>::reduceToStateBasedRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, bool reduceToStateRewards);
template void StandardRewardModel<storm::RationalNumber>::reduceToStateBasedRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, bool reduceToStateRewards, std::vector<storm::RationalNumber> const* weights);
template void StandardRewardModel<storm::RationalNumber>::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalNumber const & newValue);
template void StandardRewardModel<storm::RationalNumber>::setStateReward(uint_fast64_t state, storm::RationalNumber const & newValue);
template class StandardRewardModel<storm::RationalNumber>;
@ -420,13 +431,13 @@ namespace storm {
template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::BitVector const& filter) const;
template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix) const;
template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<storm::RationalFunction> const& weights, bool scaleTransAndActions) const;
template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<storm::RationalFunction> const& weights) const;
template storm::storage::BitVector StandardRewardModel<storm::RationalFunction>::getStatesWithZeroReward(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix) const;
template storm::storage::BitVector StandardRewardModel<storm::RationalFunction>::getChoicesWithZeroReward(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix) const;
template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalActionRewardVector(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<storm::RationalFunction> const& stateRewardWeights) const;
template storm::RationalFunction StandardRewardModel<storm::RationalFunction>::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::RationalFunction const& stateRewardWeight, storm::RationalFunction const& actionRewardWeight) const;
template void StandardRewardModel<storm::RationalFunction>::reduceToStateBasedRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, bool reduceToStateRewards);
template void StandardRewardModel<storm::RationalFunction>::reduceToStateBasedRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, bool reduceToStateRewards, std::vector<storm::RationalFunction> const* weights);
template void StandardRewardModel<storm::RationalFunction>::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalFunction const & newValue);
template void StandardRewardModel<storm::RationalFunction>::setStateReward(uint_fast64_t state, storm::RationalFunction const & newValue);
template class StandardRewardModel<storm::RationalFunction>;
@ -434,13 +445,13 @@ namespace storm {
template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::BitVector const& filter) const;
template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix) const;
template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<double> const& weights, bool scaleTransAndActions) const;
template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<double> const& weights) const;
template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalActionRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<double> const& stateRewardWeights) const;
template void StandardRewardModel<storm::Interval>::setStateActionReward(uint_fast64_t choiceIndex, double const & newValue);
template void StandardRewardModel<storm::Interval>::setStateActionReward(uint_fast64_t choiceIndex, storm::Interval const & newValue);
template void StandardRewardModel<storm::Interval>::setStateReward(uint_fast64_t state, double const & newValue);
template void StandardRewardModel<storm::Interval>::setStateReward(uint_fast64_t state, storm::Interval const & newValue);
template void StandardRewardModel<storm::Interval>::reduceToStateBasedRewards(storm::storage::SparseMatrix<double> const& transitionMatrix, bool reduceToStateRewards);
template void StandardRewardModel<storm::Interval>::reduceToStateBasedRewards(storm::storage::SparseMatrix<double> const& transitionMatrix, bool reduceToStateRewards, std::vector<double> const* weights);
template class StandardRewardModel<storm::Interval>;
template std::ostream& operator<<<storm::Interval>(std::ostream& out, StandardRewardModel<storm::Interval> const& rewardModel);
#endif

10
src/storm/models/sparse/StandardRewardModel.h
View File

@ -191,9 +191,13 @@ namespace storm {
* but not all reward-based properties.
*
* @param transitionMatrix The transition matrix that is used to weight the rewards in the reward matrix.
* @param reduceToStateRewards If set, the state-action rewards and the state rewards are summed so the
* model only has a state reward vector left.
* @param weights If given and if the reduction to state rewards only is enabled, this vector is used to
* weight the state-action and transition rewards
*/
template<typename MatrixValueType>
void reduceToStateBasedRewards(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, bool reduceToStateRewards = false);
void reduceToStateBasedRewards(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, bool reduceToStateRewards = false, std::vector<MatrixValueType> const* weights = nullptr);
/*!
* Creates a vector representing the complete reward vector based on the state-, state-action- and
@ -211,12 +215,10 @@ namespace storm {
*
* @param transitionMatrix The matrix that is used to weight the values of the transition reward matrix.
* @param weights A vector used for scaling the entries of transition and/or state-action rewards (if present).
* @param scaleTransAndActions If true both transition rewards and state-action rewards are scaled by the
* weights. Otherwise, only the state-action rewards are scaled.
* @return The full state-action reward vector.
*/
template<typename MatrixValueType>
std::vector<ValueType> getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::vector<MatrixValueType> const& weights, bool scaleTransAndActions) const;
std::vector<ValueType> getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::vector<MatrixValueType> const& weights) const;
/*!
* Creates a vector representing the complete reward vector based on the state-, state-action- and

7
src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp
View File

@ -21,7 +21,7 @@ namespace storm {
// For this, we use the signature computer/refiner of this class.
STORM_LOG_TRACE("Refining choice partition.");
Partition<DdType, ValueType> newChoicePartition = this->internalRefine(this->signatureComputer, this->signatureRefiner, choicePartition, this->statePartition, mode);
Partition<DdType, ValueType> newChoicePartition = this->internalRefine(this->signatureComputer, this->signatureRefiner, this->choicePartition, this->statePartition, mode);
if (newChoicePartition == choicePartition) {
this->status = Status::FixedPoint;
@ -48,6 +48,11 @@ namespace storm {
return choicePartition;
}
template<storm::dd::DdType DdType, typename ValueType>
bool MdpPartitionRefiner<DdType, ValueType>::refineWrtStateActionRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& stateActionRewards) {
Partition<DdType, ValueType> newChoicePartition = this->signatureRefiner.refine(this->choicePartition, Signature<DdType, ValueType>(stateActionRewards));
}
template class MdpPartitionRefiner<storm::dd::DdType::CUDD, double>;
template class MdpPartitionRefiner<storm::dd::DdType::Sylvan, double>;

2
src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h
View File

@ -32,6 +32,8 @@ namespace storm {
Partition<DdType, ValueType> const& getChoicePartition() const;
private:
virtual bool refineWrtStateActionRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& stateActionRewards) override;
// The choice partition in the refinement process.
Partition<DdType, ValueType> choicePartition;

33
src/storm/storage/dd/bisimulation/PartitionRefiner.cpp
View File

@ -2,6 +2,9 @@
#include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/NotSupportedException.h"
namespace storm {
namespace dd {
namespace bisimulation {
@ -69,6 +72,36 @@ namespace storm {
}
}
template <storm::dd::DdType DdType, typename ValueType>
bool PartitionRefiner<DdType, ValueType>::refineWrtRewardModel(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::models::symbolic::StandardRewardModel<DdType, ValueType> const& rewardModel) {
STORM_LOG_THROW(rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Symbolic bisimulation currently does not support transition rewards.");
bool result = false;
if (rewardModel.hasStateActionRewards()) {
result |= refineWrtStateActionRewards(model, rewardModel.getStateActionRewardVector());
}
if (rewardModel.hasStateRewards()) {
result |= refineWrtStateRewards(model, rewardModel.getStateActionRewardVector());
}
return result;
}
template <storm::dd::DdType DdType, typename ValueType>
bool PartitionRefiner<DdType, ValueType>::refineWrtStateRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& stateRewards) {
Partition<DdType, ValueType> newPartition = signatureRefiner.refine(statePartition, Signature<DdType, ValueType>(stateRewards));
if (newPartition == statePartition) {
return false;
} else {
this->statePartition = newPartition;
return true;
}
}
template <storm::dd::DdType DdType, typename ValueType>
bool PartitionRefiner<DdType, ValueType>::refineWrtStateActionRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& stateActionRewards) {
// By default, we treat state-action rewards just like state-rewards, which works for DTMCs and CTMCs.
return refineWrtStateRewards(model, stateActionRewards);
}
template <storm::dd::DdType DdType, typename ValueType>
Partition<DdType, ValueType> const& PartitionRefiner<DdType, ValueType>::getStatePartition() const {
return statePartition;

9
src/storm/storage/dd/bisimulation/PartitionRefiner.h
View File

@ -32,6 +32,12 @@ namespace storm {
*/
virtual bool refine(SignatureMode const& mode = SignatureMode::Eager);
/*!
* 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<DdType, ValueType> const& model, storm::models::symbolic::StandardRewardModel<DdType, ValueType> const& rewardModel);
/*!
* Retrieves the current state partition in the refinement process.
*/
@ -45,6 +51,9 @@ namespace storm {
protected:
Partition<DdType, ValueType> internalRefine(SignatureComputer<DdType, ValueType>& stateSignatureComputer, SignatureRefiner<DdType, ValueType>& signatureRefiner, Partition<DdType, ValueType> const& oldPartition, Partition<DdType, ValueType> const& targetPartition, SignatureMode const& mode = SignatureMode::Eager);
virtual bool refineWrtStateRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& stateRewards);
virtual bool refineWrtStateActionRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& stateActionRewards);
// The current status.
Status status;

23
src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
View File

@ -838,12 +838,29 @@ namespace storm {
storm::dd::Bdd<DdType> quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero();
storm::dd::Bdd<DdType> deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(blockPrimeVariableSet) && reachableStates;
std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<DdType, ValueType>> quotientRewardModels;
for (auto const& rewardModelName : preservationInformation.getRewardModelNames()) {
auto const& rewardModel = model.getRewardModel(rewardModelName);
boost::optional<storm::dd::Add<DdType, ValueType>> quotientStateRewards;
if (rewardModel.hasStateRewards()) {
quotientStateRewards = rewardModel.getStateRewardVector().multiplyMatrix(partitionAsAdd, model.getRowVariables());
}
boost::optional<storm::dd::Add<DdType, ValueType>> quotientStateActionRewards;
if (rewardModel.hasStateActionRewards()) {
quotientStateActionRewards = rewardModel.getStateActionRewardVector().multiplyMatrix(partitionAsAdd, model.getRowVariables());
}
quotientRewardModels.emplace(rewardModelName, storm::models::symbolic::StandardRewardModel<DdType, ValueType>(quotientStateRewards, quotientStateActionRewards, boost::none));
}
if (modelType == storm::models::ModelType::Dtmc) {
return std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>>(new storm::models::symbolic::Dtmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, {}));
return std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>>(new storm::models::symbolic::Dtmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, quotientRewardModels));
} else if (modelType == storm::models::ModelType::Ctmc) {
return std::shared_ptr<storm::models::symbolic::Ctmc<DdType, ValueType>>(new storm::models::symbolic::Ctmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, {}));
return std::shared_ptr<storm::models::symbolic::Ctmc<DdType, ValueType>>(new storm::models::symbolic::Ctmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, quotientRewardModels));
} else if (modelType == storm::models::ModelType::Mdp) {
return std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>>(new storm::models::symbolic::Mdp<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getNondeterminismVariables(), preservedLabelBdds, {}));
return std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>>(new storm::models::symbolic::Mdp<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unsupported quotient type.");
}

Write Preview
Loading…
Cancel
Save