From 248b257f20136f5cad8001795ab00a53ac6a5252 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 25 Jun 2016 19:43:43 +0200 Subject: [PATCH] enabled rationals/rational functions in CTMC model checker Former-commit-id: dc15cd6020fea361dcbd24f467e3f0ae88e38a55 --- .../csl/SparseCtmcCslModelChecker.cpp | 31 +- .../csl/SparseCtmcCslModelChecker.h | 8 + .../csl/helper/HybridCtmcCslHelper.cpp | 16 +- .../csl/helper/SparseCtmcCslHelper.cpp | 388 ++++++++++-------- .../csl/helper/SparseCtmcCslHelper.h | 37 +- .../prctl/SparseDtmcPrctlModelChecker.cpp | 2 +- .../prctl/helper/SparseDtmcPrctlHelper.cpp | 2 +- 7 files changed, 288 insertions(+), 196 deletions(-) diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 5e29689bf..4d2d8fbea 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -35,10 +35,23 @@ namespace storm { template bool SparseCtmcCslModelChecker::canHandle(CheckTask const& checkTask) const { + return SparseCtmcCslModelChecker::canHandleImplementation(checkTask); + } + + template + template::SupportsExponential, int>::type> + bool SparseCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true)); } + template + template::SupportsExponential, int>::type> + bool SparseCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { + storm::logic::Formula const& formula = checkTask.getFormula(); + return formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true)); + } + template std::unique_ptr SparseCtmcCslModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); @@ -56,7 +69,7 @@ namespace storm { upperBound = pathFormula.getDiscreteTimeBound(); } - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), checkTask.isQualitativeSet(), lowerBound, upperBound, *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), checkTask.isQualitativeSet(), lowerBound, upperBound, *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -65,7 +78,7 @@ namespace storm { storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeNextProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeNextProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -76,21 +89,21 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseCtmcCslModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -100,7 +113,7 @@ namespace storm { std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -110,8 +123,8 @@ namespace storm { std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - storm::storage::SparseMatrix probabilityMatrix = storm::modelchecker::helper::SparseCtmcCslHelper::computeProbabilityMatrix(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(probabilityMatrix, subResult.getTruthValuesVector(), &this->getModel().getExitRateVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); + storm::storage::SparseMatrix probabilityMatrix = storm::modelchecker::helper::SparseCtmcCslHelper::computeProbabilityMatrix(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(probabilityMatrix, subResult.getTruthValuesVector(), &this->getModel().getExitRateVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -121,7 +134,7 @@ namespace storm { std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityTimes(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), this->getModel().getInitialStates(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityTimes(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), this->getModel().getInitialStates(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/modelchecker/csl/SparseCtmcCslModelChecker.h index 070f81ffd..f63aba841 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -7,6 +7,8 @@ #include "src/solver/LinearEquationSolver.h" +#include "src/utility/NumberTraits.h" + namespace storm { namespace modelchecker { @@ -31,6 +33,12 @@ namespace storm { virtual std::unique_ptr computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; private: + template::SupportsExponential, int>::type = 0> + bool canHandleImplementation(CheckTask const& checkTask) const; + + template::SupportsExponential, int>::type = 0> + bool canHandleImplementation(CheckTask const& checkTask) const; + // An object that is used for solving linear equations and performing matrix-vector multiplication. std::unique_ptr> linearEquationSolverFactory; }; diff --git a/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp b/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp index 91581e987..cffe634e7 100644 --- a/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp @@ -87,7 +87,7 @@ namespace storm { // Finally compute the transient probabilities. std::vector values(statesWithProbabilityGreater0NonPsi.getNonZeroCount(), storm::utility::zero()); - std::vector subresult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, &explicitB, upperBound, uniformizationRate, values, linearEquationSolverFactory); + std::vector subresult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, &explicitB, upperBound, uniformizationRate, values, linearEquationSolverFactory); return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), (psiStates || !statesWithProbabilityGreater0) && model.getReachableStates(), @@ -125,7 +125,7 @@ namespace storm { storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); // Compute the transient probabilities. - result = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, result, linearEquationSolverFactory); + result = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, result, linearEquationSolverFactory); return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), !relevantStates && model.getReachableStates(), model.getManager().template getAddZero(), relevantStates, odd, result)); } else { @@ -151,7 +151,7 @@ namespace storm { // Compute the transient probabilities. std::vector values(statesWithProbabilityGreater0NonPsi.getNonZeroCount(), storm::utility::zero()); - std::vector subResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, &explicitB, upperBound - lowerBound, uniformizationRate, values, linearEquationSolverFactory); + std::vector subResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, &explicitB, upperBound - lowerBound, uniformizationRate, values, linearEquationSolverFactory); // Transform the explicit result to a hybrid check result, so we can easily convert it to // a symbolic qualitative format. @@ -186,7 +186,7 @@ namespace storm { uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, relevantStates, uniformizationRate); explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); - newSubresult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, linearEquationSolverFactory); + newSubresult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, linearEquationSolverFactory); return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), !relevantStates && model.getReachableStates(), model.getManager().template getAddZero(), relevantStates, odd, newSubresult)); } else { @@ -206,7 +206,7 @@ namespace storm { storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, statesWithProbabilityGreater0, uniformizationRate); storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); - newSubresult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, linearEquationSolverFactory); + newSubresult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, linearEquationSolverFactory); return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), !statesWithProbabilityGreater0 && model.getReachableStates(), model.getManager().template getAddZero(), statesWithProbabilityGreater0, odd, newSubresult)); } @@ -237,7 +237,7 @@ namespace storm { storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, model.getReachableStates(), uniformizationRate); storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); - result = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, timeBound, uniformizationRate, result, linearEquationSolverFactory); + result = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, timeBound, uniformizationRate, result, linearEquationSolverFactory); } return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), odd, result)); @@ -271,7 +271,7 @@ namespace storm { std::vector explicitTotalRewardVector = totalRewardVector.toVector(odd); // Finally, compute the transient probabilities. - std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::template computeTransientProbabilities(explicitUniformizedMatrix, nullptr, timeBound, uniformizationRate, explicitTotalRewardVector, linearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, timeBound, uniformizationRate, explicitTotalRewardVector, linearEquationSolverFactory); return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); } @@ -285,7 +285,7 @@ namespace storm { storm::storage::SparseMatrix explicitProbabilityMatrix = probabilityMatrix.toMatrix(odd, odd); std::vector explicitExitRateVector = exitRateVector.toVector(odd); - std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(explicitProbabilityMatrix, psiStates.toVector(odd), &explicitExitRateVector, qualitative, linearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(explicitProbabilityMatrix, psiStates.toVector(odd), &explicitExitRateVector, qualitative, 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/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 1dbe8fcde..0f6f7535f 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -19,14 +19,15 @@ #include "src/utility/graph.h" #include "src/utility/numerical.h" +#include "src/exceptions/InvalidOperationException.h" #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidPropertyException.h" namespace storm { namespace modelchecker { namespace helper { - template - std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + template ::SupportsExponential, int>::type> + std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { uint_fast64_t numberOfStates = rateMatrix.getRowCount(); @@ -105,7 +106,7 @@ namespace storm { storm::storage::SparseMatrix uniformizedMatrix = computeUniformizedMatrix(rateMatrix, relevantStates, uniformizationRate, exitRates); // Compute the transient probabilities. - subResult = computeTransientProbabilities(uniformizedMatrix, nullptr, lowerBound, uniformizationRate, subResult, linearEquationSolverFactory); + subResult = computeTransientProbabilities(uniformizedMatrix, nullptr, lowerBound, uniformizationRate, subResult, linearEquationSolverFactory); // Fill in the correct values. storm::utility::vector::setVectorValues(result, ~relevantStates, storm::utility::zero()); @@ -153,7 +154,7 @@ namespace storm { // Finally, we compute the second set of transient probabilities. uniformizedMatrix = computeUniformizedMatrix(rateMatrix, relevantStates, uniformizationRate, exitRates); - newSubresult = computeTransientProbabilities(uniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, linearEquationSolverFactory); + newSubresult = computeTransientProbabilities(uniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, linearEquationSolverFactory); // Fill in the correct values. result = std::vector(numberOfStates, storm::utility::zero()); @@ -176,7 +177,7 @@ namespace storm { // Finally, we compute the second set of transient probabilities. storm::storage::SparseMatrix uniformizedMatrix = computeUniformizedMatrix(rateMatrix, statesWithProbabilityGreater0, uniformizationRate, exitRates); - newSubresult = computeTransientProbabilities(uniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, linearEquationSolverFactory); + newSubresult = computeTransientProbabilities(uniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, linearEquationSolverFactory); // Fill in the correct values. result = std::vector(numberOfStates, storm::utility::zero()); @@ -190,125 +191,23 @@ namespace storm { return result; } + template ::SupportsExponential, int>::type> + std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded until probabilities is unsupported for this value type."); + } + template - std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { return SparseDtmcPrctlHelper::computeUntilProbabilities(computeProbabilityMatrix(rateMatrix, exitRateVector), backwardTransitions, phiStates, psiStates, qualitative, linearEquationSolverFactory); } template - std::vector SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { return SparseDtmcPrctlHelper::computeNextProbabilities(computeProbabilityMatrix(rateMatrix, exitRateVector), nextStates, linearEquationSolverFactory); } - template - storm::storage::SparseMatrix SparseCtmcCslHelper::computeUniformizedMatrix(storm::storage::SparseMatrix const& rateMatrix, storm::storage::BitVector const& maybeStates, ValueType uniformizationRate, std::vector const& exitRates) { - STORM_LOG_DEBUG("Computing uniformized matrix using uniformization rate " << uniformizationRate << "."); - STORM_LOG_DEBUG("Keeping " << maybeStates.getNumberOfSetBits() << " rows."); - - // Create the submatrix that only contains the states with a positive probability (including the - // psi states) and reserve space for elements on the diagonal. - storm::storage::SparseMatrix uniformizedMatrix = rateMatrix.getSubmatrix(false, maybeStates, maybeStates, true); - - // Now we need to perform the actual uniformization. That is, all entries need to be divided by - // the uniformization rate, and the diagonal needs to be set to the negative exit rate of the - // state plus the self-loop rate and then increased by one. - uint_fast64_t currentRow = 0; - for (auto const& state : maybeStates) { - for (auto& element : uniformizedMatrix.getRow(currentRow)) { - if (element.getColumn() == currentRow) { - element.setValue((element.getValue() - exitRates[state]) / uniformizationRate + storm::utility::one()); - } else { - element.setValue(element.getValue() / uniformizationRate); - } - } - ++currentRow; - } - - return uniformizedMatrix; - } - - template - template - std::vector SparseCtmcCslHelper::computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, std::vector const* addVector, ValueType timeBound, ValueType uniformizationRate, std::vector values, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { - - ValueType lambda = timeBound * uniformizationRate; - - // If no time can pass, the current values are the result. - if (storm::utility::isZero(lambda)) { - return values; - } - - // Use Fox-Glynn to get the truncation points and the weights. - std::tuple> foxGlynnResult = storm::utility::numerical::getFoxGlynnCutoff(lambda, 1e-300, 1e+300, storm::settings::getModule().getPrecision() / 8.0); - STORM_LOG_DEBUG("Fox-Glynn cutoff points: left=" << std::get<0>(foxGlynnResult) << ", right=" << std::get<1>(foxGlynnResult)); - - // Scale the weights so they add up to one. - for (auto& element : std::get<3>(foxGlynnResult)) { - element /= std::get<2>(foxGlynnResult); - } - - // If the cumulative reward is to be computed, we need to adjust the weights. - if (computeCumulativeReward) { - ValueType sum = storm::utility::zero(); - - for (auto& element : std::get<3>(foxGlynnResult)) { - sum += element; - element = (1 - sum) / uniformizationRate; - } - } - - STORM_LOG_DEBUG("Starting iterations with " << uniformizedMatrix.getRowCount() << " x " << uniformizedMatrix.getColumnCount() << " matrix."); - - // Initialize result. - std::vector result; - uint_fast64_t startingIteration = std::get<0>(foxGlynnResult); - if (startingIteration == 0) { - result = values; - storm::utility::vector::scaleVectorInPlace(result, std::get<3>(foxGlynnResult)[0]); - ++startingIteration; - } else { - if (computeCumulativeReward) { - result = std::vector(values.size()); - std::function scaleWithUniformizationRate = [&uniformizationRate] (ValueType const& a) -> ValueType { return a / uniformizationRate; }; - storm::utility::vector::applyPointwise(values, result, scaleWithUniformizationRate); - } else { - result = std::vector(values.size()); - } - } - std::vector multiplicationResult(result.size()); - - std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(uniformizedMatrix)); - - if (!computeCumulativeReward && std::get<0>(foxGlynnResult) > 1) { - // Perform the matrix-vector multiplications (without adding). - solver->performMatrixVectorMultiplication(values, addVector, std::get<0>(foxGlynnResult) - 1, &multiplicationResult); - } else if (computeCumulativeReward) { - std::function addAndScale = [&uniformizationRate] (ValueType const& a, ValueType const& b) { return a + b / uniformizationRate; }; - - // For the iterations below the left truncation point, we need to add and scale the result with the uniformization rate. - for (uint_fast64_t index = 1; index < startingIteration; ++index) { - solver->performMatrixVectorMultiplication(values, nullptr, 1, &multiplicationResult); - storm::utility::vector::applyPointwise(result, values, result, addAndScale); - } - } - - // For the indices that fall in between the truncation points, we need to perform the matrix-vector - // multiplication, scale and add the result. - ValueType weight = 0; - std::function addAndScale = [&weight] (ValueType const& a, ValueType const& b) { return a + weight * b; }; - for (uint_fast64_t index = startingIteration; index <= std::get<1>(foxGlynnResult); ++index) { - solver->performMatrixVectorMultiplication(values, addVector, 1, &multiplicationResult); - - weight = std::get<3>(foxGlynnResult)[index - std::get<0>(foxGlynnResult)]; - storm::utility::vector::applyPointwise(result, values, result, addAndScale); - } - - return result; - } - - template - template - std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + template ::SupportsExponential, int>::type> + std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has a state-based reward this->getModel(). STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -327,15 +226,19 @@ namespace storm { STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); storm::storage::SparseMatrix uniformizedMatrix = computeUniformizedMatrix(rateMatrix, storm::storage::BitVector(numberOfStates, true), uniformizationRate, exitRateVector); - result = computeTransientProbabilities(uniformizedMatrix, nullptr, timeBound, uniformizationRate, result, linearEquationSolverFactory); + result = computeTransientProbabilities(uniformizedMatrix, nullptr, timeBound, uniformizationRate, result, linearEquationSolverFactory); } return result; } - template - template - std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + template ::SupportsExponential, int>::type> + std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing instantaneous rewards is unsupported for this value type."); + } + + template ::SupportsExponential, int>::type> + std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has a state-based reward this->getModel(). STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -362,12 +265,36 @@ namespace storm { std::vector totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, exitRateVector); // Finally, compute the transient probabilities. - return computeTransientProbabilities(uniformizedMatrix, nullptr, timeBound, uniformizationRate, totalRewardVector, linearEquationSolverFactory); + return computeTransientProbabilities(uniformizedMatrix, nullptr, timeBound, uniformizationRate, totalRewardVector, linearEquationSolverFactory); + } + + template ::SupportsExponential, int>::type> + std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing cumulative rewards is unsupported for this value type."); } template - template - std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + // Compute expected time on CTMC by reduction to DTMC with rewards. + storm::storage::SparseMatrix probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); + + // Initialize rewards. + std::vector totalRewardVector; + for (size_t i = 0; i < exitRateVector.size(); ++i) { + if (targetStates[i] || storm::utility::isZero(exitRateVector[i])) { + // Set reward for target states or states without outgoing transitions to 0. + totalRewardVector.push_back(storm::utility::zero()); + } else { + // Reward is (1 / exitRate). + totalRewardVector.push_back(storm::utility::one() / exitRateVector[i]); + } + } + + return storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(probabilityMatrix, backwardTransitions, totalRewardVector, targetStates, qualitative, linearEquationSolverFactory); + } + + template ::SupportsExponential, int>::type> + std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); storm::storage::SparseMatrix probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); @@ -397,36 +324,13 @@ namespace storm { return storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(probabilityMatrix, backwardTransitions, totalRewardVector, targetStates, qualitative, linearEquationSolverFactory); } - template - storm::storage::SparseMatrix SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates) { - // Turn the rates into probabilities by scaling each row with the exit rate of the state. - storm::storage::SparseMatrix result(rateMatrix); - for (uint_fast64_t row = 0; row < result.getRowCount(); ++row) { - for (auto& entry : result.getRow(row)) { - entry.setValue(entry.getValue() / exitRates[row]); - } - } - return result; - } - - template - storm::storage::SparseMatrix SparseCtmcCslHelper::computeGeneratorMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates) { - storm::storage::SparseMatrix generatorMatrix(rateMatrix, true); - - // Place the negative exit rate on the diagonal. - for (uint_fast64_t row = 0; row < generatorMatrix.getRowCount(); ++row) { - for (auto& entry : generatorMatrix.getRow(row)) { - if (entry.getColumn() == row) { - entry.setValue(-exitRates[row]); - } - } - } - - return generatorMatrix; + template ::SupportsExponential, int>::type> + std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing reachability rewards is unsupported for this value type."); } template - std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // If there are no goal states, we avoid the computation and directly return zero. uint_fast64_t numberOfStates = probabilityMatrix.getRowCount(); if (psiStates.empty()) { @@ -648,35 +552,181 @@ namespace storm { return result; } + + template ::SupportsExponential, int>::type> + storm::storage::SparseMatrix SparseCtmcCslHelper::computeUniformizedMatrix(storm::storage::SparseMatrix const& rateMatrix, storm::storage::BitVector const& maybeStates, ValueType uniformizationRate, std::vector const& exitRates) { + STORM_LOG_DEBUG("Computing uniformized matrix using uniformization rate " << uniformizationRate << "."); + STORM_LOG_DEBUG("Keeping " << maybeStates.getNumberOfSetBits() << " rows."); + + // Create the submatrix that only contains the states with a positive probability (including the + // psi states) and reserve space for elements on the diagonal. + storm::storage::SparseMatrix uniformizedMatrix = rateMatrix.getSubmatrix(false, maybeStates, maybeStates, true); + + // Now we need to perform the actual uniformization. That is, all entries need to be divided by + // the uniformization rate, and the diagonal needs to be set to the negative exit rate of the + // state plus the self-loop rate and then increased by one. + uint_fast64_t currentRow = 0; + for (auto const& state : maybeStates) { + for (auto& element : uniformizedMatrix.getRow(currentRow)) { + if (element.getColumn() == currentRow) { + element.setValue((element.getValue() - exitRates[state]) / uniformizationRate + storm::utility::one()); + } else { + element.setValue(element.getValue() / uniformizationRate); + } + } + ++currentRow; + } + + return uniformizedMatrix; + } + + template::SupportsExponential, int>::type> + std::vector SparseCtmcCslHelper::computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, std::vector const* addVector, ValueType timeBound, ValueType uniformizationRate, std::vector values, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + + ValueType lambda = timeBound * uniformizationRate; + + // If no time can pass, the current values are the result. + if (storm::utility::isZero(lambda)) { + return values; + } + + // Use Fox-Glynn to get the truncation points and the weights. + std::tuple> foxGlynnResult = storm::utility::numerical::getFoxGlynnCutoff(lambda, 1e-300, 1e+300, storm::settings::getModule().getPrecision() / 8.0); + STORM_LOG_DEBUG("Fox-Glynn cutoff points: left=" << std::get<0>(foxGlynnResult) << ", right=" << std::get<1>(foxGlynnResult)); + + // Scale the weights so they add up to one. + for (auto& element : std::get<3>(foxGlynnResult)) { + element /= std::get<2>(foxGlynnResult); + } + + // If the cumulative reward is to be computed, we need to adjust the weights. + if (useMixedPoissonProbabilities) { + ValueType sum = storm::utility::zero(); + + for (auto& element : std::get<3>(foxGlynnResult)) { + sum += element; + element = (1 - sum) / uniformizationRate; + } + } + + STORM_LOG_DEBUG("Starting iterations with " << uniformizedMatrix.getRowCount() << " x " << uniformizedMatrix.getColumnCount() << " matrix."); + + // Initialize result. + std::vector result; + uint_fast64_t startingIteration = std::get<0>(foxGlynnResult); + if (startingIteration == 0) { + result = values; + storm::utility::vector::scaleVectorInPlace(result, std::get<3>(foxGlynnResult)[0]); + ++startingIteration; + } else { + if (useMixedPoissonProbabilities) { + result = std::vector(values.size()); + std::function scaleWithUniformizationRate = [&uniformizationRate] (ValueType const& a) -> ValueType { return a / uniformizationRate; }; + storm::utility::vector::applyPointwise(values, result, scaleWithUniformizationRate); + } else { + result = std::vector(values.size()); + } + } + std::vector multiplicationResult(result.size()); + + std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(uniformizedMatrix)); + + if (!useMixedPoissonProbabilities && std::get<0>(foxGlynnResult) > 1) { + // Perform the matrix-vector multiplications (without adding). + solver->performMatrixVectorMultiplication(values, addVector, std::get<0>(foxGlynnResult) - 1, &multiplicationResult); + } else if (useMixedPoissonProbabilities) { + std::function addAndScale = [&uniformizationRate] (ValueType const& a, ValueType const& b) { return a + b / uniformizationRate; }; + + // For the iterations below the left truncation point, we need to add and scale the result with the uniformization rate. + for (uint_fast64_t index = 1; index < startingIteration; ++index) { + solver->performMatrixVectorMultiplication(values, nullptr, 1, &multiplicationResult); + storm::utility::vector::applyPointwise(result, values, result, addAndScale); + } + } + + // For the indices that fall in between the truncation points, we need to perform the matrix-vector + // multiplication, scale and add the result. + ValueType weight = 0; + std::function addAndScale = [&weight] (ValueType const& a, ValueType const& b) { return a + weight * b; }; + for (uint_fast64_t index = startingIteration; index <= std::get<1>(foxGlynnResult); ++index) { + solver->performMatrixVectorMultiplication(values, addVector, 1, &multiplicationResult); + + weight = std::get<3>(foxGlynnResult)[index - std::get<0>(foxGlynnResult)]; + storm::utility::vector::applyPointwise(result, values, result, addAndScale); + } + + return result; + } + template - std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { - // Compute expected time on CTMC by reduction to DTMC with rewards. - storm::storage::SparseMatrix probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); + storm::storage::SparseMatrix SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates) { + // Turn the rates into probabilities by scaling each row with the exit rate of the state. + storm::storage::SparseMatrix result(rateMatrix); + for (uint_fast64_t row = 0; row < result.getRowCount(); ++row) { + for (auto& entry : result.getRow(row)) { + entry.setValue(entry.getValue() / exitRates[row]); + } + } + return result; + } + + template + storm::storage::SparseMatrix SparseCtmcCslHelper::computeGeneratorMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates) { + storm::storage::SparseMatrix generatorMatrix(rateMatrix, true); - // Initialize rewards. - std::vector totalRewardVector; - for (size_t i = 0; i < exitRateVector.size(); ++i) { - if (targetStates[i] || storm::utility::isZero(exitRateVector[i])) { - // Set reward for target states or states without outgoing transitions to 0. - totalRewardVector.push_back(storm::utility::zero()); - } else { - // Reward is (1 / exitRate). - totalRewardVector.push_back(storm::utility::one() / exitRateVector[i]); + // Place the negative exit rate on the diagonal. + for (uint_fast64_t row = 0; row < generatorMatrix.getRowCount(); ++row) { + for (auto& entry : generatorMatrix.getRow(row)) { + if (entry.getColumn() == row) { + entry.setValue(-exitRates[row]); + } } } - return storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(probabilityMatrix, backwardTransitions, totalRewardVector, targetStates, qualitative, linearEquationSolverFactory); + return generatorMatrix; } - template class SparseCtmcCslHelper; - template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template storm::storage::SparseMatrix SparseCtmcCslHelper::computeUniformizedMatrix(storm::storage::SparseMatrix const& rateMatrix, storm::storage::BitVector const& maybeStates, double uniformizationRate, std::vector const& exitRates); + + template storm::storage::SparseMatrix SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates); + template storm::storage::SparseMatrix SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates); + template storm::storage::SparseMatrix SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates); - template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, std::vector const* addVector, double timeBound, double uniformizationRate, std::vector values, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); } } } diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.h b/src/modelchecker/csl/helper/SparseCtmcCslHelper.h index 2bbb6a3c8..c5e6d7db8 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.h +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.h @@ -5,29 +5,47 @@ #include "src/solver/LinearEquationSolver.h" +#include "src/utility/NumberTraits.h" + namespace storm { namespace modelchecker { namespace helper { - template class SparseCtmcCslHelper { public: + template ::SupportsExponential, int>::type = 0> static std::vector computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template ::SupportsExponential, int>::type = 0> + static std::vector computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template static std::vector computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template + static std::vector computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template + template ::SupportsExponential, int>::type = 0> static std::vector computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template + template ::SupportsExponential, int>::type = 0> + static std::vector computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template ::SupportsExponential, int>::type = 0> static std::vector computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - - template + + template ::SupportsExponential, int>::type = 0> + static std::vector computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template ::SupportsExponential, int>::type = 0> static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - + + template ::SupportsExponential, int>::type = 0> + static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template static std::vector computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template static std::vector computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); /*! @@ -39,6 +57,7 @@ namespace storm { * @param exitRates The exit rates of all states. * @return The uniformized matrix. */ + template ::SupportsExponential, int>::type = 0> static storm::storage::SparseMatrix computeUniformizedMatrix(storm::storage::SparseMatrix const& rateMatrix, storm::storage::BitVector const& maybeStates, ValueType uniformizationRate, std::vector const& exitRates); /*! @@ -55,7 +74,7 @@ namespace storm { * poisson probabilities are used. * @return The vector of transient probabilities. */ - template + template::SupportsExponential, int>::type = 0> static std::vector computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, std::vector const* addVector, ValueType timeBound, ValueType uniformizationRate, std::vector values, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); /*! @@ -65,6 +84,7 @@ namespace storm { * @param exitRates The exit rate vector. * @return The †ransition matrix of the embedded DTMC. */ + template static storm::storage::SparseMatrix computeProbabilityMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates); /*! @@ -74,6 +94,7 @@ namespace storm { * @param exitRates The exit rate vector. * @return The generator matrix. */ + template static storm::storage::SparseMatrix computeGeneratorMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates); }; } diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 92ec6d2be..bb3a1a701 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -111,7 +111,7 @@ namespace storm { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), nullptr, checkTask.isQualitativeSet(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), nullptr, checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index c46a76af5..391bd994d 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -225,7 +225,7 @@ namespace storm { template std::vector SparseDtmcPrctlHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { - return SparseCtmcCslHelper::computeLongRunAverageProbabilities(transitionMatrix, psiStates, nullptr, qualitative, linearEquationSolverFactory); + return SparseCtmcCslHelper::computeLongRunAverageProbabilities(transitionMatrix, psiStates, nullptr, qualitative, linearEquationSolverFactory); } template