diff --git a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp index 281d8ffa6..0f6fb9a4b 100644 --- a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp @@ -224,7 +224,7 @@ namespace storm { STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); // Create ODD for the translation. - storm::dd::Odd odd =model.getReachableStates().createOdd(); + storm::dd::Odd odd = model.getReachableStates().createOdd(); // Initialize result to state rewards of the model. std::vector result = rewardModel.getStateRewardVector().toVector(odd); @@ -267,7 +267,7 @@ namespace storm { storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); // Then compute the state reward vector to use in the computation. - storm::dd::Add totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, model.getColumnVariables(), exitRateVector); + storm::dd::Add totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, model.getColumnVariables(), exitRateVector, false); std::vector explicitTotalRewardVector = totalRewardVector.toVector(odd); // Finally, compute the transient probabilities. @@ -292,6 +292,8 @@ namespace storm { template std::unique_ptr HybridCtmcCslHelper::computeLongRunAverageRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + + STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); storm::dd::Add probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); // Create ODD for the translation. @@ -300,7 +302,7 @@ namespace storm { storm::storage::SparseMatrix explicitProbabilityMatrix = probabilityMatrix.toMatrix(odd, odd); std::vector explicitExitRateVector = exitRateVector.toVector(odd); - std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards(explicitProbabilityMatrix, rewardModel.getStateRewardVector().toVector(odd), &explicitExitRateVector, linearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards(explicitProbabilityMatrix, rewardModel.getTotalRewardVector(probabilityMatrix, model.getColumnVariables(), exitRateVector, true).toVector(odd), &explicitExitRateVector, linearEquationSolverFactory); return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); } diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 899c642db..15cbe2c64 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -262,7 +262,7 @@ namespace storm { storm::storage::SparseMatrix uniformizedMatrix = computeUniformizedMatrix(rateMatrix, storm::storage::BitVector(numberOfStates, true), uniformizationRate, exitRateVector); // Compute the total state reward vector. - std::vector totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, exitRateVector); + std::vector totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, exitRateVector, false); // Finally, compute the transient probabilities. return computeTransientProbabilities(uniformizedMatrix, nullptr, timeBound, uniformizationRate, totalRewardVector, linearEquationSolverFactory); @@ -360,14 +360,9 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix const& probabilityMatrix, RewardModelType const& rewardModel, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory 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(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 @@ -490,7 +485,7 @@ namespace storm { storm::storage::StronglyConnectedComponent const& bscc = bsccDecomposition[bsccIndex]; for (auto const& state : bscc) { - bsccEquationSystemSolution[indexInStatesInBsccs[state]] = one / bscc.size(); + bsccEquationSystemSolution[indexInStatesInBsccs[state]] = one / bscc.size(); } } @@ -501,6 +496,12 @@ namespace storm { solver->solveEquations(bsccEquationSystemSolution, bsccEquationSystemRightSide); } +// std::vector tmp(probabilityMatrix.getRowCount(), storm::utility::zero()); +// 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 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]; diff --git a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp index 5cc94ae35..8870456cd 100644 --- a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp @@ -264,7 +264,7 @@ namespace storm { storm::dd::Odd odd = model.getReachableStates().createOdd(); storm::storage::SparseMatrix explicitProbabilityMatrix = model.getTransitionMatrix().toMatrix(odd, odd); - std::vector result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeLongRunAverageRewards(explicitProbabilityMatrix, rewardModel.getStateRewardVector().toVector(odd), linearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeLongRunAverageRewards(explicitProbabilityMatrix, rewardModel.getTotalRewardVector(model.getTransitionMatrix(), model.getColumnVariables()).toVector(odd), linearEquationSolverFactory); return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); } diff --git a/src/storm/models/sparse/StandardRewardModel.cpp b/src/storm/models/sparse/StandardRewardModel.cpp index 8b7e8c349..1866be5d2 100644 --- a/src/storm/models/sparse/StandardRewardModel.cpp +++ b/src/storm/models/sparse/StandardRewardModel.cpp @@ -165,6 +165,11 @@ namespace storm { template template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const { + if (this->hasStateActionRewards()) { + for (auto const& e : this->getStateActionRewardVector()) { + std::cout << "e " << e << std::endl; + } + } std::vector result = this->hasTransitionRewards() ? transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()) : (this->hasStateActionRewards() ? this->getStateActionRewardVector() : std::vector(transitionMatrix.getRowCount())); if (this->hasStateActionRewards() && this->hasTransitionRewards()) { storm::utility::vector::addVectors(result, this->getStateActionRewardVector(), result); @@ -177,16 +182,16 @@ namespace storm { template template - std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const { - std::vector result = this->hasTransitionRewards() ? transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()) : (this->hasStateActionRewards() ? this->getStateActionRewardVector() : std::vector(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); - } - 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(weights, this->getStateActionRewardVector(), result, [] (MatrixValueType const& weight, ValueType const& rewardElement, ValueType const& resultElement) { return resultElement + weight * rewardElement; } ); + std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const { + std::vector result; + if (this->hasTransitionRewards()) { + result = transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()); + storm::utility::vector::applyPointwise(weights, this->getStateActionRewardVector(), result, [] (MatrixValueType const& weight, ValueType const& rewardElement, ValueType const& resultElement) { return weight * (resultElement + rewardElement); } ); + } else { + result = std::vector(transitionMatrix.getRowCount()); + if (this->hasStateActionRewards()) { + storm::utility::vector::applyPointwise(weights, this->getStateActionRewardVector(), result, [] (MatrixValueType const& weight, ValueType const& rewardElement, ValueType const& resultElement) { return 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 StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; - template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; + template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, double const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, double const & newValue); @@ -328,7 +333,7 @@ namespace storm { template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; - template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; + template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, float const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, float const & newValue); @@ -338,7 +343,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; - template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; + template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalNumber const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, storm::RationalNumber const & newValue); @@ -347,7 +352,7 @@ namespace storm { template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; - template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; + template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalFunction const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, storm::RationalFunction const & newValue); @@ -356,7 +361,7 @@ namespace storm { template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; - template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; + template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, double const & newValue); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::Interval const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, double const & newValue); diff --git a/src/storm/models/sparse/StandardRewardModel.h b/src/storm/models/sparse/StandardRewardModel.h index 8fcfa48ef..85d6b5382 100644 --- a/src/storm/models/sparse/StandardRewardModel.h +++ b/src/storm/models/sparse/StandardRewardModel.h @@ -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 - std::vector getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; + std::vector getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; /*! * Creates a vector representing the complete reward vector based on the state-, state-action- and diff --git a/src/storm/models/symbolic/StandardRewardModel.cpp b/src/storm/models/symbolic/StandardRewardModel.cpp index e42fc4b70..0a3e37e79 100644 --- a/src/storm/models/symbolic/StandardRewardModel.cpp +++ b/src/storm/models/symbolic/StandardRewardModel.cpp @@ -113,7 +113,7 @@ namespace storm { } template - storm::dd::Add StandardRewardModel::getTotalRewardVector(storm::dd::Add const& transitionMatrix, std::set const& columnVariables, storm::dd::Add const& weights) const { + storm::dd::Add StandardRewardModel::getTotalRewardVector(storm::dd::Add const& transitionMatrix, std::set const& columnVariables, storm::dd::Add const& weights, bool scaleTransAndActions) const { storm::dd::Add result = transitionMatrix.getDdManager().template getAddZero(); if (this->hasStateRewards()) { result += optionalStateRewardVector.get(); @@ -122,7 +122,11 @@ namespace storm { result += optionalStateActionRewardVector.get() * weights; } if (this->hasTransitionRewards()) { - result += (transitionMatrix * this->getTransitionRewardMatrix()).sumAbstract(columnVariables); + if (scaleTransAndActions) { + result += weights * (transitionMatrix * this->getTransitionRewardMatrix()).sumAbstract(columnVariables); + } else { + result += (transitionMatrix * this->getTransitionRewardMatrix()).sumAbstract(columnVariables); + } } return result; } diff --git a/src/storm/models/symbolic/StandardRewardModel.h b/src/storm/models/symbolic/StandardRewardModel.h index d44a96868..a4e9fb573 100644 --- a/src/storm/models/symbolic/StandardRewardModel.h +++ b/src/storm/models/symbolic/StandardRewardModel.h @@ -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 getTotalRewardVector(storm::dd::Add const& transitionMatrix, std::set const& columnVariables, storm::dd::Add const& weights) const; + storm::dd::Add getTotalRewardVector(storm::dd::Add const& transitionMatrix, std::set const& columnVariables, storm::dd::Add const& weights, bool scaleTransAndActions) const; /*! * Multiplies all components of the reward model with the given DD. diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index 450d68fc8..86b34f19f 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -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(conditionalFormula); - 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(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(eventuallyFormula); +// debug(atomicStateFormula); +// debug(booleanLiteralFormula); +// debug(labelFormula); +// debug(expressionFormula); +// debug(rewardPathFormula); +// debug(cumulativeRewardFormula); +// debug(totalRewardFormula); +// debug(instantaneousRewardFormula); +// debug(multiObjectiveFormula); // Enable error reporting. qi::on_error(start, handler(qi::_1, qi::_2, qi::_3, qi::_4));