diff --git a/src/storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.cpp index 4ef4b4542..5a9f61b66 100644 --- a/src/storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.cpp @@ -4,6 +4,7 @@ #include "storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h" #include "storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.h" +#include "storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -26,7 +27,7 @@ namespace storm { template bool HybridMarkovAutomatonCslModelChecker::canHandleStatic(CheckTask const& checkTask) { - auto singleObjectiveFragment = storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setRewardAccumulationAllowed(true).setInstantaneousFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false); + auto singleObjectiveFragment = storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(false).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(false).setLongRunAverageRewardFormulasAllowed(false).setRewardAccumulationAllowed(true).setInstantaneousFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false); if (!storm::NumberTraits::SupportsExponential) { singleObjectiveFragment.setBoundedUntilFormulasAllowed(false); } @@ -38,17 +39,18 @@ namespace storm { return canHandleStatic(checkTask); } -/* template + template std::unique_ptr HybridMarkovAutomatonCslModelChecker::computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) { + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridMarkovAutomatonCslHelper::computeUntilProbabilities(env, this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getMarkovianStates(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet()); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeUntilProbabilities(env, checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet()); } - */ + template std::unique_ptr HybridMarkovAutomatonCslModelChecker::computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); @@ -59,24 +61,26 @@ namespace storm { return storm::modelchecker::helper::HybridMarkovAutomatonCslHelper::computeReachabilityRewards(env, checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getMarkovianStates(), this->getModel().getExitRateVector(), rewardModel.get(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); } - /* template + template std::unique_ptr HybridMarkovAutomatonCslModelChecker::computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); storm::models::symbolic::StandardRewardModel timeRewardModel(this->getModel().getManager().getConstant(storm::utility::one()), boost::none, boost::none); - return storm::modelchecker::helper::HybridMarkovAutomatonCslHelper::computeReachabilityRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getMarkovianStates(), this->getModel().getExitRateVector(), timeRewardModel, subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); + return storm::modelchecker::helper::HybridMarkovAutomatonCslHelper::computeReachabilityRewards(env, checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getMarkovianStates(), this->getModel().getExitRateVector(), timeRewardModel, subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); } template std::unique_ptr HybridMarkovAutomatonCslModelChecker::computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); - std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); + STORM_LOG_THROW(pathFormula.getLeftSubformula().isTrueFormula(), storm::exceptions::NotImplementedException, "Only bounded properties of the form 'true U[t1, t2] phi' are currently supported."); std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); - SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(pathFormula.getTimeBoundReference().isTimeBound(), storm::exceptions::NotImplementedException, "Currently step-bounded and reward-bounded properties on MarkovAutomatons are not supported."); double lowerBound = 0; double upperBound = 0; @@ -89,24 +93,9 @@ namespace storm { upperBound = storm::utility::infinity(); } - return storm::modelchecker::helper::HybridMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(env, this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getMarkovianStates(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), lowerBound, upperBound); + return storm::modelchecker::helper::HybridMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(env, checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getMarkovianStates(), this->getModel().getExitRateVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), lowerBound, upperBound); } - template - std::unique_ptr HybridMarkovAutomatonCslModelChecker::computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) { - storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); - std::unique_ptr subResultPointer = this->check(env, stateFormula); - SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - - return storm::modelchecker::helper::HybridMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(env, this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getMarkovianStates(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector()); - } - - template - std::unique_ptr HybridMarkovAutomatonCslModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { - auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); - return storm::modelchecker::helper::HybridMarkovAutomatonCslHelper::computeLongRunAverageRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getMarkovianStates(), this->getModel().getExitRateVector(), rewardModel.get()); - } - */ // Explicitly instantiate the model checker. template class HybridMarkovAutomatonCslModelChecker>; template class HybridMarkovAutomatonCslModelChecker>; diff --git a/src/storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.h b/src/storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.h index e7c293b95..2790f13ef 100644 --- a/src/storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.h +++ b/src/storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.h @@ -23,16 +23,10 @@ namespace storm { // The implemented methods of the AbstractModelChecker interface. static bool canHandleStatic(CheckTask const& checkTask); virtual bool canHandle(CheckTask const& checkTask) const override; - /* virtual std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; - virtual std::unique_ptr computeNextProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; - virtual std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; - - virtual std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeInstantaneousRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - */ virtual std::unique_ptr computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - //virtual std::unique_ptr computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; }; diff --git a/src/storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.cpp index d1a2bb761..e265ab864 100644 --- a/src/storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.cpp @@ -44,222 +44,40 @@ namespace storm { return HybridMdpPrctlHelper::computeReachabilityRewards(env, dir, model, transitionMatrix, discretizedRewardModel, targetStates, qualitative); } - /* - template - std::unique_ptr HybridMarkovAutomatonCslHelper::computeUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative) { - return HybridMdpPrctlHelper::computeUntilProbabilities(env, model, computeProbabilityMatrix(rateMatrix, exitRateVector), phiStates, psiStates, qualitative); - } template::SupportsExponential, int>::type> - std::unique_ptr HybridMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound) { - + std::unique_ptr HybridMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, OptimizationDirection dir, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& markovianStates, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound) { // If the time bounds are [0, inf], we rather call untimed reachability. if (storm::utility::isZero(lowerBound) && upperBound == storm::utility::infinity()) { - return computeUntilProbabilities(env, model, rateMatrix, exitRateVector, phiStates, psiStates, qualitative); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeUntilProbabilities(env, dir, model, transitionMatrix, psiStates.getDdManager().getBddOne(), psiStates, qualitative); + } + // If the interval is of the form [0,0], we can return the result directly + if (storm::utility::isZero(upperBound)) { + // In this case, the interval is of the form [0, 0]. + return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), psiStates.template toAdd())); } - // 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(model, rateMatrix.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 we reach this point, we convert this query to an instance for the sparse engine. + storm::utility::Stopwatch conversionWatch(true); + // Create ODD for the translation. + storm::dd::Odd odd = model.getReachableStates().createOdd(); + storm::storage::SparseMatrix explicitTransitionMatrix = transitionMatrix.toMatrix(model.getNondeterminismVariables(), odd, odd); + std::vector explicitExitRateVector = exitRateVector.toVector(odd); + conversionWatch.stop(); + STORM_LOG_INFO("Converting symbolic matrix to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms."); - if (!statesWithProbabilityGreater0NonPsi.isZero()) { - if (storm::utility::isZero(upperBound)) { - // In this case, the interval is of the form [0, 0]. - return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), psiStates.template toAdd())); - } else { - if (storm::utility::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.template toAdd() * exitRateVector).getMax(); - STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); - - // Compute the uniformized matrix. - storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, statesWithProbabilityGreater0NonPsi, uniformizationRate); - - // Compute the vector that is to be added as a compensation for removing the absorbing states. - storm::dd::Add b = (statesWithProbabilityGreater0NonPsi.template toAdd() * rateMatrix * psiStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd()).sumAbstract(model.getColumnVariables()) / model.getManager().getConstant(uniformizationRate); - - storm::utility::Stopwatch conversionWatch(true); - - // Create an ODD for the translation to an explicit representation. - storm::dd::Odd odd = statesWithProbabilityGreater0NonPsi.createOdd(); - - // Convert the symbolic parts to their explicit representation. - storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); - std::vector explicitB = b.toVector(odd); - conversionWatch.stop(); - STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms."); - - // Finally compute the transient probabilities. - std::vector values(statesWithProbabilityGreater0NonPsi.getNonZeroCount(), storm::utility::zero()); - std::vector subresult = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeTransientProbabilities(env, explicitUniformizedMatrix, &explicitB, upperBound, uniformizationRate, values); - - return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), - (psiStates || !statesWithProbabilityGreater0) && model.getReachableStates(), - psiStates.template toAdd(), statesWithProbabilityGreater0NonPsi, odd, subresult)); - } else if (upperBound == storm::utility::infinity()) { - // 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 = computeUntilProbabilities(env, model, rateMatrix, exitRateVector, phiStates, psiStates, qualitative); - - // Compute the set of relevant states. - storm::dd::Bdd relevantStates = statesWithProbabilityGreater0 && phiStates; - - // Filter the unbounded result such that it only contains values for the relevant states. - unboundedResult->filter(SymbolicQualitativeCheckResult(model.getReachableStates(), relevantStates)); - - storm::utility::Stopwatch conversionWatch; - - // Build an ODD for the relevant states. - conversionWatch.start(); - storm::dd::Odd odd = relevantStates.createOdd(); - conversionWatch.stop(); - - std::vector result; - if (unboundedResult->isHybridQuantitativeCheckResult()) { - conversionWatch.start(); - std::unique_ptr explicitUnboundedResult = unboundedResult->asHybridQuantitativeCheckResult().toExplicitQuantitativeCheckResult(); - conversionWatch.stop(); - 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.template toAdd() * exitRateVector).getMax(); - - // Compute the uniformized matrix. - storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, relevantStates, uniformizationRate); - conversionWatch.start(); - storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); - conversionWatch.stop(); - STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms."); - - // Compute the transient probabilities. - result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeTransientProbabilities(env, explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, result); - - return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), !relevantStates && model.getReachableStates(), model.getManager().template getAddZero(), relevantStates, odd, result)); - } else { - // In this case, the interval is of the form [t, t'] with t != 0 and t' != inf. - - if (lowerBound != upperBound) { - // In this case, the interval is of the form [t, t'] with t != 0, t' != inf and t != t'. - - // Find the maximal rate of all 'maybe' states to take it as the uniformization rate. - ValueType uniformizationRate = 1.02 * (statesWithProbabilityGreater0NonPsi.template toAdd() * exitRateVector).getMax(); - STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); - - // Compute the (first) uniformized matrix. - storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, statesWithProbabilityGreater0NonPsi, uniformizationRate); - - // Create the one-step vector. - storm::dd::Add b = (statesWithProbabilityGreater0NonPsi.template toAdd() * rateMatrix * psiStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd()).sumAbstract(model.getColumnVariables()) / model.getManager().getConstant(uniformizationRate); - - // Build an ODD for the relevant states and translate the symbolic parts to their explicit representation. - storm::utility::Stopwatch conversionWatch(true); - storm::dd::Odd odd = statesWithProbabilityGreater0NonPsi.createOdd(); - storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); - std::vector explicitB = b.toVector(odd); - conversionWatch.stop(); - - // Compute the transient probabilities. - std::vector values(statesWithProbabilityGreater0NonPsi.getNonZeroCount(), storm::utility::zero()); - std::vector subResult = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeTransientProbabilities(env, explicitUniformizedMatrix, &explicitB, upperBound - lowerBound, uniformizationRate, values); - - // Transform the explicit result to a hybrid check result, so we can easily convert it to - // a symbolic qualitative format. - HybridQuantitativeCheckResult hybridResult(model.getReachableStates(), psiStates || (!statesWithProbabilityGreater0 && model.getReachableStates()), - psiStates.template toAdd(), statesWithProbabilityGreater0NonPsi, odd, subResult); - - // Compute the set of relevant states. - storm::dd::Bdd relevantStates = statesWithProbabilityGreater0 && phiStates; - - // Filter the unbounded result such that it only contains values for the relevant states. - hybridResult.filter(SymbolicQualitativeCheckResult(model.getReachableStates(), relevantStates)); - - // Build an ODD for the relevant states. - conversionWatch.start(); - odd = relevantStates.createOdd(); - - std::unique_ptr explicitResult = hybridResult.toExplicitQuantitativeCheckResult(); - conversionWatch.stop(); - std::vector 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 MarkovAutomaton, so we need to compute the second uniformized matrix. - uniformizationRate = 1.02 * (relevantStates.template toAdd() * exitRateVector).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) { - odd = relevantStates.createOdd(); - newSubresult = psiStates.template toAdd().toVector(odd); - } - - // Finally, we compute the second set of transient probabilities. - uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, relevantStates, uniformizationRate); - conversionWatch.start(); - explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); - conversionWatch.stop(); - STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms."); - - newSubresult = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeTransientProbabilities(env, explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult); - - return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), !relevantStates && model.getReachableStates(), model.getManager().template getAddZero(), relevantStates, odd, newSubresult)); - } else { - // In this case, the interval is of the form [t, t] with t != 0, t != inf. - - storm::utility::Stopwatch conversionWatch; - - // Build an ODD for the relevant states. - conversionWatch.start(); - storm::dd::Odd odd = statesWithProbabilityGreater0.createOdd(); - - std::vector newSubresult = psiStates.template toAdd().toVector(odd); - conversionWatch.stop(); - - // Then compute the transient probabilities of being in such a state after t time units. For this, - // we must re-uniformize the MarkovAutomaton, so we need to compute the second uniformized matrix. - ValueType uniformizationRate = 1.02 * (statesWithProbabilityGreater0.template toAdd() * exitRateVector).getMax(); - STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); - - // Finally, we compute the second set of transient probabilities. - storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, statesWithProbabilityGreater0, uniformizationRate); - conversionWatch.start(); - storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); - conversionWatch.stop(); - STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms."); - - newSubresult = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeTransientProbabilities(env, explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult); - - return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), !statesWithProbabilityGreater0 && model.getReachableStates(), model.getManager().template getAddZero(), statesWithProbabilityGreater0, odd, newSubresult)); - } - } - } - } else { - return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), psiStates.template toAdd())); - } + auto explicitResult = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(env, dir, explicitTransitionMatrix, explicitExitRateVector, markovianStates.toVector(odd), psiStates.toVector(odd), {lowerBound, upperBound}); + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(explicitResult))); } template::SupportsExponential, int>::type> - std::unique_ptr HybridMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound) { + std::unique_ptr HybridMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const&, OptimizationDirection, storm::models::symbolic::MarkovAutomaton const&, storm::dd::Add const&, storm::dd::Bdd const&, storm::dd::Add const&, storm::dd::Bdd const&, bool, double, double) { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded until probabilities is unsupported for this value type."); + } - template + /* template std::unique_ptr HybridMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates) { storm::utility::Stopwatch conversionWatch(true); @@ -303,24 +121,21 @@ namespace storm { // Cudd, double. template std::unique_ptr HybridMarkovAutomatonCslHelper::computeReachabilityRewards(Environment const& env, OptimizationDirection dir, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& markovianStates, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative); + template std::unique_ptr HybridMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, OptimizationDirection dir, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& markovianStates, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound); /* - template std::unique_ptr HybridMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound); - template std::unique_ptr HybridMarkovAutomatonCslHelper::computeUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative); template std::unique_ptr HybridMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates); template std::unique_ptr HybridMarkovAutomatonCslHelper::computeLongRunAverageRewards(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel); */ // Sylvan, double. template std::unique_ptr HybridMarkovAutomatonCslHelper::computeReachabilityRewards(Environment const& env, OptimizationDirection dir, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& markovianStates, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative); - /* template std::unique_ptr HybridMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound); - template std::unique_ptr HybridMarkovAutomatonCslHelper::computeUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative); - template std::unique_ptr HybridMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates); + template std::unique_ptr HybridMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, OptimizationDirection dir, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& markovianStates, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound); + /* template std::unique_ptr HybridMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates); template std::unique_ptr HybridMarkovAutomatonCslHelper::computeLongRunAverageRewards(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel); */ // Sylvan, rational number. template std::unique_ptr HybridMarkovAutomatonCslHelper::computeReachabilityRewards(Environment const& env, OptimizationDirection dir, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& markovianStates, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative); - /* template std::unique_ptr HybridMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound); - template std::unique_ptr HybridMarkovAutomatonCslHelper::computeUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative); - template std::unique_ptr HybridMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates); + template std::unique_ptr HybridMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, OptimizationDirection dir, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& markovianStates, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound); + /* template std::unique_ptr HybridMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates); template std::unique_ptr HybridMarkovAutomatonCslHelper::computeLongRunAverageRewards(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel); */ diff --git a/src/storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.h b/src/storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.h index 30f04956e..098669bcc 100644 --- a/src/storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.h +++ b/src/storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.h @@ -21,22 +21,11 @@ namespace storm { template static std::unique_ptr computeReachabilityRewards(Environment const& env, OptimizationDirection dir, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& markovianStates, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative); - /* template::SupportsExponential, int>::type = 0> - static std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound); + static std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, OptimizationDirection dir, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& markovianStates, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound); template::SupportsExponential, int>::type = 0> - static std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound); - - template - static std::unique_ptr computeUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative); - - template - static std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates); - - template - static std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel); - */ + static std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, OptimizationDirection dir, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& markovianStates, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound); };