From 9be488b9698e11fdf3f654f7a4d19e6960d08c9c Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 25 Oct 2018 14:48:21 +0200 Subject: [PATCH] Enabling expected time queries for ctmcs in the hybrid engine. --- .../csl/HybridCtmcCslModelChecker.cpp | 17 ++++++++++++++--- .../csl/HybridCtmcCslModelChecker.h | 1 + .../csl/SparseCtmcCslModelChecker.cpp | 2 +- 3 files changed, 16 insertions(+), 4 deletions(-) diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp index b7b71dfaa..6e41f2782 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -7,6 +7,7 @@ #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "storm/storage/dd/DdManager.h" #include "storm/storage/dd/Add.h" #include "storm/storage/dd/Bdd.h" @@ -30,14 +31,14 @@ namespace storm { template::SupportsExponential, int>::type> bool HybridCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true)); + return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTimeOperatorsAllowed(true)); } template template::SupportsExponential, int>::type> bool HybridCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false)); + return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTimeOperatorsAllowed(true).setBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false)); } template @@ -60,7 +61,6 @@ namespace storm { return storm::modelchecker::helper::HybridCtmcCslHelper::computeNextProbabilities(env, this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector()); } - template std::unique_ptr HybridCtmcCslModelChecker::computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); @@ -70,6 +70,17 @@ namespace storm { return storm::modelchecker::helper::HybridCtmcCslHelper::computeReachabilityRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); } + template + std::unique_ptr HybridCtmcCslModelChecker::computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { + 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::HybridCtmcCslHelper::computeReachabilityRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), timeRewardModel, subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); + } + + template std::unique_ptr HybridCtmcCslModelChecker::computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h index f66f3c10e..eaa55d42e 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h @@ -32,6 +32,7 @@ namespace storm { 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; private: template::SupportsExponential, int>::type = 0> diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 08fc02cad..cf2aa5bcb 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -44,7 +44,7 @@ namespace storm { template::SupportsExponential, int>::type> bool SparseCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTotalRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false)); + return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTotalRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false)); } template