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

some more work on reward model 

Former-commit-id: 8533357f34
main
dehnert 10 years ago
parent
dcd42d5653
commit
6fa1078fb1
8 changed files with 202 additions and 156 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. 19
      src/builder/ExplicitPrismModelBuilder.cpp
  2. 79
      src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
  3. 55
      src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
  4. 52
      src/models/sparse/StandardRewardModel.cpp
  5. 43
      src/models/sparse/StandardRewardModel.h
  6. 32
      src/models/sparse/StochasticTwoPlayerGame.cpp
  7. 13
      src/models/sparse/StochasticTwoPlayerGame.h
  8. 65
      src/utility/vector.h

19
src/builder/ExplicitPrismModelBuilder.cpp
View File

@ -165,15 +165,28 @@ namespace storm {
ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModel, options);
std::shared_ptr<storm::models::sparse::Model<ValueType>> result;
std::map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModels;
if (options.buildRewards) {
std::string rewardModelName;
if (options.rewardModelName) {
rewardModelName = options.rewardModelName.get();
} else {
rewardModelName = "";
}
rewardModels.emplace(rewardModelName, rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(),
boost::optional<std::vector<ValueType>>(),
rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>());
}
switch (program.getModelType()) {
case storm::prism::Program::ModelType::DTMC:
result = std::shared_ptr<storm::models::sparse::Model<ValueType>>(new storm::models::sparse::Dtmc<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
result = std::shared_ptr<storm::models::sparse::Model<ValueType>>(new storm::models::sparse::Dtmc<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(rewardModels), std::move(modelComponents.choiceLabeling)));
break;
case storm::prism::Program::ModelType::CTMC:
result = std::shared_ptr<storm::models::sparse::Model<ValueType>>(new storm::models::sparse::Ctmc<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
result = std::shared_ptr<storm::models::sparse::Model<ValueType>>(new storm::models::sparse::Ctmc<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(rewardModels), std::move(modelComponents.choiceLabeling)));
break;
case storm::prism::Program::ModelType::MDP:
result = std::shared_ptr<storm::models::sparse::Model<ValueType>>(new storm::models::sparse::Mdp<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
result = std::shared_ptr<storm::models::sparse::Model<ValueType>>(new storm::models::sparse::Mdp<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(rewardModels), std::move(modelComponents.choiceLabeling)));
break;
default:
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating model from probabilistic program: cannot handle this model type.");

79
src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
View File

@ -164,36 +164,10 @@ namespace storm {
template<typename SparseDtmcModelType>
std::vector<typename SparseDtmcPrctlModelChecker<SparseDtmcModelType>::ValueType> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeCumulativeRewardsHelper(RewardModelType const& rewardModel, uint_fast64_t stepBound) const {
// Compute the reward vector to add in each step based on the available reward models.
std::vector<ValueType> totalRewardVector;
if (rewardModel.hasTransitionRewards()) {
totalRewardVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(rewardModel.getTransitionRewardMatrix());
if (rewardModel.hasStateRewards()) {
storm::utility::vector::addVectors(totalRewardVector, rewardModel.getStateRewardVector(), totalRewardVector);
}
if (rewardModel.hasStateActionRewards()) {
storm::utility::vector::addVectors(totalRewardVector, rewardModel.getStateActionRewardVector(), totalRewardVector);
}
} else if (rewardModel.hasStateRewards()) {
totalRewardVector = std::vector<ValueType>(rewardModel.getStateRewardVector());
if (rewardModel.hasStateActionRewards()) {
storm::utility::vector::addVectors(totalRewardVector, rewardModel.getStateActionRewardVector(), totalRewardVector);
}
} else {
totalRewardVector = std::vector<ValueType>(rewardModel.getStateActionRewardVector());
}
std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(this->getModel().getTransitionMatrix());
// Initialize result to either the state rewards of the model or the null vector.
std::vector<ValueType> result;
if (rewardModel.hasStateRewards()) {
result = std::vector<ValueType>(rewardModel.getStateRewardVector());
if (rewardModel.hasStateActionRewards()) {
storm::utility::vector::addVectors(result, rewardModel.getStateActionRewardVector(), result);
}
} else if (rewardModel.hasStateActionRewards()) {
result = std::vector<ValueType>(rewardModel.getStateRewardVector());
} else {
result.resize(this->getModel().getNumberOfStates());
}
std::vector<ValueType> result = rewardModel.getTotalStateActionRewardVector(this->getModel().getNumberOfStates(), this->getModel().getTransitionMatrix().getRowGroupIndices());
// Perform the matrix vector multiplication as often as required by the formula bound.
STORM_LOG_THROW(linearEquationSolverFactory != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available.");
@ -215,15 +189,7 @@ namespace storm {
STORM_LOG_THROW(rewardModel.hasStateRewards() || rewardModel.hasStateActionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
// Initialize result to state rewards of the model.
std::vector<ValueType> result(this->getModel().getNumberOfStates());
if (rewardModel.hasStateRewards()) {
if (rewardModel.hasStateRewards()) {
storm::utility::vector::addVectors(result, rewardModel.getStateRewardVector(), result);
}
if (rewardModel.hasStateActionRewards()) {
storm::utility::vector::addVectors(result, rewardModel.getStateActionRewardVector(), result);
}
}
std::vector<ValueType> result = rewardModel.getTotalStateActionRewardVector(this->getModel().getNumberOfStates(), this->getModel().getTransitionMatrix().getRowGroupIndices());
// Perform the matrix vector multiplication as often as required by the formula bound.
STORM_LOG_THROW(linearEquationSolverFactory != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available.");
@ -273,44 +239,7 @@ namespace storm {
std::vector<ValueType> x(submatrix.getColumnCount(), storm::utility::one<ValueType>());
// Prepare the right-hand side of the equation system.
std::vector<ValueType> b(submatrix.getRowCount());
if (rewardModel.hasTransitionRewards()) {
// If a transition-based reward model is available, we initialize the right-hand
// side to the vector resulting from summing the rows of the pointwise product
// of the transition probability matrix and the transition reward matrix.
std::vector<ValueType> pointwiseProductRowSumVector = transitionMatrix.getPointwiseProductRowSumVector(rewardModel.getTransitionRewardMatrix());
storm::utility::vector::selectVectorValues(b, maybeStates, pointwiseProductRowSumVector);
if (rewardModel.hasStateRewards() || rewardModel.hasStateActionRewards()) {
// If a state-based reward model is also available, we need to add this vector
// as well. As the state reward vector contains entries not just for the states
// that we still consider (i.e. maybeStates), we need to extract these values
// first.
std::vector<ValueType> subStateRewards(b.size());
if (rewardModel.hasStateRewards()) {
storm::utility::vector::selectVectorValues(subStateRewards, maybeStates, rewardModel.getStateRewardVector());
storm::utility::vector::addVectors(b, subStateRewards, b);
}
if (rewardModel.hasStateActionRewards()) {
storm::utility::vector::selectVectorValues(subStateRewards, maybeStates, rewardModel.getStateActionRewardVector());
storm::utility::vector::addVectors(b, subStateRewards, b);
}
}
} else {
// If only a state-based reward model is available, we take this vector as the
// right-hand side. As the state reward vector contains entries not just for the
// states that we still consider (i.e. maybeStates), we need to extract these values
// first.
std::vector<ValueType> subStateRewards(b.size());
if (rewardModel.hasStateRewards()) {
storm::utility::vector::selectVectorValues(subStateRewards, maybeStates, rewardModel.getStateRewardVector());
storm::utility::vector::addVectors(b, subStateRewards, b);
}
if (rewardModel.hasStateActionRewards()) {
storm::utility::vector::selectVectorValues(subStateRewards, maybeStates, rewardModel.getStateActionRewardVector());
storm::utility::vector::addVectors(b, subStateRewards, b);
}
}
std::vector<ValueType> b = rewardModel.getTotalRewardVector(submatrix.getRowCount(), transitionMatrix, maybeStates);
// Now solve the resulting equation system.
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(submatrix);

55
src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
View File

@ -180,24 +180,12 @@ namespace storm {
STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
// Compute the reward vector to add in each step based on the available reward models.
std::vector<ValueType> totalRewardVector;
if (rewardModel.hasTransitionRewards()) {
totalRewardVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(rewardModel.getTransitionRewardMatrix());
std::vector<ValueType>
if (rewardModel.hasStateRewards()) {
storm::utility::vector::addVectors(totalRewardVector, this->getModel().getStateRewardVector(), totalRewardVector);
}
if (rewardModel.hasStateActionRewards()) {
}
} else {
totalRewardVector = std::vector<ValueType>(this->getModel().getStateRewardVector());
}
std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(this->getModel().getTransitionMatrix());
// Initialize result to either the state rewards of the model or the null vector.
std::vector<ValueType> result;
if (this->getModel().hasStateRewards()) {
result = std::vector<ValueType>(this->getModel().getStateRewardVector());
if (rewardModel.hasStateRewards()) {
result = rewardModel.getStateRewardVector();
} else {
result.resize(this->getModel().getNumberOfStates());
}
@ -218,10 +206,10 @@ namespace storm {
template<typename SparseMdpModelType>
std::vector<typename SparseMdpModelType::ValueType> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeInstantaneousRewardsHelper(RewardModelType const& rewardModel, bool minimize, uint_fast64_t stepCount) const {
// Only compute the result if the model has a state-based reward this->getModel().
STORM_LOG_THROW(this->getModel().hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
// Initialize result to state rewards of the this->getModel().
std::vector<ValueType> result(this->getModel().getStateRewardVector());
std::vector<ValueType> result(rewardModel.getStateRewardVector());
STORM_LOG_THROW(MinMaxLinearEquationSolverFactory != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available.");
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = MinMaxLinearEquationSolverFactory->create(this->getModel().getTransitionMatrix());
@ -238,9 +226,9 @@ namespace storm {
}
template<typename SparseMdpModelType>
std::vector<typename SparseMdpModelType::ValueType> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeReachabilityRewardsHelper(RewardModelType const& rewardModel, bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, boost::optional<std::vector<ValueType>> const& stateRewardVector, boost::optional<storm::storage::SparseMatrix<ValueType>> const& transitionRewardMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& MinMaxLinearEquationSolverFactory, bool qualitative) const {
std::vector<typename SparseMdpModelType::ValueType> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeReachabilityRewardsHelper(RewardModelType const& rewardModel, bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& MinMaxLinearEquationSolverFactory, bool qualitative) const {
// Only compute the result if the model has at least one reward this->getModel().
STORM_LOG_THROW(stateRewardVector || transitionRewardMatrix, storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
// Determine which states have a reward of infinity by definition.
storm::storage::BitVector infinityStates;
@ -272,33 +260,8 @@ namespace storm {
// whose reward values are already known.
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false);
// Prepare the right-hand side of the equation system. For entry i this corresponds to
// the accumulated probability of going from state i to some 'yes' state.
std::vector<ValueType> b(submatrix.getRowCount());
if (transitionRewardMatrix) {
// If a transition-based reward model is available, we initialize the right-hand
// side to the vector resulting from summing the rows of the pointwise product
// of the transition probability matrix and the transition reward matrix.
std::vector<ValueType> pointwiseProductRowSumVector = transitionMatrix.getPointwiseProductRowSumVector(transitionRewardMatrix.get());
storm::utility::vector::selectVectorValues(b, maybeStates, transitionMatrix.getRowGroupIndices(), pointwiseProductRowSumVector);
if (stateRewardVector) {
// If a state-based reward model is also available, we need to add this vector
// as well. As the state reward vector contains entries not just for the states
// that we still consider (i.e. maybeStates), we need to extract these values
// first.
std::vector<ValueType> subStateRewards(b.size());
storm::utility::vector::selectVectorValuesRepeatedly(subStateRewards, maybeStates, transitionMatrix.getRowGroupIndices(), stateRewardVector.get());
storm::utility::vector::addVectors(b, subStateRewards, b);
}
} else {
// If only a state-based reward model is available, we take this vector as the
// right-hand side. As the state reward vector contains entries not just for the
// states that we still consider (i.e. maybeStates), we need to extract these values
// first.
storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, transitionMatrix.getRowGroupIndices(), stateRewardVector.get());
}
// Prepare the right-hand side of the equation system.
std::vector<ValueType> b = rewardModel.getTotalRewardVector(submatrix.getRowCount(), transitionMatrix, maybeStates);
// Create vector for results for maybe states.
std::vector<ValueType> x(maybeStates.getNumberOfSetBits());

52
src/models/sparse/StandardRewardModel.cpp
View File

@ -95,6 +95,58 @@ namespace storm {
this->optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<ValueType>>();
}
template<typename ValueType>
template<typename MatrixValueType>
std::vector<ValueType> StandardRewardModel<ValueType>::getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix) const {
std::vector<ValueType> result = this->hasTransitionRewards() ? transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()) : (this->hasStateActionRewards() ? this->getStateActionRewardVector() : std::vector<ValueType>(transitionMatrix.getRowCount()));
if (this->hasStateActionRewards() && this->hasStateActionRewards()) {
storm::utility::vector::addVectors(result, this->getStateActionRewardVector(), result);
}
if (this->hasStateRewards()) {
storm::utility::vector::addVectorToGroupedVector(result, this->getStateRewardVector(), transitionMatrix.getRowGroupIndices());
}
}
template<typename ValueType>
template<typename MatrixValueType>
std::vector<ValueType> StandardRewardModel<ValueType>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, storm::storage::BitVector const& filter) const {
std::vector<ValueType> pointwiseProductRowSumVector;
std::vector<ValueType> result(numberOfRows);
if (this->hasTransitionRewards()) {
pointwiseProductRowSumVector = transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix());
storm::utility::vector::selectVectorValues(result, filter, transitionMatrix.getRowGroupIndices(), pointwiseProductRowSumVector);
}
if (this->hasStateActionRewards()) {
storm::utility::vector::addFilteredVectorGroupsToGroupedVector(result, this->getStateActionRewardVector(), filter, transitionMatrix.getRowGroupIndices());
}
if (this->hasStateRewards()) {
storm::utility::vector::addFilteredVectorToGroupedVector(result, this->getStateRewardVector(), filter, transitionMatrix.getRowGroupIndices());
}
}
template<typename ValueType>
std::vector<ValueType> StandardRewardModel<ValueType>::getTotalStateActionRewardVector(uint_fast64_t numberOfRows, std::vector<uint_fast64_t> const& rowGroupIndices) const {
std::vector<ValueType> result = this->hasStateActionRewards() ? this->getStateActionRewardVector() : std::vector<ValueType>(numberOfRows);
if (this->hasStateRewards()) {
storm::utility::vector::addVectorToGroupedVector(result, this->getStateRewardVector(), rowGroupIndices);
}
return result;
}
template<typename ValueType>
std::vector<ValueType> StandardRewardModel<ValueType>::getTotalStateActionRewardVector(uint_fast64_t numberOfRows, std::vector<uint_fast64_t> const& rowGroupIndices, storm::storage::BitVector const& filter) const {
std::vector<ValueType> result(numberOfRows);
if (this->hasStateRewards()) {
storm::utility::vector::selectVectorValuesRepeatedly(result, filter, rowGroupIndices, this->getStateRewardVector());
}
if (this->hasStateActionRewards()) {
storm::utility::vector::addFilteredVectorGroupsToGroupedVector(result, this->getStateActionRewardVector(), filter, rowGroupIndices);
}
return result;
}
template<typename ValueType>
bool StandardRewardModel<ValueType>::empty() const {
return !(static_cast<bool>(this->optionalStateRewardVector) || static_cast<bool>(this->optionalStateActionRewardVector) || static_cast<bool>(this->optionalTransitionRewardMatrix));

43
src/models/sparse/StandardRewardModel.h
View File

@ -126,6 +126,49 @@ namespace storm {
*/
template<typename MatrixValueType>
void convertTransitionRewardsToStateActionRewards(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix);
/*!
* Creates a vector representing the complete reward vector based on the state-, state-action- and
* transition-based rewards in the reward model.
*
* @param transitionMatrix The matrix that is used to weight the values of the transition reward matrix.
* @return The full state-action reward vector.
*/
template<typename MatrixValueType>
std::vector<ValueType> getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix) const;
/*!
* Creates a vector representing the complete reward vector based on the state-, state-action- and
* transition-based rewards in the reward model.
*
* @param transitionMatrix The matrix that is used to weight the values of the transition reward matrix.
* @param numberOfRows The total number of rows of the resulting vector.
* @param filter A bit vector indicating which row groups to select.
* @return The full state-action reward vector.
*/
template<typename MatrixValueType>
std::vector<ValueType> getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, storm::storage::BitVector const& filter) const;
/*!
* Creates a vector representing the complete state action reward vector based on the state-, state-action-
* and transition-based rewards in the reward model.
*
* @param numberOfRows The total number of rows of the resulting vector.
* @param rowGroupIndices The starting indices of the row groups.
* @return The full state-action reward vector.
*/
std::vector<ValueType> getTotalStateActionRewardVector(uint_fast64_t numberOfRows, std::vector<uint_fast64_t> const& rowGroupIndices) const;
/*!
* Creates a vector representing the complete state action reward vector based on the state- and
* state-action rewards in the reward model.
*
* @param numberOfRows The total number of rows of the resulting vector.
* @param rowGroupIndices The starting indices of the row groups.
* @param filter A bit vector indicating which row groups to select.
* @return The full state-action reward vector.
*/
std::vector<ValueType> getTotalStateActionRewardVector(uint_fast64_t numberOfRows, std::vector<uint_fast64_t> const& rowGroupIndices, storm::storage::BitVector const& filter) const;
/*!
* Retrieves whether the reward model is empty, i.e. contains no state-, state-action- or transition-based

32
src/models/sparse/StochasticTwoPlayerGame.cpp
View File

@ -6,26 +6,26 @@ namespace storm {
namespace models {
namespace sparse {
template <typename ValueType>
StochasticTwoPlayerGame<ValueType>::StochasticTwoPlayerGame(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix,
storm::storage::SparseMatrix<ValueType> const& player2Matrix,
storm::models::sparse::StateLabeling const& stateLabeling,
boost::optional<std::vector<ValueType>> const& optionalStateRewardVector,
boost::optional<std::vector<LabelSet>> const& optionalPlayer1ChoiceLabeling,
boost::optional<std::vector<LabelSet>> const& optionalPlayer2ChoiceLabeling)
: NondeterministicModel<ValueType>(storm::models::ModelType::S2pg, player2Matrix, stateLabeling, optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<ValueType>>(), optionalPlayer2ChoiceLabeling), player1Matrix(player1Matrix), player1Labels(optionalPlayer1ChoiceLabeling) {
template <typename ValueType, typename RewardModelType>
StochasticTwoPlayerGame<ValueType, RewardModelType>::StochasticTwoPlayerGame(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix,
storm::storage::SparseMatrix<ValueType> const& player2Matrix,
storm::models::sparse::StateLabeling const& stateLabeling,
std::map<std::string, RewardModelType> const& rewardModels,
boost::optional<std::vector<LabelSet>> const& optionalPlayer1ChoiceLabeling,
boost::optional<std::vector<LabelSet>> const& optionalPlayer2ChoiceLabeling)
: NondeterministicModel<ValueType>(storm::models::ModelType::S2pg, player2Matrix, stateLabeling, rewardModels, optionalPlayer2ChoiceLabeling), player1Matrix(player1Matrix), player1Labels(optionalPlayer1ChoiceLabeling) {
// Intentionally left empty.
}
template <typename ValueType>
StochasticTwoPlayerGame<ValueType>::StochasticTwoPlayerGame(storm::storage::SparseMatrix<storm::storage::sparse::state_type>&& player1Matrix,
storm::storage::SparseMatrix<ValueType>&& player2Matrix,
storm::models::sparse::StateLabeling&& stateLabeling,
boost::optional<std::vector<ValueType>>&& optionalStateRewardVector,
boost::optional<std::vector<LabelSet>>&& optionalPlayer1ChoiceLabeling,
boost::optional<std::vector<LabelSet>>&& optionalPlayer2ChoiceLabeling)
: NondeterministicModel<ValueType>(storm::models::ModelType::S2pg, std::move(player2Matrix), std::move(stateLabeling), std::move(optionalStateRewardVector), boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(optionalPlayer2ChoiceLabeling)), player1Matrix(std::move(player1Matrix)), player1Labels(std::move(optionalPlayer1ChoiceLabeling)) {
template <typename ValueType, typename RewardModelType>
StochasticTwoPlayerGame<ValueType, RewardModelType>::StochasticTwoPlayerGame(storm::storage::SparseMatrix<storm::storage::sparse::state_type>&& player1Matrix,
storm::storage::SparseMatrix<ValueType>&& player2Matrix,
storm::models::sparse::StateLabeling&& stateLabeling,
std::map<std::string, RewardModelType>&& rewardModels,
boost::optional<std::vector<LabelSet>>&& optionalPlayer1ChoiceLabeling,
boost::optional<std::vector<LabelSet>>&& optionalPlayer2ChoiceLabeling)
: NondeterministicModel<ValueType>(storm::models::ModelType::S2pg, std::move(player2Matrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalPlayer2ChoiceLabeling)), player1Matrix(std::move(player1Matrix)), player1Labels(std::move(optionalPlayer1ChoiceLabeling)) {
// Intentionally left empty.
}

13
src/models/sparse/StochasticTwoPlayerGame.h
View File

@ -11,23 +11,24 @@ namespace storm {
/*!
* This class represents a (discrete-time) stochastic two-player game.
*/
template <typename ValueType>
class StochasticTwoPlayerGame : public NondeterministicModel<ValueType> {
template<class ValueType, typename RewardModelType = StandardRewardModel<ValueType>>
class StochasticTwoPlayerGame : public NondeterministicModel<ValueType, RewardModelType> {
public:
/*!
* Constructs a model from the given data.
*
* @param player1Matrix The matrix representing the choices of player 1.
* @param player2Matrix The matrix representing the choices of player 2.
* @param stateLabeling The labeling of the states.
* @param optionalStateRewardVector The reward values associated with the states.
* @param rewardModels A mapping of reward model names to reward models.
* @param optionalPlayer1ChoiceLabeling A vector that represents the labels associated with the choices of each player 1 state.
* @param optionalPlayer2ChoiceLabeling A vector that represents the labels associated with the choices of each player 2 state.
*/
StochasticTwoPlayerGame(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix,
storm::storage::SparseMatrix<ValueType> const& player2Matrix,
storm::models::sparse::StateLabeling const& stateLabeling,
boost::optional<std::vector<ValueType>> const& optionalStateRewardVector = boost::optional<std::vector<ValueType>>(),
std::map<std::string, RewardModelType> const& rewardModels = std::map<std::string, RewardModelType>(),
boost::optional<std::vector<LabelSet>> const& optionalPlayer1ChoiceLabeling = boost::optional<std::vector<LabelSet>>(),
boost::optional<std::vector<LabelSet>> const& optionalPlayer2ChoiceLabeling = boost::optional<std::vector<LabelSet>>());
@ -37,14 +38,14 @@ namespace storm {
* @param player1Matrix The matrix representing the choices of player 1.
* @param player2Matrix The matrix representing the choices of player 2.
* @param stateLabeling The labeling of the states.
* @param optionalStateRewardVector The reward values associated with the states.
* @param rewardModels A mapping of reward model names to reward models.
* @param optionalPlayer1ChoiceLabeling A vector that represents the labels associated with the choices of each player 1 state.
* @param optionalPlayer2ChoiceLabeling A vector that represents the labels associated with the choices of each player 2 state.
*/
StochasticTwoPlayerGame(storm::storage::SparseMatrix<storm::storage::sparse::state_type>&& player1Matrix,
storm::storage::SparseMatrix<ValueType>&& player2Matrix,
storm::models::sparse::StateLabeling&& stateLabeling,
boost::optional<std::vector<ValueType>>&& optionalStateRewardVector = boost::optional<std::vector<ValueType>>(),
std::map<std::string, RewardModelType>&& rewardModels = std::map<std::string, RewardModelType>(),
boost::optional<std::vector<LabelSet>>&& optionalPlayer1ChoiceLabeling = boost::optional<std::vector<LabelSet>>(),
boost::optional<std::vector<LabelSet>>&& optionalPlayer2ChoiceLabeling = boost::optional<std::vector<LabelSet>>());

65
src/utility/vector.h
View File

@ -129,20 +129,65 @@ namespace storm {
}
}
template<class T>
void addFilteredVectorGroupsToGroupedVector(std::vector<T>& target, std::vector<T> const& source, storm::storage::BitVector const& filter, std::vector<uint_fast64_t> const& rowGroupIndices) {
uint_fast64_t currentPosition = 0;
for (auto group : filter) {
auto it = source.cbegin() + rowGroupIndices[group];
auto ite = source.cbegin() + rowGroupIndices[group + 1];
while (it != ite) {
target[currentPosition] = *it;
++it;
}
}
}
/*!
* Applies the given operation pointwise on the two given vectors and writes the result to the third vector.
* It does so by selecting the elements of the first operand given by the bit vector and uses this element
* for the next
* To obtain an in-place operation, the third vector may be equal to any of the other two vectors.
* Adds the source vector to the target vector in a way such that the i-th entry is added to all elements of
* the i-th row group in the target vector.
*
* @param firstOperand The first operand.
* @param positions The
* @param secondOperand The second operand.
* @param target The target vector.
* @param target The target ("row grouped") vector.
* @param source The source vector.
* @param rowGroupIndices A vector representing the row groups in the target vector.
*/
template<class T>
void applyPointwiseRepeatedly(std::vector<T> const& firstOperand, storm::storage::BitVector const& positions, std::vector<uint_fast64_t> const& rowGrouping, std::vector<T> const& secondOperand, std::vector<T>& target, std::function<T (T const&, T const&)> function) {
void addVectorToGroupedVector(std::vector<T>& target, std::vector<T> const& source, std::vector<uint_fast64_t> const& rowGroupIndices) {
auto targetIt = target.begin();
auto targetIte = target.end();
auto sourceIt = source.cbegin();
auto sourceIte = source.cend();
auto rowGroupIt = rowGroupIndices.cbegin();
for (; sourceIt != sourceIte; ++sourceIt) {
uint_fast64_t current = *rowGroupIt;
++rowGroupIt;
uint_fast64_t next = *rowGroupIt;
while (current < next) {
*targetIt = *source;
++targetIt;
}
}
}
/*!
* Adds the source vector to the target vector in a way such that the i-th selected entry is added to all
* elements of the i-th row group in the target vector.
*
* @param target The target ("row grouped") vector.
* @param source The source vector.
* @param rowGroupIndices A vector representing the row groups in the target vector.
*/
template<class T>
void addFilteredVectorToGroupedVector(std::vector<T>& target, std::vector<T> const& source, storm::storage::BitVector const& filter, std::vector<uint_fast64_t> const& rowGroupIndices) {
uint_fast64_t currentPosition = 0;
for (auto group : filter) {
uint_fast64_t current = rowGroupIndices[group];
uint_fast64_t next = rowGroupIndices[group + 1];
while (current < next) {
target[currentPosition] = source[group];
++currentPosition;
}
}
}
/*!

Write Preview
Loading…
Cancel
Save