From 0332935451c3343e6662a908353b11496078e8f9 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 6 Aug 2018 13:40:31 +0200 Subject: [PATCH] Supporting TimeOperatorFormulas for MDPs and DTMCs in Sparse, Hybrid, and Dd engine --- .../prctl/HybridDtmcPrctlModelChecker.cpp | 11 ++++++++++- .../prctl/HybridDtmcPrctlModelChecker.h | 1 + .../prctl/HybridMdpPrctlModelChecker.cpp | 11 ++++++++++- .../prctl/HybridMdpPrctlModelChecker.h | 1 + .../prctl/SparseDtmcPrctlModelChecker.cpp | 11 ++++++++++- .../prctl/SparseDtmcPrctlModelChecker.h | 2 +- .../prctl/SparseMdpPrctlModelChecker.cpp | 16 +++++++++++++++- .../prctl/SparseMdpPrctlModelChecker.h | 1 + .../prctl/SymbolicDtmcPrctlModelChecker.cpp | 12 +++++++++++- .../prctl/SymbolicDtmcPrctlModelChecker.h | 2 +- .../prctl/SymbolicMdpPrctlModelChecker.cpp | 11 ++++++++++- .../prctl/SymbolicMdpPrctlModelChecker.h | 2 +- .../prctl/helper/HybridDtmcPrctlHelper.cpp | 6 ++++++ .../prctl/helper/HybridDtmcPrctlHelper.h | 2 ++ .../prctl/helper/HybridMdpPrctlHelper.cpp | 7 +++++++ .../prctl/helper/HybridMdpPrctlHelper.h | 2 ++ .../prctl/helper/SparseDtmcPrctlHelper.cpp | 15 +++++++++++++++ .../prctl/helper/SparseDtmcPrctlHelper.h | 2 ++ .../prctl/helper/SparseMdpPrctlHelper.cpp | 16 ++++++++++++++++ .../prctl/helper/SparseMdpPrctlHelper.h | 2 ++ .../prctl/helper/SymbolicDtmcPrctlHelper.cpp | 6 ++++++ .../prctl/helper/SymbolicDtmcPrctlHelper.h | 2 ++ .../prctl/helper/SymbolicMdpPrctlHelper.cpp | 7 +++++++ .../prctl/helper/SymbolicMdpPrctlHelper.h | 2 ++ src/storm/storage/jani/JSONExporter.cpp | 12 ++++++++---- 25 files changed, 149 insertions(+), 13 deletions(-) diff --git a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index 94b7ca4e1..0654a9788 100644 --- a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -33,7 +33,7 @@ namespace storm { template bool HybridDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true)); + return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true)); } template @@ -95,6 +95,15 @@ namespace storm { SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeReachabilityRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); } + + template + std::unique_ptr HybridDtmcPrctlModelChecker::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(); + + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeReachabilityTimes(env, this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); + } template diff --git a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h index d76ae69ac..854fae195 100644 --- a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h @@ -31,6 +31,7 @@ namespace storm { virtual std::unique_ptr computeCumulativeRewards(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 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/prctl/HybridMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index 6ae7ea4bc..9af47c767 100644 --- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -39,7 +39,7 @@ namespace storm { template bool HybridMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - if(formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false))) { + if (formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true))) { return true; } else { // Check whether we consider a multi-objective formula @@ -117,6 +117,15 @@ namespace storm { SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); return storm::modelchecker::helper::HybridMdpPrctlHelper::computeReachabilityRewards(env, checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); } + + template + std::unique_ptr HybridMdpPrctlModelChecker::computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { + storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); + SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeReachabilityTimes(env, checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); + } template std::unique_ptr HybridMdpPrctlModelChecker::checkMultiObjectiveFormula(Environment const& env, CheckTask const& checkTask) { diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h index 246a991d5..68eb12baa 100644 --- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h @@ -35,6 +35,7 @@ namespace storm { virtual std::unique_ptr computeCumulativeRewards(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 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 checkMultiObjectiveFormula(Environment const& env, CheckTask const& checkTask) override; }; diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 082ddd813..f561d3e98 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -31,7 +31,7 @@ namespace storm { template bool SparseDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true)); + return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true)); } template @@ -124,6 +124,15 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } + template + std::unique_ptr SparseDtmcPrctlModelChecker::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()); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityTimes(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.getHint()); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } + template std::unique_ptr SparseDtmcPrctlModelChecker::computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeTotalRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), checkTask.isQualitativeSet(), checkTask.getHint()); diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 6500da487..1aafc0efb 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -33,7 +33,7 @@ namespace storm { virtual std::unique_ptr computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeConditionalRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageRewards(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; }; } // namespace modelchecker diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index ba5aac431..b78ad3856 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -38,7 +38,7 @@ namespace storm { template bool SparseMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - if (formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true))) { + if (formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true))) { return true; } else { // Check whether we consider a multi-objective formula @@ -173,6 +173,20 @@ namespace storm { return result; } + template + std::unique_ptr SparseMdpPrctlModelChecker::computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { + storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeReachabilityTimes(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), checkTask.getHint()); + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); + if (checkTask.isProduceSchedulersSet() && ret.scheduler) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); + } + return result; + } + template std::unique_ptr SparseMdpPrctlModelChecker::computeTotalRewards(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."); diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 5667549e3..19c2cc6a1 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -29,6 +29,7 @@ namespace storm { virtual std::unique_ptr computeInstantaneousRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeTotalRewards(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 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 checkMultiObjectiveFormula(Environment const& env, CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index e8af30350..a6a099833 100644 --- a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -30,7 +30,7 @@ namespace storm { template bool SymbolicDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false)); + return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true)); } template @@ -100,6 +100,16 @@ namespace storm { return std::make_unique>(this->getModel().getReachableStates(), numericResult); } + + template + std::unique_ptr SymbolicDtmcPrctlModelChecker::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::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeReachabilityTimes(env, this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); + return std::make_unique>(this->getModel().getReachableStates(), numericResult); + } + template class SymbolicDtmcPrctlModelChecker>; template class SymbolicDtmcPrctlModelChecker>; diff --git a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h index 311669bf7..1186c0271 100644 --- a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h @@ -26,7 +26,7 @@ namespace storm { virtual std::unique_ptr computeCumulativeRewards(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 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; }; } // namespace modelchecker diff --git a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp index 3c813d001..713ce3295 100644 --- a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp @@ -30,7 +30,7 @@ namespace storm { template bool SymbolicMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false)); + return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true)); } template @@ -99,6 +99,15 @@ namespace storm { SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeReachabilityRewards(env, checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector()); } + + template + std::unique_ptr SymbolicMdpPrctlModelChecker::computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { + storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); + SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeReachabilityTimes(env, checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); + } template class SymbolicMdpPrctlModelChecker>; template class SymbolicMdpPrctlModelChecker>; diff --git a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h index b116af0fc..bf259e8b7 100644 --- a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h @@ -27,7 +27,7 @@ namespace storm { virtual std::unique_ptr computeCumulativeRewards(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 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; }; } // namespace modelchecker diff --git a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp index 659a17cab..ce5bf4467 100644 --- a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp @@ -338,6 +338,12 @@ namespace storm { } } + template + std::unique_ptr HybridDtmcPrctlHelper::computeReachabilityTimes(Environment const& env, storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& targetStates, bool qualitative) { + RewardModelType rewardModel(model.getManager().getConstant(storm::utility::one()), boost::none, boost::none); + return computeReachabilityRewards(env, model, transitionMatrix, rewardModel, targetStates, qualitative); + } + template std::unique_ptr HybridDtmcPrctlHelper::computeLongRunAverageProbabilities(Environment const& env, storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& targetStates) { // Create ODD for the translation. diff --git a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h index 67896c8bc..9e20c5e2c 100644 --- a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h @@ -37,6 +37,8 @@ namespace storm { static std::unique_ptr computeReachabilityRewards(Environment const& env, storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative); + static std::unique_ptr computeReachabilityTimes(Environment const& env, storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& targetStates, bool qualitative); + static std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& targetStates); static std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel); diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index cca377b9d..7cb054574 100644 --- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -676,6 +676,13 @@ namespace storm { } } + template + std::unique_ptr HybridMdpPrctlHelper::computeReachabilityTimes(Environment const& env, OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& targetStates, bool qualitative) { + RewardModelType rewardModel(model.getManager().getConstant(storm::utility::one()), boost::none, boost::none); + return computeReachabilityRewards(env, dir, model, transitionMatrix, rewardModel, targetStates, qualitative); + } + + template class HybridMdpPrctlHelper; template class HybridMdpPrctlHelper; diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.h b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.h index 78ee1f7d3..ce7072624 100644 --- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.h @@ -37,6 +37,8 @@ namespace storm { static std::unique_ptr computeInstantaneousRewards(Environment const& env, OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound); static std::unique_ptr computeReachabilityRewards(Environment const& env, OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative); + + static std::unique_ptr computeReachabilityTimes(Environment const& env, OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& targetStates, bool qualitative); }; } diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 2745569ad..0e5cf1849 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -423,6 +423,21 @@ namespace storm { hint); } + template + std::vector SparseDtmcPrctlHelper::computeReachabilityTimes(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, bool qualitative, ModelCheckerHint const& hint) { + + return computeReachabilityRewards(env, std::move(goal), transitionMatrix, backwardTransitions, + [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix const&, storm::storage::BitVector const&) { + return std::vector(numberOfRows, storm::utility::one()); + }, + targetStates, qualitative, + [&] () { + return storm::storage::BitVector(transitionMatrix.getRowGroupCount(), false); + }, + hint); + } + + // This function computes an upper bound on the reachability rewards (see Baier et al, CAV'17). template std::vector computeUpperRewardBounds(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& rewards, std::vector const& oneStepTargetProbabilities) { diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h index 49fe21deb..16702ffed 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h @@ -47,6 +47,8 @@ namespace storm { static std::vector computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, ModelCheckerHint const& hint = ModelCheckerHint()); static std::vector computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, ModelCheckerHint const& hint = ModelCheckerHint()); + + static std::vector computeReachabilityTimes(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, bool qualitative, ModelCheckerHint const& hint = ModelCheckerHint()); static std::vector computeLongRunAverageProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates); diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 4b29d2324..58c94a95b 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -933,6 +933,22 @@ namespace storm { hint); } + template + MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeReachabilityTimes(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, ModelCheckerHint const& hint) { + return computeReachabilityRewardsHelper(env, std::move(goal), transitionMatrix, backwardTransitions, + [] (uint_fast64_t rowCount, storm::storage::SparseMatrix const&, storm::storage::BitVector const&) { + return std::vector(rowCount, storm::utility::one()); + }, + targetStates, qualitative, produceScheduler, + [&] () { + return storm::storage::BitVector(transitionMatrix.getRowGroupCount(), false); + }, + [&] () { + return storm::storage::BitVector(transitionMatrix.getRowCount(), false); + }, + hint); + } + #ifdef STORM_HAVE_CARL template std::vector SparseMdpPrctlHelper::computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& intervalRewardModel, bool lowerBoundOfIntervals, storm::storage::BitVector const& targetStates, bool qualitative) { diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index b1de7a442..0be4ad060 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -61,6 +61,8 @@ namespace storm { template static MDPSparseModelCheckingHelperReturnType computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); + static MDPSparseModelCheckingHelperReturnType computeReachabilityTimes(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); + #ifdef STORM_HAVE_CARL static std::vector computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& intervalRewardModel, bool lowerBoundOfIntervals, storm::storage::BitVector const& targetStates, bool qualitative); #endif diff --git a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp index 2b64db267..8f2468a70 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp @@ -202,6 +202,12 @@ namespace storm { return infinityStates.ite(model.getManager().getConstant(storm::utility::infinity()), result); } + template + storm::dd::Add SymbolicDtmcPrctlHelper::computeReachabilityTimes(Environment const& env, storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& targetStates, bool qualitative, boost::optional> const& startValues) { + RewardModelType rewardModel(model.getManager().getConstant(storm::utility::one()), boost::none, boost::none); + return computeReachabilityRewards(env, model, transitionMatrix, rewardModel, targetStates, qualitative, startValues); + } + template class SymbolicDtmcPrctlHelper; template class SymbolicDtmcPrctlHelper; diff --git a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.h index 995936786..ecf6a6fe4 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.h @@ -37,6 +37,8 @@ namespace storm { static storm::dd::Add computeReachabilityRewards(Environment const& env, storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, boost::optional> const& startValues = boost::none); static storm::dd::Add computeReachabilityRewards(Environment const& env, storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& targetStates, storm::dd::Bdd const& infinityStates, boost::optional> const& startValues = boost::none); + + static storm::dd::Add computeReachabilityTimes(Environment const& env, storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& targetStates, bool qualitative, boost::optional> const& startValues = boost::none); }; } diff --git a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp index d5c9fea6e..5080d90a8 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp @@ -300,6 +300,13 @@ namespace storm { } } + template + std::unique_ptr SymbolicMdpPrctlHelper::computeReachabilityTimes(Environment const& env, OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& targetStates, boost::optional> const& startValues) { + RewardModelType rewardModel(model.getManager().getConstant(storm::utility::one()), boost::none, boost::none); + return computeReachabilityRewards(env, dir, model, transitionMatrix, rewardModel, targetStates, startValues); + } + + template class SymbolicMdpPrctlHelper; template class SymbolicMdpPrctlHelper; diff --git a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h index e21342008..51f5f7dd1 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h @@ -41,6 +41,8 @@ namespace storm { static std::unique_ptr computeReachabilityRewards(Environment const& env, OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, boost::optional> const& startValues = boost::none); static std::unique_ptr computeReachabilityRewards(Environment const& env, OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& transitionMatrixBdd, RewardModelType const& rewardModel, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& targetStates, storm::dd::Bdd const& infinityStates, boost::optional> const& startValues = boost::none); + + static std::unique_ptr computeReachabilityTimes(Environment const& env, OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& targetStates, boost::optional> const& startValues = boost::none); }; } diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index c48927a78..59ca13d86 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -249,8 +249,12 @@ namespace storm { boost::any FormulaToJaniJson::visit(storm::logic::TimeOperatorFormula const& f, boost::any const& data) const { modernjson::json opDecl; - std::vector tvec; - tvec.push_back("time"); + std::vector accvec; + if (model.isDiscreteTimeModel()) { + accvec.push_back("steps"); + } else { + accvec.push_back("time"); + } if(f.hasBound()) { auto bound = f.getBound(); opDecl["op"] = comparisonTypeToJani(bound.comparisonType); @@ -266,7 +270,7 @@ namespace storm { opDecl["left"]["reach"] = boost::any_cast(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data)); } opDecl["left"]["exp"] = modernjson::json(1); - opDecl["left"]["accumulate"] = modernjson::json(tvec); + opDecl["left"]["accumulate"] = modernjson::json(accvec); opDecl["right"] = buildExpression(bound.threshold, model.getConstants(), model.getGlobalVariables()); } else { if(f.hasOptimalityType()) { @@ -282,7 +286,7 @@ namespace storm { opDecl["reach"] = boost::any_cast(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data)); } opDecl["exp"] = modernjson::json(1); - opDecl["accumulate"] = modernjson::json(tvec); + opDecl["accumulate"] = modernjson::json(accvec); } return opDecl; }