From 86506e2b2500c365c6c4fde82ac5d87c621a7be8 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 3 Dec 2019 13:55:58 +0100 Subject: [PATCH] Added LRA distribution equation system for computing the LRA of a BSCC. Fixes in the gain/bias characterization. --- .../csl/helper/SparseCtmcCslHelper.cpp | 252 +++++++++++++----- .../csl/helper/SparseCtmcCslHelper.h | 8 +- 2 files changed, 189 insertions(+), 71 deletions(-) diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 4d381e885..528182ea5 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -451,15 +451,23 @@ namespace storm { std::vector bsccLra; bsccLra.reserve(bsccDecomposition.size()); + auto underlyingSolverEnvironment = env; + auto precision = env.solver().lra().getPrecision(); + if (env.solver().isForceSoundness()) { + // For sound computations, the error in the MECS plus the error in the remaining system should be less then the user defined precision. + precision /= storm::utility::convertNumber(2); + underlyingSolverEnvironment.solver().lra().setPrecision(precision); + } + underlyingSolverEnvironment.solver().setLinearEquationSolverPrecision(precision, env.solver().lra().getRelativeTerminationCriterion()); + // Keep track of the maximal and minimal value occuring in one of the BSCCs ValueType maxValue, minValue; storm::storage::BitVector statesInBsccs(numberOfStates); - auto backwardTransitions = rateMatrix.transpose(); for (auto const& bscc : bsccDecomposition) { for (auto const& state : bscc) { statesInBsccs.set(state); } - bsccLra.push_back(computeLongRunAveragesForBscc(env, bscc, rateMatrix, backwardTransitions, valueGetter, exitRateVector)); + bsccLra.push_back(computeLongRunAveragesForBscc(underlyingSolverEnvironment, bscc, rateMatrix, valueGetter, exitRateVector)); if (bsccLra.size() == 1) { maxValue = bsccLra.back(); minValue = bsccLra.back(); @@ -505,7 +513,7 @@ namespace storm { // Compute reachability rewards storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; - bool isEqSysFormat = linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; + bool isEqSysFormat = linearEquationSolverFactory.getEquationProblemFormat(underlyingSolverEnvironment) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; storm::storage::SparseMatrix rewardEquationSystemMatrix = rateMatrix.getSubmatrix(false, statesNotInBsccs, statesNotInBsccs, isEqSysFormat); if (exitRateVector) { uint64_t localRow = 0; @@ -520,14 +528,12 @@ namespace storm { rewardEquationSystemMatrix.convertToEquationSystem(); } rewardSolution = std::vector(rewardEquationSystemMatrix.getColumnCount(), (maxValue + minValue) / storm::utility::convertNumber(2)); - // std::cout << rewardEquationSystemMatrix << std::endl; - // std::cout << storm::utility::vector::toString(rewardRightSide) << std::endl; - std::unique_ptr> solver = linearEquationSolverFactory.create(env, std::move(rewardEquationSystemMatrix)); + std::unique_ptr> solver = linearEquationSolverFactory.create(underlyingSolverEnvironment, std::move(rewardEquationSystemMatrix)); solver->setBounds(minValue, maxValue); // Check solver requirements - auto requirements = solver->getRequirements(env); + auto requirements = solver->getRequirements(underlyingSolverEnvironment); STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); - solver->solveEquations(env, rewardSolution, rewardRightSide); + solver->solveEquations(underlyingSolverEnvironment, rewardSolution, rewardRightSide); } // Fill the result vector. @@ -553,13 +559,7 @@ namespace storm { } template - ValueType SparseCtmcCslHelper::computeLongRunAveragesForBscc(Environment const& env, storm::storage::StronglyConnectedComponent const& bscc, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function const& valueGetter, std::vector const* exitRateVector) { - std::cout << std::endl << "========== BSCC =======" << std::endl; - storm::storage::BitVector bsccStates(rateMatrix.getRowCount()); - for (auto const& s : bscc) { bsccStates.set(s); std::cout << s << ": " << valueGetter(s) << "\t";} - auto subm = rateMatrix.getSubmatrix(false,bsccStates,bsccStates); - std::cout << std::endl << subm << std::endl; - + ValueType SparseCtmcCslHelper::computeLongRunAveragesForBscc(Environment const& env, storm::storage::StronglyConnectedComponent const& bscc, storm::storage::SparseMatrix const& rateMatrix, std::function const& valueGetter, std::vector const* exitRateVector) { // Catch the case where all values are the same (this includes the special case where the bscc is of size 1) auto it = bscc.begin(); @@ -571,28 +571,28 @@ namespace storm { } if (it == bscc.end()) { // All entries have the same LRA - std::cout << std::endl << "==== TRIVIAL: RESULT=" << val << "=======" << std::endl; return val; } - std::cout << std::endl << "========== SOLVING =======" << std::endl; storm::solver::LraMethod method = env.solver().lra().getDetLraMethod(); if (method == storm::solver::LraMethod::ValueIteration) { - return computeLongRunAveragesForBsccVi(env, bscc, rateMatrix, backwardTransitions, valueGetter, exitRateVector); + return computeLongRunAveragesForBsccVi(env, bscc, rateMatrix, valueGetter, exitRateVector); } else if (method == storm::solver::LraMethod::LraDistributionEquations) { - //return computeLongRunAveragesForBsccLraDistrEqSys(env, bscc, rateMatrix, backwardTransitions, valueGetter, exitRateVector); + // We only need the first element of the pair as the lra distribution is not relevant at this point. + return computeLongRunAveragesForBsccLraDistr(env, bscc, rateMatrix, valueGetter, exitRateVector).first; } STORM_LOG_WARN_COND(method == storm::solver::LraMethod::GainBiasEquations, "Unsupported lra method selected. Defaulting to gain-bias-equations."); - return computeLongRunAveragesForBsccEqSys(env, bscc, rateMatrix, backwardTransitions, valueGetter, exitRateVector); + // We don't need the bias values + return computeLongRunAveragesForBsccGainBias(env, bscc, rateMatrix, valueGetter, exitRateVector).first; } template <> - storm::RationalFunction SparseCtmcCslHelper::computeLongRunAveragesForBsccVi(Environment const&, storm::storage::StronglyConnectedComponent const&, storm::storage::SparseMatrix const&, storm::storage::SparseMatrix const&, std::function const&, std::vector const*) { + storm::RationalFunction SparseCtmcCslHelper::computeLongRunAveragesForBsccVi(Environment const&, storm::storage::StronglyConnectedComponent const&, storm::storage::SparseMatrix const&, std::function const&, std::vector const*) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The requested Method for LRA computation is not supported for parametric models."); } template - ValueType SparseCtmcCslHelper::computeLongRunAveragesForBsccVi(Environment const& env, storm::storage::StronglyConnectedComponent const& bscc, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function const& valueGetter, std::vector const* exitRateVector) { + ValueType SparseCtmcCslHelper::computeLongRunAveragesForBsccVi(Environment const& env, storm::storage::StronglyConnectedComponent const& bscc, storm::storage::SparseMatrix const& rateMatrix, std::function const& valueGetter, std::vector const* exitRateVector) { // Initialize data about the bscc storm::storage::BitVector bsccStates(rateMatrix.getRowGroupCount(), false); @@ -678,24 +678,24 @@ namespace storm { if ((maxDiff - minDiff) <= (relative ? (precision * minDiff) : precision)) { break; } - + } + if (maxIter.is_initialized() && iter == maxIter.get()) { + STORM_LOG_WARN("LRA computation did not converge within " << iter << " iterations."); + } else { + STORM_LOG_TRACE("LRA computation converged after " << iter << " iterations."); } return (maxDiff + minDiff) * uniformizationRate / (storm::utility::convertNumber(2.0)); } - template <> - storm::RationalFunction SparseCtmcCslHelper::computeLongRunAveragesForBsccEqSys(Environment const&, storm::storage::StronglyConnectedComponent const&, storm::storage::SparseMatrix const&, storm::storage::SparseMatrix const&, std::function const&, std::vector const*) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The requested Method for LRA computation is not supported for parametric models."); - // This is not possible due to uniformization - } - template - ValueType SparseCtmcCslHelper::computeLongRunAveragesForBsccEqSys(Environment const& env, storm::storage::StronglyConnectedComponent const& bscc, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function const& valueGetter, std::vector const* exitRateVector) { + std::pair> SparseCtmcCslHelper::computeLongRunAveragesForBsccGainBias(Environment const& env, storm::storage::StronglyConnectedComponent const& bscc, storm::storage::SparseMatrix const& rateMatrix, std::function const& valueGetter, std::vector const* exitRateVector) { // We build the equation system as in Line 3 of Algorithm 3 from // Kretinsky, Meggendorfer: Efficient Strategy Iteration for Mean Payoff in Markov Decision Processes (ATVA 2017) // The first variable corresponds to the gain of the bscc whereas the subsequent variables yield the bias for each state s_1, s_2, .... // No bias variable for s_0 is needed since it is always set to zero, yielding an nxn equation system matrix - // To properly deal with CMTC, we also need to uniformize the transitions. + // To make this work for CTMC, we could uniformize the model. This preserves LRA and ensures that we can compute the + // LRA as for a DTMC (the soujourn time in each state is the same). If we then multiply the equations with the uniformization rate, + // the uniformization rate cancels out. Hence, we obtain the equation system below. // Get a mapping from global state indices to local ones. std::unordered_map toLocalIndexMap; @@ -705,12 +705,6 @@ namespace storm { ++localIndex; } - // Get the uniformization rate - ValueType uniformizationRate = storm::utility::one(); - if (exitRateVector) { - uniformizationRate = *std::max_element(exitRateVector->begin(), exitRateVector->end()); - } - // Build the equation system matrix and vector. storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; bool isEquationSystemFormat = linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; @@ -730,14 +724,10 @@ namespace storm { builder.addNextValue(row, 0, -storm::utility::one()); } // Compute weighted sum over successor state. As this is a BSCC, each successor state will again be in the BSCC. - bool needDiagonalEntry = ((exitRateVector && (*exitRateVector)[globalState] != uniformizationRate) || isEquationSystemFormat) && (row > 0); + bool needDiagonalEntry = isEquationSystemFormat && (row > 0); ValueType diagonalValue; if (needDiagonalEntry) { - if (isEquationSystemFormat) { - diagonalValue = (*exitRateVector)[globalState] / uniformizationRate; // 1 - (1 - r(s)/unifrate) - } else { - diagonalValue = storm::utility::one() - (*exitRateVector)[globalState] / uniformizationRate; - } + diagonalValue = exitRateVector ? (*exitRateVector)[globalState] : storm::utility::one(); } for (auto const& entry : rateMatrix.getRow(globalState)) { uint64_t col = toLocalIndexMap[entry.getColumn()]; @@ -746,9 +736,6 @@ namespace storm { continue; } entryValue = entry.getValue(); - if (exitRateVector) { - // entryValue /= uniformizationRate; - } if (isEquationSystemFormat) { entryValue = -entryValue; } @@ -765,31 +752,160 @@ namespace storm { if (needDiagonalEntry) { builder.addNextValue(row, row, diagonalValue); } - if (exitRateVector) { - eqsysVector.push_back(valueGetter(globalState) / uniformizationRate); - } else { - eqsysVector.push_back(valueGetter(globalState)); - } + eqsysVector.push_back(valueGetter(globalState)); ++row; } // Create a linear equation solver - auto matrix = builder.build(); - std::cout << matrix << std::endl; - std::cout << "RHS: " << storm::utility::vector::toString(eqsysVector) << std::endl; - auto solver = linearEquationSolverFactory.create(env, std::move(matrix)); + auto subEnv = env; + subEnv.solver().setLinearEquationSolverPrecision(env.solver().lra().getPrecision(), env.solver().lra().getRelativeTerminationCriterion()); + auto solver = linearEquationSolverFactory.create(subEnv, builder.build()); // Check solver requirements. - auto requirements = solver->getRequirements(env); + auto requirements = solver->getRequirements(subEnv); STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); // Todo: Find bounds on the bias variable. Just inserting the maximal value from the vector probably does not work. std::vector eqSysSol(bscc.size(), storm::utility::zero()); // Take the mean of the rewards as an initial guess for the gain eqSysSol.front() = std::accumulate(eqsysVector.begin(), eqsysVector.end(), storm::utility::zero()) / storm::utility::convertNumber(bscc.size()); - solver->solveEquations(env, eqSysSol, eqsysVector); + solver->solveEquations(subEnv, eqSysSol, eqsysVector); + + ValueType gain = eqSysSol.front(); + // insert bias value for state 0 + eqSysSol.front() = storm::utility::zero(); + // Return the gain and the bias values + return std::pair>(std::move(gain), std::move(eqSysSol)); + } + + template + std::pair> SparseCtmcCslHelper::computeLongRunAveragesForBsccLraDistr(Environment const& env, storm::storage::StronglyConnectedComponent const& bscc, storm::storage::SparseMatrix const& rateMatrix, std::function const& valueGetter, std::vector const* exitRateVector) { + + // Let A be ab auxiliary Matrix with A[s,s] = R(s,s) - r(s) & A[s,s'] = R(s,s') for s,s' in BSCC and s!=s'. + // We build and solve the equation system for + // x*A=0 & x_0+...+x_n=1 <=> A^t*x=0=x-x & x_0+...+x_n=1 <=> (1+A^t)*x = x & 1-x_0-...-x_n-1=x_n + // Then, x[i] will be the fraction of the time we are in state i. + + // This method assumes that this BSCC consist of more than one state + if (bscc.size() == 1) { + return { storm::utility::one(), {storm::utility::one()} }; + } - std::cout << std::endl << "========== Result = " << eqSysSol.front() << "*" << uniformizationRate << " =======" << std::endl; - return eqSysSol.front();// * uniformizationRate; + // Get a mapping from global state indices to local ones as well as a bitvector containing states within the BSCC. + std::unordered_map toLocalIndexMap; + storm::storage::BitVector bsccStates(rateMatrix.getRowCount(), false); + uint64_t localIndex = 0; + for (auto const& globalIndex : bscc) { + bsccStates.set(globalIndex, true); + toLocalIndexMap[globalIndex] = localIndex; + ++localIndex; + } + + // Build the auxiliary Matrix A. + auto auxMatrix = rateMatrix.getSubmatrix(false, bsccStates, bsccStates, true); // add diagonal entries! + uint64_t row = 0; + for (auto const& globalIndex : bscc) { + for (auto& entry : auxMatrix.getRow(row)) { + if (entry.getColumn() == row) { + // This value is non-zero since we have a BSCC with more than one state + if (exitRateVector) { + entry.setValue(entry.getValue() - (*exitRateVector)[globalIndex]); + } else { + entry.setValue(entry.getValue() - storm::utility::one()); + } + } + } + ++row; + } + assert(row == auxMatrix.getRowCount()); + + // We need to consider A^t. This will not delete diagonal entries since they are non-zero. + auxMatrix = auxMatrix.transpose(); + + // Check whether we need the fixpoint characterization + storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; + bool isFixpointFormat = linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::FixedPointSystem; + + if (isFixpointFormat) { + // Add a 1 on the diagonal + for (row = 0; row < auxMatrix.getRowCount(); ++row) { + for (auto& entry : auxMatrix) { + if (entry.getColumn() == row) { + entry.setValue(storm::utility::one() + entry.getValue()); + } + } + } + } + + // We now build the equation system matrix. + // We can drop the last row of A and add ones in this row instead to assert that the variables sum up to one + // Phase 1: replace the existing entries of the last row with ones + uint64_t col = 0; + uint64_t lastRow = auxMatrix.getRowCount() - 1; + for (auto& entry : auxMatrix.getRow(lastRow)) { + entry.setColumn(col); + if (isFixpointFormat) { + if (col == lastRow) { + entry.setValue(storm::utility::zero()); + } else { + entry.setValue(-storm::utility::one()); + } + } else { + entry.setValue(storm::utility::one()); + } + ++col; + } + storm::storage::SparseMatrixBuilder builder(std::move(auxMatrix)); + for (; col <= lastRow; ++col) { + if (isFixpointFormat) { + if (col != lastRow) { + builder.addNextValue(lastRow, col, -storm::utility::one()); + } + } else { + builder.addNextValue(lastRow, col, storm::utility::one()); + } + } + + std::vector bsccEquationSystemRightSide(bscc.size(), storm::utility::zero()); + bsccEquationSystemRightSide.back() = storm::utility::one(); + + // Create a linear equation solver + auto subEnv = env; + subEnv.solver().setLinearEquationSolverPrecision(env.solver().lra().getPrecision(), env.solver().lra().getRelativeTerminationCriterion()); + auto solver = linearEquationSolverFactory.create(subEnv, builder.build()); + solver->setBounds(storm::utility::zero(), storm::utility::one()); + // Check solver requirements. + auto requirements = solver->getRequirements(subEnv); + STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); + + std::vector lraDistr(bscc.size(), storm::utility::one() / storm::utility::convertNumber(bscc.size())); + solver->solveEquations(subEnv, lraDistr, bsccEquationSystemRightSide); + // If exit rates were given, we need to 'fix' the results to also account for the timing behaviour. + if (false && exitRateVector != nullptr) { + ValueType totalValue = storm::utility::zero(); + auto solIt = lraDistr.begin(); + for (auto const& globalState : bscc) { + totalValue += (*solIt) * (storm::utility::one() / (*exitRateVector)[globalState]); + ++solIt; + } + assert(solIt == lraDistr.end()); + solIt = lraDistr.begin(); + for (auto const& globalState : bscc) { + *solIt = ((*solIt) * (storm::utility::one() / (*exitRateVector)[globalState])) / totalValue; + ++solIt; + } + assert(solIt == lraDistr.end()); + } + + // Calculate final LRA Value + ValueType result = storm::utility::zero(); + auto solIt = lraDistr.begin(); + for (auto const& globalState : bscc) { + result += valueGetter(globalState) * (*solIt); + ++solIt; + } + assert(solIt == lraDistr.end()); + + return std::pair>(std::move(result), std::move(lraDistr)); } template ::SupportsExponential, int>::type> @@ -1012,9 +1128,9 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeTotalRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, bool qualitative); - template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector); - template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const* exitRateVector); - template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& stateRewardVector, std::vector const* exitRateVector); + template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector); + template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const* exitRateVector); + template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& stateRewardVector, std::vector const* exitRateVector); template std::vector SparseCtmcCslHelper::computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound); @@ -1049,14 +1165,14 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeTotalRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, bool qualitative); template std::vector SparseCtmcCslHelper::computeTotalRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, bool qualitative); - template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector); - template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector); + template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector); + template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector); - template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const* exitRateVector); - template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const* exitRateVector); + template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const* exitRateVector); + template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const* exitRateVector); - template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& stateRewardVector, std::vector const* exitRateVector); - template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& stateRewardVector, std::vector const* exitRateVector); + template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& stateRewardVector, std::vector const* exitRateVector); + template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& stateRewardVector, std::vector const* exitRateVector); template std::vector SparseCtmcCslHelper::computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound); template std::vector SparseCtmcCslHelper::computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound); diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h index 8a45ea75f..95840ae19 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h @@ -125,11 +125,13 @@ namespace storm { template static std::vector computeLongRunAverages(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::function const& valueGetter, std::vector const* exitRateVector); template - static ValueType computeLongRunAveragesForBscc(Environment const& env, storm::storage::StronglyConnectedComponent const& bscc, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function const& valueGetter, std::vector const* exitRateVector); + static ValueType computeLongRunAveragesForBscc(Environment const& env, storm::storage::StronglyConnectedComponent const& bscc, storm::storage::SparseMatrix const& rateMatrix, std::function const& valueGetter, std::vector const* exitRateVector); template - static ValueType computeLongRunAveragesForBsccVi(Environment const& env, storm::storage::StronglyConnectedComponent const& bscc, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function const& valueGetter, std::vector const* exitRateVector); + static ValueType computeLongRunAveragesForBsccVi(Environment const& env, storm::storage::StronglyConnectedComponent const& bscc, storm::storage::SparseMatrix const& rateMatrix, std::function const& valueGetter, std::vector const* exitRateVector); template - static ValueType computeLongRunAveragesForBsccEqSys(Environment const& env, storm::storage::StronglyConnectedComponent const& bscc, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function const& valueGetter, std::vector const* exitRateVector); + static std::pair> computeLongRunAveragesForBsccGainBias(Environment const& env, storm::storage::StronglyConnectedComponent const& bscc, storm::storage::SparseMatrix const& rateMatrix, std::function const& valueGetter, std::vector const* exitRateVector); + template + static std::pair> computeLongRunAveragesForBsccLraDistr(Environment const& env, storm::storage::StronglyConnectedComponent const& bscc, storm::storage::SparseMatrix const& rateMatrix, std::function const& valueGetter, std::vector const* exitRateVector); }; }