From 76b99a5515a06961338bb0bd8cb2eddce94d98ce Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 8 Apr 2015 16:55:58 +0200 Subject: [PATCH] Commit to switch workplace. Former-commit-id: e80da5e90bc3fa9b315aab6f229ef1c82a909590 --- .../csl/HybridCtmcCslModelChecker.cpp | 356 ++++++++++++++++++ .../csl/HybridCtmcCslModelChecker.h | 96 +++++ .../csl/SparseCtmcCslModelChecker.cpp | 14 +- .../csl/SparseCtmcCslModelChecker.h | 7 +- .../prctl/HybridDtmcPrctlModelChecker.cpp | 13 +- .../prctl/HybridDtmcPrctlModelChecker.h | 7 +- .../results/HybridQuantitativeCheckResult.cpp | 11 + .../results/HybridQuantitativeCheckResult.h | 2 + src/models/symbolic/Ctmc.cpp | 7 +- src/models/symbolic/Ctmc.h | 10 + src/models/symbolic/Model.cpp | 10 + src/models/symbolic/Model.h | 14 + src/storage/dd/CuddOdd.cpp | 14 + src/storage/dd/CuddOdd.h | 24 +- 14 files changed, 566 insertions(+), 19 deletions(-) create mode 100644 src/modelchecker/csl/HybridCtmcCslModelChecker.cpp create mode 100644 src/modelchecker/csl/HybridCtmcCslModelChecker.h diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp new file mode 100644 index 000000000..a8c088aeb --- /dev/null +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -0,0 +1,356 @@ +#include "src/modelchecker/csl/HybridCtmcCslModelChecker.h" +#include "src/modelchecker/csl/SparseCtmcCslModelChecker.h" +#include "src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" + +#include "src/storage/dd/CuddOdd.h" + +#include "src/utility/macros.h" +#include "src/utility/graph.h" + +#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" +#include "src/modelchecker/results/HybridQuantitativeCheckResult.h" + +#include "src/exceptions/InvalidStateException.h" +#include "src/exceptions/InvalidPropertyException.h" + +namespace storm { + namespace modelchecker { + template + HybridCtmcCslModelChecker::HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(new storm::utility::solver::LinearEquationSolverFactory()) { + // Intentionally left empty. + } + + template + HybridCtmcCslModelChecker::HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model, std::unique_ptr>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { + // Intentionally left empty. + } + + template + bool HybridCtmcCslModelChecker::canHandle(storm::logic::Formula const& formula) const { + return formula.isCslStateFormula() || formula.isCslPathFormula() || formula.isRewardPathFormula(); + } + + template + storm::dd::Add HybridCtmcCslModelChecker::computeProbabilityMatrix(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector) { + return rateMatrix / exitRateVector.swapVariables(model.getRowColumnMetaVariablePairs()); + } + + template + std::unique_ptr HybridCtmcCslModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); + std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); + SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); + SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); + + return HybridDtmcPrctlModelChecker::computeUntilProbabilitiesHelper(this->getModel(), this->computeProbabilityMatrix(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + } + + template + std::unique_ptr HybridCtmcCslModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); + SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); + return std::unique_ptr(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), HybridDtmcPrctlModelChecker::computeNextProbabilitiesHelper(this->getModel(), this->computeProbabilityMatrix(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()), subResult.getTruthValuesVector()))); + } + + template + storm::models::symbolic::Ctmc const& HybridCtmcCslModelChecker::getModel() const { + return this->template getModelAs>(); + } + + template + storm::dd::Add HybridCtmcCslModelChecker::computeUniformizedMatrix(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& maybeStates, ValueType uniformizationRate) { + STORM_LOG_DEBUG("Computing uniformized matrix using uniformization rate " << uniformizationRate << "."); + STORM_LOG_DEBUG("Keeping " << maybeStates.getNonZeroCount() << " rows."); + + // Cut all non-maybe rows/columns from the transition matrix. + storm::dd::Add uniformizedMatrix = transitionMatrix * maybeStates.toAdd() * maybeStates.swapVariables(model.getRowColumnMetaVariablePairs()).toAdd(); + + // Now perform the uniformization. + uniformizedMatrix = uniformizedMatrix / model.getManager().getConstant(uniformizationRate); + storm::dd::Add diagonalOffset = model.getRowColumnIdentity(); + diagonalOffset -= model.getRowColumnIdentity() * (exitRateVector / model.getManager().getConstant(uniformizationRate)); + uniformizedMatrix = uniformizedMatrix + diagonalOffset; + + return uniformizedMatrix; + } + + template + std::unique_ptr HybridCtmcCslModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); + SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); + + boost::optional> modifiedStateRewardVector; + if (this->getModel().hasStateRewards()) { + modifiedStateRewardVector = this->getModel().getStateRewardVector() / this->getModel().getTransitionMatrix().sumAbstract(this->getModel().getColumnVariables()); + } + + return HybridDtmcPrctlModelChecker::computeReachabilityRewardsHelper(this->getModel(), this->computeProbabilityMatrix(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()), modifiedStateRewardVector, this->getModel().getOptionalTransitionRewardMatrix(), subResult.getTruthValuesVector(), *linearEquationSolverFactory, qualitative); + } + + template + std::unique_ptr HybridCtmcCslModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); + std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); + SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); + SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); + double lowerBound = 0; + double upperBound = 0; + if (!pathFormula.hasDiscreteTimeBound()) { + std::pair const& intervalBounds = pathFormula.getIntervalBounds(); + lowerBound = intervalBounds.first; + upperBound = intervalBounds.second; + } else { + upperBound = pathFormula.getDiscreteTimeBound(); + } + + return this->computeBoundedUntilProbabilitiesHelper(leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), qualitative, lowerBound, upperBound); + } + + template + std::unique_ptr HybridCtmcCslModelChecker::computeBoundedUntilProbabilitiesHelper(storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Add const& exitRates, bool qualitative, double lowerBound, double upperBound) const { + // If the time bounds are [0, inf], we rather call untimed reachability. + storm::utility::ConstantsComparator comparator; + if (comparator.isZero(lowerBound) && comparator.isInfinity(upperBound)) { + return HybridDtmcPrctlModelChecker::computeUntilProbabilitiesHelper(this->getModel(), this->computeProbabilityMatrix(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()), phiStates, psiStates, qualitative, *this->linearEquationSolverFactory); + } + + // From this point on, we know that we have to solve a more complicated problem [t, t'] with either t != 0 + // or t' != inf. + + // If we identify the states that have probability 0 of reaching the target states, we can exclude them from the + // further computations. + storm::dd::Bdd statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel(), this->getModel().getTransitionMatrix().notZero(), phiStates, psiStates); + STORM_LOG_INFO("Found " << statesWithProbabilityGreater0.getNonZeroCount() << " states with probability greater 0."); + storm::dd::Bdd statesWithProbabilityGreater0NonPsi = statesWithProbabilityGreater0 && !psiStates; + STORM_LOG_INFO("Found " << statesWithProbabilityGreater0NonPsi.getNonZeroCount() << " 'maybe' states."); + + if (!statesWithProbabilityGreater0NonPsi.isZero()) { + if (comparator.isZero(upperBound)) { + // In this case, the interval is of the form [0, 0]. + return std::unique_ptr(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), psiStates.toAdd())); + } else { + if (comparator.isZero(lowerBound)) { + // In this case, the interval is of the form [0, t]. + // Note that this excludes [0, inf] since this is untimed reachability and we considered this case earlier. + + // Find the maximal rate of all 'maybe' states to take it as the uniformization rate. + ValueType uniformizationRate = 1.02 * (statesWithProbabilityGreater0NonPsi.toAdd() * exitRates).getMax(); + STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); + + // Compute the uniformized matrix. + storm::dd::Add uniformizedMatrix = this->computeUniformizedMatrix(this->getModel(), this->getModel().getTransitionMatrix(), exitRates, statesWithProbabilityGreater0NonPsi, uniformizationRate); + + // Compute the vector that is to be added as a compensation for removing the absorbing states. + storm::dd::Add b = (statesWithProbabilityGreater0NonPsi.toAdd() * this->getModel().getTransitionMatrix() * psiStates.swapVariables(this->getModel().getRowColumnMetaVariablePairs()).toAdd()).sumAbstract(this->getModel().getColumnVariables()) / this->getModel().getManager().getConstant(uniformizationRate); + + // Create an ODD for the translation to an explicit representation. + storm::dd::Odd odd(statesWithProbabilityGreater0NonPsi); + + // Convert the symbolic parts to their explicit representation. + storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); + std::vector explicitB = b.template toVector(odd); + + // Finally compute the transient probabilities. + std::vector values(statesWithProbabilityGreater0NonPsi.getNonZeroCount(), storm::utility::zero()); + std::vector subresult = SparseCtmcCslModelChecker::computeTransientProbabilities(explicitUniformizedMatrix, &explicitB, upperBound, uniformizationRate, values, *this->linearEquationSolverFactory); + + return std::unique_ptr(new HybridQuantitativeCheckResult(this->getModel().getReachableStates(), + (psiStates || !statesWithProbabilityGreater0) && this->getModel().getReachableStates(), + psiStates.toAdd(), + statesWithProbabilityGreater0NonPsi, + odd, subresult)); + } else if (comparator.isInfinity(upperBound)) { + // In this case, the interval is of the form [t, inf] with t != 0. + + // Start by computing the (unbounded) reachability probabilities of reaching psi states while + // staying in phi states. + std::unique_ptr unboundedResult = HybridDtmcPrctlModelChecker::computeUntilProbabilitiesHelper(this->getModel(), this->computeProbabilityMatrix(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()), phiStates, psiStates, qualitative, *this->linearEquationSolverFactory); + + // Determine the set of states that achieved a strictly positive probability. + std::unique_ptr statesWithValuesGreaterZero = unboundedResult->asQuantitativeCheckResult().compareAgainstBound(storm::logic::ComparisonType::Greater, storm::utility::zero()); + + // And use it to compute the set of relevant states. + storm::dd::Bdd relevantStates = storm::utility::graph::performProbGreater0(this->getModel(), this->getModel().getTransitionMatrix(), phiStates, statesWithValuesGreaterZero->asSymbolicQualitativeCheckResult().getTruthValuesVector()); + + // Filter the unbounded result such that it only contains values for the relevant states. + unboundedResult->filter(SymbolicQualitativeCheckResult(this->getModel().getReachableStates(), relevantStates)); + + // Build an ODD for the relevant states. + storm::dd::Odd odd(relevantStates); + + std::vector result; + if (unboundedResult->isHybridQuantitativeCheckResult()) { + std::unique_ptr explicitUnboundedResult = unboundedResult->asHybridQuantitativeCheckResult().toExplicitQuantitativeCheckResult(); + result = std::move(explicitUnboundedResult->asExplicitQuantitativeCheckResult().getValueVector()); + } else { + STORM_LOG_THROW(unboundedResult->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidStateException, "Expected check result of different type."); + result = unboundedResult->asSymbolicQuantitativeCheckResult().getValueVector().toVector(odd); + } + + // Determine the uniformization rate for the transient probability computation. + ValueType uniformizationRate = 1.02 * (relevantStates.toAdd() * exitRates).getMax(); + + // Compute the uniformized matrix. + storm::dd::Add uniformizedMatrix = this->computeUniformizedMatrix(this->getModel(), this->getModel().getTransitionMatrix(), exitRates, relevantStates, uniformizationRate); + storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); + + // Compute the transient probabilities. + std::vector subResult = SparseCtmcCslModelChecker::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, subResult, *this->linearEquationSolverFactory); + + return std::unique_ptr(new HybridQuantitativeCheckResult(this->getModel().getReachableStates(), !relevantStates && this->getModel().getReachableStates(), this->getModel().getManager().getAddZero(), relevantStates, odd, subResult)); + } else { + // In this case, the interval is of the form [t, t'] with t != 0 and t' != inf. + + // Prepare some variables that are used by the two following blocks. + storm::dd::Bdd relevantStates; + ValueType uniformizationRate = 0; + storm::dd::Add uniformizedMatrix; + std::vector newSubresult; + storm::dd::Odd odd; + + if (lowerBound == upperBound) { + relevantStates = statesWithProbabilityGreater0; + } else { + // Find the maximal rate of all 'maybe' states to take it as the uniformization rate. + ValueType uniformizationRate = 1.02 * (statesWithProbabilityGreater0NonPsi.toAdd() * exitRates).getMax(); + STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); + + // Compute the (first) uniformized matrix. + uniformizedMatrix = this->computeUniformizedMatrix(this->getModel(), this->getModel().getTransitionMatrix(), exitRates, statesWithProbabilityGreater0NonPsi, uniformizationRate); + + // Create the one-step vector. + storm::dd::Add b = (statesWithProbabilityGreater0NonPsi.toAdd() * this->getModel().getTransitionMatrix() * psiStates.swapVariables(this->getModel().getRowColumnMetaVariablePairs()).toAdd()).sumAbstract(this->getModel().getColumnVariables()) / this->getModel().getManager().getConstant(uniformizationRate); + + // Build an ODD for the relevant states and translate the symbolic parts to their explicit representation. + odd(statesWithProbabilityGreater0NonPsi); + storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); + std::vector explicitB = b.toVector(odd); + + // Compute the transient probabilities. + std::vector values(statesWithProbabilityGreater0NonPsi.getNonZeroCount(), storm::utility::zero()); + std::vector subResult = SparseCtmcCslModelChecker::computeTransientProbabilities(explicitUniformizedMatrix, &explicitB, upperBound - lowerBound, uniformizationRate, values, *this->linearEquationSolverFactory); + + // Transform the explicit result to a hybrid check result, so we can easily convert it to + // a symbolic qualitative format. + HybridQuantitativeCheckResult hybridResult(this->getModel().getReachableStates(), psiStates || (!statesWithProbabilityGreater0 && this->getModel().getReachableStates()), + psiStates.toAdd(), statesWithProbabilityGreater0NonPsi, subResult); + + // Determine the set of states that achieved a strictly positive probability. + std::unique_ptr statesWithValuesGreaterZero = hybridResult.compareAgainstBound(storm::logic::ComparisonType::Greater, storm::utility::zero()); + + // And use it to compute the set of relevant states. + storm::dd::Bdd relevantStates = storm::utility::graph::performProbGreater0(this->getModel(), this->getModel().getTransitionMatrix(), phiStates, statesWithValuesGreaterZero->asSymbolicQualitativeCheckResult().getTruthValuesVector()); + + // Filter the unbounded result such that it only contains values for the relevant states. + hybridResult->filter(SymbolicQualitativeCheckResult(this->getModel().getReachableStates(), relevantStates)); + + // Build an ODD for the relevant states. + odd = storm::dd::Odd(relevantStates); + + std::vector result; + std::unique_ptr explicitResult = hybridResult.toExplicitQuantitativeCheckResult(); + newSubresult = std::move(explicitResult->asExplicitQuantitativeCheckResult().getValueVector()); + } + + // Then compute the transient probabilities of being in such a state after t time units. For this, + // we must re-uniformize the CTMC, so we need to compute the second uniformized matrix. + uniformizationRate = 1.02 * (relevantStates.toAdd() * exitRates).getMax(); + STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); + + // If the lower and upper bounds coincide, we have only determined the relevant states at this + // point, but we still need to construct the starting vector. + if (lowerBound == upperBound) { + newSubresult = psiStates.toAdd().toVector(odd); std::vector(relevantStates.getNonZeroCount()); + } + + // Finally, we compute the second set of transient probabilities. + uniformizedMatrix = this->computeUniformizedMatrix(this->getModel(), this->getModel().getTransitionMatrix(), exitRates, relevantStates, uniformizationRate); + storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); + + newSubresult = SparseCtmcCslModelChecker::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, *this->linearEquationSolverFactory); + + return std::unique_ptr(new HybridQuantitativeCheckResult(this->getModel().getReachableStates(), !relevantStates && this->getModel().getReachableStates(), this->getModel().getManager().getAddZero(), relevantStates, newSubresult)); + } + } + } else { + return std::unique_ptr(new SymbolicQuantitativeCheckResult>(this->getModel().getReachableStates(), psiStates.toAdd())); + } + } + +// template +// std::unique_ptr HybridCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { +// return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeInstantaneousRewardsHelper(rewardPathFormula.getContinuousTimeBound()))); +// } +// +// template +// std::vector HybridCtmcCslModelChecker::computeInstantaneousRewardsHelper(double timeBound) const { +// // Only compute the result if the model has a state-based reward this->getModel(). +// STORM_LOG_THROW(this->getModel().hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); +// +// // Initialize result to state rewards of the this->getModel(). +// std::vector result(this->getModel().getStateRewardVector()); +// +// // If the time-bound is not zero, we need to perform a transient analysis. +// if (timeBound > 0) { +// ValueType uniformizationRate = 0; +// for (auto const& rate : this->getModel().getExitRateVector()) { +// uniformizationRate = std::max(uniformizationRate, rate); +// } +// uniformizationRate *= 1.02; +// STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); +// +// storm::storage::SparseMatrix uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), storm::storage::BitVector(this->getModel().getNumberOfStates(), true), uniformizationRate, this->getModel().getExitRateVector()); +// result = this->computeTransientProbabilities(uniformizedMatrix, nullptr, timeBound, uniformizationRate, result, *this->linearEquationSolverFactory); +// } +// +// return result; +// } +// +// template +// std::unique_ptr HybridCtmcCslModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { +// return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeCumulativeRewardsHelper(rewardPathFormula.getContinuousTimeBound()))); +// } +// +// template +// std::vector HybridCtmcCslModelChecker::computeCumulativeRewardsHelper(double timeBound) const { +// // Only compute the result if the model has a state-based reward this->getModel(). +// STORM_LOG_THROW(this->getModel().hasStateRewards() || this->getModel().hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); +// +// // If the time bound is zero, the result is the constant zero vector. +// if (timeBound == 0) { +// return std::vector(this->getModel().getNumberOfStates(), storm::utility::zero()); +// } +// +// // Otherwise, we need to perform some computations. +// +// // Start with the uniformization. +// ValueType uniformizationRate = 0; +// for (auto const& rate : this->getModel().getExitRateVector()) { +// uniformizationRate = std::max(uniformizationRate, rate); +// } +// uniformizationRate *= 1.02; +// STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); +// +// storm::storage::SparseMatrix uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), storm::storage::BitVector(this->getModel().getNumberOfStates(), true), uniformizationRate, this->getModel().getExitRateVector()); +// +// // Compute the total state reward vector. +// std::vector totalRewardVector; +// if (this->getModel().hasTransitionRewards()) { +// totalRewardVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(this->getModel().getTransitionRewardMatrix()); +// if (this->getModel().hasStateRewards()) { +// storm::utility::vector::addVectors(totalRewardVector, this->getModel().getStateRewardVector(), totalRewardVector); +// } +// } else { +// totalRewardVector = std::vector(this->getModel().getStateRewardVector()); +// } +// +// // Finally, compute the transient probabilities. +// return this->computeTransientProbabilities(uniformizedMatrix, nullptr, timeBound, uniformizationRate, totalRewardVector, *this->linearEquationSolverFactory); +// } + + // Explicitly instantiate the model checker. + template class HybridCtmcCslModelChecker; + + } // namespace modelchecker +} // namespace storm \ No newline at end of file diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.h b/src/modelchecker/csl/HybridCtmcCslModelChecker.h new file mode 100644 index 000000000..ffc2d2694 --- /dev/null +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.h @@ -0,0 +1,96 @@ +#ifndef STORM_MODELCHECKER_HYBRIDCTMCCSLMODELCHECKER_H_ +#define STORM_MODELCHECKER_HYBRIDCTMCCSLMODELCHECKER_H_ + +#include "src/modelchecker/propositional/SymbolicPropositionalModelChecker.h" +#include "src/models/symbolic/Ctmc.h" +#include "src/utility/solver.h" +#include "src/solver/LinearEquationSolver.h" + +namespace storm { + namespace modelchecker { + + template + class HybridCtmcCslModelChecker : public SymbolicPropositionalModelChecker { + public: + explicit HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model); + explicit HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model, std::unique_ptr>&& linearEquationSolverFactory); + + // The implemented methods of the AbstractModelChecker interface. + virtual bool canHandle(storm::logic::Formula const& formula) const override; + virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + + protected: + storm::models::symbolic::Ctmc const& getModel() const override; + + private: + /*! + * Converts the given rate-matrix into a time-abstract probability matrix. + * + * @param model The symbolic model. + * @param rateMatrix The rate matrix. + * @param exitRateVector The exit rate vector of the model. + * @return The probability matrix. + */ + static storm::dd::Add computeProbabilityMatrix(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector); + + /*! + * Computes the matrix representing the transitions of the uniformized CTMC. + * + * @param model The symbolic model. + * @param transitionMatrix The matrix to uniformize. + * @param exitRateVector The exit rate vector. + * @param maybeStates The states that need to be considered. + * @param uniformizationRate The rate to be used for uniformization. + * @return The uniformized matrix. + */ + static storm::dd::Add computeUniformizedMatrix(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& maybeStates, ValueType uniformizationRate); + + // The methods that perform the actual checking. + std::unique_ptr computeBoundedUntilProbabilitiesHelper(storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Add const& exitRates, bool qualitative, double lowerBound, double upperBound) const; + +// std::vector computeBoundedUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound) const; +// std::vector computeInstantaneousRewardsHelper(double timeBound) const; +// std::vector computeCumulativeRewardsHelper(double timeBound) const; +// std::vector computeReachabilityRewardsHelper(storm::storage::BitVector const& targetStates, bool qualitative) const; +// +// /*! +// * Computes the matrix representing the transitions of the uniformized CTMC. +// * +// * @param transitionMatrix The matrix to uniformize. +// * @param maybeStates The states that need to be considered. +// * @param uniformizationRate The rate to be used for uniformization. +// * @param exitRates The exit rates of all states. +// * @return The uniformized matrix. +// */ +// static storm::storage::SparseMatrix computeUniformizedMatrix(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates, ValueType uniformizationRate, std::vector const& exitRates); +// +// /*! +// * Computes the transient probabilities for lambda time steps. +// * +// * @param uniformizedMatrix The uniformized transition matrix. +// * @param addVector A vector that is added in each step as a possible compensation for removing absorbing states +// * with a non-zero initial value. If this is not supposed to be used, it can be set to nullptr. +// * @param timeBound The time bound to use. +// * @param uniformizationRate The used uniformization rate. +// * @param values A vector mapping each state to an initial probability. +// * @param linearEquationSolverFactory The factory to use when instantiating new linear equation solvers. +// * @param useMixedPoissonProbabilities If set to true, instead of taking the poisson probabilities, mixed +// * poisson probabilities are used. +// * @return The vector of transient probabilities. +// */ +// template +// std::vector computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, std::vector const* addVector, ValueType timeBound, ValueType uniformizationRate, std::vector values, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) const; + + // An object that is used for solving linear equations and performing matrix-vector multiplication. + std::unique_ptr> linearEquationSolverFactory; + }; + + } // namespace modelchecker +} // namespace storm + +#endif /* STORM_MODELCHECKER_HYBRIDCTMCCSLMODELCHECKER_H_ */ diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 74540327b..0a1a71c42 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -49,9 +49,7 @@ namespace storm { upperBound = pathFormula.getDiscreteTimeBound(); } - std::unique_ptr result = std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeBoundedUntilProbabilitiesHelper(leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), qualitative, lowerBound, upperBound))); - - return result; + return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeBoundedUntilProbabilitiesHelper(leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), qualitative, lowerBound, upperBound))); } template @@ -192,7 +190,7 @@ namespace storm { // Start by computing the transient probabilities of reaching a psi state in time t' - t. std::vector values(statesWithProbabilityGreater0NonPsi.getNumberOfSetBits(), storm::utility::zero()); - std::vector subresult = this->computeTransientProbabilities(uniformizedMatrix, &b, upperBound - lowerBound, uniformizationRate, values, *this->linearEquationSolverFactory); + std::vector subresult = computeTransientProbabilities(uniformizedMatrix, &b, upperBound - lowerBound, uniformizationRate, values, *this->linearEquationSolverFactory); // Determine the set of states that must be considered further. relevantStates = storm::utility::vector::filterGreaterZero(subresult); @@ -215,12 +213,12 @@ namespace storm { // point, but we still need to construct the starting vector. if (lowerBound == upperBound) { newSubresult = std::vector(relevantStates.getNumberOfSetBits()); - storm::utility::vector::setVectorValues(newSubresult, psiStates % statesWithProbabilityGreater0, storm::utility::one()); + storm::utility::vector::setVectorValues(newSubresult, psiStates % relevantStates, storm::utility::one()); } // Finally, we compute the second set of transient probabilities. uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), relevantStates, uniformizationRate, exitRates); - newSubresult = this->computeTransientProbabilities(uniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, *this->linearEquationSolverFactory); + newSubresult = computeTransientProbabilities(uniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, *this->linearEquationSolverFactory); // Fill in the correct values. result = std::vector(this->getModel().getNumberOfStates(), storm::utility::zero()); @@ -249,7 +247,7 @@ namespace storm { for (auto const& state : maybeStates) { for (auto& element : uniformizedMatrix.getRow(currentRow)) { if (element.getColumn() == currentRow) { - element.setValue(-(exitRates[state] - element.getValue()) / uniformizationRate + storm::utility::one()); + element.setValue((element.getValue() - exitRates[state]) / uniformizationRate + storm::utility::one()); } else { element.setValue(element.getValue() / uniformizationRate); } @@ -262,7 +260,7 @@ namespace storm { template template - std::vector SparseCtmcCslModelChecker::computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, std::vector const* addVector, ValueType timeBound, ValueType uniformizationRate, std::vector values, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) const { + std::vector SparseCtmcCslModelChecker::computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, std::vector const* addVector, ValueType timeBound, ValueType uniformizationRate, std::vector values, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { ValueType lambda = timeBound * uniformizationRate; diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/modelchecker/csl/SparseCtmcCslModelChecker.h index b74967ac5..ffa89f904 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -3,12 +3,16 @@ #include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "src/models/sparse/Ctmc.h" +#include "src/storage/dd/DdType.h" #include "src/utility/solver.h" #include "src/solver/LinearEquationSolver.h" namespace storm { namespace modelchecker { + template + class HybridCtmcCslModelChecker; + template class SparseCtmcCslModelChecker : public SparsePropositionalModelChecker { public: @@ -33,7 +37,6 @@ namespace storm { static std::vector computeUntilProbabilitiesHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); std::vector computeInstantaneousRewardsHelper(double timeBound) const; std::vector computeCumulativeRewardsHelper(double timeBound) const; - std::vector computeReachabilityRewardsHelper(storm::storage::BitVector const& targetStates, bool qualitative) const; /*! * Computes the matrix representing the transitions of the uniformized CTMC. @@ -61,7 +64,7 @@ namespace storm { * @return The vector of transient probabilities. */ template - std::vector computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, std::vector const* addVector, ValueType timeBound, ValueType uniformizationRate, std::vector values, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) const; + static std::vector computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, std::vector const* addVector, ValueType timeBound, ValueType uniformizationRate, std::vector values, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); /*! * Converts the given rate-matrix into a time-abstract probability matrix. diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index 4ddda3339..231c17a94 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -235,9 +235,10 @@ namespace storm { } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeReachabilityRewardsHelper(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& targetStates, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, bool qualitative) { - // Only compute the result if the model has at least one reward model. - STORM_LOG_THROW(model.hasStateRewards() || model.hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); + std::unique_ptr HybridDtmcPrctlModelChecker::computeReachabilityRewardsHelper(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, boost::optional> const& stateRewardVector, boost::optional> const& transitionRewardMatrix, storm::dd::Bdd const& targetStates, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, bool qualitative) { + + // Only compute the result if there is at least one reward model. + STORM_LOG_THROW(stateRewardVector || transitionRewardMatrix, storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); // Determine which states have a reward of infinity by definition. storm::dd::Bdd infinityStates = storm::utility::graph::performProb1(model, transitionMatrix.notZero(), model.getReachableStates(), targetStates); @@ -266,9 +267,9 @@ namespace storm { storm::dd::Add submatrix = transitionMatrix * maybeStatesAdd; // Then compute the state reward vector to use in the computation. - storm::dd::Add subvector = model.hasStateRewards() ? maybeStatesAdd * model.getStateRewardVector() : model.getManager().getAddZero(); - if (model.hasTransitionRewards()) { - subvector += (submatrix * model.getTransitionRewardMatrix()).sumAbstract(model.getColumnVariables()); + storm::dd::Add subvector = stateRewardVector ? maybeStatesAdd * stateRewardVector.get() : model.getManager().getAddZero(); + if (transitionRewardMatrix) { + subvector += (submatrix * transitionRewardMatrix.get()).sumAbstract(model.getColumnVariables()); } // Finally cut away all columns targeting non-maybe states and convert the matrix into the matrix needed diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h index bb7a263a9..b3ab51279 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h @@ -7,9 +7,14 @@ namespace storm { namespace modelchecker { + template + class HybridCtmcCslModelChecker; + template class HybridDtmcPrctlModelChecker : public SymbolicPropositionalModelChecker { public: + friend class HybridCtmcCslModelChecker; + explicit HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model); explicit HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model, std::unique_ptr>&& linearEquationSolverFactory); @@ -32,7 +37,7 @@ namespace storm { static std::unique_ptr computeUntilProbabilitiesHelper(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); static std::unique_ptr computeCumulativeRewardsHelper(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); static std::unique_ptr computeInstantaneousRewardsHelper(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeReachabilityRewardsHelper(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& targetStates, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, bool qualitative); + static std::unique_ptr computeReachabilityRewardsHelper(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, boost::optional> const& stateRewardVector, boost::optional> const& transitionRewardMatrix, storm::dd::Bdd const& targetStates, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, bool qualitative); // An object that is used for retrieving linear equation solvers. std::unique_ptr> linearEquationSolverFactory; diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp index 8132b75b6..7019786ad 100644 --- a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp @@ -1,5 +1,6 @@ #include "src/modelchecker/results/HybridQuantitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/storage/dd/CuddDdManager.h" #include "src/exceptions/InvalidOperationException.h" @@ -32,6 +33,16 @@ namespace storm { return std::unique_ptr>(new SymbolicQualitativeCheckResult(reachableStates, symbolicResult)); } + template + std::unique_ptr HybridQuantitativeCheckResult::toExplicitQuantitativeCheckResult() const { + storm::dd::Bdd allStates = symbolicStates || explicitStates; + storm::dd::Odd allStatesOdd(allStates); + + std::vector fullExplicitValues = symbolicValues.template toVector(allStatesOdd); + this->odd.expandExplicitVector(allStatesOdd, this->explicitValues, fullExplicitValues); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(fullExplicitValues))); + } + template bool HybridQuantitativeCheckResult::isHybrid() const { return true; diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.h b/src/modelchecker/results/HybridQuantitativeCheckResult.h index 160bbbb6d..05033f78f 100644 --- a/src/modelchecker/results/HybridQuantitativeCheckResult.h +++ b/src/modelchecker/results/HybridQuantitativeCheckResult.h @@ -25,6 +25,8 @@ namespace storm { virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const override; + std::unique_ptr toExplicitQuantitativeCheckResult() const; + virtual bool isHybrid() const override; virtual bool isResultForAllStates() const override; diff --git a/src/models/symbolic/Ctmc.cpp b/src/models/symbolic/Ctmc.cpp index b90aa5afd..01f4cb4d7 100644 --- a/src/models/symbolic/Ctmc.cpp +++ b/src/models/symbolic/Ctmc.cpp @@ -18,7 +18,12 @@ namespace storm { boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix) : DeterministicModel(storm::models::ModelType::Ctmc, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, optionalStateRewardVector, optionalTransitionRewardMatrix) { - // Intentionally left empty. + exitRates = this->getTransitionMatrix().sumAbstract(this->getColumnVariables()); + } + + template + storm::dd::Add const& Ctmc::getExitRateVector() const { + return exitRates; } // Explicitly instantiate the template class. diff --git a/src/models/symbolic/Ctmc.h b/src/models/symbolic/Ctmc.h index 7d46dcd73..e2f975f76 100644 --- a/src/models/symbolic/Ctmc.h +++ b/src/models/symbolic/Ctmc.h @@ -52,6 +52,16 @@ namespace storm { std::map labelToExpressionMap = std::map(), boost::optional> const& optionalStateRewardVector = boost::optional>(), boost::optional> const& optionalTransitionRewardMatrix = boost::optional>()); + + /*! + * Retrieves the exit rate vector of the CTMC. + * + * @return The exit rate vector. + */ + storm::dd::Add const& getExitRateVector() const; + + private: + storm::dd::Add exitRates; }; } // namespace symbolic diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp index 0fe4f0d13..8b72f3687 100644 --- a/src/models/symbolic/Model.cpp +++ b/src/models/symbolic/Model.cpp @@ -87,11 +87,21 @@ namespace storm { return transitionRewardMatrix.get(); } + template + boost::optional> const& Model::getOptionalTransitionRewardMatrix() const { + return transitionRewardMatrix; + } + template storm::dd::Add const& Model::getStateRewardVector() const { return stateRewardVector.get(); } + template + boost::optional> const& Model::getOptionalStateRewardVector() const { + return stateRewardVector; + } + template bool Model::hasStateRewards() const { return static_cast(stateRewardVector); diff --git a/src/models/symbolic/Model.h b/src/models/symbolic/Model.h index 211a4cc66..23d2030f3 100644 --- a/src/models/symbolic/Model.h +++ b/src/models/symbolic/Model.h @@ -134,6 +134,13 @@ namespace storm { */ storm::dd::Add& getTransitionMatrix(); + /*! + * Retrieves the (optional) matrix representing the transition rewards of the model. + * + * @return The matrix representing the transition rewards of the model. + */ + boost::optional> const& getOptionalTransitionRewardMatrix() const; + /*! * Retrieves the matrix representing the transition rewards of the model. Note that calling this method * is only valid if the model has transition rewards. @@ -157,6 +164,13 @@ namespace storm { * @return A vector representing the state rewards of the model. */ storm::dd::Add const& getStateRewardVector() const; + + /*! + * Retrieves an (optional) vector representing the state rewards of the model. + * + * @return A vector representing the state rewards of the model. + */ + boost::optional> const& getOptionalStateRewardVector() const; /*! * Retrieves whether this model has state rewards. diff --git a/src/storage/dd/CuddOdd.cpp b/src/storage/dd/CuddOdd.cpp index 46ed679b6..d78882b2f 100644 --- a/src/storage/dd/CuddOdd.cpp +++ b/src/storage/dd/CuddOdd.cpp @@ -106,6 +106,20 @@ namespace storm { return result; } + void Odd::expandExplicitVector(storm::dd::Odd const& newOdd, std::vector const& oldValues, std::vector& newValues) const { + expandValuesToVectorRec(0, *this, oldValues, 0, newOdd, newValues); + } + + void Odd::expandValuesToVectorRec(uint_fast64_t oldOffset, storm::dd::Odd const& oldOdd, std::vector const& oldValues, uint_fast64_t newOffset, storm::dd::Odd const& newOdd, std::vector& newValues) { + if (oldOdd.isTerminalNode()) { + STORM_LOG_THROW(newOdd.isTerminalNode(), storm::exceptions::InvalidArgumentException, "The ODDs for the translation must have the same height."); + newValues[newOffset] += oldValues[oldOffset]; + } else { + expandValuesToVectorRec(oldOffset, oldOdd.getElseSuccessor(), oldValues, newOffset, newOdd.getElseSuccessor(), newValues); + expandValuesToVectorRec(oldOffset + oldOdd.getElseOffset(), oldOdd.getThenSuccessor(), oldValues, newOffset + newOdd.getElseOffset(), newOdd.getThenSuccessor(), newValues); + } + } + void Odd::addSelectedValuesToVectorRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector& result, uint_fast64_t& currentIndex, std::vector const& values) { // If there are no more values to select, we can directly return. if (dd == Cudd_ReadLogicZero(manager.getManager()) && !complement) { diff --git a/src/storage/dd/CuddOdd.h b/src/storage/dd/CuddOdd.h index 4a03a3c26..e00bdd2c7 100644 --- a/src/storage/dd/CuddOdd.h +++ b/src/storage/dd/CuddOdd.h @@ -112,6 +112,16 @@ namespace storm { */ std::vector filterExplicitVector(storm::dd::Bdd const& selectedValues, std::vector const& values) const; + /*! + * Adds the old values to the new values. It does so by writing the old values at their correct positions + * wrt. to the new ODD. + * + * @param newOdd The new ODD to use. + * @param oldValues The old vector of values (which is being read). + * @param newValues The new vector of values (which is being written). + */ + void expandExplicitVector(storm::dd::Odd const& newOdd, std::vector const& oldValues, std::vector& newValues) const; + private: // Declare a hash functor that is used for the unique tables in the construction process. class HashFunctor { @@ -159,7 +169,6 @@ namespace storm { */ static std::shared_ptr> buildOddFromBddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector, std::shared_ptr>, HashFunctor>>& uniqueTableForLevels); - /*! * Adds the selected values the target vector. * @@ -176,6 +185,19 @@ namespace storm { */ static void addSelectedValuesToVectorRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector& result, uint_fast64_t& currentIndex, std::vector const& values); + /*! + * Adds the values of the old explicit values to the new explicit values where the positions in the old vector + * are given by the current old ODD and the positions in the new vector are given by the new ODD. + * + * @param oldOffset The offset in the old explicit values. + * @param oldOdd The ODD to use for the old explicit values. + * @param oldValues The vector of old values. + * @param newOffset The offset in the new explicit values. + * @param newOdd The ODD to use for the new explicit values. + * @param newValues The vector of new values. + */ + static void expandValuesToVectorRec(uint_fast64_t oldOffset, storm::dd::Odd const& oldOdd, std::vector const& oldValues, uint_fast64_t newOffset, storm::dd::Odd const& newOdd, std::vector& newValues); + // The then- and else-nodes. std::shared_ptr> elseNode; std::shared_ptr> thenNode;