dehnert
10 years ago
33 changed files with 898 additions and 622 deletions
-
25src/logic/RewardOperatorFormula.cpp
-
36src/logic/RewardOperatorFormula.h
-
22src/modelchecker/AbstractModelChecker.cpp
-
8src/modelchecker/AbstractModelChecker.h
-
151src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
-
30src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
-
103src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
-
30src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
-
42src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
-
16src/modelchecker/propositional/SparsePropositionalModelChecker.h
-
2src/models/ModelBase.h
-
26src/models/sparse/Ctmc.cpp
-
16src/models/sparse/Ctmc.h
-
22src/models/sparse/DeterministicModel.cpp
-
16src/models/sparse/DeterministicModel.h
-
49src/models/sparse/Dtmc.cpp
-
16src/models/sparse/Dtmc.h
-
68src/models/sparse/MarkovAutomaton.cpp
-
14src/models/sparse/MarkovAutomaton.h
-
45src/models/sparse/Mdp.cpp
-
16src/models/sparse/Mdp.h
-
204src/models/sparse/Model.cpp
-
117src/models/sparse/Model.h
-
47src/models/sparse/NondeterministicModel.cpp
-
16src/models/sparse/NondeterministicModel.h
-
122src/models/sparse/StandardRewardModel.cpp
-
159src/models/sparse/StandardRewardModel.h
-
9src/parser/FormulaParser.cpp
-
3src/parser/FormulaParser.h
-
48src/storage/StronglyConnectedComponentDecomposition.cpp
-
12src/storage/StronglyConnectedComponentDecomposition.h
-
12src/storage/prism/Update.cpp
-
18src/utility/vector.h
@ -0,0 +1,122 @@ |
|||
#include "src/models/sparse/StandardRewardModel.h"
|
|||
|
|||
#include "src/utility/vector.h"
|
|||
|
|||
#include "src/exceptions/InvalidOperationException.h"
|
|||
|
|||
namespace storm { |
|||
namespace models { |
|||
namespace sparse { |
|||
template<typename ValueType> |
|||
StandardRewardModel<ValueType>::StandardRewardModel(boost::optional<std::vector<ValueType>> const& optionalStateRewardVector, |
|||
boost::optional<std::vector<ValueType>> const& optionalStateActionRewardVector, |
|||
boost::optional<storm::storage::SparseMatrix<ValueType>> const& optionalTransitionRewardMatrix) |
|||
: optionalStateRewardVector(optionalStateRewardVector), optionalStateActionRewardVector(optionalStateActionRewardVector), optionalTransitionRewardMatrix(optionalTransitionRewardMatrix) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<typename ValueType> |
|||
StandardRewardModel<ValueType>::StandardRewardModel(boost::optional<std::vector<ValueType>>&& optionalStateRewardVector, |
|||
boost::optional<std::vector<ValueType>>&& optionalStateActionRewardVector, |
|||
boost::optional<storm::storage::SparseMatrix<ValueType>>&& optionalTransitionRewardMatrix) |
|||
: optionalStateRewardVector(std::move(optionalStateRewardVector)), optionalStateActionRewardVector(std::move(optionalStateActionRewardVector)), optionalTransitionRewardMatrix(std::move(optionalTransitionRewardMatrix)) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool StandardRewardModel<ValueType>::hasStateRewards() const { |
|||
return static_cast<bool>(this->optionalStateRewardVector); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::vector<ValueType> const& StandardRewardModel<ValueType>::getStateRewardVector() const { |
|||
return this->optionalStateRewardVector.get(); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
boost::optional<std::vector<ValueType>> const& StandardRewardModel<ValueType>::getOptionalStateRewardVector() const { |
|||
return this->optionalStateRewardVector; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool StandardRewardModel<ValueType>::hasStateActionRewards() const { |
|||
return static_cast<bool>(this->optionalStateActionRewardVector); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::vector<ValueType> const& StandardRewardModel<ValueType>::getStateActionRewardVector() const { |
|||
return this->optionalStateActionRewardVector.get(); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
boost::optional<std::vector<ValueType>> const& StandardRewardModel<ValueType>::getOptionalStateActionRewardVector() const { |
|||
return this->optionalStateActionRewardVector; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool StandardRewardModel<ValueType>::hasTransitionRewards() const { |
|||
return static_cast<bool>(this->optionalTransitionRewardMatrix); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
storm::storage::SparseMatrix<ValueType> const& StandardRewardModel<ValueType>::getTransitionRewardMatrix() const { |
|||
return this->optionalTransitionRewardMatrix.get(); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
boost::optional<storm::storage::SparseMatrix<ValueType>> const& StandardRewardModel<ValueType>::getOptionalTransitionRewardMatrix() const { |
|||
return this->optionalTransitionRewardMatrix; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
StandardRewardModel<ValueType> StandardRewardModel<ValueType>::restrictActions(storm::storage::BitVector const& enabledActions) const { |
|||
boost::optional<std::vector<ValueType>> newStateRewardVector(this->getOptionalStateRewardVector()); |
|||
boost::optional<std::vector<ValueType>> newStateActionRewardVector; |
|||
if (this->hasStateActionRewards()) { |
|||
newStateActionRewardVector = std::vector<ValueType>(enabledActions.getNumberOfSetBits()); |
|||
storm::utility::vector::selectVectorValues(newStateActionRewardVector.get(), enabledActions, this->getStateActionRewardVector()); |
|||
} |
|||
boost::optional<storm::storage::SparseMatrix<ValueType>> newTransitionRewardMatrix; |
|||
if (this->hasTransitionRewards()) { |
|||
newTransitionRewardMatrix = this->getTransitionRewardMatrix().restrictRows(enabledActions); |
|||
} |
|||
return StandardRewardModel(std::move(newStateRewardVector), std::move(newStateActionRewardVector), std::move(newTransitionRewardMatrix)); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
template<typename MatrixValueType> |
|||
void StandardRewardModel<ValueType>::convertTransitionRewardsToStateActionRewards(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix) { |
|||
STORM_LOG_THROW(this->hasTransitionRewards(), storm::exceptions::InvalidOperationException, "Cannot reduce non-existant transition rewards to state rewards."); |
|||
if (this->hasStateActionRewards()) { |
|||
storm::utility::vector::addVectors(this->getStateActionRewardVector(), transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()), this->getStateActionRewardVector); |
|||
} else { |
|||
this->optionalStateActionRewardVector = transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()); |
|||
} |
|||
this->optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<ValueType>>(); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool StandardRewardModel<ValueType>::empty() const { |
|||
return !(static_cast<bool>(this->optionalStateRewardVector) || static_cast<bool>(this->optionalStateActionRewardVector) || static_cast<bool>(this->optionalTransitionRewardMatrix)); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::size_t StandardRewardModel<ValueType>::getSizeInBytes() const { |
|||
std::size_t result = 0; |
|||
if (this->hasStateRewards()) { |
|||
result += this->getStateRewardVector().size() * sizeof(ValueType); |
|||
} |
|||
if (this->hasStateActionRewards()) { |
|||
result += this->getStateActionRewardVector().size() * sizeof(ValueType); |
|||
} |
|||
if (this->hasTransitionRewards()) { |
|||
result += this->getTransitionRewardMatrix().getSizeInBytes(); |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
// Explicitly instantiate the class.
|
|||
template class StandardRewardModel<double>; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,159 @@ |
|||
#ifndef STORM_MODELS_SPARSE_STANDARDREWARDMODEL_H_ |
|||
#define STORM_MODELS_SPARSE_STANDARDREWARDMODEL_H_ |
|||
|
|||
#include <vector> |
|||
#include <boost/optional.hpp> |
|||
|
|||
#include "src/storage/SparseMatrix.h" |
|||
#include "src/utility/OsDetection.h" |
|||
|
|||
namespace storm { |
|||
namespace models { |
|||
namespace sparse { |
|||
template <typename ValueType> |
|||
class StandardRewardModel { |
|||
public: |
|||
/*! |
|||
* Constructs a reward model by copying the given data. |
|||
* |
|||
* @param optionalStateRewardVector The reward values associated with the states. |
|||
* @param optionalStateActionRewardVector The reward values associated with state-action pairs. |
|||
* @param optionalTransitionRewardMatrix The reward values associated with the transitions of the model. |
|||
*/ |
|||
StandardRewardModel(boost::optional<std::vector<ValueType>> const& optionalStateRewardVector = boost::optional<std::vector<ValueType>>(), |
|||
boost::optional<std::vector<ValueType>> const& optionalStateActionRewardVector = boost::optional<std::vector<ValueType>>(), |
|||
boost::optional<storm::storage::SparseMatrix<ValueType>> const& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<ValueType>>()); |
|||
|
|||
/*! |
|||
* Constructs a reward model by moving the given data. |
|||
* |
|||
* @param optionalStateRewardVector The reward values associated with the states. |
|||
* @param optionalStateActionRewardVector The reward values associated with state-action pairs. |
|||
* @param optionalTransitionRewardMatrix The reward values associated with the transitions of the model. |
|||
*/ |
|||
StandardRewardModel(boost::optional<std::vector<ValueType>>&& optionalStateRewardVector = boost::optional<std::vector<ValueType>>(), |
|||
boost::optional<std::vector<ValueType>>&& optionalStateActionRewardVector = boost::optional<std::vector<ValueType>>(), |
|||
boost::optional<storm::storage::SparseMatrix<ValueType>>&& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<ValueType>>()); |
|||
|
|||
StandardRewardModel(StandardRewardModel<ValueType> const& dtmc) = default; |
|||
StandardRewardModel& operator=(StandardRewardModel<ValueType> const& dtmc) = default; |
|||
|
|||
#ifndef WINDOWS |
|||
StandardRewardModel(StandardRewardModel<ValueType>&& dtmc) = default; |
|||
StandardRewardModel& operator=(StandardRewardModel<ValueType>&& dtmc) = default; |
|||
#endif |
|||
|
|||
/*! |
|||
* Retrieves whether the reward model has state rewards. |
|||
* |
|||
* @return True iff the reward model has state rewards. |
|||
*/ |
|||
bool hasStateRewards() const; |
|||
|
|||
/*! |
|||
* Retrieves the state rewards of the reward model. Note that it is illegal to call this function if the |
|||
* reward model does not have state rewards. |
|||
* |
|||
* @return The state reward vector. |
|||
*/ |
|||
std::vector<ValueType> const& getStateRewardVector() const; |
|||
|
|||
/*! |
|||
* Retrieves an optional value that contains the state reward vector if there is one. |
|||
* |
|||
* @return The state reward vector if there is one. |
|||
*/ |
|||
boost::optional<std::vector<ValueType>> const& getOptionalStateRewardVector() const; |
|||
|
|||
/*! |
|||
* Retrieves whether the reward model has state-action rewards. |
|||
* |
|||
* @return True iff the reward model has state-action rewards. |
|||
*/ |
|||
bool hasStateActionRewards() const; |
|||
|
|||
/*! |
|||
* Retrieves the state-action rewards of the reward model. Note that it is illegal to call this function |
|||
* if the reward model does not have state-action rewards. |
|||
* |
|||
* @return The state-action reward vector. |
|||
*/ |
|||
std::vector<ValueType> const& getStateActionRewardVector() const; |
|||
|
|||
/*! |
|||
* Retrieves an optional value that contains the state-action reward vector if there is one. |
|||
* |
|||
* @return The state-action reward vector if there is one. |
|||
*/ |
|||
boost::optional<std::vector<ValueType>> const& getOptionalStateActionRewardVector() const; |
|||
|
|||
/*! |
|||
* Retrieves whether the reward model has transition rewards. |
|||
* |
|||
* @return True iff the reward model has transition rewards. |
|||
*/ |
|||
bool hasTransitionRewards() const; |
|||
|
|||
/*! |
|||
* Retrieves the transition rewards of the reward model. Note that it is illegal to call this function |
|||
* if the reward model does not have transition rewards. |
|||
* |
|||
* @return The transition reward matrix. |
|||
*/ |
|||
storm::storage::SparseMatrix<ValueType> const& getTransitionRewardMatrix() const; |
|||
|
|||
/*! |
|||
* Retrieves an optional value that contains the transition reward matrix if there is one. |
|||
* |
|||
* @return The transition reward matrix if there is one. |
|||
*/ |
|||
boost::optional<storm::storage::SparseMatrix<ValueType>> const& getOptionalTransitionRewardMatrix() const; |
|||
|
|||
/*! |
|||
* Creates a new reward model by restricting the actions of the action-based rewards. |
|||
* |
|||
* @param enabledActions A bit vector representing the enabled actions. |
|||
* @return The restricted reward model. |
|||
*/ |
|||
StandardRewardModel<ValueType> restrictActions(storm::storage::BitVector const& enabledActions) const; |
|||
|
|||
/*! |
|||
* Converts the transition-based rewards to state-action rewards by taking the average of each row. Note |
|||
* that this preserves expected rewards, but not all reward-based properties. Also note that it is only |
|||
* legal to do this transformation if the reward model has transition rewards. |
|||
* |
|||
* @param transitionMatrix The transition matrix that is used to weight the rewards in the reward matrix. |
|||
*/ |
|||
template<typename MatrixValueType> |
|||
void convertTransitionRewardsToStateActionRewards(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix); |
|||
|
|||
/*! |
|||
* Retrieves whether the reward model is empty, i.e. contains no state-, state-action- or transition-based |
|||
* rewards. |
|||
* |
|||
* @return True iff the reward model is empty. |
|||
*/ |
|||
bool empty() const; |
|||
|
|||
/*! |
|||
* Retrieves (an approximation of) the size of the model in bytes. |
|||
* |
|||
* @return The size of the internal representation of the model measured in bytes. |
|||
*/ |
|||
std::size_t getSizeInBytes() const; |
|||
|
|||
private: |
|||
// An (optional) vector representing the state rewards. |
|||
boost::optional<std::vector<ValueType>> optionalStateRewardVector; |
|||
|
|||
// An (optional) vector representing the state-action rewards. |
|||
boost::optional<std::vector<ValueType>> optionalStateActionRewardVector; |
|||
|
|||
// An (optional) matrix representing the transition rewards. |
|||
boost::optional<storm::storage::SparseMatrix<ValueType>> optionalTransitionRewardMatrix; |
|||
}; |
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELS_SPARSE_STANDARDREWARDMODEL_H_ */ |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue