diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index a9b86d8c8..b7e42e1db 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -108,7 +108,7 @@ namespace storm { std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeExpectedTimes(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), this->getModel().getInitialStates(), subResult.getTruthValuesVector(), qualitative/*, *linearEquationSolverFactory*/); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeExpectedTimes(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), this->getModel().getInitialStates(), subResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index a8471c990..ae656b5ee 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -195,6 +195,12 @@ namespace storm { return SparseDtmcPrctlHelper::computeUntilProbabilities(computeProbabilityMatrix(rateMatrix, exitRateVector), backwardTransitions, phiStates, psiStates, qualitative, linearEquationSolverFactory); } + template + std::vector SparseCtmcCslHelper::computeUntilProbabilitiesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) { + // Use "normal" function again, if RationalFunction finally is supported. + return storm::modelchecker::SparseDtmcEliminationModelChecker>::computeUntilProbabilities(computeProbabilityMatrix(rateMatrix, exitRateVector), backwardTransitions, initialStates, phiStates, psiStates, false); + } + template std::vector SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { return SparseDtmcPrctlHelper::computeNextProbabilities(computeProbabilityMatrix(rateMatrix, exitRateVector), nextStates, linearEquationSolverFactory); @@ -648,9 +654,31 @@ namespace storm { return result; } + + template + std::vector SparseCtmcCslHelper::computeExpectedTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + // Compute expected time on CTMC by reduction to DTMC with rewards. + storm::storage::SparseMatrix probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); + + // Initialize rewards. + std::vector totalRewardVector; + for (size_t i = 0; i < exitRateVector.size(); ++i) { + if (targetStates[i]) { + // Set reward for target states to 0. + totalRewardVector.push_back(storm::utility::zero()); + } else { + // Reward is (1 / exitRate). + totalRewardVector.push_back(storm::utility::one() / exitRateVector[i]); + } + } + + return storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(probabilityMatrix, backwardTransitions, totalRewardVector, targetStates, qualitative, linearEquationSolverFactory); + } + template - std::vector SparseCtmcCslHelper::computeExpectedTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative/*, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory*/) { + std::vector SparseCtmcCslHelper::computeExpectedTimesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative) { + // Use "normal" function again, if RationalFunction finally is supported. // Compute expected time on CTMC by reduction to DTMC with rewards. storm::storage::SparseMatrix probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); @@ -667,8 +695,6 @@ namespace storm { } return storm::modelchecker::SparseDtmcEliminationModelChecker>::computeReachabilityRewards(probabilityMatrix, backwardTransitions, initialStates, targetStates, totalRewardVector, false, qualitative); - // Enable again, if RationalFunction finally is supported. - //return storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(probabilityMatrix, backwardTransitions, totalRewardVector, targetStates, qualitative, linearEquationSolverFactory); } template class SparseCtmcCslHelper; @@ -677,7 +703,8 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); #ifdef STORM_HAVE_CARL - template std::vector SparseCtmcCslHelper::computeExpectedTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative/*, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory*/); + template std::vector SparseCtmcCslHelper::computeUntilProbabilitiesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative); + template std::vector SparseCtmcCslHelper::computeExpectedTimesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative); #endif } } diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.h b/src/modelchecker/csl/helper/SparseCtmcCslHelper.h index 94752a974..14a98f752 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.h +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.h @@ -16,6 +16,7 @@ namespace storm { static std::vector computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); static std::vector computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeUntilProbabilitiesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative); template static std::vector computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); @@ -28,7 +29,8 @@ namespace storm { static std::vector computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeExpectedTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative/*, storm::utility::solver::LinearEquationSolverFactory const& minMaxLinearEquationSolverFactory*/); + static std::vector computeExpectedTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeExpectedTimesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative); /*! * Computes the matrix representing the transitions of the uniformized CTMC. diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 41324957b..279ef5089 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -512,66 +512,74 @@ namespace storm { template std::unique_ptr SparseDtmcEliminationModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + // Retrieve the appropriate bitvectors by model checking the subformulas. std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); storm::storage::BitVector const& phiStates = leftResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); storm::storage::BitVector const& psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); - + + std::vector result = computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), phiStates, psiStates, this->computeResultsForInitialStatesOnly); + + // Construct check result. + std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); + return checkResult; + } + + template + std::vector SparseDtmcEliminationModelChecker::computeUntilProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool computeForInitialStatesOnly) { + // Then, compute the subset of states that has a probability of 0 or 1, respectively. - std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->getModel(), phiStates, psiStates); + std::pair statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates); storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first; storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second; storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); // Determine whether we need to perform some further computation. bool furtherComputationNeeded = true; - if (computeResultsForInitialStatesOnly && this->getModel().getInitialStates().isDisjointFrom(maybeStates)) { + if (computeForInitialStatesOnly && initialStates.isDisjointFrom(maybeStates)) { STORM_LOG_DEBUG("The probability for all initial states was found in a preprocessing step."); furtherComputationNeeded = false; } else if (maybeStates.empty()) { STORM_LOG_DEBUG("The probability for all states was found in a preprocessing step."); furtherComputationNeeded = false; } - + std::vector result(maybeStates.size()); if (furtherComputationNeeded) { // If we compute the results for the initial states only, we can cut off all maybe state that are not // reachable from them. - if (computeResultsForInitialStatesOnly) { + if (computeForInitialStatesOnly) { // Determine the set of states that is reachable from the initial state without jumping over a target state. - storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), maybeStates, statesWithProbability1); + storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(probabilityMatrix, initialStates, maybeStates, statesWithProbability1); // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). maybeStates &= reachableStates; } - + // Create a vector for the probabilities to go to a state with probability 1 in one step. - std::vector oneStepProbabilities = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1); - + std::vector oneStepProbabilities = probabilityMatrix.getConstrainedRowSumVector(maybeStates, statesWithProbability1); + // Determine the set of initial states of the sub-model. - storm::storage::BitVector newInitialStates = this->getModel().getInitialStates() % maybeStates; - + storm::storage::BitVector newInitialStates = initialStates % maybeStates; + // We then build the submatrix that only has the transitions of the maybe states. - storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); + storm::storage::SparseMatrix submatrix = probabilityMatrix.getSubmatrix(false, maybeStates, maybeStates); storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); - - std::vector subresult = computeReachabilityValues(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, computeResultsForInitialStatesOnly, phiStates, psiStates, oneStepProbabilities); + + std::vector subresult = computeReachabilityValues(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, computeForInitialStatesOnly, phiStates, psiStates, oneStepProbabilities); storm::utility::vector::setVectorValues(result, maybeStates, subresult); } // Construct full result. storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::zero()); storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::one()); - - // Construct check result based on whether we have computed values for all states or just the initial states. - std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); - if (computeResultsForInitialStatesOnly) { + if (computeForInitialStatesOnly) { // If we computed the results for the initial (and prob 0 and prob1) states only, we need to filter the // result to only communicate these results. - checkResult->filter(ExplicitQualitativeCheckResult(~maybeStates | this->getModel().getInitialStates())); + result = storm::utility::vector::filterVector(result, ~maybeStates | initialStates); } - return checkResult; + return result; } template @@ -588,7 +596,7 @@ namespace storm { STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model."); std::vector result = computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), targetStates, stateRewardValues, this->computeResultsForInitialStatesOnly, qualitative, optimalityType); - // Construct check result + // Construct check result. std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); return checkResult; } diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index a840cef88..5b000b4f2 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -25,12 +25,19 @@ namespace storm { // 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 computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + static std::vector computeUntilProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool computeForInitialStatesOnly); + virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::vector const& stateRewardValues, bool computeForInitialStatesOnly, bool qualitative, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeLongRunAverageRewards(storm::logic::LongRunAverageRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; private: diff --git a/src/utility/storm.h b/src/utility/storm.h index 4bdf22556..2b08aa6ae 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -332,17 +332,51 @@ namespace storm { } else if (model->getType() == storm::models::ModelType::Ctmc) { // Hack to avoid instantiating the CTMC Model Checker which currently does not work for rational functions if (formula->isExpectedTimeOperatorFormula()) { - // We can only solve expected time for pCTMCs at the moment - std::shared_ptr> ctmc = model->template as>(); + // Compute expected time for pCTMCs + STORM_LOG_THROW(formula->asExpectedTimeOperatorFormula().getSubformula().isEventuallyFormula(), storm::exceptions::NotSupportedException, "The parametric engine only supports Eventually formulas for this property"); + storm::logic::EventuallyFormula eventuallyFormula = formula->asExpectedTimeOperatorFormula().getSubformula().asEventuallyFormula(); + STORM_LOG_THROW(eventuallyFormula.getSubformula().isPropositionalFormula(), storm::exceptions::NotSupportedException, "The parametric engine does not support nested formulas on CTMCs"); // Compute goal states - storm::logic::EventuallyFormula eventuallyFormula = formula->asExpectedTimeOperatorFormula().getSubformula().asEventuallyFormula(); + std::shared_ptr> ctmc = model->template as>(); storm::modelchecker::SparsePropositionalModelChecker> propositionalModelchecker(*ctmc); std::unique_ptr subResultPointer = propositionalModelchecker.check(eventuallyFormula.getSubformula()); - storm::modelchecker::ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + storm::storage::BitVector const& targetStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeExpectedTimes(ctmc->getTransitionMatrix(), ctmc->getBackwardTransitions(), ctmc->getExitRateVector(), ctmc->getInitialStates(), subResult.getTruthValuesVector(), false); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeExpectedTimesElimination(ctmc->getTransitionMatrix(), ctmc->getBackwardTransitions(), ctmc->getExitRateVector(), ctmc->getInitialStates(), targetStates, false); result = std::unique_ptr(new storm::modelchecker::ExplicitQuantitativeCheckResult(std::move(numericResult))); + + } else if (formula->isProbabilityOperatorFormula()) { + // Compute reachability probability for pCTMCs + storm::logic::ProbabilityOperatorFormula probOpFormula = formula->asProbabilityOperatorFormula(); + STORM_LOG_THROW(probOpFormula.getSubformula().isUntilFormula() || probOpFormula.getSubformula().isEventuallyFormula(), storm::exceptions::NotSupportedException, "The parametric engine only supports Until formulas for this property"); + + // Compute phi and psi states + std::shared_ptr> ctmc = model->template as>(); + storm::modelchecker::SparsePropositionalModelChecker> propositionalModelchecker(*ctmc); + storm::storage::BitVector phiStates(model->getNumberOfStates(), true); + storm::storage::BitVector psiStates; + if (probOpFormula.getSubformula().isUntilFormula()) { + // Until formula + storm::logic::UntilFormula untilFormula = formula->asProbabilityOperatorFormula().getSubformula().asUntilFormula(); + STORM_LOG_THROW(untilFormula.getLeftSubformula().isPropositionalFormula(), storm::exceptions::NotSupportedException, "The parametric engine does not support nested formulas on CTMCs"); + STORM_LOG_THROW(untilFormula.getRightSubformula().isPropositionalFormula(), storm::exceptions::NotSupportedException, "The parametric engine does not support nested formulas on CTMCs"); + std::unique_ptr leftResultPointer = propositionalModelchecker.check(untilFormula.getLeftSubformula()); + std::unique_ptr rightResultPointer = propositionalModelchecker.check(untilFormula.getRightSubformula()); + phiStates = leftResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); + psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); + } else { + // Eventually formula + assert(probOpFormula.getSubformula().isEventuallyFormula()); + storm::logic::EventuallyFormula eventuallyFormula = probOpFormula.getSubformula().asEventuallyFormula(); + STORM_LOG_THROW(eventuallyFormula.getSubformula().isPropositionalFormula(), storm::exceptions::NotSupportedException, "The parametric engine does not support nested formulas on CTMCs"); + std::unique_ptr resultPointer = propositionalModelchecker.check(eventuallyFormula.getSubformula()); + psiStates = resultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); + } + + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeUntilProbabilitiesElimination(ctmc->getTransitionMatrix(), ctmc->getBackwardTransitions(), ctmc->getExitRateVector(), ctmc->getInitialStates(), phiStates, psiStates, false); + result = std::unique_ptr(new storm::modelchecker::ExplicitQuantitativeCheckResult(std::move(numericResult))); + } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The parametric engine currently does not support this property on CTMCs."); }