From 7f7778533a565c8568caaab98e6c31939f3233a5 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 2 Apr 2018 17:46:31 +0200 Subject: [PATCH 01/14] Typos --- .../modelchecker/dft/DFTModelChecker.cpp | 6 ++-- src/storm-dft/storage/dft/DFT.cpp | 29 +++++++++---------- src/storm/models/sparse/MarkovAutomaton.cpp | 14 ++++----- src/storm/utility/DirectEncodingExporter.cpp | 2 +- 4 files changed, 25 insertions(+), 26 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 31ba6789d..8d277d60d 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -54,14 +54,14 @@ namespace storm { case storm::storage::DFTElementType::AND: STORM_LOG_TRACE("top modularisation called AND"); dfts = dft.topModularisation(); - STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules."); + STORM_LOG_TRACE("Modularisation into " << dfts.size() << " submodules."); nrK = dfts.size(); nrM = dfts.size(); break; case storm::storage::DFTElementType::OR: STORM_LOG_TRACE("top modularisation called OR"); dfts = dft.topModularisation(); - STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules."); + STORM_LOG_TRACE("Modularisation into " << dfts.size() << " submodules."); nrK = 0; nrM = dfts.size(); invResults = true; @@ -69,7 +69,7 @@ namespace storm { case storm::storage::DFTElementType::VOT: STORM_LOG_TRACE("top modularisation called VOT"); dfts = dft.topModularisation(); - STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules."); + STORM_LOG_TRACE("Modularisation into " << dfts.size() << " submodules."); nrK = std::static_pointer_cast const>(dft.getTopLevelGate())->threshold(); nrM = dfts.size(); if(nrK <= nrM/2) { diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 81784ea96..ad89354f3 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -293,22 +293,22 @@ namespace storm { } return max; } - + template DFT DFT::optimize() const { std::vector modIdea = findModularisationRewrite(); STORM_LOG_DEBUG("Modularisation idea: " << storm::utility::vector::toString(modIdea)); - + if (modIdea.empty()) { // No rewrite needed return *this; } - + std::vector> rewriteIds; rewriteIds.push_back(modIdea); - + storm::builder::DFTBuilder builder; - + // Accumulate elements which must be rewritten std::set rewriteSet; for (std::vector rewrites : rewriteIds) { @@ -320,7 +320,7 @@ namespace storm { builder.copyElement(elem); } } - + // Add rewritten elements for (std::vector rewrites : rewriteIds) { STORM_LOG_ASSERT(rewrites.size() > 1, "No rewritten elements."); @@ -359,7 +359,7 @@ namespace storm { STORM_LOG_ASSERT(false, "Dft type can not be rewritten."); break; } - + // Add parent with the new child newParent and all its remaining children childrenNames.clear(); childrenNames.push_back(newParentName); @@ -371,7 +371,7 @@ namespace storm { } builder.copyGate(originalParent, childrenNames); } - + builder.setTopLevel(mElements[mTopLevelIndex]->name()); // TODO use reference? DFT newDft = builder.build(); @@ -750,11 +750,10 @@ namespace storm { // suitable parent gate! - Lets check the independent submodules of the children auto const& children = std::static_pointer_cast>(e)->children(); for(auto const& child : children) { - - + auto ISD = std::static_pointer_cast>(child)->independentSubDft(true); // In the ISD, check for other children: - + std::vector rewrite = {e->id(), child->id()}; for(size_t isdElemId : ISD) { if(isdElemId == child->id()) continue; @@ -765,13 +764,13 @@ namespace storm { if(rewrite.size() > 2 && rewrite.size() < children.size() - 1) { return rewrite; } - - } + + } } - } + } return {}; } - + template std::tuple, std::vector, std::vector> DFT::getSortedParentAndDependencyIds(size_t index) const { diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index 9c077e2c4..587a28a7b 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -181,7 +181,7 @@ namespace storm { // Get number of choices in current state uint_fast64_t numberChoices = this->getTransitionMatrix().getRowGroupIndices()[state + 1] - this->getTransitionMatrix().getRowGroupIndices()[state]; if (isMarkovianState(state)) { - STORM_LOG_ASSERT(numberChoices == 1, "Wrong number of choices for markovian state."); + STORM_LOG_ASSERT(numberChoices == 1, "Wrong number of choices for Markovian state."); } if (numberChoices > 1) { STORM_LOG_ASSERT(isProbabilisticState(state), "State is not probabilistic."); @@ -211,7 +211,7 @@ namespace storm { storm::storage::FlexibleSparseMatrix flexibleMatrix(this->getTransitionMatrix()); storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(this->getTransitionMatrix().transpose()); storm::solver::stateelimination::StateEliminator stateEliminator(flexibleMatrix, flexibleBackwardTransitions); - + for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { STORM_LOG_ASSERT(!this->isHybridState(state), "State is hybrid."); if (this->isProbabilisticState(state)) { @@ -220,7 +220,7 @@ namespace storm { STORM_LOG_TRACE("Flexible matrix after eliminating state " << state << ":" << std::endl << flexibleMatrix); } } - + // Create the rate matrix for the CTMC storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, 0, 0, false, false); // Remember state to keep @@ -230,7 +230,7 @@ namespace storm { // State is eliminated and can be discarded keepStates.set(state, false); } else { - STORM_LOG_ASSERT(this->isMarkovianState(state), "State is not markovian."); + STORM_LOG_ASSERT(this->isMarkovianState(state), "State is not Markovian."); // Copy transitions for (uint_fast64_t row = flexibleMatrix.getRowGroupIndices()[state]; row < flexibleMatrix.getRowGroupIndices()[state + 1]; ++row) { for (auto const& entry : flexibleMatrix.getRow(row)) { @@ -240,20 +240,20 @@ namespace storm { } } } - + storm::storage::SparseMatrix rateMatrix = transitionMatrixBuilder.build(); rateMatrix = rateMatrix.getSubmatrix(false, keepStates, keepStates, false); STORM_LOG_TRACE("New CTMC matrix:" << std::endl << rateMatrix); // Construct CTMC storm::models::sparse::StateLabeling stateLabeling = this->getStateLabeling().getSubLabeling(keepStates); - + //TODO update reward models and choice labels according to kept states STORM_LOG_WARN_COND(this->getRewardModels().empty(), "Conversion of MA to CTMC does not preserve rewards."); std::unordered_map rewardModels = this->getRewardModels(); STORM_LOG_WARN_COND(!this->hasChoiceLabeling(), "Conversion of MA to CTMC does not preserve choice labels."); STORM_LOG_WARN_COND(!this->hasStateValuations(), "Conversion of MA to CTMC does not preserve choice labels."); STORM_LOG_WARN_COND(!this->hasChoiceOrigins(), "Conversion of MA to CTMC does not preserve choice labels."); - + return std::make_shared>(std::move(rateMatrix), std::move(stateLabeling), std::move(rewardModels)); } diff --git a/src/storm/utility/DirectEncodingExporter.cpp b/src/storm/utility/DirectEncodingExporter.cpp index 9953a4108..ec29cbe1e 100644 --- a/src/storm/utility/DirectEncodingExporter.cpp +++ b/src/storm/utility/DirectEncodingExporter.cpp @@ -73,7 +73,7 @@ namespace storm { } if(rewardModelEntry.second.hasStateRewards()) { - os << rewardModelEntry.second.getStateRewardVector().at(group); + os << storm::utility::to_string(rewardModelEntry.second.getStateRewardVector().at(group)); } else { os << "0"; } From 333d1ae3750ce674fedeef92bd2b8ba6700a11eb Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 3 Apr 2018 23:41:29 +0200 Subject: [PATCH 02/14] Function for computing all transient probabilities --- .../csl/SparseCtmcCslModelChecker.cpp | 16 ++++ .../csl/SparseCtmcCslModelChecker.h | 2 + .../csl/helper/SparseCtmcCslHelper.cpp | 78 +++++++++++++++++++ .../csl/helper/SparseCtmcCslHelper.h | 5 ++ 4 files changed, 101 insertions(+) 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. * From e513015b494ac9da456cc8b5e68ea2ca45fc3557 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 8 Apr 2018 22:09:00 +0200 Subject: [PATCH 03/14] Compute all reachabilities probabilities in a forward manner --- .../csl/helper/SparseCtmcCslHelper.cpp | 12 ++- .../csl/helper/SparseCtmcCslHelper.h | 3 + .../prctl/helper/SparseDtmcPrctlHelper.cpp | 82 ++++++++++++++++++- .../prctl/helper/SparseDtmcPrctlHelper.h | 2 + src/storm/storage/SparseMatrix.cpp | 13 +++ src/storm/storage/SparseMatrix.h | 5 ++ 6 files changed, 115 insertions(+), 2 deletions(-) diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 0a6dabcd8..3b6e4fb70 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -205,7 +205,12 @@ namespace storm { std::vector SparseCtmcCslHelper::computeUntilProbabilities(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& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) { return SparseDtmcPrctlHelper::computeUntilProbabilities(env, std::move(goal), computeProbabilityMatrix(rateMatrix, exitRateVector), backwardTransitions, phiStates, psiStates, qualitative); } - + + template + std::vector SparseCtmcCslHelper::computeAllUntilProbabilities(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& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + return SparseDtmcPrctlHelper::computeAllUntilProbabilities(env, std::move(goal), computeProbabilityMatrix(rateMatrix, exitRateVector), backwardTransitions, initialStates, phiStates, psiStates); + } + template std::vector SparseCtmcCslHelper::computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates) { return SparseDtmcPrctlHelper::computeNextProbabilities(env, computeProbabilityMatrix(rateMatrix, exitRateVector), nextStates); @@ -808,6 +813,8 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeUntilProbabilities(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& phiStates, storm::storage::BitVector const& psiStates, bool qualitative); + template std::vector SparseCtmcCslHelper::computeAllUntilProbabilities(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& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template std::vector SparseCtmcCslHelper::computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates); template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound); @@ -835,6 +842,9 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeUntilProbabilities(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& phiStates, storm::storage::BitVector const& psiStates, bool qualitative); template std::vector SparseCtmcCslHelper::computeUntilProbabilities(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& phiStates, storm::storage::BitVector const& psiStates, bool qualitative); + template std::vector SparseCtmcCslHelper::computeAllUntilProbabilities(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& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template std::vector SparseCtmcCslHelper::computeAllUntilProbabilities(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& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template std::vector SparseCtmcCslHelper::computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates); template std::vector SparseCtmcCslHelper::computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates); diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h index 4ecd66abc..233e695ff 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h @@ -27,6 +27,9 @@ namespace storm { template static std::vector computeUntilProbabilities(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& phiStates, storm::storage::BitVector const& psiStates, bool qualitative); + template + static std::vector computeAllUntilProbabilities(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& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template static std::vector computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates); diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 03d3fb1a0..dd8bbce8f 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -330,7 +330,87 @@ namespace storm { } return result; } - + + template + std::vector SparseDtmcPrctlHelper::computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + + uint_fast64_t numberOfStates = transitionMatrix.getRowCount(); + std::vector result(numberOfStates, storm::utility::zero()); + + // We need to identify the maybe states (states which have a probability for satisfying the until formula + // that is strictly between 0 and 1) and the states that satisfy the formula with probability 1. + //storm::storage::BitVector maybeStates, statesWithProbability1; + storm::storage::BitVector relevantStates(numberOfStates, true); + + // Get all states that have probability 0 and 1 of satisfying the until-formula. + //std::pair statesWithProbability01 = storm::utility::graph::performProb01(transitionMatrix, phiStates, initialStates); + //storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first); + //statesWithProbability1 = std::move(statesWithProbability01.second); + //maybeStates = ~(statesWithProbability0 | statesWithProbability1); + + //STORM_LOG_INFO("Preprocessing: " << statesWithProbability1.getNumberOfSetBits() << " states with probability 1, " << statesWithProbability0.getNumberOfSetBits() << " with probability 0 (" << maybeStates.getNumberOfSetBits() << " states remaining)."); + + // Set values of resulting vector that are known exactly. + //storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::zero()); + //storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::one()); + + // Compute exact probabilities for some states. + if (!relevantStates.empty()) { + // In this case we have to compute the probabilities. + + // Check whether we need to convert the input to equation system format. + storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; + bool convertToEquationSystem = linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; + + // We can eliminate the rows and columns from the original transition probability matrix. + storm::storage::SparseMatrix submatrix(transitionMatrix); + submatrix.makeRowsAbsorbing(psiStates); + submatrix.deleteDiagonalEntries(psiStates); + storm::storage::BitVector failState(numberOfStates, false); + failState.set(0, true); + submatrix.deleteDiagonalEntries(failState); + submatrix = submatrix.transpose(); + submatrix = submatrix.getSubmatrix(true, relevantStates, relevantStates, convertToEquationSystem); + + if (convertToEquationSystem) { + // Converting the matrix from the fixpoint notation to the form needed for the equation + // system. That is, we go from x = A*x + b to (I-A)x = b. + submatrix.convertToEquationSystem(); + } + + // Initialize the x vector with 0.5 for each element. + // This is the initial guess for the iterative solvers. It should be safe as for all + // 'maybe' states we know that the probability is strictly larger than 0. + std::vector x = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::convertNumber(0.5)); + //std::vector x = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::zero()); + + std::vector b(relevantStates.getNumberOfSetBits(), storm::utility::zero()); + // Set initial states + size_t i = 0; + ValueType initDist = storm::utility::one() / storm::utility::convertNumber(initialStates.getNumberOfSetBits()); + for (auto const& state : relevantStates) { + if (initialStates.get(state)) { + b[i] = initDist; + } + ++i; + } + + // Prepare the right-hand side of the equation system. For entry i this corresponds to + // the accumulated probability of going from state i to some 'yes' state. + //std::vector b = transitionMatrix.getConstrainedRowSumVector(relevantStates, statesWithProbability1); + + // Now solve the created system of linear equations. + goal.restrictRelevantValues(relevantStates); + std::unique_ptr> solver = storm::solver::configureLinearEquationSolver(env, std::move(goal), linearEquationSolverFactory, std::move(submatrix)); + solver->setBounds(storm::utility::zero(), storm::utility::one()); + solver->solveEquations(env, x, b); + + // Set values of resulting vector according to result. + storm::utility::vector::setVectorValues(result, relevantStates, x); + } + return result; + } + template std::vector SparseDtmcPrctlHelper::computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative) { goal.oneMinus(); diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h index a4e2882bc..1492b29df 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h @@ -36,6 +36,8 @@ namespace storm { static std::vector computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, ModelCheckerHint const& hint = ModelCheckerHint()); + static std::vector computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + static std::vector computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative); static std::vector computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound); diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 729b85b46..49cef9e4e 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -1301,6 +1301,19 @@ namespace storm { } } } + + template + void SparseMatrix::deleteDiagonalEntries(storm::storage::BitVector const& states) { + // Iterate over all rows and negate all the elements that are not on the diagonal. + for (index_type group = 0; group < this->getRowGroupCount(); ++group) { + for (auto& entry : this->getRowGroup(group)) { + if (entry.getColumn() == group && states[group]) { + --this->nonzeroEntryCount; + entry.setValue(storm::utility::zero()); + } + } + } + } template typename std::pair, std::vector> SparseMatrix::getJacobiDecomposition() const { diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index 4013a7cbf..e61d34624 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -799,6 +799,11 @@ namespace storm { * Sets all diagonal elements to zero. */ void deleteDiagonalEntries(); + + /*! + * Sets all diagonal elements to zero. + */ + void deleteDiagonalEntries(storm::storage::BitVector const& states); /*! * Calculates the Jacobi decomposition of this sparse matrix. For this operation, the matrix must be square. From cab33179e7b0e27d8f7e569bca85744f424580d7 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 8 Apr 2018 22:09:16 +0200 Subject: [PATCH 04/14] Typo --- src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index dd8bbce8f..ddd430087 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -250,7 +250,7 @@ namespace storm { std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); // We need to identify the maybe states (states which have a probability for satisfying the until formula - // that is strictly between 0 and 1) and the states that satisfy the formula with probablity 1. + // that is strictly between 0 and 1) and the states that satisfy the formula with probability 1. storm::storage::BitVector maybeStates, statesWithProbability1; if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().getComputeOnlyMaybeStates()) { @@ -290,7 +290,7 @@ namespace storm { storm::utility::vector::setVectorValues(result, maybeStates, storm::utility::convertNumber(0.5)); } else { if (!maybeStates.empty()) { - // In this case we have have to compute the probabilities. + // In this case we have to compute the probabilities. // Check whether we need to convert the input to equation system format. storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; From bf88eca92f6c33c0fe3aea26d95abb9e77978c47 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 10 Apr 2018 15:25:45 +0200 Subject: [PATCH 05/14] Export DRN format for model composed from DFT modularisation --- src/storm-dft/modelchecker/dft/DFTModelChecker.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 8d277d60d..997113bd2 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -28,6 +28,18 @@ namespace storm { if (properties[0]->isTimeOperatorFormula() && allowModularisation) { // Use parallel composition as modularisation approach for expected time std::shared_ptr> model = buildModelViaComposition(dft, properties, symred, true, enableDC, approximationError); + + // Export the model if required + // TODO move this outside of the model checker? + if (storm::settings::getModule().isExportExplicitSet()) { + std::ofstream stream; + storm::utility::openFile(storm::settings::getModule().getExportExplicitFilename(), stream); + std::vector parameterNames; + // TODO fill parameter names + storm::exporter::explicitExportSparseModel(stream, model, parameterNames); + storm::utility::closeFile(stream); + } + // Model checking std::vector resultsValue = checkModel(model, properties); for (ValueType result : resultsValue) { From 87edc3abe08d1f7c7121e6fef048db2c9efb2201 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 17 Apr 2018 13:46:10 +0200 Subject: [PATCH 06/14] Better debug output --- src/storm-dft/modelchecker/dft/DFTModelChecker.cpp | 2 +- src/storm-dft/storage/dft/DFT.cpp | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 997113bd2..a1887a4ba 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -202,7 +202,7 @@ namespace storm { } // Build a single CTMC - STORM_LOG_DEBUG("Building Model..."); + STORM_LOG_DEBUG("Building Model from DFT with top level element " << ft.getElement(ft.getTopLevelIndex())->toString() << " ..."); storm::builder::ExplicitDFTModelBuilder builder(ft, symmetries, enableDC); typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties); builder.buildModel(labeloptions, 0, 0.0); diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index ad89354f3..e9ed0267b 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -328,14 +328,14 @@ namespace storm { STORM_LOG_ASSERT(mElements[rewrites[1]]->parents().front()->isGate(), "Rewritten element has no parent gate."); DFTGatePointer originalParent = std::static_pointer_cast>(mElements[rewrites[1]]->parents().front()); std::string newParentName = builder.getUniqueName(originalParent->name()); - + // Accumulate children names std::vector childrenNames; for (size_t i = 1; i < rewrites.size(); ++i) { - STORM_LOG_ASSERT(mElements[rewrites[i]]->parents().front()->id() == originalParent->id(), "Children have the same father"); + STORM_LOG_ASSERT(mElements[rewrites[i]]->parents().front()->id() == originalParent->id(), "Children have not the same father for rewrite " << mElements[rewrites[i]]->name()); childrenNames.push_back(mElements[rewrites[i]]->name()); } - + // Add element inbetween parent and children switch (originalParent->type()) { case DFTElementType::AND: From 006ccaa2ee9ef40caac956e0d4213c0ba5c5fb9d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 17 Apr 2018 13:46:42 +0200 Subject: [PATCH 07/14] Build all labels for DFT model if export is enabled --- src/storm-dft/modelchecker/dft/DFTModelChecker.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index a1887a4ba..28a6afd8e 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -204,7 +204,7 @@ namespace storm { // Build a single CTMC STORM_LOG_DEBUG("Building Model from DFT with top level element " << ft.getElement(ft.getTopLevelIndex())->toString() << " ..."); storm::builder::ExplicitDFTModelBuilder builder(ft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties); + typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties, storm::settings::getModule().isExportExplicitSet()); builder.buildModel(labeloptions, 0, 0.0); std::shared_ptr> model = builder.getModel(); explorationTimer.stop(); @@ -256,7 +256,7 @@ namespace storm { STORM_LOG_DEBUG("Building Model..."); storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties); + typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties, storm::settings::getModule().isExportExplicitSet()); builder.buildModel(labeloptions, 0, 0.0); std::shared_ptr> model = builder.getModel(); //model->printModelInformationToStream(std::cout); @@ -288,7 +288,7 @@ namespace storm { std::shared_ptr> model; std::vector newResult; storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties); + typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties, storm::settings::getModule().isExportExplicitSet()); // TODO Matthias: compute approximation for all properties simultaneously? std::shared_ptr property = properties[0]; From 0f357366cb36f81bb4abfdb5a7e110fda91e4aa3 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 17 Apr 2018 14:11:17 +0200 Subject: [PATCH 08/14] Improved variable names in findModularisationRewrite --- src/storm-dft/storage/dft/DFT.cpp | 49 ++++++++++++++++--------------- 1 file changed, 25 insertions(+), 24 deletions(-) diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index e9ed0267b..4b43f6b6e 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -745,30 +745,31 @@ namespace storm { template std::vector DFT::findModularisationRewrite() const { - for(auto const& e : mElements) { - if(e->isGate() && (e->type() == DFTElementType::AND || e->type() == DFTElementType::OR) ) { - // suitable parent gate! - Lets check the independent submodules of the children - auto const& children = std::static_pointer_cast>(e)->children(); - for(auto const& child : children) { - - auto ISD = std::static_pointer_cast>(child)->independentSubDft(true); - // In the ISD, check for other children: - - std::vector rewrite = {e->id(), child->id()}; - for(size_t isdElemId : ISD) { - if(isdElemId == child->id()) continue; - if(std::find_if(children.begin(), children.end(), [&isdElemId](std::shared_ptr> const& e) { return e->id() == isdElemId; } ) != children.end()) { - rewrite.push_back(isdElemId); - } - } - if(rewrite.size() > 2 && rewrite.size() < children.size() - 1) { - return rewrite; - } - - } - } - } - return {}; + for (auto const& element : mElements) { + if (element->isGate() && (element->type() == DFTElementType::AND || element->type() == DFTElementType::OR) ) { + // suitable parent gate! - Lets check the independent submodules of the children + auto const& children = std::static_pointer_cast>(element)->children(); + for(auto const& child : children) { + + auto independentSubtree = std::static_pointer_cast>(child)->independentSubDft(true); + // In the independent subtree, check for other children: + + std::vector rewrite = {element->id(), child->id()}; + for(size_t independentSubtreeElementId : independentSubtree) { + if (independentSubtreeElementId == child->id()) continue; + if (std::find_if(children.begin(), children.end(), [&independentSubtreeElementId](std::shared_ptr> const& e) { return e->id() == independentSubtreeElementId; } ) != children.end()) { + // element in subtree is also child + rewrite.push_back(independentSubtreeElementId); + } + } + if(rewrite.size() > 2 && rewrite.size() < children.size() - 1) { + return rewrite; + } + + } + } + } + return {}; } From e1af4158ae00e916cf1d74bcc88e669bc1cc29d1 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 9 May 2019 11:14:35 +0200 Subject: [PATCH 09/14] Removed unused argument --- .../csl/SparseCtmcCslModelChecker.cpp | 10 +++++----- .../csl/helper/SparseCtmcCslHelper.cpp | 17 +++++++---------- .../csl/helper/SparseCtmcCslHelper.h | 4 ++-- 3 files changed, 14 insertions(+), 17 deletions(-) diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 3c953a95f..5d1b0a60d 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -158,16 +158,16 @@ namespace storm { template std::vector SparseCtmcCslModelChecker::computeTransientProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); + 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::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); + std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeAllTransientProbabilities(env, this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), upperBound); return result; } diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 2875a69dc..9d4cca741 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -654,14 +654,14 @@ namespace storm { } 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) { + std::vector SparseCtmcCslHelper::computeAllTransientProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, 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; + std::vector result = std::vector(numberOfStates, storm::utility::zero()); storm::storage::SparseMatrix transposedMatrix(rateMatrix); transposedMatrix.makeRowsAbsorbing(psiStates); @@ -676,7 +676,7 @@ namespace storm { //storm::storage::BitVector relevantStates = statesWithProbabilityGreater0 & ~initialStates;//phiStates | psiStates; storm::storage::BitVector relevantStates(numberOfStates, true); - STORM_LOG_INFO(relevantStates.getNumberOfSetBits() << " relevant states."); + STORM_LOG_DEBUG(relevantStates.getNumberOfSetBits() << " relevant states."); if (!relevantStates.empty()) { // Find the maximal rate of all relevant states to take it as the uniformization rate. @@ -712,17 +712,14 @@ namespace storm { // 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) { + std::vector SparseCtmcCslHelper::computeAllTransientProbabilities(Environment 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."); } @@ -882,7 +879,7 @@ 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::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::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); @@ -925,8 +922,8 @@ 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 std::vector SparseCtmcCslHelper::computeAllTransientProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, 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::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); diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h index f5f050a3d..c988603e4 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h @@ -64,9 +64,9 @@ namespace storm { 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); + static std::vector computeAllTransientProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, 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); + static std::vector computeAllTransientProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, 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. From 161c3ac6bf4e81cb40d18f90d11dfaba2f2ef14b Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 9 May 2019 11:14:53 +0200 Subject: [PATCH 10/14] Test case for transient probabilities --- .../modelchecker/CtmcCslModelCheckerTest.cpp | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp index fc906da6c..fcb8b53df 100644 --- a/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp @@ -16,6 +16,7 @@ #include "storm/models/symbolic/Ctmc.h" #include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h" #include "storm/modelchecker/csl/HybridCtmcCslModelChecker.h" +#include "storm/modelchecker/csl/helper/SparseCtmcCslHelper.h" #include "storm/modelchecker/results/QuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -458,4 +459,23 @@ namespace { } } + + TEST(CtmcCslModelCheckerTest, TransientProbabilities) { + // Example from lecture + storm::storage::SparseMatrixBuilder matrixBuilder; + matrixBuilder.addNextValue(0, 1, 3.0); + matrixBuilder.addNextValue(1, 0, 2.0); + storm::storage::SparseMatrix matrix = matrixBuilder.build(); + + std::vector exitRates = {3, 2}; + storm::storage::BitVector initialStates(2); + initialStates.set(0); + storm::storage::BitVector phiStates(2); + storm::storage::BitVector psiStates(2); + storm::Environment env; + std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeAllTransientProbabilities(env, matrix, initialStates, phiStates, psiStates, exitRates, 1); + + EXPECT_NEAR(0.404043, result[0], 1e-6); + EXPECT_NEAR(0.595957, result[1], 1e-6); + } } From a35735a63054070782e0ba40e4b5a9921bf6eaf6 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 9 May 2019 11:18:19 +0200 Subject: [PATCH 11/14] Fixed computation of all until probabilities --- .../modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 9b6f08428..a76da19b1 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -290,10 +290,10 @@ namespace storm { // We can eliminate the rows and columns from the original transition probability matrix. storm::storage::SparseMatrix submatrix(transitionMatrix); submatrix.makeRowsAbsorbing(psiStates); - submatrix.deleteDiagonalEntries(psiStates); - storm::storage::BitVector failState(numberOfStates, false); - failState.set(0, true); - submatrix.deleteDiagonalEntries(failState); + //submatrix.deleteDiagonalEntries(psiStates); + //storm::storage::BitVector failState(numberOfStates, false); + //failState.set(0, true); + submatrix.deleteDiagonalEntries(); submatrix = submatrix.transpose(); submatrix = submatrix.getSubmatrix(true, relevantStates, relevantStates, convertToEquationSystem); From 65a310dc8bfcd1e4f91eb17f84aaef93fc060a5d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 17 May 2019 10:34:53 +0200 Subject: [PATCH 12/14] Test for allUntilProbabilities --- .../csl/SparseCtmcCslModelChecker.cpp | 2 +- .../csl/SparseCtmcCslModelChecker.h | 5 +- .../csl/helper/SparseCtmcCslHelper.cpp | 10 ++-- .../csl/helper/SparseCtmcCslHelper.h | 2 +- .../prctl/helper/SparseDtmcPrctlHelper.cpp | 28 ++-------- .../prctl/helper/SparseDtmcPrctlHelper.h | 2 +- .../DtmcPrctlModelCheckerTest.cpp | 53 +++++++++++++++++++ 7 files changed, 69 insertions(+), 33 deletions(-) diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 5d1b0a60d..89a2c9e03 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -156,7 +156,7 @@ namespace storm { } template - std::vector SparseCtmcCslModelChecker::computeTransientProbabilities(Environment const& env, CheckTask const& checkTask) { + std::vector SparseCtmcCslModelChecker::computeAllTransientProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); 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."); diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h index d0af959f4..d7f432f53 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -35,7 +35,10 @@ namespace storm { virtual std::unique_ptr computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - std::vector computeTransientProbabilities(Environment const& env, CheckTask const& checkTask); + /*! + * Compute transient probabilities for all states. + */ + std::vector computeAllTransientProbabilities(Environment const& env, CheckTask const& checkTask); private: template::SupportsExponential, int>::type = 0> diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 9d4cca741..ed87a9e1a 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -210,8 +210,8 @@ namespace storm { } template - std::vector SparseCtmcCslHelper::computeAllUntilProbabilities(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& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - return SparseDtmcPrctlHelper::computeAllUntilProbabilities(env, std::move(goal), computeProbabilityMatrix(rateMatrix, exitRateVector), backwardTransitions, initialStates, phiStates, psiStates); + std::vector SparseCtmcCslHelper::computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + return SparseDtmcPrctlHelper::computeAllUntilProbabilities(env, std::move(goal), computeProbabilityMatrix(rateMatrix, exitRateVector), initialStates, phiStates, psiStates); } template @@ -861,7 +861,7 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeUntilProbabilities(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& phiStates, storm::storage::BitVector const& psiStates, bool qualitative); - template std::vector SparseCtmcCslHelper::computeAllUntilProbabilities(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& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template std::vector SparseCtmcCslHelper::computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::vector SparseCtmcCslHelper::computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates); @@ -892,8 +892,8 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeUntilProbabilities(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& phiStates, storm::storage::BitVector const& psiStates, bool qualitative); template std::vector SparseCtmcCslHelper::computeUntilProbabilities(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& phiStates, storm::storage::BitVector const& psiStates, bool qualitative); - template std::vector SparseCtmcCslHelper::computeAllUntilProbabilities(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& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template std::vector SparseCtmcCslHelper::computeAllUntilProbabilities(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& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template std::vector SparseCtmcCslHelper::computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template std::vector SparseCtmcCslHelper::computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::vector SparseCtmcCslHelper::computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates); template std::vector SparseCtmcCslHelper::computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates); diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h index c988603e4..4fb01d5ff 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h @@ -28,7 +28,7 @@ namespace storm { static std::vector computeUntilProbabilities(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& phiStates, storm::storage::BitVector const& psiStates, bool qualitative); template - static std::vector computeAllUntilProbabilities(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& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + static std::vector computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template static std::vector computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates); diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index a76da19b1..a03914c8c 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -257,38 +257,22 @@ namespace storm { } template - std::vector SparseDtmcPrctlHelper::computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + std::vector SparseDtmcPrctlHelper::computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { uint_fast64_t numberOfStates = transitionMatrix.getRowCount(); std::vector result(numberOfStates, storm::utility::zero()); - // We need to identify the maybe states (states which have a probability for satisfying the until formula - // that is strictly between 0 and 1) and the states that satisfy the formula with probability 1. - //storm::storage::BitVector maybeStates, statesWithProbability1; + // All states are relevant storm::storage::BitVector relevantStates(numberOfStates, true); - // Get all states that have probability 0 and 1 of satisfying the until-formula. - //std::pair statesWithProbability01 = storm::utility::graph::performProb01(transitionMatrix, phiStates, initialStates); - //storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first); - //statesWithProbability1 = std::move(statesWithProbability01.second); - //maybeStates = ~(statesWithProbability0 | statesWithProbability1); - - //STORM_LOG_INFO("Preprocessing: " << statesWithProbability1.getNumberOfSetBits() << " states with probability 1, " << statesWithProbability0.getNumberOfSetBits() << " with probability 0 (" << maybeStates.getNumberOfSetBits() << " states remaining)."); - - // Set values of resulting vector that are known exactly. - //storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::zero()); - //storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::one()); - // Compute exact probabilities for some states. if (!relevantStates.empty()) { - // In this case we have to compute the probabilities. - // Check whether we need to convert the input to equation system format. storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; bool convertToEquationSystem = linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; - // We can eliminate the rows and columns from the original transition probability matrix. storm::storage::SparseMatrix submatrix(transitionMatrix); + submatrix.makeRowsAbsorbing(phiStates); submatrix.makeRowsAbsorbing(psiStates); //submatrix.deleteDiagonalEntries(psiStates); //storm::storage::BitVector failState(numberOfStates, false); @@ -307,8 +291,8 @@ namespace storm { // This is the initial guess for the iterative solvers. It should be safe as for all // 'maybe' states we know that the probability is strictly larger than 0. std::vector x = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::convertNumber(0.5)); - //std::vector x = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::zero()); + // Prepare the right-hand side of the equation system. std::vector b(relevantStates.getNumberOfSetBits(), storm::utility::zero()); // Set initial states size_t i = 0; @@ -320,10 +304,6 @@ namespace storm { ++i; } - // Prepare the right-hand side of the equation system. For entry i this corresponds to - // the accumulated probability of going from state i to some 'yes' state. - //std::vector b = transitionMatrix.getConstrainedRowSumVector(relevantStates, statesWithProbability1); - // Now solve the created system of linear equations. goal.restrictRelevantValues(relevantStates); std::unique_ptr> solver = storm::solver::configureLinearEquationSolver(env, std::move(goal), linearEquationSolverFactory, std::move(submatrix)); diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h index 60a026571..e22e4bfc4 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h @@ -36,7 +36,7 @@ namespace storm { static std::vector computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, ModelCheckerHint const& hint = ModelCheckerHint()); - static std::vector computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + static std::vector computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); static std::vector computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative); diff --git a/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp index ff0e4630d..6c5f08c86 100644 --- a/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp @@ -17,6 +17,7 @@ #include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" #include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h" +#include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" #include "storm/modelchecker/results/QuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -644,5 +645,57 @@ namespace { EXPECT_NEAR(this->parseNumber("25/24"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } + TEST(DtmcPrctlModelCheckerTest, AllUntilProbabilities) { + std::string formulasString = "P=? [F \"one\"]"; + formulasString += "; P=? [F \"two\"]"; + formulasString += "; P=? [F \"three\"]"; + + storm::prism::Program program = storm::api::parseProgram(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); + auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program)); + std::vector> tasks; + for (auto const& f : formulas) { + tasks.emplace_back(*f); + } + auto model = storm::api::buildSparseModel(program, formulas)->template as>(); + EXPECT_EQ(13ul, model->getNumberOfStates()); + EXPECT_EQ(20ul, model->getNumberOfTransitions()); + + storm::storage::SparseMatrix matrix = model->getTransitionMatrix(); + storm::storage::BitVector initialStates(13); + initialStates.set(0); + storm::storage::BitVector phiStates(13); + storm::storage::BitVector psiStates(13); + psiStates.set(7); + psiStates.set(8); + psiStates.set(9); + psiStates.set(10); + psiStates.set(11); + psiStates.set(12); + storm::Environment env; + storm::solver::SolveGoal goal(*model, tasks[0]); + std::vector result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeAllUntilProbabilities(env, std::move(goal), matrix, initialStates, phiStates, psiStates); + + EXPECT_NEAR(1.0/6, result[7], 1e-6); + EXPECT_NEAR(1.0/6, result[8], 1e-6); + EXPECT_NEAR(1.0/6, result[9], 1e-6); + EXPECT_NEAR(1.0/6, result[10], 1e-6); + EXPECT_NEAR(1.0/6, result[11], 1e-6); + EXPECT_NEAR(1.0/6, result[12], 1e-6); + + phiStates.set(6); + psiStates.set(1); + result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeAllUntilProbabilities(env, std::move(goal), matrix, initialStates, phiStates, psiStates); + + EXPECT_NEAR(1, result[0], 1e-6); + EXPECT_NEAR(0.5, result[1], 1e-6); + EXPECT_NEAR(0.5, result[2], 1e-6); + EXPECT_NEAR(0.25, result[5], 1e-6); + EXPECT_NEAR(0, result[7], 1e-6); + EXPECT_NEAR(0, result[8], 1e-6); + EXPECT_NEAR(0, result[9], 1e-6); + EXPECT_NEAR(0.125, result[10], 1e-6); + EXPECT_NEAR(0.125, result[11], 1e-6); + EXPECT_NEAR(0, result[12], 1e-6); + } } From 9ebd1af7373e7ce2c559966ca86400b442fdf1df Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 17 May 2019 10:35:06 +0200 Subject: [PATCH 13/14] Removed unused method again --- src/storm/storage/SparseMatrix.cpp | 13 ------------- src/storm/storage/SparseMatrix.h | 5 ----- 2 files changed, 18 deletions(-) diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 324bc0477..cdeaaf9a2 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -1306,19 +1306,6 @@ namespace storm { } } } - - template - void SparseMatrix::deleteDiagonalEntries(storm::storage::BitVector const& states) { - // Iterate over all rows and negate all the elements that are not on the diagonal. - for (index_type group = 0; group < this->getRowGroupCount(); ++group) { - for (auto& entry : this->getRowGroup(group)) { - if (entry.getColumn() == group && states[group]) { - --this->nonzeroEntryCount; - entry.setValue(storm::utility::zero()); - } - } - } - } template typename std::pair, std::vector> SparseMatrix::getJacobiDecomposition() const { diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index d4c5d6c4c..dbdd4086d 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -806,11 +806,6 @@ namespace storm { * Sets all diagonal elements to zero. */ void deleteDiagonalEntries(); - - /*! - * Sets all diagonal elements to zero. - */ - void deleteDiagonalEntries(storm::storage::BitVector const& states); /*! * Calculates the Jacobi decomposition of this sparse matrix. For this operation, the matrix must be square. From 777d6001a16229e8080d39f237a981e01361c2c0 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 20 May 2019 11:44:06 +0200 Subject: [PATCH 14/14] SettingsManager: Better error message when an option argument can not be parsed. --- src/storm/settings/SettingsManager.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index 69ad4a909..3b8dcfade 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -385,7 +385,7 @@ namespace storm { for (uint_fast64_t i = 0; i < argumentCache.size(); ++i) { ArgumentBase& argument = option->getArgument(i); bool conversionOk = argument.setFromStringValue(argumentCache[i]); - STORM_LOG_THROW(conversionOk, storm::exceptions::OptionParserException, "Value '" << argumentCache[i] << "' is invalid for argument '" << argument.getName() << "' of option " << option->getModuleName() << ":" << option->getLongName() << "."); + STORM_LOG_THROW(conversionOk, storm::exceptions::OptionParserException, "Value '" << argumentCache[i] << "' is invalid for argument <" << argument.getName() << "> of option:\n" << *option); } // In case there are optional arguments that were not set, we set them to their default value.