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

fixed a bug when reducing state-action rewards to state rewards for CTMCs

main
dehnert 8 years ago
parent
5302cc5231
commit
9e8d6eee90
8 changed files with 80 additions and 60 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. 6
      src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp
  2. 22
      src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
  3. 2
      src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
  4. 33
      src/storm/models/sparse/StandardRewardModel.cpp
  5. 6
      src/storm/models/sparse/StandardRewardModel.h
  6. 6
      src/storm/models/symbolic/StandardRewardModel.cpp
  7. 6
      src/storm/models/symbolic/StandardRewardModel.h
  8. 47
      src/storm/parser/FormulaParserGrammar.cpp

6
src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp
View File

@ -267,7 +267,7 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
// Then compute the state reward vector to use in the computation.
storm::dd::Add<DdType, ValueType> totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, model.getColumnVariables(), exitRateVector);
storm::dd::Add<DdType, ValueType> totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, model.getColumnVariables(), exitRateVector, false);
std::vector<ValueType> explicitTotalRewardVector = totalRewardVector.toVector(odd);
// Finally, compute the transient probabilities.
@ -292,6 +292,8 @@ namespace storm {
template<storm::dd::DdType DdType, class ValueType>
std::unique_ptr<CheckResult> HybridCtmcCslHelper<DdType, ValueType>::computeLongRunAverageRewards(storm::models::symbolic::Ctmc<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& rateMatrix, storm::dd::Add<DdType, ValueType> const& exitRateVector, RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
storm::dd::Add<DdType, ValueType> probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector);
// Create ODD for the translation.
@ -300,7 +302,7 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> explicitProbabilityMatrix = probabilityMatrix.toMatrix(odd, odd);
std::vector<ValueType> explicitExitRateVector = exitRateVector.toVector(odd);
std::vector<ValueType> result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards(explicitProbabilityMatrix, rewardModel.getStateRewardVector().toVector(odd), &explicitExitRateVector, linearEquationSolverFactory);
std::vector<ValueType> result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards(explicitProbabilityMatrix, rewardModel.getTotalRewardVector(probabilityMatrix, model.getColumnVariables(), exitRateVector, true).toVector(odd), &explicitExitRateVector, linearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), std::move(odd), std::move(result)));
}

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

@ -262,7 +262,7 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> uniformizedMatrix = computeUniformizedMatrix(rateMatrix, storm::storage::BitVector(numberOfStates, true), uniformizationRate, exitRateVector);
// Compute the total state reward vector.
std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, exitRateVector);
std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, exitRateVector, false);
// Finally, compute the transient probabilities.
return computeTransientProbabilities<ValueType, true>(uniformizedMatrix, nullptr, timeBound, uniformizationRate, totalRewardVector, linearEquationSolverFactory);
@ -360,14 +360,9 @@ namespace storm {
template <typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, RewardModelType const& rewardModel, std::vector<ValueType> const* exitRateVector, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
// Only compute the result if the model has a state-based reward model.
STORM_LOG_THROW(!rewardModel.hasStateRewards(), 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.");
return computeLongRunAverages<ValueType>(probabilityMatrix,
[&rewardModel] (storm::storage::sparse::state_type const& state) -> ValueType {
return rewardModel.getStateReward(state);
},
exitRateVector,
linearEquationSolverFactory);
return computeLongRunAverageRewards(probabilityMatrix, rewardModel.getTotalRewardVector(probabilityMatrix, *exitRateVector, true), exitRateVector, linearEquationSolverFactory);
}
template <typename ValueType>
@ -501,6 +496,12 @@ namespace storm {
solver->solveEquations(bsccEquationSystemSolution, bsccEquationSystemRightSide);
}
// std::vector<ValueType> tmp(probabilityMatrix.getRowCount(), storm::utility::zero<ValueType>());
// probabilityMatrix.multiplyVectorWithMatrix(bsccEquationSystemSolution, tmp);
// for (uint64_t i = 0; i < tmp.size(); ++i) {
// std::cout << tmp[i] << " vs. " << bsccEquationSystemSolution[i] << std::endl;
// }
// If exit rates were given, we need to 'fix' the results to also account for the timing behaviour.
if (exitRateVector != nullptr) {
std::vector<ValueType> bsccTotalValue(bsccDecomposition.size(), zero);
@ -512,6 +513,11 @@ namespace storm {
bsccEquationSystemSolution[indexInStatesInBsccs[*stateIter]] = (bsccEquationSystemSolution[indexInStatesInBsccs[*stateIter]] * (one / (*exitRateVector)[*stateIter])) / bsccTotalValue[stateToBsccIndexMap[indexInStatesInBsccs[*stateIter]]];
}
}
// for (auto const& val : bsccEquationSystemSolution) {
// std::cout << "val: " << val << std::endl;
// }
// Calculate LRA Value for each BSCC from steady state distribution in BSCCs.
for (uint_fast64_t bsccIndex = 0; bsccIndex < bsccDecomposition.size(); ++bsccIndex) {
storm::storage::StronglyConnectedComponent const& bscc = bsccDecomposition[bsccIndex];

2
src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
View File

@ -264,7 +264,7 @@ namespace storm {
storm::dd::Odd odd = model.getReachableStates().createOdd();
storm::storage::SparseMatrix<ValueType> explicitProbabilityMatrix = model.getTransitionMatrix().toMatrix(odd, odd);
std::vector<ValueType> result = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeLongRunAverageRewards(explicitProbabilityMatrix, rewardModel.getStateRewardVector().toVector(odd), linearEquationSolverFactory);
std::vector<ValueType> result = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeLongRunAverageRewards(explicitProbabilityMatrix, rewardModel.getTotalRewardVector(model.getTransitionMatrix(), model.getColumnVariables()).toVector(odd), linearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), std::move(odd), std::move(result)));
}

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

@ -165,6 +165,11 @@ namespace storm {
template<typename ValueType>
template<typename MatrixValueType>
std::vector<ValueType> StandardRewardModel<ValueType>::getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix) const {
if (this->hasStateActionRewards()) {
for (auto const& e : this->getStateActionRewardVector()) {
std::cout << "e " << e << std::endl;
}
}
std::vector<ValueType> result = this->hasTransitionRewards() ? transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()) : (this->hasStateActionRewards() ? this->getStateActionRewardVector() : std::vector<ValueType>(transitionMatrix.getRowCount()));
if (this->hasStateActionRewards() && this->hasTransitionRewards()) {
storm::utility::vector::addVectors(result, this->getStateActionRewardVector(), result);
@ -177,16 +182,16 @@ namespace storm {
template<typename ValueType>
template<typename MatrixValueType>
std::vector<ValueType> StandardRewardModel<ValueType>::getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::vector<MatrixValueType> const& weights) const {
std::vector<ValueType> result = this->hasTransitionRewards() ? transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()) : (this->hasStateActionRewards() ? this->getStateActionRewardVector() : std::vector<ValueType>(transitionMatrix.getRowCount()));
if (!this->hasTransitionRewards() && this->hasStateActionRewards()) {
// If we initialized the result with the state-action rewards we can scale the result in place.
storm::utility::vector::multiplyVectorsPointwise(result, weights, result);
std::vector<ValueType> StandardRewardModel<ValueType>::getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::vector<MatrixValueType> const& weights, bool scaleTransAndActions) const {
std::vector<ValueType> result;
if (this->hasTransitionRewards()) {
result = transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix());
storm::utility::vector::applyPointwise<MatrixValueType, ValueType, ValueType>(weights, this->getStateActionRewardVector(), result, [] (MatrixValueType const& weight, ValueType const& rewardElement, ValueType const& resultElement) { return weight * (resultElement + rewardElement); } );
} else {
result = std::vector<ValueType>(transitionMatrix.getRowCount());
if (this->hasStateActionRewards()) {
storm::utility::vector::applyPointwise<MatrixValueType, ValueType, ValueType>(weights, this->getStateActionRewardVector(), result, [] (MatrixValueType const& weight, ValueType const& rewardElement, ValueType const& resultElement) { return weight * rewardElement; } );
}
if (this->hasStateActionRewards() && this->hasTransitionRewards()) {
// If we initialized the result with the transition rewards and still have state-action rewards,
// we need to add the scaled vector directly.
storm::utility::vector::applyPointwise<MatrixValueType, ValueType, ValueType>(weights, this->getStateActionRewardVector(), result, [] (MatrixValueType const& weight, ValueType const& rewardElement, ValueType const& resultElement) { return resultElement + weight * rewardElement; } );
}
if (this->hasStateRewards()) {
storm::utility::vector::addVectorToGroupedVector(result, this->getStateRewardVector(), transitionMatrix.getRowGroupIndices());
@ -319,7 +324,7 @@ namespace storm {
// Explicitly instantiate the class.
template std::vector<double> StandardRewardModel<double>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix) const;
template std::vector<double> StandardRewardModel<double>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::BitVector const& filter) const;
template std::vector<double> StandardRewardModel<double>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<double> const& weights) const;
template std::vector<double> StandardRewardModel<double>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<double> const& weights, bool scaleTransAndActions) 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);
@ -328,7 +333,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) const;
template std::vector<float> StandardRewardModel<float>::getTotalRewardVector(storm::storage::SparseMatrix<float> const& transitionMatrix, std::vector<float> const& weights, bool scaleTransAndActions) 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);
@ -338,7 +343,7 @@ namespace storm {
#ifdef STORM_HAVE_CARL
template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::BitVector const& filter) const;
template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix) const;
template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<storm::RationalNumber> const& weights) 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 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);
@ -347,7 +352,7 @@ namespace storm {
template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::BitVector const& filter) const;
template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix) const;
template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<storm::RationalFunction> const& weights) 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 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);
@ -356,7 +361,7 @@ namespace storm {
template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::BitVector const& filter) const;
template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix) const;
template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<double> const& weights) 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 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);

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

@ -198,11 +198,13 @@ namespace storm {
* transition-based rewards in the reward model.
*
* @param transitionMatrix The matrix that is used to weight the values of the transition reward matrix.
* @param weights A vector used for scaling the entries of the state-action rewards (if present).
* @param weights A vector used for scaling the entries of transition and/or state-action rewards (if present).
* @param scaleTransAndActions If true both transition rewards and state-action rewards are scaled by the
* weights. Otherwise, only the state-action rewards are scaled.
* @return The full state-action reward vector.
*/
template<typename MatrixValueType>
std::vector<ValueType> getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::vector<MatrixValueType> const& weights) const;
std::vector<ValueType> getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::vector<MatrixValueType> const& weights, bool scaleTransAndActions) const;
/*!
* Creates a vector representing the complete reward vector based on the state-, state-action- and

6
src/storm/models/symbolic/StandardRewardModel.cpp
View File

@ -113,7 +113,7 @@ namespace storm {
}
template <storm::dd::DdType Type, typename ValueType>
storm::dd::Add<Type, ValueType> StandardRewardModel<Type, ValueType>::getTotalRewardVector(storm::dd::Add<Type, ValueType> const& transitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, storm::dd::Add<Type, ValueType> const& weights) const {
storm::dd::Add<Type, ValueType> StandardRewardModel<Type, ValueType>::getTotalRewardVector(storm::dd::Add<Type, ValueType> const& transitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, storm::dd::Add<Type, ValueType> const& weights, bool scaleTransAndActions) const {
storm::dd::Add<Type, ValueType> result = transitionMatrix.getDdManager().template getAddZero<ValueType>();
if (this->hasStateRewards()) {
result += optionalStateRewardVector.get();
@ -122,8 +122,12 @@ namespace storm {
result += optionalStateActionRewardVector.get() * weights;
}
if (this->hasTransitionRewards()) {
if (scaleTransAndActions) {
result += weights * (transitionMatrix * this->getTransitionRewardMatrix()).sumAbstract(columnVariables);
} else {
result += (transitionMatrix * this->getTransitionRewardMatrix()).sumAbstract(columnVariables);
}
}
return result;
}

6
src/storm/models/symbolic/StandardRewardModel.h
View File

@ -167,10 +167,12 @@ namespace storm {
*
* @param transitionMatrix The matrix that is used to weight the values of the transition reward matrix.
* @param columnVariables The column variables of the model.
* @param weights The weights used to scale the state-action reward vector.
* @param weights The weights used to scale the transition rewards and/or state-action rewards.
* @param scaleTransAndActions If true both transition rewards and state-action rewards are scaled by the
* weights. Otherwise, only the state-action rewards are scaled.
* @return The full state-action reward vector.
*/
storm::dd::Add<Type, ValueType> getTotalRewardVector(storm::dd::Add<Type, ValueType> const& transitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, storm::dd::Add<Type, ValueType> const& weights) const;
storm::dd::Add<Type, ValueType> getTotalRewardVector(storm::dd::Add<Type, ValueType> const& transitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, storm::dd::Add<Type, ValueType> const& weights, bool scaleTransAndActions) const;
/*!
* Multiplies all components of the reward model with the given DD.

47
src/storm/parser/FormulaParserGrammar.cpp
View File

@ -17,6 +17,7 @@ namespace storm {
for (auto variableTypePair : *constManager) {
identifiers_.add(variableTypePair.first.getName(), variableTypePair.first);
}
// Set the identifier mapping to actually generate expressions.
expressionParser.setIdentifierMapping(&identifiers_);
@ -126,32 +127,30 @@ namespace storm {
start.name("start");
// Enable the following lines to print debug output for most the rules.
/*
debug(start);
debug(constantDefinition);
debug(stateFormula);
debug(orStateFormula);
debug(andStateFormula);
debug(probabilityOperator);
debug(rewardOperator);
debug(longRunAverageOperator);
debug(timeOperator);
debug(pathFormulaWithoutUntil);
debug(pathFormula);
// debug(start);
// debug(constantDefinition);
// debug(stateFormula);
// debug(orStateFormula);
// debug(andStateFormula);
// debug(probabilityOperator);
// debug(rewardOperator);
// debug(longRunAverageOperator);
// debug(timeOperator);
// debug(pathFormulaWithoutUntil);
// debug(pathFormula);
// debug(conditionalFormula);
debug(nextFormula);
debug(globallyFormula);
// debug(nextFormula);
// debug(globallyFormula);
// debug(eventuallyFormula);
debug(atomicStateFormula);
debug(booleanLiteralFormula);
debug(labelFormula);
debug(expressionFormula);
debug(rewardPathFormula);
debug(cumulativeRewardFormula);
debug(totalRewardFormula);
debug(instantaneousRewardFormula);
debug(multiObjectiveFormula);
*/
// debug(atomicStateFormula);
// debug(booleanLiteralFormula);
// debug(labelFormula);
// debug(expressionFormula);
// debug(rewardPathFormula);
// debug(cumulativeRewardFormula);
// debug(totalRewardFormula);
// debug(instantaneousRewardFormula);
// debug(multiObjectiveFormula);
// Enable error reporting.
qi::on_error<qi::fail>(start, handler(qi::_1, qi::_2, qi::_3, qi::_4));

Write Preview
Loading…
Cancel
Save