From 6fa1078fb1959d3fab4d9de89b7a617f131b4236 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 11 Aug 2015 22:11:45 +0200 Subject: [PATCH] some more work on reward model Former-commit-id: 8533357f3432f43d1982f981aa8ca5fc48f40aca --- src/builder/ExplicitPrismModelBuilder.cpp | 19 ++++- .../prctl/SparseDtmcPrctlModelChecker.cpp | 79 +------------------ .../prctl/SparseMdpPrctlModelChecker.cpp | 55 +++---------- src/models/sparse/StandardRewardModel.cpp | 52 ++++++++++++ src/models/sparse/StandardRewardModel.h | 43 ++++++++++ src/models/sparse/StochasticTwoPlayerGame.cpp | 32 ++++---- src/models/sparse/StochasticTwoPlayerGame.h | 13 +-- src/utility/vector.h | 65 ++++++++++++--- 8 files changed, 202 insertions(+), 156 deletions(-) diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 8b3dbffa0..469520364 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -165,15 +165,28 @@ namespace storm { ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModel, options); std::shared_ptr> result; + std::map> 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>(), + boost::optional>(), + rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>()); + } + switch (program.getModelType()) { case storm::prism::Program::ModelType::DTMC: - result = std::shared_ptr>(new storm::models::sparse::Dtmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); + result = std::shared_ptr>(new storm::models::sparse::Dtmc(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>(new storm::models::sparse::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); + result = std::shared_ptr>(new storm::models::sparse::Ctmc(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>(new storm::models::sparse::Mdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); + result = std::shared_ptr>(new storm::models::sparse::Mdp(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."); diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 659af00d6..d8d2f1378 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -164,36 +164,10 @@ namespace storm { template std::vector::ValueType> SparseDtmcPrctlModelChecker::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 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(rewardModel.getStateRewardVector()); - if (rewardModel.hasStateActionRewards()) { - storm::utility::vector::addVectors(totalRewardVector, rewardModel.getStateActionRewardVector(), totalRewardVector); - } - } else { - totalRewardVector = std::vector(rewardModel.getStateActionRewardVector()); - } + std::vector totalRewardVector = rewardModel.getTotalRewardVector(this->getModel().getTransitionMatrix()); // Initialize result to either the state rewards of the model or the null vector. - std::vector result; - if (rewardModel.hasStateRewards()) { - result = std::vector(rewardModel.getStateRewardVector()); - if (rewardModel.hasStateActionRewards()) { - storm::utility::vector::addVectors(result, rewardModel.getStateActionRewardVector(), result); - } - } else if (rewardModel.hasStateActionRewards()) { - result = std::vector(rewardModel.getStateRewardVector()); - } else { - result.resize(this->getModel().getNumberOfStates()); - } + std::vector 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 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 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 x(submatrix.getColumnCount(), storm::utility::one()); // Prepare the right-hand side of the equation system. - std::vector 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 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 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 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 b = rewardModel.getTotalRewardVector(submatrix.getRowCount(), transitionMatrix, maybeStates); // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix); diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 0b834bf5f..b079ff63c 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -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 totalRewardVector; - if (rewardModel.hasTransitionRewards()) { - totalRewardVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(rewardModel.getTransitionRewardMatrix()); - std::vector - if (rewardModel.hasStateRewards()) { - storm::utility::vector::addVectors(totalRewardVector, this->getModel().getStateRewardVector(), totalRewardVector); - } - if (rewardModel.hasStateActionRewards()) { - - } - } else { - totalRewardVector = std::vector(this->getModel().getStateRewardVector()); - } + std::vector totalRewardVector = rewardModel.getTotalRewardVector(this->getModel().getTransitionMatrix()); // Initialize result to either the state rewards of the model or the null vector. std::vector result; - if (this->getModel().hasStateRewards()) { - result = std::vector(this->getModel().getStateRewardVector()); + if (rewardModel.hasStateRewards()) { + result = rewardModel.getStateRewardVector(); } else { result.resize(this->getModel().getNumberOfStates()); } @@ -218,10 +206,10 @@ namespace storm { template std::vector SparseMdpPrctlModelChecker::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 result(this->getModel().getStateRewardVector()); + std::vector result(rewardModel.getStateRewardVector()); STORM_LOG_THROW(MinMaxLinearEquationSolverFactory != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available."); std::unique_ptr> solver = MinMaxLinearEquationSolverFactory->create(this->getModel().getTransitionMatrix()); @@ -238,9 +226,9 @@ namespace storm { } template - std::vector SparseMdpPrctlModelChecker::computeReachabilityRewardsHelper(RewardModelType const& rewardModel, bool minimize, storm::storage::SparseMatrix const& transitionMatrix, boost::optional> const& stateRewardVector, boost::optional> const& transitionRewardMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::utility::solver::MinMaxLinearEquationSolverFactory const& MinMaxLinearEquationSolverFactory, bool qualitative) const { + std::vector SparseMdpPrctlModelChecker::computeReachabilityRewardsHelper(RewardModelType const& rewardModel, bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::utility::solver::MinMaxLinearEquationSolverFactory 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 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 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 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 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 b = rewardModel.getTotalRewardVector(submatrix.getRowCount(), transitionMatrix, maybeStates); // Create vector for results for maybe states. std::vector x(maybeStates.getNumberOfSetBits()); diff --git a/src/models/sparse/StandardRewardModel.cpp b/src/models/sparse/StandardRewardModel.cpp index 928d388c2..f33672c07 100644 --- a/src/models/sparse/StandardRewardModel.cpp +++ b/src/models/sparse/StandardRewardModel.cpp @@ -95,6 +95,58 @@ namespace storm { this->optionalTransitionRewardMatrix = boost::optional>(); } + template + template + std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const { + std::vector result = this->hasTransitionRewards() ? transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()) : (this->hasStateActionRewards() ? this->getStateActionRewardVector() : std::vector(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 + template + std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const { + std::vector pointwiseProductRowSumVector; + + std::vector 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 + std::vector StandardRewardModel::getTotalStateActionRewardVector(uint_fast64_t numberOfRows, std::vector const& rowGroupIndices) const { + std::vector result = this->hasStateActionRewards() ? this->getStateActionRewardVector() : std::vector(numberOfRows); + if (this->hasStateRewards()) { + storm::utility::vector::addVectorToGroupedVector(result, this->getStateRewardVector(), rowGroupIndices); + } + return result; + } + + template + std::vector StandardRewardModel::getTotalStateActionRewardVector(uint_fast64_t numberOfRows, std::vector const& rowGroupIndices, storm::storage::BitVector const& filter) const { + std::vector 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 bool StandardRewardModel::empty() const { return !(static_cast(this->optionalStateRewardVector) || static_cast(this->optionalStateActionRewardVector) || static_cast(this->optionalTransitionRewardMatrix)); diff --git a/src/models/sparse/StandardRewardModel.h b/src/models/sparse/StandardRewardModel.h index b7f9fdc13..7723a3d72 100644 --- a/src/models/sparse/StandardRewardModel.h +++ b/src/models/sparse/StandardRewardModel.h @@ -126,6 +126,49 @@ namespace storm { */ template void convertTransitionRewardsToStateActionRewards(storm::storage::SparseMatrix 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 + std::vector getTotalRewardVector(storm::storage::SparseMatrix 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 + std::vector getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix 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 getTotalStateActionRewardVector(uint_fast64_t numberOfRows, std::vector 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 getTotalStateActionRewardVector(uint_fast64_t numberOfRows, std::vector 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 diff --git a/src/models/sparse/StochasticTwoPlayerGame.cpp b/src/models/sparse/StochasticTwoPlayerGame.cpp index 8e6daa52a..acdde7b30 100644 --- a/src/models/sparse/StochasticTwoPlayerGame.cpp +++ b/src/models/sparse/StochasticTwoPlayerGame.cpp @@ -6,26 +6,26 @@ namespace storm { namespace models { namespace sparse { - template - StochasticTwoPlayerGame::StochasticTwoPlayerGame(storm::storage::SparseMatrix const& player1Matrix, - storm::storage::SparseMatrix const& player2Matrix, - storm::models::sparse::StateLabeling const& stateLabeling, - boost::optional> const& optionalStateRewardVector, - boost::optional> const& optionalPlayer1ChoiceLabeling, - boost::optional> const& optionalPlayer2ChoiceLabeling) - : NondeterministicModel(storm::models::ModelType::S2pg, player2Matrix, stateLabeling, optionalStateRewardVector, boost::optional>(), optionalPlayer2ChoiceLabeling), player1Matrix(player1Matrix), player1Labels(optionalPlayer1ChoiceLabeling) { + template + StochasticTwoPlayerGame::StochasticTwoPlayerGame(storm::storage::SparseMatrix const& player1Matrix, + storm::storage::SparseMatrix const& player2Matrix, + storm::models::sparse::StateLabeling const& stateLabeling, + std::map const& rewardModels, + boost::optional> const& optionalPlayer1ChoiceLabeling, + boost::optional> const& optionalPlayer2ChoiceLabeling) + : NondeterministicModel(storm::models::ModelType::S2pg, player2Matrix, stateLabeling, rewardModels, optionalPlayer2ChoiceLabeling), player1Matrix(player1Matrix), player1Labels(optionalPlayer1ChoiceLabeling) { // Intentionally left empty. } - template - StochasticTwoPlayerGame::StochasticTwoPlayerGame(storm::storage::SparseMatrix&& player1Matrix, - storm::storage::SparseMatrix&& player2Matrix, - storm::models::sparse::StateLabeling&& stateLabeling, - boost::optional>&& optionalStateRewardVector, - boost::optional>&& optionalPlayer1ChoiceLabeling, - boost::optional>&& optionalPlayer2ChoiceLabeling) - : NondeterministicModel(storm::models::ModelType::S2pg, std::move(player2Matrix), std::move(stateLabeling), std::move(optionalStateRewardVector), boost::optional>(), std::move(optionalPlayer2ChoiceLabeling)), player1Matrix(std::move(player1Matrix)), player1Labels(std::move(optionalPlayer1ChoiceLabeling)) { + template + StochasticTwoPlayerGame::StochasticTwoPlayerGame(storm::storage::SparseMatrix&& player1Matrix, + storm::storage::SparseMatrix&& player2Matrix, + storm::models::sparse::StateLabeling&& stateLabeling, + std::map&& rewardModels, + boost::optional>&& optionalPlayer1ChoiceLabeling, + boost::optional>&& optionalPlayer2ChoiceLabeling) + : NondeterministicModel(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. } diff --git a/src/models/sparse/StochasticTwoPlayerGame.h b/src/models/sparse/StochasticTwoPlayerGame.h index cbd2988ca..6bc33b4d7 100644 --- a/src/models/sparse/StochasticTwoPlayerGame.h +++ b/src/models/sparse/StochasticTwoPlayerGame.h @@ -11,23 +11,24 @@ namespace storm { /*! * This class represents a (discrete-time) stochastic two-player game. */ - template - class StochasticTwoPlayerGame : public NondeterministicModel { + template> + class StochasticTwoPlayerGame : public NondeterministicModel { 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 const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix, storm::models::sparse::StateLabeling const& stateLabeling, - boost::optional> const& optionalStateRewardVector = boost::optional>(), + std::map const& rewardModels = std::map(), boost::optional> const& optionalPlayer1ChoiceLabeling = boost::optional>(), boost::optional> const& optionalPlayer2ChoiceLabeling = boost::optional>()); @@ -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&& player1Matrix, storm::storage::SparseMatrix&& player2Matrix, storm::models::sparse::StateLabeling&& stateLabeling, - boost::optional>&& optionalStateRewardVector = boost::optional>(), + std::map&& rewardModels = std::map(), boost::optional>&& optionalPlayer1ChoiceLabeling = boost::optional>(), boost::optional>&& optionalPlayer2ChoiceLabeling = boost::optional>()); diff --git a/src/utility/vector.h b/src/utility/vector.h index adc1b9fb3..52556fd0c 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -129,20 +129,65 @@ namespace storm { } } + template + void addFilteredVectorGroupsToGroupedVector(std::vector& target, std::vector const& source, storm::storage::BitVector const& filter, std::vector 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 - void applyPointwiseRepeatedly(std::vector const& firstOperand, storm::storage::BitVector const& positions, std::vector const& rowGrouping, std::vector const& secondOperand, std::vector& target, std::function function) { - + void addVectorToGroupedVector(std::vector& target, std::vector const& source, std::vector 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 + void addFilteredVectorToGroupedVector(std::vector& target, std::vector const& source, storm::storage::BitVector const& filter, std::vector 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; + } + } } /*!