From ecfff3d2f97ccee3abf3358741c20134764b281b Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 4 Feb 2016 19:03:07 +0100 Subject: [PATCH] in the spirit of JP: up Former-commit-id: 3d7982c083da8816df9f6e399e6050d06376abf0 --- src/modelchecker/AbstractModelChecker.cpp | 236 +++++++----------- src/modelchecker/AbstractModelChecker.h | 50 ++-- src/modelchecker/CheckTask.cpp | 129 ---------- src/modelchecker/CheckTask.h | 124 +++++++-- .../prctl/SparseMdpPrctlModelChecker.h | 13 - 5 files changed, 220 insertions(+), 332 deletions(-) delete mode 100644 src/modelchecker/CheckTask.cpp diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index 2487949b6..764b02427 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -11,138 +11,144 @@ namespace storm { namespace modelchecker { - std::unique_ptr AbstractModelChecker::check(storm::logic::Formula const& formula, boost::optional> checkSettings) { + std::unique_ptr AbstractModelChecker::check(CheckTask const& checkTask) { + storm::logic::Formula const& formula = checkTask.getFormula(); STORM_LOG_THROW(this->canHandle(formula), storm::exceptions::InvalidArgumentException, "The model checker is not able to check the formula '" << formula << "'."); - CheckSettings newCheckSettings = checkSettings ? checkSettings.get() : CheckSettings::fromNestedFormula(formula); if (formula.isStateFormula()) { - return this->checkStateFormula(formula.asStateFormula(), newCheckSettings); + return this->checkStateFormula(checkTask.replaceFormula(formula.asStateFormula())); } else if (formula.isPathFormula()) { - return this->computeProbabilities(formula.asPathFormula(), newCheckSettings); + return this->computeProbabilities(checkTask.replaceFormula(formula.asPathFormula())); } else if (formula.isRewardPathFormula()) { - return this->computeRewards(formula.asRewardPathFormula(), newCheckSettings); + return this->computeRewards(checkTask.replaceFormula(formula.asRewardPathFormula())); } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid."); } - std::unique_ptr AbstractModelChecker::computeProbabilities(storm::logic::PathFormula const& pathFormula, boost::optional> checkSettings) { + std::unique_ptr AbstractModelChecker::computeProbabilities(CheckTask const& checkTask) { + storm::logic::PathFormula const& pathFormula = checkTask.getFormula(); if (pathFormula.isBoundedUntilFormula()) { - return this->computeBoundedUntilProbabilities(pathFormula.asBoundedUntilFormula(), checkSettings); + return this->computeBoundedUntilProbabilities(checkTask.replaceFormula(pathFormula.asBoundedUntilFormula())); } else if (pathFormula.isConditionalPathFormula()) { - return this->computeConditionalProbabilities(pathFormula.asConditionalPathFormula(), checkSettings); + return this->computeConditionalProbabilities(checkTask.replaceFormula(pathFormula.asConditionalPathFormula())); } else if (pathFormula.isEventuallyFormula()) { - return this->computeEventuallyProbabilities(pathFormula.asEventuallyFormula(), checkSettings); + return this->computeEventuallyProbabilities(checkTask.replaceFormula(pathFormula.asEventuallyFormula())); } else if (pathFormula.isGloballyFormula()) { - return this->computeGloballyProbabilities(pathFormula.asGloballyFormula(), checkSettings); + return this->computeGloballyProbabilities(checkTask.replaceFormula(pathFormula.asGloballyFormula())); } else if (pathFormula.isUntilFormula()) { - return this->computeUntilProbabilities(pathFormula.asUntilFormula(), checkSettings); + return this->computeUntilProbabilities(checkTask.replaceFormula(pathFormula.asUntilFormula())); } else if (pathFormula.isNextFormula()) { - return this->computeNextProbabilities(pathFormula.asNextFormula(), checkSettings); + return this->computeNextProbabilities(checkTask.replaceFormula(pathFormula.asNextFormula())); } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << pathFormula << "' is invalid."); } - std::unique_ptr AbstractModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, boost::optional> checkSettings) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << "."); + std::unique_ptr AbstractModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - std::unique_ptr AbstractModelChecker::computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, boost::optional> checkSettings) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << "."); + std::unique_ptr AbstractModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - std::unique_ptr AbstractModelChecker::computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, boost::optional> checkSettings) { + std::unique_ptr AbstractModelChecker::computeEventuallyProbabilities(CheckTask const& checkTask) { + storm::logic::EventuallyFormula const& pathFormula = checkTask.getFormula(); storm::logic::UntilFormula newFormula(storm::logic::Formula::getTrueFormula(), pathFormula.getSubformula().asSharedPointer()); - return this->computeUntilProbabilities(newFormula, checkSettings); + return this->computeUntilProbabilities(checkTask.replaceFormula(newFormula)); } - std::unique_ptr AbstractModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, boost::optional> checkSettings) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << "."); + std::unique_ptr AbstractModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - std::unique_ptr AbstractModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, boost::optional> checkSettings) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << "."); + std::unique_ptr AbstractModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - std::unique_ptr AbstractModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, boost::optional> checkSettings) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << "."); + std::unique_ptr AbstractModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - std::unique_ptr AbstractModelChecker::computeRewards(storm::logic::RewardPathFormula const& rewardPathFormula, boost::optional> checkSettings) { + std::unique_ptr AbstractModelChecker::computeRewards(CheckTask const& checkTask) { + storm::logic::RewardPathFormula const& rewardPathFormula = checkTask.getFormula(); if (rewardPathFormula.isCumulativeRewardFormula()) { - return this->computeCumulativeRewards(rewardPathFormula.asCumulativeRewardFormula(), checkSettings); + return this->computeCumulativeRewards(checkTask.replaceFormula(rewardPathFormula.asCumulativeRewardFormula())); } else if (rewardPathFormula.isInstantaneousRewardFormula()) { - return this->computeInstantaneousRewards(rewardPathFormula.asInstantaneousRewardFormula(), checkSettings); + return this->computeInstantaneousRewards(checkTask.replaceFormula(rewardPathFormula.asInstantaneousRewardFormula())); } else if (rewardPathFormula.isReachabilityRewardFormula()) { - return this->computeReachabilityRewards(rewardPathFormula.asReachabilityRewardFormula(), checkSettings); + return this->computeReachabilityRewards(checkTask.replaceFormula(rewardPathFormula.asReachabilityRewardFormula())); } else if (rewardPathFormula.isLongRunAverageRewardFormula()) { - return this->computeLongRunAverageRewards(rewardPathFormula.asLongRunAverageRewardFormula(), checkSettings); + return this->computeLongRunAverageRewards(checkTask.replaceFormula(rewardPathFormula.asLongRunAverageRewardFormula())); } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardPathFormula << "' is invalid."); } - std::unique_ptr AbstractModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional> checkSettings) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << rewardPathFormula << "."); + std::unique_ptr AbstractModelChecker::computeCumulativeRewards(CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - std::unique_ptr AbstractModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional> checkSettings) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << rewardPathFormula << "."); + std::unique_ptr AbstractModelChecker::computeInstantaneousRewards(CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - std::unique_ptr AbstractModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional> checkSettings) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << rewardPathFormula << "."); + std::unique_ptr AbstractModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - std::unique_ptr AbstractModelChecker::computeLongRunAverageRewards(storm::logic::LongRunAverageRewardFormula const& rewardPathFormula, boost::optional> checkSettings) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << rewardPathFormula << "."); + std::unique_ptr AbstractModelChecker::computeLongRunAverageRewards(CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - std::unique_ptr AbstractModelChecker::computeLongRunAverageProbabilities(storm::logic::StateFormula const& eventuallyFormula, boost::optional> checkSettings) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the computation of long-run averages."); + std::unique_ptr AbstractModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - std::unique_ptr AbstractModelChecker::computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, boost::optional> checkSettings) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the computation of expected times."); + std::unique_ptr AbstractModelChecker::computeExpectedTimes(CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - std::unique_ptr AbstractModelChecker::checkStateFormula(storm::logic::StateFormula const& stateFormula, boost::optional> checkSettings) { + std::unique_ptr AbstractModelChecker::checkStateFormula(CheckTask const& checkTask) { + storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); if (stateFormula.isBinaryBooleanStateFormula()) { - return this->checkBinaryBooleanStateFormula(stateFormula.asBinaryBooleanStateFormula(), checkSettings); + return this->checkBinaryBooleanStateFormula(checkTask.replaceFormula(stateFormula.asBinaryBooleanStateFormula())); } else if (stateFormula.isUnaryBooleanStateFormula()) { - return this->checkUnaryBooleanStateFormula(stateFormula.asUnaryBooleanStateFormula(), checkSettings); + return this->checkUnaryBooleanStateFormula(checkTask.replaceFormula(stateFormula.asUnaryBooleanStateFormula())); } else if (stateFormula.isBooleanLiteralFormula()) { - return this->checkBooleanLiteralFormula(stateFormula.asBooleanLiteralFormula(), checkSettings); + return this->checkBooleanLiteralFormula(checkTask.replaceFormula(stateFormula.asBooleanLiteralFormula())); } else if (stateFormula.isProbabilityOperatorFormula()) { - return this->checkProbabilityOperatorFormula(stateFormula.asProbabilityOperatorFormula(), checkSettings); + return this->checkProbabilityOperatorFormula(checkTask.replaceFormula(stateFormula.asProbabilityOperatorFormula())); } else if (stateFormula.isRewardOperatorFormula()) { - return this->checkRewardOperatorFormula(stateFormula.asRewardOperatorFormula(), checkSettings); + return this->checkRewardOperatorFormula(checkTask.replaceFormula(stateFormula.asRewardOperatorFormula())); } else if (stateFormula.isExpectedTimeOperatorFormula()) { - return this->checkExpectedTimeOperatorFormula(stateFormula.asExpectedTimeOperatorFormula(), checkSettings); + return this->checkExpectedTimeOperatorFormula(checkTask.replaceFormula(stateFormula.asExpectedTimeOperatorFormula())); } else if (stateFormula.isLongRunAverageOperatorFormula()) { - return this->checkLongRunAverageOperatorFormula(stateFormula.asLongRunAverageOperatorFormula(), checkSettings); + return this->checkLongRunAverageOperatorFormula(checkTask.replaceFormula(stateFormula.asLongRunAverageOperatorFormula())); } else if (stateFormula.isAtomicExpressionFormula()) { - return this->checkAtomicExpressionFormula(stateFormula.asAtomicExpressionFormula(), checkSettings); + return this->checkAtomicExpressionFormula(checkTask.replaceFormula(stateFormula.asAtomicExpressionFormula())); } else if (stateFormula.isAtomicLabelFormula()) { - return this->checkAtomicLabelFormula(stateFormula.asAtomicLabelFormula(), checkSettings); + return this->checkAtomicLabelFormula(checkTask.replaceFormula(stateFormula.asAtomicLabelFormula())); } else if (stateFormula.isBooleanLiteralFormula()) { - return this->checkBooleanLiteralFormula(stateFormula.asBooleanLiteralFormula(), checkSettings); + return this->checkBooleanLiteralFormula(checkTask.replaceFormula(stateFormula.asBooleanLiteralFormula())); } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid."); } - std::unique_ptr AbstractModelChecker::checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula, boost::optional> checkSettings) { + std::unique_ptr AbstractModelChecker::checkAtomicExpressionFormula(CheckTask const& checkTask) { + storm::logic::AtomicExpressionFormula const& stateFormula = checkTask.getFormula(); std::stringstream stream; stream << stateFormula.getExpression(); - return this->checkAtomicLabelFormula(storm::logic::AtomicLabelFormula(stream.str()), checkSettings); + return this->checkAtomicLabelFormula(checkTask.replaceFormula(storm::logic::AtomicLabelFormula(stream.str()))); } - std::unique_ptr AbstractModelChecker::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula, boost::optional> checkSettings) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << stateFormula << "."); + std::unique_ptr AbstractModelChecker::checkAtomicLabelFormula(CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - std::unique_ptr AbstractModelChecker::checkBinaryBooleanStateFormula(storm::logic::BinaryBooleanStateFormula const& stateFormula, boost::optional> checkSettings) { + std::unique_ptr AbstractModelChecker::checkBinaryBooleanStateFormula(CheckTask const& checkTask) { + storm::logic::BinaryBooleanStateFormula const& stateFormula = checkTask.getFormula(); STORM_LOG_THROW(stateFormula.getLeftSubformula().isStateFormula() && stateFormula.getRightSubformula().isStateFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); - std::unique_ptr leftResult = this->check(stateFormula.getLeftSubformula().asStateFormula()); - std::unique_ptr rightResult = this->check(stateFormula.getRightSubformula().asStateFormula()); + std::unique_ptr leftResult = this->check(checkTask.replaceFormula(stateFormula.getLeftSubformula().asStateFormula())); + std::unique_ptr rightResult = this->check(checkTask.replaceFormula(stateFormula.getRightSubformula().asStateFormula())); STORM_LOG_THROW(leftResult->isQualitative() && rightResult->isQualitative(), storm::exceptions::InternalTypeErrorException, "Expected qualitative results."); @@ -157,35 +163,15 @@ namespace storm { return leftResult; } - std::unique_ptr AbstractModelChecker::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula, boost::optional> checkSettings) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << stateFormula << "."); + std::unique_ptr AbstractModelChecker::checkBooleanLiteralFormula(CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - std::unique_ptr AbstractModelChecker::checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula, boost::optional> checkSettings) { + std::unique_ptr AbstractModelChecker::checkProbabilityOperatorFormula(CheckTask const& checkTask) { + storm::logic::ProbabilityOperatorFormula const& stateFormula = checkTask.getFormula(); STORM_LOG_THROW(stateFormula.getSubformula().isPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); - CheckSettings newCheckSettings = - - // If the probability bound is 0 or 1, is suffices to do qualitative model checking. - bool qualitative = false; - if (stateFormula.hasBound()) { - if (storm::utility::isZero(stateFormula.getBound()) || storm::utility::isOne(stateFormula.getBound())) { - qualitative = true; - } - } - - std::unique_ptr result; - if (stateFormula.hasOptimalityType()) { - result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative, stateFormula.getOptimalityType()); - } else if (stateFormula.hasBound()) { - if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || stateFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual) { - result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative, OptimizationDirection::Maximize); - } else { - result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative, OptimizationDirection::Minimize); - } - } else { - result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative); - } + std::unique_ptr result = this->computeProbabilities(checkTask.replaceFormula(stateFormula.getSubformula().asPathFormula())); if (stateFormula.hasBound()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); @@ -195,95 +181,51 @@ namespace storm { } } - std::unique_ptr AbstractModelChecker::checkRewardOperatorFormula(storm::logic::RewardOperatorFormula const& stateFormula, boost::optional> checkSettings) { + std::unique_ptr AbstractModelChecker::checkRewardOperatorFormula(CheckTask const& checkTask) { + storm::logic::RewardOperatorFormula const& stateFormula = checkTask.getFormula(); STORM_LOG_THROW(stateFormula.getSubformula().isRewardPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); - // If the reward bound is 0, is suffices to do qualitative model checking. - bool qualitative = false; - if (stateFormula.hasBound()) { - if (storm::utility::isZero(stateFormula.getBound())) { - qualitative = true; - } - } - - std::unique_ptr result; - if (stateFormula.hasOptimalityType()) { - result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), stateFormula.getOptionalRewardModelName(), qualitative, stateFormula.getOptimalityType()); - } else if (stateFormula.hasBound()) { - if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || stateFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual) { - result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), stateFormula.getOptionalRewardModelName(), qualitative, OptimizationDirection::Maximize); - } else { - result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), stateFormula.getOptionalRewardModelName(), qualitative, OptimizationDirection::Minimize); - } - } else { - result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), stateFormula.getOptionalRewardModelName(), qualitative); - } + std::unique_ptr result = this->computeRewards(checkTask.replaceFormula(stateFormula.getSubformula().asRewardPathFormula())); - if (stateFormula.hasBound()) { + if (checkTask.isBoundSet()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound()); + return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundValue()); } else { return result; } } - std::unique_ptr AbstractModelChecker::checkExpectedTimeOperatorFormula(storm::logic::ExpectedTimeOperatorFormula const& stateFormula, boost::optional> checkSettings) { + std::unique_ptr AbstractModelChecker::checkExpectedTimeOperatorFormula(CheckTask const& checkTask) { + storm::logic::ExpectedTimeOperatorFormula const& stateFormula = checkTask.getFormula(); STORM_LOG_THROW(stateFormula.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); - // If the reward bound is 0, is suffices to do qualitative model checking. - bool qualitative = false; - if (stateFormula.hasBound()) { - if (storm::utility::isZero(stateFormula.getBound())) { - qualitative = true; - } - } - - std::unique_ptr result; - if (stateFormula.hasOptimalityType()) { - result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), qualitative, stateFormula.getOptimalityType()); - } else if (stateFormula.hasBound()) { - if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || stateFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual) { - result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), qualitative, OptimizationDirection::Maximize); - } else { - result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), qualitative, OptimizationDirection::Minimize); - } - } else { - result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), qualitative); - } + std::unique_ptr result = this->computeExpectedTimes(checkTask.replaceFormula(stateFormula.getSubformula().asEventuallyFormula())); - if (stateFormula.hasBound()) { + if (checkTask.isBoundSet()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound()); + return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundValue()); } else { return result; } } - std::unique_ptr AbstractModelChecker::checkLongRunAverageOperatorFormula(storm::logic::LongRunAverageOperatorFormula const& stateFormula, boost::optional> checkSettings) { + std::unique_ptr AbstractModelChecker::checkLongRunAverageOperatorFormula(CheckTask const& checkTask) { + storm::logic::LongRunAverageOperatorFormula const& stateFormula = checkTask.getFormula(); STORM_LOG_THROW(stateFormula.getSubformula().isStateFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); - std::unique_ptr result; - if (stateFormula.hasOptimalityType()) { - result = this->computeLongRunAverageProbabilities(stateFormula.getSubformula().asStateFormula(), false, stateFormula.getOptimalityType()); - } else if (stateFormula.hasBound()) { - if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || stateFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual) { - result = this->computeLongRunAverageProbabilities(stateFormula.getSubformula().asStateFormula(), false, OptimizationDirection::Maximize); - } else { - result = this->computeLongRunAverageProbabilities(stateFormula.getSubformula().asStateFormula(), false, OptimizationDirection::Minimize); - } - } else { - result = this->computeLongRunAverageProbabilities(stateFormula.getSubformula().asStateFormula(), false); - } + std::unique_ptr result = this->computeLongRunAverageProbabilities(checkTask.replaceFormula(stateFormula.getSubformula().asStateFormula())); - if (stateFormula.hasBound()) { - return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound()); + if (checkTask.isBoundSet()) { + STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); + return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundValue()); } else { return result; } } - std::unique_ptr AbstractModelChecker::checkUnaryBooleanStateFormula(storm::logic::UnaryBooleanStateFormula const& stateFormula, boost::optional> checkSettings) { - std::unique_ptr subResult = this->check(stateFormula.getSubformula()); + std::unique_ptr AbstractModelChecker::checkUnaryBooleanStateFormula(CheckTask const& checkTask) { + storm::logic::UnaryBooleanStateFormula const& stateFormula = checkTask.getFormula(); + std::unique_ptr subResult = this->check(checkTask.replaceFormula(stateFormula.getSubformula())); STORM_LOG_THROW(subResult->isQualitative(), storm::exceptions::InternalTypeErrorException, "Expected qualitative result."); if (stateFormula.isNot()) { subResult->asQualitativeCheckResult().complement(); diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h index 7acbac752..f76638aea 100644 --- a/src/modelchecker/AbstractModelChecker.h +++ b/src/modelchecker/AbstractModelChecker.h @@ -33,39 +33,39 @@ namespace storm { * @param checkSettings If provided, this object is used to customize the checking process. * @return The verification result. */ - virtual std::unique_ptr check(CheckTask<> storm::logic::Formula const& formula, boost::optional> checkSettings = boost::none); + virtual std::unique_ptr check(CheckTask const& checkTask); // The methods to compute probabilities for path formulas. - virtual std::unique_ptr computeProbabilities(storm::logic::PathFormula const& pathFormula, boost::optional> checkSettings = boost::none); - virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, boost::optional> checkSettings = boost::none); - virtual std::unique_ptr computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, boost::optional> checkSettings = boost::none); - virtual std::unique_ptr computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, boost::optional> checkSettings = boost::none); - virtual std::unique_ptr computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, boost::optional> checkSettings = boost::none); - virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, boost::optional> checkSettings = boost::none); - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, boost::optional> checkSettings = boost::none); + virtual std::unique_ptr computeProbabilities(CheckTask const& checkTask); + virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask); + virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask); + virtual std::unique_ptr computeEventuallyProbabilities(CheckTask const& checkTask); + virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask); + virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask); + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask); // The methods to compute the rewards for path formulas. - virtual std::unique_ptr computeRewards(storm::logic::RewardPathFormula const& rewardPathFormula, boost::optional> checkSettings = boost::none); - virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional> checkSettings = boost::none); - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional> checkSettings = boost::none); - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional> checkSettings = boost::none); - virtual std::unique_ptr computeLongRunAverageRewards(storm::logic::LongRunAverageRewardFormula const& rewardPathFormula, boost::optional> checkSettings = boost::none); + virtual std::unique_ptr computeRewards(CheckTask const& checkTask); + virtual std::unique_ptr computeCumulativeRewards(CheckTask const& checkTask); + virtual std::unique_ptr computeInstantaneousRewards(CheckTask const& checkTask); + virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask); + virtual std::unique_ptr computeLongRunAverageRewards(CheckTask const& checkTask); // The methods to compute the long-run average and expected time. - virtual std::unique_ptr computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, boost::optional> checkSettings = boost::none); - virtual std::unique_ptr computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, boost::optional> checkSettings = boost::none); + virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask); + virtual std::unique_ptr computeExpectedTimes(CheckTask const& checkTask); // The methods to check state formulas. - virtual std::unique_ptr checkStateFormula(storm::logic::StateFormula const& stateFormula, boost::optional> checkSettings); - virtual std::unique_ptr checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula, boost::optional> checkSettings = boost::none); - virtual std::unique_ptr checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula, boost::optional> checkSettings = boost::none); - virtual std::unique_ptr checkBinaryBooleanStateFormula(storm::logic::BinaryBooleanStateFormula const& stateFormula, boost::optional> checkSettings = boost::none); - virtual std::unique_ptr checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula, boost::optional> checkSettings = boost::none); - virtual std::unique_ptr checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula, boost::optional> checkSettings = boost::none); - virtual std::unique_ptr checkRewardOperatorFormula(storm::logic::RewardOperatorFormula const& stateFormula, boost::optional> checkSettings = boost::none); - virtual std::unique_ptr checkExpectedTimeOperatorFormula(storm::logic::ExpectedTimeOperatorFormula const& stateFormula, boost::optional> checkSettings = boost::none); - virtual std::unique_ptr checkLongRunAverageOperatorFormula(storm::logic::LongRunAverageOperatorFormula const& stateFormula, boost::optional> checkSettings = boost::none); - virtual std::unique_ptr checkUnaryBooleanStateFormula(storm::logic::UnaryBooleanStateFormula const& stateFormula, boost::optional> checkSettings = boost::none); + virtual std::unique_ptr checkStateFormula(CheckTask const& stateFormula); + virtual std::unique_ptr checkAtomicExpressionFormula(CheckTask const& checkTask); + virtual std::unique_ptr checkAtomicLabelFormula(CheckTask const& checkTask); + virtual std::unique_ptr checkBinaryBooleanStateFormula(CheckTask const& checkTask); + virtual std::unique_ptr checkBooleanLiteralFormula(CheckTask const& checkTask); + virtual std::unique_ptr checkProbabilityOperatorFormula(CheckTask const& checkTask); + virtual std::unique_ptr checkRewardOperatorFormula(CheckTask const& checkTask); + virtual std::unique_ptr checkExpectedTimeOperatorFormula(CheckTask const& checkTask); + virtual std::unique_ptr checkLongRunAverageOperatorFormula(CheckTask const& checkTask); + virtual std::unique_ptr checkUnaryBooleanStateFormula(CheckTask const& checkTask); }; } } diff --git a/src/modelchecker/CheckTask.cpp b/src/modelchecker/CheckTask.cpp deleted file mode 100644 index d88939823..000000000 --- a/src/modelchecker/CheckTask.cpp +++ /dev/null @@ -1,129 +0,0 @@ -#include "src/modelchecker/CheckTask.h" - -#include "src/logic/Formulas.h" - -#include "src/utility/constants.h" - -namespace storm { - namespace modelchecker { - - template - CheckTask::CheckTask() : CheckTask(boost::none, boost::none, boost::none, false, boost::none, false, false) { - // Intentionally left empty. - } - - template - CheckTask::CheckTask(boost::optional> const& formula, boost::optional const& optimizationDirection, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional> const& initialStatesBound, bool qualitative, bool produceStrategies) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), initialStatesBound(initialStatesBound), qualitative(qualitative), produceStrategies(produceStrategies) { - // Intentionally left empty. - } - - template - CheckTask::CheckTask(FormulaType const& formula) { - this->onlyInitialStatesRelevant = false; - this->produceStrategies = true; - this->qualitative = false; - - if (formula.isProbabilityOperatorFormula()) { - storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula(); - if (probabilityOperatorFormula.hasOptimalityType()) { - this->optimizationDirection = probabilityOperatorFormula.getOptimalityType(); - } - - if (probabilityOperatorFormula.hasBound()) { - if (onlyInitialStatesRelevant) { - this->initialStatesBound = std::make_pair(probabilityOperatorFormula.getComparisonType(), static_cast(probabilityOperatorFormula.getBound())); - } - if (probabilityOperatorFormula.getBound() == storm::utility::zero() || probabilityOperatorFormula.getBound() == storm::utility::one()) { - this->qualitative = true; - } - if (!optimizationDirection) { - this->optimizationDirection = probabilityOperatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || probabilityOperatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize; - } - } - } else if (formula.isRewardOperatorFormula()) { - storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.asRewardOperatorFormula(); - this->rewardModel = rewardOperatorFormula.getOptionalRewardModelName(); - - if (rewardOperatorFormula.hasOptimalityType()) { - this->optimizationDirection = rewardOperatorFormula.getOptimalityType(); - } - - if (rewardOperatorFormula.hasBound()) { - if (onlyInitialStatesRelevant) { - this->initialStatesBound = std::make_pair(rewardOperatorFormula.getComparisonType(), static_cast(rewardOperatorFormula.getBound())); - } - if (rewardOperatorFormula.getBound() == storm::utility::zero()) { - this->qualitative = true; - } - if (!optimizationDirection) { - this->optimizationDirection = rewardOperatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || rewardOperatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize; - } - } - } - } - - template - template - CheckTask CheckTask::convert() { - return CheckTask(); - } - - template - bool CheckTask::hasFormula() const { - return static_cast(formula); - } - - template - FormulaType const& CheckTask::getFormula() const { - return formula.get().get(); - } - - template - bool CheckTask::isOptimizationDirectionSet() const { - return static_cast(optimizationDirection); - } - - template - storm::OptimizationDirection const& CheckTask::getOptimizationDirection() const { - return optimizationDirection.get(); - } - - template - bool CheckTask::isRewardModelSet() const { - return static_cast(rewardModel); - } - - template - std::string const& CheckTask::getRewardModel() const { - return rewardModel.get(); - } - - template - bool CheckTask::isOnlyInitialStatesRelevantSet() const { - return onlyInitialStatesRelevant; - } - - template - bool CheckTask::isInitialStatesBoundSet() const { - return static_cast(initialStatesBound); - } - - template - std::pair const& CheckTask::getInitialStatesBound() const { - return initialStatesBound.get(); - } - - template - bool CheckTask::isQualitativeSet() const { - return qualitative; - } - - template - bool CheckTask::isProduceStrategiesSet() const { - return produceStrategies; - } - - template class CheckTask; - - } -} \ No newline at end of file diff --git a/src/modelchecker/CheckTask.h b/src/modelchecker/CheckTask.h index f41ee6e40..042daf40d 100644 --- a/src/modelchecker/CheckTask.h +++ b/src/modelchecker/CheckTask.h @@ -3,6 +3,9 @@ #include +#include "src/logic/Formulas.h" +#include "src/utility/constants.h" + #include "src/solver/OptimizationDirection.h" #include "src/logic/ComparisonType.h" @@ -22,74 +25,157 @@ namespace storm { /*! * Creates an empty task object with the default options. */ - CheckTask(); + CheckTask() : CheckTask(boost::none, boost::none, boost::none, false, boost::none, false, false) { + // Intentionally left empty. + } /*! * Creates a task object with the default options for the given formula. */ - CheckTask(FormulaType const& formula); + CheckTask(FormulaType const& formula) { + this->onlyInitialStatesRelevant = false; + this->produceStrategies = true; + this->qualitative = false; + + if (formula.isProbabilityOperatorFormula()) { + storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula(); + if (probabilityOperatorFormula.hasOptimalityType()) { + this->optimizationDirection = probabilityOperatorFormula.getOptimalityType(); + } + + if (probabilityOperatorFormula.hasBound()) { + if (onlyInitialStatesRelevant) { + this->initialStatesBound = std::make_pair(probabilityOperatorFormula.getComparisonType(), static_cast(probabilityOperatorFormula.getBound())); + } + if (probabilityOperatorFormula.getBound() == storm::utility::zero() || probabilityOperatorFormula.getBound() == storm::utility::one()) { + this->qualitative = true; + } + if (!optimizationDirection) { + this->optimizationDirection = probabilityOperatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || probabilityOperatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize; + } + } + } else if (formula.isRewardOperatorFormula()) { + storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.asRewardOperatorFormula(); + this->rewardModel = rewardOperatorFormula.getOptionalRewardModelName(); + + if (rewardOperatorFormula.hasOptimalityType()) { + this->optimizationDirection = rewardOperatorFormula.getOptimalityType(); + } + + if (rewardOperatorFormula.hasBound()) { + if (onlyInitialStatesRelevant) { + this->initialStatesBound = std::make_pair(rewardOperatorFormula.getComparisonType(), static_cast(rewardOperatorFormula.getBound())); + } + if (rewardOperatorFormula.getBound() == storm::utility::zero()) { + this->qualitative = true; + } + if (!optimizationDirection) { + this->optimizationDirection = rewardOperatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || rewardOperatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize; + } + } + } + } /*! - * Converts the check task object to one with the given new formula type. + * Copies the check task from the source while replacing the formula with the new one. In particular, this + * changes the formula type of the check task object. */ template - CheckTask convert(); + CheckTask replaceFormula(NewFormulaType const& newFormula) const { + return CheckTask(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->initialStatesBound, this->qualitative, this->produceStrategies); + } /*! * Retrieves whether this task is associated with a formula. */ - bool hasFormula() const; + bool hasFormula() const { + return static_cast(formula); + } /*! * Retrieves the formula from this task. */ - FormulaType const& getFormula() const; + FormulaType const& getFormula() const { + return formula.get().get(); + } /*! * Retrieves whether an optimization direction was set. */ - bool isOptimizationDirectionSet() const; + bool isOptimizationDirectionSet() const { + return static_cast(optimizationDirection); + } /*! * Retrieves the optimization direction (if set). */ - storm::OptimizationDirection const& getOptimizationDirection() const; + storm::OptimizationDirection const& getOptimizationDirection() const { + return optimizationDirection.get(); + } /*! * Retrieves whether a reward model was set. */ - bool isRewardModelSet() const; + bool isRewardModelSet() const { + return static_cast(rewardModel); + } /*! * Retrieves the reward model over which to perform the checking (if set). */ - std::string const& getRewardModel() const; + std::string const& getRewardModel() const { + return rewardModel.get(); + } /*! * Retrieves whether only the initial states are relevant in the computation. */ - bool isOnlyInitialStatesRelevantSet() const; + bool isOnlyInitialStatesRelevantSet() const { + return onlyInitialStatesRelevant; + } + + /*! + * Retrieves whether there is a bound with which the values for the states will be compared. + */ + bool isBoundSet() const { + return static_cast(bound); + } + + /*! + * Retrieves the value of the bound (if set). + */ + ValueType const& getBoundValue() const { + return bound.get().second; + } /*! - * Retrieves whether there is a bound with which the values for the initial states will be compared. + * Retrieves the comparison type of the bound (if set). */ - bool isInitialStatesBoundSet() const; + storm::logic::ComparisonType const& getBoundComparisonType() const { + return bound.get().first; + } /*! * Retrieves the bound for the initial states (if set). */ - std::pair const& getInitialStatesBound() const; + std::pair const& getBound() const { + return bound.get(); + } /*! * Retrieves whether the computation only needs to be performed qualitatively, because the values will only * be compared to 0/1. */ - bool isQualitativeSet() const; + bool isQualitativeSet() const { + return qualitative; + } /*! * Retrieves whether strategies are to be produced (if supported). */ - bool isProduceStrategiesSet() const; + bool isProduceStrategiesSet() const { + return produceStrategies; + } private: /*! @@ -107,7 +193,9 @@ namespace storm { * @param produceStrategies If supported by the model checker and the model formalism, strategies to achieve * a value will be produced if this flag is set. */ - CheckTask(boost::optional> const& formula, boost::optional const& optimizationDirection, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional> const& initialStatesBound, bool qualitative, bool produceStrategies); + CheckTask(boost::optional> const& formula, boost::optional const& optimizationDirection, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional> const& bound, bool qualitative, bool produceStrategies) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceStrategies(produceStrategies) { + // Intentionally left empty. + } // The formula that is to be checked. boost::optional> formula; @@ -122,7 +210,7 @@ namespace storm { bool onlyInitialStatesRelevant; // The bound with which the initial states will be compared. - boost::optional> initialStatesBound; + boost::optional> bound; // A flag specifying whether the property needs to be checked qualitatively, i.e. compared with bounds 0/1. bool qualitative; diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 18a5e9091..030368317 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -8,16 +8,6 @@ #include "src/solver/MinMaxLinearEquationSolver.h" namespace storm { - namespace counterexamples { - template - class SMTMinimalCommandSetGenerator; - - template - class MILPMinimalLabelSetGenerator; - } - - - namespace modelchecker { template class SparseMdpPrctlModelChecker : public SparsePropositionalModelChecker { @@ -25,9 +15,6 @@ namespace storm { typedef typename SparseMdpModelType::ValueType ValueType; typedef typename SparseMdpModelType::RewardModelType RewardModelType; - friend class storm::counterexamples::SMTMinimalCommandSetGenerator; - friend class storm::counterexamples::MILPMinimalLabelSetGenerator; - explicit SparseMdpPrctlModelChecker(SparseMdpModelType const& model); explicit SparseMdpPrctlModelChecker(SparseMdpModelType const& model, std::unique_ptr>&& MinMaxLinearEquationSolverFactory);