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

fixed bug when computing expected reachability rewards on MAs

tempestpy_adaptions
TimQu 8 years ago
parent
5bfb6b817a
commit
0bb1c5855e
4 changed files with 93 additions and 80 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. 97
      src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
  2. 9
      src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h
  3. 40
      src/storm/models/sparse/StandardRewardModel.cpp
  4. 27
      src/storm/models/sparse/StandardRewardModel.h

97
src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
View File

@ -190,8 +190,12 @@ namespace storm {
template <typename ValueType>
template <typename RewardModelType>
std::vector<ValueType> SparseMarkovAutomatonCslHelper<ValueType>::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix.getRowCount(), transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true));
return computeExpectedRewards(dir, transitionMatrix, backwardTransitions, exitRateVector, markovianStates, psiStates, totalRewardVector, minMaxLinearEquationSolverFactory);
std::vector<ValueType> stateRewardWeights(transitionMatrix.getRowGroupCount());
for (auto const markovianState : markovianStates) {
stateRewardWeights[markovianState] = storm::utility::one<ValueType>() / exitRateVector[markovianState];
}
std::vector<ValueType> totalRewardVector = rewardModel.getTotalActionRewardVector(transitionMatrix, stateRewardWeights);
return computeExpectedRewards(dir, transitionMatrix, backwardTransitions, psiStates, totalRewardVector, minMaxLinearEquationSolverFactory);
}
template<typename ValueType>
@ -351,58 +355,77 @@ namespace storm {
template <typename ValueType>
std::vector<ValueType> SparseMarkovAutomatonCslHelper<ValueType>::computeTimes(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount();
std::vector<ValueType> rewardValues(numberOfStates, storm::utility::zero<ValueType>());
storm::utility::vector::setVectorValues(rewardValues, markovianStates, storm::utility::one<ValueType>());
return computeExpectedRewards(dir, transitionMatrix, backwardTransitions, exitRateVector, markovianStates, psiStates, rewardValues, minMaxLinearEquationSolverFactory);
std::vector<ValueType> rewardValues(transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
for (auto const markovianState : markovianStates) {
rewardValues[transitionMatrix.getRowGroupIndices()[markovianState]] = storm::utility::one<ValueType>() / exitRateVector[markovianState];
}
return computeExpectedRewards(dir, transitionMatrix, backwardTransitions, psiStates, rewardValues, minMaxLinearEquationSolverFactory);
}
template <typename ValueType>
std::vector<ValueType> SparseMarkovAutomatonCslHelper<ValueType>::computeExpectedRewards(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, std::vector<ValueType> const& stateRewards, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
template<typename ValueType>
std::vector<ValueType>
SparseMarkovAutomatonCslHelper<ValueType>::computeExpectedRewards(OptimizationDirection dir,
storm::storage::SparseMatrix<ValueType> const &transitionMatrix,
storm::storage::SparseMatrix<ValueType> const &backwardTransitions,
storm::storage::BitVector const &goalStates,
std::vector<ValueType> const &stateActionRewardVector,
storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const &minMaxLinearEquationSolverFactory) {
uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount();
// First, we need to check which states have infinite expected time (by definition).
storm::storage::BitVector infinityStates;
if (dir ==OptimizationDirection::Minimize) {
if (dir == OptimizationDirection::Minimize) {
// If we need to compute the minimum expected times, we have to set the values of those states to infinity that, under all schedulers,
// reach a bottom SCC without a goal state.
// So we start by computing all bottom SCCs without goal states.
storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition(transitionMatrix, ~goalStates, true, true);
storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition(transitionMatrix,
~goalStates, true,
true);
// Now form the union of all these SCCs.
storm::storage::BitVector unionOfNonGoalBSccs(numberOfStates);
for (auto const& scc : sccDecomposition) {
for (auto const &scc : sccDecomposition) {
for (auto state : scc) {
unionOfNonGoalBSccs.set(state);
}
}
// Finally, if this union is non-empty, compute the states such that all schedulers reach some state of the union.
if (!unionOfNonGoalBSccs.empty()) {
infinityStates = storm::utility::graph::performProbGreater0A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, storm::storage::BitVector(numberOfStates, true), unionOfNonGoalBSccs);
infinityStates = storm::utility::graph::performProbGreater0A(transitionMatrix,
transitionMatrix.getRowGroupIndices(),
backwardTransitions,
storm::storage::BitVector(
numberOfStates, true),
unionOfNonGoalBSccs);
} else {
// Otherwise, we have no infinity states.
infinityStates = storm::storage::BitVector(numberOfStates);
}
} else {
// If we maximize the property, the expected time of a state is infinite, if an end-component without any goal state is reachable.
// So we start by computing all MECs that have no goal state.
storm::storage::MaximalEndComponentDecomposition<double> mecDecomposition(transitionMatrix, backwardTransitions, ~goalStates);
storm::storage::MaximalEndComponentDecomposition<double> mecDecomposition(transitionMatrix,
backwardTransitions,
~goalStates);
// Now we form the union of all states in these end components.
storm::storage::BitVector unionOfNonGoalMaximalEndComponents(numberOfStates);
for (auto const& mec : mecDecomposition) {
for (auto const& stateActionPair : mec) {
for (auto const &mec : mecDecomposition) {
for (auto const &stateActionPair : mec) {
unionOfNonGoalMaximalEndComponents.set(stateActionPair.first);
}
}
if (!unionOfNonGoalMaximalEndComponents.empty()) {
// Now we need to check for which states there exists a scheduler that reaches one of the previously computed states.
infinityStates = storm::utility::graph::performProbGreater0E(backwardTransitions, storm::storage::BitVector(numberOfStates, true), unionOfNonGoalMaximalEndComponents);
infinityStates = storm::utility::graph::performProbGreater0E(backwardTransitions,
storm::storage::BitVector(
numberOfStates, true),
unionOfNonGoalMaximalEndComponents);
} else {
// Otherwise, we have no infinity states.
infinityStates = storm::storage::BitVector(numberOfStates);
@ -413,33 +436,31 @@ namespace storm {
// Create resulting vector.
std::vector<ValueType> result(numberOfStates);
if (!maybeStates.empty()) {
// Then, we can eliminate the rows and columns for all states whose values are already known.
std::vector<ValueType> x(maybeStates.getNumberOfSetBits());
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates);
// Now prepare the expected reward values for all states so they can be used as the right-hand side of the equation system.
std::vector<ValueType> rewardValues(stateRewards);
for (auto state : markovianStates) {
rewardValues[state] = rewardValues[state] / exitRateVector[state];
}
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, maybeStates,
maybeStates);
// Finally, prepare the actual right-hand side.
std::vector<ValueType> b(submatrix.getRowCount());
storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, transitionMatrix.getRowGroupIndices(), rewardValues);
storm::utility::vector::selectVectorValues(b, maybeStates,
transitionMatrix.getRowGroupIndices(),
stateActionRewardVector);
// Solve the corresponding system of equations.
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(submatrix);
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(
submatrix);
solver->solveEquations(dir, x, b);
// Set values of resulting vector according to previous result and return the result.
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, x);
}
storm::utility::vector::setVectorValues(result, goalStates, storm::utility::zero<ValueType>());
storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity<ValueType>());
return result;
}

9
src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h
View File

@ -32,7 +32,7 @@ namespace storm {
/*!
* Computes the long-run average value for the given maximal end component of a Markov automaton.
*
* @param minimize Sets whether the long-run average is to be minimized or maximized.
* @param dir Sets whether the long-run average is to be minimized or maximized.
* @param transitionMatrix The transition matrix of the underlying Markov automaton.
* @param markovianStates A bit vector storing all markovian states.
* @param exitRateVector A vector with exit rates for all states. Exit rates of probabilistic states are
@ -46,12 +46,9 @@ namespace storm {
/*!
* Computes the expected reward that is gained from each state before entering any of the goal states.
*
* @param minimize Indicates whether minimal or maximal rewards are to be computed.
* @param dir Indicates whether minimal or maximal rewards are to be computed.
* @param transitionMatrix The transition matrix of the underlying Markov automaton.
* @param backwardTransitions The reversed transition relation of the underlying Markov automaton.
* @param exitRateVector A vector with exit rates for all states. Exit rates of probabilistic states are
* assumed to be zero.
* @param markovianStates A bit vector storing all markovian states.
* @param goalStates The goal states that define until which point rewards are gained.
* @param stateRewards A vector that defines the reward gained in each state. For probabilistic states,
* this is an instantaneous reward that is fully gained and for Markovian states the actually gained
@ -59,7 +56,7 @@ namespace storm {
* of the state.
* @return A vector that contains the expected reward for each state of the model.
*/
static std::vector<ValueType> computeExpectedRewards(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, std::vector<ValueType> const& stateRewards, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
static std::vector<ValueType> computeExpectedRewards(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& goalStates, std::vector<ValueType> const& stateRewards, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
};
}

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

@ -161,7 +161,7 @@ namespace storm {
this->optionalStateActionRewardVector = boost::none;
}
}
template<typename ValueType>
template<typename MatrixValueType>
std::vector<ValueType> StandardRewardModel<ValueType>::getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix) const {
@ -211,24 +211,23 @@ namespace storm {
}
return result;
}
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());
template<typename MatrixValueType>
std::vector<ValueType> StandardRewardModel<ValueType>::getTotalActionRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::vector<MatrixValueType> const& stateRewardWeights) const {
std::vector<ValueType> result;
if (this->hasTransitionRewards()) {
result = transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix());
} else {
result = std::vector<ValueType>(transitionMatrix.getRowCount());
}
if (this->hasStateActionRewards()) {
storm::utility::vector::addFilteredVectorGroupsToGroupedVector(result, this->getStateActionRewardVector(), filter, rowGroupIndices);
storm::utility::vector::addVectors(result, this->getStateActionRewardVector(), result);
}
if (this->hasStateRewards()) {
std::vector<ValueType> scaledStateRewardVector(transitionMatrix.getRowGroupCount());
storm::utility::vector::multiplyVectorsPointwise(this->getStateRewardVector(), stateRewardWeights, scaledStateRewardVector);
storm::utility::vector::addVectorToGroupedVector(result, scaledStateRewardVector, transitionMatrix.getRowGroupIndices());
}
return result;
}
@ -304,6 +303,7 @@ namespace storm {
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>::getTotalActionRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<double> const& stateRewardWeights) const;
template void StandardRewardModel<double>::reduceToStateBasedRewards(storm::storage::SparseMatrix<double> const& transitionMatrix, bool reduceToStateRewards);
template void StandardRewardModel<double>::setStateActionReward(uint_fast64_t choiceIndex, double const & newValue);
template void StandardRewardModel<double>::setStateReward(uint_fast64_t state, double const & newValue);
@ -313,6 +313,7 @@ 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>::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>::setStateActionReward(uint_fast64_t choiceIndex, float const & newValue);
template void StandardRewardModel<float>::setStateReward(uint_fast64_t state, float const & newValue);
@ -323,24 +324,27 @@ namespace storm {
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>::getTotalActionRewardVector(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<storm::RationalNumber> const& stateRewardWeights) const;
template void StandardRewardModel<storm::RationalNumber>::reduceToStateBasedRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, bool reduceToStateRewards);
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>;
template std::ostream& operator<<<storm::RationalNumber>(std::ostream& out, StandardRewardModel<storm::RationalNumber> const& rewardModel);
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>::getTotalActionRewardVector(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<storm::RationalFunction> const& stateRewardWeights) const;
template void StandardRewardModel<storm::RationalFunction>::reduceToStateBasedRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, bool reduceToStateRewards);
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>;
template std::ostream& operator<<<storm::RationalFunction>(std::ostream& out, StandardRewardModel<storm::RationalFunction> const& rewardModel);
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>::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);

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

@ -217,28 +217,19 @@ namespace storm {
*/
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.
* Creates a vector representing the complete action-based rewards, i.e., state-action- and
* transition-based rewards
*
* @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.
* @param transitionMatrix The matrix that is used to weight the values of the transition reward matrix.
* @return The state-action reward vector that considers state-action rewards and transition rewards of this reward model.
*/
std::vector<ValueType> getTotalStateActionRewardVector(uint_fast64_t numberOfRows, std::vector<uint_fast64_t> const& rowGroupIndices, storm::storage::BitVector const& filter) const;
template<typename MatrixValueType>
std::vector<ValueType> getTotalActionRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::vector<MatrixValueType> const& stateRewardWeights) const;
/*!
* Sets the given value in the state-action reward vector at the given row. This assumes that the reward
* model has state-action rewards.

Write Preview
Loading…
Cancel
Save