diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 52d49815e..066a1b116 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -145,6 +145,22 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } + template + std::vector SparseCtmcCslModelChecker::computeTransientProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); + std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); + std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();; + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + + STORM_LOG_THROW(pathFormula.getTimeBoundReference().isTimeBound(), storm::exceptions::NotImplementedException, "Currently step-bounded or reward-bounded properties on CTMCs are not supported."); + STORM_LOG_THROW(pathFormula.hasUpperBound(), storm::exceptions::NotImplementedException, "Computation needs upper limit for time bound."); + double upperBound = pathFormula.getNonStrictUpperBound(); + + std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeAllTransientProbabilities(env, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), upperBound); + return result; + } + // Explicitly instantiate the model checker. template class SparseCtmcCslModelChecker>; diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h index 9bf94fe93..9f056f4be 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -34,6 +34,8 @@ namespace storm { virtual std::unique_ptr computeInstantaneousRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + std::vector computeTransientProbabilities(Environment const& env, CheckTask const& checkTask); + private: template::SupportsExponential, int>::type = 0> bool canHandleImplementation(CheckTask const& checkTask) const; diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 7e50785d0..0a6dabcd8 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -597,6 +597,79 @@ namespace storm { return result; } + template ::SupportsExponential, int>::type> + std::vector SparseCtmcCslHelper::computeAllTransientProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, double timeBound) { + + // Compute transient probabilities going from initial state + // Instead of y=Px we now compute y=xP <=> y^T=P^Tx^T via transposition + uint_fast64_t numberOfStates = rateMatrix.getRowCount(); + + // Create the result vector. + std::vector result; + + storm::storage::SparseMatrix transposedMatrix(rateMatrix); + transposedMatrix.makeRowsAbsorbing(psiStates); + std::vector newRates = exitRates; + for (auto const& state : psiStates) { + newRates[state] = storm::utility::one(); + } + + // Identify all maybe states which have a probability greater than 0 to be reached from the initial state. + //storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(transposedMatrix, phiStates, initialStates); + //STORM_LOG_INFO("Found " << statesWithProbabilityGreater0.getNumberOfSetBits() << " states with probability greater 0."); + + //storm::storage::BitVector relevantStates = statesWithProbabilityGreater0 & ~initialStates;//phiStates | psiStates; + storm::storage::BitVector relevantStates(numberOfStates, true); + STORM_LOG_INFO(relevantStates.getNumberOfSetBits() << " relevant states."); + + if (!relevantStates.empty()) { + // Find the maximal rate of all relevant states to take it as the uniformization rate. + ValueType uniformizationRate = 0; + for (auto const& state : relevantStates) { + uniformizationRate = std::max(uniformizationRate, newRates[state]); + } + uniformizationRate *= 1.02; + STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); + + transposedMatrix = transposedMatrix.transpose(); + + // Compute the uniformized matrix. + storm::storage::SparseMatrix uniformizedMatrix = computeUniformizedMatrix(transposedMatrix, relevantStates, uniformizationRate, newRates); + + // Compute the vector that is to be added as a compensation for removing the absorbing states. + /*std::vector b = transposedMatrix.getConstrainedRowSumVector(relevantStates, initialStates); + for (auto& element : b) { + element /= uniformizationRate; + std::cout << element << std::endl; + }*/ + + std::vector values(relevantStates.getNumberOfSetBits(), storm::utility::zero()); + // Set initial states + size_t i = 0; + ValueType initDist = storm::utility::one() / initialStates.getNumberOfSetBits(); + for (auto const& state : relevantStates) { + if (initialStates.get(state)) { + values[i] = initDist; + } + ++i; + } + // Finally compute the transient probabilities. + std::vector subresult = computeTransientProbabilities(env, uniformizedMatrix, nullptr, timeBound, uniformizationRate, values); + + result = std::vector(numberOfStates, storm::utility::zero()); + storm::utility::vector::setVectorValues(result, relevantStates, subresult); + } else { + result = std::vector(numberOfStates, storm::utility::zero()); + } + + return result; + } + + template ::SupportsExponential, int>::type> + std::vector SparseCtmcCslHelper::computeAllTransientProbabilities(Environment const&, storm::storage::SparseMatrix const&, storm::storage::SparseMatrix const&, storm::storage::BitVector const&, storm::storage::BitVector const&, storm::storage::BitVector const&, std::vector const&, double) { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded until probabilities is unsupported for this value type."); + } + 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 << "."); @@ -748,6 +821,8 @@ namespace storm { 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::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::computeAllTransientProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, double timeBound); template storm::storage::SparseMatrix SparseCtmcCslHelper::computeUniformizedMatrix(storm::storage::SparseMatrix const& rateMatrix, storm::storage::BitVector const& maybeStates, double uniformizationRate, std::vector const& exitRates); @@ -784,6 +859,9 @@ namespace storm { 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); + template std::vector SparseCtmcCslHelper::computeAllTransientProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, double timeBound); + template std::vector SparseCtmcCslHelper::computeAllTransientProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, double timeBound); + 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); diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h index 28125c7c9..4ecd66abc 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h @@ -57,6 +57,11 @@ namespace storm { template static std::vector computeReachabilityTimes(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative); + template ::SupportsExponential, int>::type = 0> + static std::vector computeAllTransientProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, double timeBound); + template ::SupportsExponential, int>::type = 0> + static std::vector computeAllTransientProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, double timeBound); + /*! * Computes the matrix representing the transitions of the uniformized CTMC. *