diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp index 4ad79b8ed..31b34cd72 100644 --- a/src/storm/modelchecker/AbstractModelChecker.cpp +++ b/src/storm/modelchecker/AbstractModelChecker.cpp @@ -64,6 +64,10 @@ namespace storm { template std::unique_ptr AbstractModelChecker::computeProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::Formula const& formula = checkTask.getFormula(); + if (formula.isStateFormula() || formula.hasQualitativeResult()) { + return this->computeStateFormulaProbabilities(env, checkTask.substituteFormula(formula)); + } + if (formula.info(false).containsComplexPathFormula()) { // we need to do LTL model checking return this->computeLTLProbabilities(env, checkTask.substituteFormula(formula.asPathFormula())); @@ -135,6 +139,11 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } + template + std::unique_ptr AbstractModelChecker::computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); + } + template std::unique_ptr AbstractModelChecker::computeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::Formula const& rewardFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/AbstractModelChecker.h b/src/storm/modelchecker/AbstractModelChecker.h index 11d781319..6eb3b0de8 100644 --- a/src/storm/modelchecker/AbstractModelChecker.h +++ b/src/storm/modelchecker/AbstractModelChecker.h @@ -65,6 +65,7 @@ namespace storm { virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask); virtual std::unique_ptr computeHOAPathProbabilities(Environment const& env, CheckTask const& checkTask); virtual std::unique_ptr computeLTLProbabilities(Environment const& env, CheckTask const& checkTask); + virtual std::unique_ptr computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask); // The methods to compute the rewards for path formulas. virtual std::unique_ptr computeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); diff --git a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index 176bba662..44bd4ab3c 100644 --- a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -81,7 +81,15 @@ namespace storm { SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeBoundedUntilProbabilities(env, this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound()); } - + + template + std::unique_ptr HybridDtmcPrctlModelChecker::computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::Formula const& formula = checkTask.getFormula(); + std::unique_ptr resultPointer = this->check(env, formula); + SymbolicQualitativeCheckResult const& result = resultPointer->asSymbolicQualitativeCheckResult(); + return std::make_unique>(result); + } + template std::unique_ptr HybridDtmcPrctlModelChecker::computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h index f779e1920..761d0168f 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 computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeGloballyProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeStateFormulaProbabilities(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 computeCumulativeRewards(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 15725a415..275527797 100644 --- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -103,6 +103,15 @@ namespace storm { return storm::modelchecker::helper::HybridMdpPrctlHelper::computeBoundedUntilProbabilities(env, checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound()); } + template + std::unique_ptr HybridMdpPrctlModelChecker::computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::Formula const& formula = checkTask.getFormula(); + std::unique_ptr resultPointer = this->check(env, formula); + SymbolicQualitativeCheckResult const& result = resultPointer->asSymbolicQualitativeCheckResult(); + // min/max does not matters + return std::make_unique>(result); + } + template std::unique_ptr HybridMdpPrctlModelChecker::computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h index cc253e753..3fa76a65a 100644 --- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h @@ -38,6 +38,8 @@ namespace storm { virtual std::unique_ptr computeNextProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeGloballyProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) override; + 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; diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 859de2fb2..ccb5d1a83 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -191,6 +191,14 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } + template + std::unique_ptr SparseDtmcPrctlModelChecker::computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) { + // recurse + std::unique_ptr resultPointer = this->check(env, checkTask.getFormula()); + ExplicitQualitativeCheckResult const& result = resultPointer->asExplicitQualitativeCheckResult(); + return std::make_unique>(result); + } + template std::unique_ptr SparseDtmcPrctlModelChecker::computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 572ecc57e..e03ba42b8 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -33,6 +33,7 @@ namespace storm { virtual std::unique_ptr computeConditionalProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeLTLProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) override; 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; diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index ffefa0e78..a56a8b3ef 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -160,6 +160,15 @@ namespace storm { return result; } + template + std::unique_ptr SparseMdpPrctlModelChecker::computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::Formula const& formula = 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 resultPointer = this->check(env, formula); + ExplicitQualitativeCheckResult const& result = resultPointer->asExplicitQualitativeCheckResult(); + return std::make_unique>(result); + } + template std::unique_ptr SparseMdpPrctlModelChecker::computeConditionalProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 44916728b..ad164df32 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -38,6 +38,7 @@ namespace storm { 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 computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr checkMultiObjectiveFormula(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr checkQuantileFormula(Environment const& env, CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index 340a48aff..6b68c945f 100644 --- a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -59,6 +59,14 @@ namespace storm { return std::make_unique>(this->getModel().getReachableStates(), numericResult); } + template + std::unique_ptr SymbolicDtmcPrctlModelChecker::computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::Formula const& formula = checkTask.getFormula(); + std::unique_ptr resultPointer = this->check(env, formula); + SymbolicQualitativeCheckResult const& result = resultPointer->asSymbolicQualitativeCheckResult(); + return std::make_unique>(result); + } + template std::unique_ptr SymbolicDtmcPrctlModelChecker::computeNextProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h index 1a115468f..17c96e927 100644 --- a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h @@ -26,6 +26,7 @@ namespace storm { virtual std::unique_ptr computeNextProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeGloballyProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) override; 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; diff --git a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp index 5479e4720..8f366034a 100644 --- a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp @@ -59,6 +59,16 @@ namespace storm { return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeGloballyProbabilities(env, checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); } + template + std::unique_ptr SymbolicMdpPrctlModelChecker::computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::Formula const& formula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr resultPointer = this->check(env, formula); + SymbolicQualitativeCheckResult const& result = resultPointer->asSymbolicQualitativeCheckResult(); + // min/max does not matters + return std::make_unique>(result); + } + template std::unique_ptr SymbolicMdpPrctlModelChecker::computeNextProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h index 4fda40be3..e54f3579d 100644 --- a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h @@ -27,6 +27,7 @@ namespace storm { virtual std::unique_ptr computeNextProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeGloballyProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) override; 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;