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<storm::dd::DdType DdType, class ValueType>
+ HybridCtmcCslModelChecker<DdType, ValueType>::HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc<DdType> const& model) : SymbolicPropositionalModelChecker<DdType>(model), linearEquationSolverFactory(new storm::utility::solver::LinearEquationSolverFactory<ValueType>()) {
+ // Intentionally left empty.
+ }
+
+ template<storm::dd::DdType DdType, class ValueType>
+ HybridCtmcCslModelChecker<DdType, ValueType>::HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc<DdType> const& model, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker<DdType>(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) {
+ // Intentionally left empty.
+ }
+
+ template<storm::dd::DdType DdType, class ValueType>
+ bool HybridCtmcCslModelChecker<DdType, ValueType>::canHandle(storm::logic::Formula const& formula) const {
+ return formula.isCslStateFormula() || formula.isCslPathFormula() || formula.isRewardPathFormula();
+ }
+
+ template<storm::dd::DdType DdType, class ValueType>
+ storm::dd::Add<DdType> HybridCtmcCslModelChecker<DdType, ValueType>::computeProbabilityMatrix(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& rateMatrix, storm::dd::Add<DdType> const& exitRateVector) {
+ return rateMatrix / exitRateVector.swapVariables(model.getRowColumnMetaVariablePairs());
+ }
+
+ template<storm::dd::DdType DdType, class ValueType>
+ std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<DdType, ValueType>::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+ std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
+ std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
+ SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>();
+ SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>();
+
+ return HybridDtmcPrctlModelChecker<DdType, ValueType>::computeUntilProbabilitiesHelper(this->getModel(), this->computeProbabilityMatrix(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory);
+ }
+
+ template<storm::dd::DdType DdType, class ValueType>
+ std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<DdType, ValueType>::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+ std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula());
+ SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
+ return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), HybridDtmcPrctlModelChecker<DdType, ValueType>::computeNextProbabilitiesHelper(this->getModel(), this->computeProbabilityMatrix(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()), subResult.getTruthValuesVector())));
+ }
+
+ template<storm::dd::DdType DdType, class ValueType>
+ storm::models::symbolic::Ctmc<DdType> const& HybridCtmcCslModelChecker<DdType, ValueType>::getModel() const {
+ return this->template getModelAs<storm::models::symbolic::Ctmc<DdType>>();
+ }
+
+ template<storm::dd::DdType DdType, class ValueType>
+ storm::dd::Add<DdType> HybridCtmcCslModelChecker<DdType, ValueType>::computeUniformizedMatrix(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Add<DdType> const& exitRateVector, storm::dd::Bdd<DdType> 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<DdType> uniformizedMatrix = transitionMatrix * maybeStates.toAdd() * maybeStates.swapVariables(model.getRowColumnMetaVariablePairs()).toAdd();
+
+ // Now perform the uniformization.
+ uniformizedMatrix = uniformizedMatrix / model.getManager().getConstant(uniformizationRate);
+ storm::dd::Add<DdType> diagonalOffset = model.getRowColumnIdentity();
+ diagonalOffset -= model.getRowColumnIdentity() * (exitRateVector / model.getManager().getConstant(uniformizationRate));
+ uniformizedMatrix = uniformizedMatrix + diagonalOffset;
+
+ return uniformizedMatrix;
+ }
+
+ template<storm::dd::DdType DdType, class ValueType>
+ std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<DdType, ValueType>::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+ std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula());
+ SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
+
+ boost::optional<storm::dd::Add<DdType>> modifiedStateRewardVector;
+ if (this->getModel().hasStateRewards()) {
+ modifiedStateRewardVector = this->getModel().getStateRewardVector() / this->getModel().getTransitionMatrix().sumAbstract(this->getModel().getColumnVariables());
+ }
+
+ return HybridDtmcPrctlModelChecker<DdType, ValueType>::computeReachabilityRewardsHelper(this->getModel(), this->computeProbabilityMatrix(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()), modifiedStateRewardVector, this->getModel().getOptionalTransitionRewardMatrix(), subResult.getTruthValuesVector(), *linearEquationSolverFactory, qualitative);
+ }
+
+ template<storm::dd::DdType DdType, class ValueType>
+ std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<DdType, ValueType>::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+ std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
+ std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
+ SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>();
+ SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>();
+ double lowerBound = 0;
+ double upperBound = 0;
+ if (!pathFormula.hasDiscreteTimeBound()) {
+ std::pair<double, double> 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<storm::dd::DdType DdType, class ValueType>
+ std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<DdType, ValueType>::computeBoundedUntilProbabilitiesHelper(storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, storm::dd::Add<DdType> const& exitRates, bool qualitative, double lowerBound, double upperBound) const {
+ // If the time bounds are [0, inf], we rather call untimed reachability.
+ storm::utility::ConstantsComparator<ValueType> comparator;
+ if (comparator.isZero(lowerBound) && comparator.isInfinity(upperBound)) {
+ return HybridDtmcPrctlModelChecker<DdType, ValueType>::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<DdType> 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<DdType> 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<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>(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<DdType> 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<DdType> 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<DdType> odd(statesWithProbabilityGreater0NonPsi);
+
+ // Convert the symbolic parts to their explicit representation.
+ storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
+ std::vector<ValueType> explicitB = b.template toVector<ValueType>(odd);
+
+ // Finally compute the transient probabilities.
+ std::vector<ValueType> values(statesWithProbabilityGreater0NonPsi.getNonZeroCount(), storm::utility::zero<ValueType>());
+ std::vector<ValueType> subresult = SparseCtmcCslModelChecker<ValueType>::computeTransientProbabilities(explicitUniformizedMatrix, &explicitB, upperBound, uniformizationRate, values, *this->linearEquationSolverFactory);
+
+ return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(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<CheckResult> unboundedResult = HybridDtmcPrctlModelChecker<DdType, ValueType>::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<CheckResult> statesWithValuesGreaterZero = unboundedResult->asQuantitativeCheckResult().compareAgainstBound(storm::logic::ComparisonType::Greater, storm::utility::zero<ValueType>());
+
+ // And use it to compute the set of relevant states.
+ storm::dd::Bdd<DdType> relevantStates = storm::utility::graph::performProbGreater0(this->getModel(), this->getModel().getTransitionMatrix(), phiStates, statesWithValuesGreaterZero->asSymbolicQualitativeCheckResult<DdType>().getTruthValuesVector());
+
+ // Filter the unbounded result such that it only contains values for the relevant states.
+ unboundedResult->filter(SymbolicQualitativeCheckResult<DdType>(this->getModel().getReachableStates(), relevantStates));
+
+ // Build an ODD for the relevant states.
+ storm::dd::Odd<DdType> odd(relevantStates);
+
+ std::vector<ValueType> result;
+ if (unboundedResult->isHybridQuantitativeCheckResult()) {
+ std::unique_ptr<CheckResult> explicitUnboundedResult = unboundedResult->asHybridQuantitativeCheckResult<DdType>().toExplicitQuantitativeCheckResult();
+ result = std::move(explicitUnboundedResult->asExplicitQuantitativeCheckResult<ValueType>().getValueVector());
+ } else {
+ STORM_LOG_THROW(unboundedResult->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidStateException, "Expected check result of different type.");
+ result = unboundedResult->asSymbolicQuantitativeCheckResult<DdType>().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<DdType> uniformizedMatrix = this->computeUniformizedMatrix(this->getModel(), this->getModel().getTransitionMatrix(), exitRates, relevantStates, uniformizationRate);
+ storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
+
+ // Compute the transient probabilities.
+ std::vector<ValueType> subResult = SparseCtmcCslModelChecker<ValueType>::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, subResult, *this->linearEquationSolverFactory);
+
+ return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(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<DdType> relevantStates;
+ ValueType uniformizationRate = 0;
+ storm::dd::Add<DdType> uniformizedMatrix;
+ std::vector<ValueType> newSubresult;
+ storm::dd::Odd<DdType> 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<DdType> 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<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
+ std::vector<ValueType> explicitB = b.toVector(odd);
+
+ // Compute the transient probabilities.
+ std::vector<ValueType> values(statesWithProbabilityGreater0NonPsi.getNonZeroCount(), storm::utility::zero<ValueType>());
+ std::vector<ValueType> subResult = SparseCtmcCslModelChecker<ValueType>::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<DdType> 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<CheckResult> statesWithValuesGreaterZero = hybridResult.compareAgainstBound(storm::logic::ComparisonType::Greater, storm::utility::zero<ValueType>());
+
+ // And use it to compute the set of relevant states.
+ storm::dd::Bdd<DdType> relevantStates = storm::utility::graph::performProbGreater0(this->getModel(), this->getModel().getTransitionMatrix(), phiStates, statesWithValuesGreaterZero->asSymbolicQualitativeCheckResult<DdType>().getTruthValuesVector());
+
+ // Filter the unbounded result such that it only contains values for the relevant states.
+ hybridResult->filter(SymbolicQualitativeCheckResult<DdType>(this->getModel().getReachableStates(), relevantStates));
+
+ // Build an ODD for the relevant states.
+ odd = storm::dd::Odd<DdType>(relevantStates);
+
+ std::vector<ValueType> result;
+ std::unique_ptr<CheckResult> explicitResult = hybridResult.toExplicitQuantitativeCheckResult();
+ newSubresult = std::move(explicitResult->asExplicitQuantitativeCheckResult<ValueType>().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<ValueType>(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<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
+
+ newSubresult = SparseCtmcCslModelChecker<ValueType>::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, *this->linearEquationSolverFactory);
+
+ return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), !relevantStates && this->getModel().getReachableStates(), this->getModel().getManager().getAddZero(), relevantStates, newSubresult));
+ }
+ }
+ } else {
+ return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>>(this->getModel().getReachableStates(), psiStates.toAdd()));
+ }
+ }
+
+// template<storm::dd::DdType DdType, class ValueType>
+// std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<DdType, ValueType>::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+// return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeInstantaneousRewardsHelper(rewardPathFormula.getContinuousTimeBound())));
+// }
+//
+// template<storm::dd::DdType DdType, class ValueType>
+// std::vector<ValueType> HybridCtmcCslModelChecker<DdType, ValueType>::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<ValueType> 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<ValueType> 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<storm::dd::DdType DdType, class ValueType>
+// std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<DdType, ValueType>::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+// return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeCumulativeRewardsHelper(rewardPathFormula.getContinuousTimeBound())));
+// }
+//
+// template<storm::dd::DdType DdType, class ValueType>
+// std::vector<ValueType> HybridCtmcCslModelChecker<DdType, ValueType>::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<ValueType>(this->getModel().getNumberOfStates(), storm::utility::zero<ValueType>());
+// }
+//
+// // 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<ValueType> 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<ValueType> 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<ValueType>(this->getModel().getStateRewardVector());
+// }
+//
+// // Finally, compute the transient probabilities.
+// return this->computeTransientProbabilities<true>(uniformizedMatrix, nullptr, timeBound, uniformizationRate, totalRewardVector, *this->linearEquationSolverFactory);
+// }
+
+ // Explicitly instantiate the model checker.
+ template class HybridCtmcCslModelChecker<storm::dd::DdType::CUDD, double>;
+
+ } // 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<storm::dd::DdType DdType, class ValueType>
+ class HybridCtmcCslModelChecker : public SymbolicPropositionalModelChecker<DdType> {
+ public:
+ explicit HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc<DdType> const& model);
+ explicit HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc<DdType> const& model, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory);
+
+ // The implemented methods of the AbstractModelChecker interface.
+ virtual bool canHandle(storm::logic::Formula const& formula) const override;
+ virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
+ virtual std::unique_ptr<CheckResult> computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
+ virtual std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
+ virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
+ virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
+ virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
+
+ protected:
+ storm::models::symbolic::Ctmc<DdType> 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<DdType> computeProbabilityMatrix(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& rateMatrix, storm::dd::Add<DdType> 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<DdType> computeUniformizedMatrix(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Add<DdType> const& exitRateVector, storm::dd::Bdd<DdType> const& maybeStates, ValueType uniformizationRate);
+
+ // The methods that perform the actual checking.
+ std::unique_ptr<CheckResult> computeBoundedUntilProbabilitiesHelper(storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, storm::dd::Add<DdType> const& exitRates, bool qualitative, double lowerBound, double upperBound) const;
+
+// std::vector<ValueType> computeBoundedUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<ValueType> const& exitRates, bool qualitative, double lowerBound, double upperBound) const;
+// std::vector<ValueType> computeInstantaneousRewardsHelper(double timeBound) const;
+// std::vector<ValueType> computeCumulativeRewardsHelper(double timeBound) const;
+// std::vector<ValueType> 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<ValueType> computeUniformizedMatrix(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates, ValueType uniformizationRate, std::vector<ValueType> 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<bool useMixedPoissonProbabilities = false>
+// std::vector<ValueType> computeTransientProbabilities(storm::storage::SparseMatrix<ValueType> const& uniformizedMatrix, std::vector<ValueType> const* addVector, ValueType timeBound, ValueType uniformizationRate, std::vector<ValueType> values, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) const;
+
+ // An object that is used for solving linear equations and performing matrix-vector multiplication.
+ std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<ValueType>> 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<CheckResult> result = std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeBoundedUntilProbabilitiesHelper(leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), qualitative, lowerBound, upperBound)));
-
- return result;
+ return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeBoundedUntilProbabilitiesHelper(leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), qualitative, lowerBound, upperBound)));
}
template<class ValueType>
@@ -192,7 +190,7 @@ namespace storm {
// Start by computing the transient probabilities of reaching a psi state in time t' - t.
std::vector<ValueType> values(statesWithProbabilityGreater0NonPsi.getNumberOfSetBits(), storm::utility::zero<ValueType>());
- std::vector<ValueType> subresult = this->computeTransientProbabilities(uniformizedMatrix, &b, upperBound - lowerBound, uniformizationRate, values, *this->linearEquationSolverFactory);
+ std::vector<ValueType> 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<ValueType>(relevantStates.getNumberOfSetBits());
- storm::utility::vector::setVectorValues(newSubresult, psiStates % statesWithProbabilityGreater0, storm::utility::one<ValueType>());
+ storm::utility::vector::setVectorValues(newSubresult, psiStates % relevantStates, storm::utility::one<ValueType>());
}
// 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<ValueType>(this->getModel().getNumberOfStates(), storm::utility::zero<ValueType>());
@@ -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<ValueType>());
+ element.setValue((element.getValue() - exitRates[state]) / uniformizationRate + storm::utility::one<ValueType>());
} else {
element.setValue(element.getValue() / uniformizationRate);
}
@@ -262,7 +260,7 @@ namespace storm {
template<class ValueType>
template<bool computeCumulativeReward>
- std::vector<ValueType> SparseCtmcCslModelChecker<ValueType>::computeTransientProbabilities(storm::storage::SparseMatrix<ValueType> const& uniformizedMatrix, std::vector<ValueType> const* addVector, ValueType timeBound, ValueType uniformizationRate, std::vector<ValueType> values, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) const {
+ std::vector<ValueType> SparseCtmcCslModelChecker<ValueType>::computeTransientProbabilities(storm::storage::SparseMatrix<ValueType> const& uniformizedMatrix, std::vector<ValueType> const* addVector, ValueType timeBound, ValueType uniformizationRate, std::vector<ValueType> values, storm::utility::solver::LinearEquationSolverFactory<ValueType> 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<storm::dd::DdType DdType, typename ValueType>
+ class HybridCtmcCslModelChecker;
+
template<class ValueType>
class SparseCtmcCslModelChecker : public SparsePropositionalModelChecker<ValueType> {
public:
@@ -33,7 +37,6 @@ namespace storm {
static std::vector<ValueType> computeUntilProbabilitiesHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
std::vector<ValueType> computeInstantaneousRewardsHelper(double timeBound) const;
std::vector<ValueType> computeCumulativeRewardsHelper(double timeBound) const;
- std::vector<ValueType> 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<bool useMixedPoissonProbabilities = false>
- std::vector<ValueType> computeTransientProbabilities(storm::storage::SparseMatrix<ValueType> const& uniformizedMatrix, std::vector<ValueType> const* addVector, ValueType timeBound, ValueType uniformizationRate, std::vector<ValueType> values, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) const;
+ static std::vector<ValueType> computeTransientProbabilities(storm::storage::SparseMatrix<ValueType> const& uniformizedMatrix, std::vector<ValueType> const* addVector, ValueType timeBound, ValueType uniformizationRate, std::vector<ValueType> values, storm::utility::solver::LinearEquationSolverFactory<ValueType> 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<storm::dd::DdType DdType, typename ValueType>
- std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeReachabilityRewardsHelper(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& targetStates, storm::utility::solver::LinearEquationSolverFactory<ValueType> 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<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeReachabilityRewardsHelper(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, boost::optional<storm::dd::Add<DdType>> const& stateRewardVector, boost::optional<storm::dd::Add<DdType>> const& transitionRewardMatrix, storm::dd::Bdd<DdType> const& targetStates, storm::utility::solver::LinearEquationSolverFactory<ValueType> 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<DdType> infinityStates = storm::utility::graph::performProb1(model, transitionMatrix.notZero(), model.getReachableStates(), targetStates);
@@ -266,9 +267,9 @@ namespace storm {
storm::dd::Add<DdType> submatrix = transitionMatrix * maybeStatesAdd;
// Then compute the state reward vector to use in the computation.
- storm::dd::Add<DdType> subvector = model.hasStateRewards() ? maybeStatesAdd * model.getStateRewardVector() : model.getManager().getAddZero();
- if (model.hasTransitionRewards()) {
- subvector += (submatrix * model.getTransitionRewardMatrix()).sumAbstract(model.getColumnVariables());
+ storm::dd::Add<DdType> 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<storm::dd::DdType DdType, typename ValueType>
+ class HybridCtmcCslModelChecker;
+
template<storm::dd::DdType DdType, typename ValueType>
class HybridDtmcPrctlModelChecker : public SymbolicPropositionalModelChecker<DdType> {
public:
+ friend class HybridCtmcCslModelChecker<DdType, ValueType>;
+
explicit HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc<DdType> const& model);
explicit HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc<DdType> const& model, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory);
@@ -32,7 +37,7 @@ namespace storm {
static std::unique_ptr<CheckResult> computeUntilProbabilitiesHelper(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::unique_ptr<CheckResult> computeCumulativeRewardsHelper(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::unique_ptr<CheckResult> computeInstantaneousRewardsHelper(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
- static std::unique_ptr<CheckResult> computeReachabilityRewardsHelper(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& targetStates, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, bool qualitative);
+ static std::unique_ptr<CheckResult> computeReachabilityRewardsHelper(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, boost::optional<storm::dd::Add<DdType>> const& stateRewardVector, boost::optional<storm::dd::Add<DdType>> const& transitionRewardMatrix, storm::dd::Bdd<DdType> const& targetStates, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, bool qualitative);
// An object that is used for retrieving linear equation solvers.
std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<ValueType>> 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<SymbolicQualitativeCheckResult<Type>>(new SymbolicQualitativeCheckResult<Type>(reachableStates, symbolicResult));
}
+ template<storm::dd::DdType Type>
+ std::unique_ptr<CheckResult> HybridQuantitativeCheckResult<Type>::toExplicitQuantitativeCheckResult() const {
+ storm::dd::Bdd<Type> allStates = symbolicStates || explicitStates;
+ storm::dd::Odd<Type> allStatesOdd(allStates);
+
+ std::vector<double> fullExplicitValues = symbolicValues.template toVector<double>(allStatesOdd);
+ this->odd.expandExplicitVector(allStatesOdd, this->explicitValues, fullExplicitValues);
+ return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<double>(std::move(fullExplicitValues)));
+ }
+
template<storm::dd::DdType Type>
bool HybridQuantitativeCheckResult<Type>::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<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const override;
+ std::unique_ptr<CheckResult> 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<storm::dd::Add<Type>> const& optionalStateRewardVector,
boost::optional<storm::dd::Add<Type>> const& optionalTransitionRewardMatrix)
: DeterministicModel<Type>(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::DdType Type>
+ storm::dd::Add<Type> const& Ctmc<Type>::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<std::string, storm::expressions::Expression> labelToExpressionMap = std::map<std::string, storm::expressions::Expression>(),
boost::optional<storm::dd::Add<Type>> const& optionalStateRewardVector = boost::optional<storm::dd::Dd<Type>>(),
boost::optional<storm::dd::Add<Type>> const& optionalTransitionRewardMatrix = boost::optional<storm::dd::Dd<Type>>());
+
+ /*!
+ * Retrieves the exit rate vector of the CTMC.
+ *
+ * @return The exit rate vector.
+ */
+ storm::dd::Add<Type> const& getExitRateVector() const;
+
+ private:
+ storm::dd::Add<Type> 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<storm::dd::DdType Type>
+ boost::optional<storm::dd::Add<Type>> const& Model<Type>::getOptionalTransitionRewardMatrix() const {
+ return transitionRewardMatrix;
+ }
+
template<storm::dd::DdType Type>
storm::dd::Add<Type> const& Model<Type>::getStateRewardVector() const {
return stateRewardVector.get();
}
+ template<storm::dd::DdType Type>
+ boost::optional<storm::dd::Add<Type>> const& Model<Type>::getOptionalStateRewardVector() const {
+ return stateRewardVector;
+ }
+
template<storm::dd::DdType Type>
bool Model<Type>::hasStateRewards() const {
return static_cast<bool>(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<Type>& getTransitionMatrix();
+ /*!
+ * Retrieves the (optional) matrix representing the transition rewards of the model.
+ *
+ * @return The matrix representing the transition rewards of the model.
+ */
+ boost::optional<storm::dd::Add<Type>> 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<Type> 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<storm::dd::Add<Type>> 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<DdType::CUDD>::expandExplicitVector(storm::dd::Odd<DdType::CUDD> const& newOdd, std::vector<double> const& oldValues, std::vector<double>& newValues) const {
+ expandValuesToVectorRec(0, *this, oldValues, 0, newOdd, newValues);
+ }
+
+ void Odd<DdType::CUDD>::expandValuesToVectorRec(uint_fast64_t oldOffset, storm::dd::Odd<DdType::CUDD> const& oldOdd, std::vector<double> const& oldValues, uint_fast64_t newOffset, storm::dd::Odd<DdType::CUDD> const& newOdd, std::vector<double>& 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<DdType::CUDD>::addSelectedValuesToVectorRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd<DdType::CUDD> const& odd, std::vector<double>& result, uint_fast64_t& currentIndex, std::vector<double> 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<double> filterExplicitVector(storm::dd::Bdd<DdType::CUDD> const& selectedValues, std::vector<double> 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<DdType::CUDD> const& newOdd, std::vector<double> const& oldValues, std::vector<double>& 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<Odd<DdType::CUDD>> buildOddFromBddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<std::pair<DdNode*, bool>, std::shared_ptr<Odd<DdType::CUDD>>, 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<uint_fast64_t> const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd<DdType::CUDD> const& odd, std::vector<double>& result, uint_fast64_t& currentIndex, std::vector<double> 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<DdType::CUDD> const& oldOdd, std::vector<double> const& oldValues, uint_fast64_t newOffset, storm::dd::Odd<DdType::CUDD> const& newOdd, std::vector<double>& newValues);
+
// The then- and else-nodes.
std::shared_ptr<Odd<DdType::CUDD>> elseNode;
std::shared_ptr<Odd<DdType::CUDD>> thenNode;