From 280af183419044666ccc2751c572fd9a770f5275 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 3 Feb 2016 17:01:37 +0100 Subject: [PATCH] still introducing check settings Former-commit-id: 0426c8f3654a182759a0afa768826c535da6a17e --- src/modelchecker/AbstractModelChecker.cpp | 44 ++++++++++++----------- src/modelchecker/CheckSettings.cpp | 6 ++++ 2 files changed, 29 insertions(+), 21 deletions(-) diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index 6a3eac1b5..e5e272d23 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -103,42 +103,42 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the computation of expected times."); } - std::unique_ptr AbstractModelChecker::checkStateFormula(storm::logic::StateFormula const& stateFormula) { + std::unique_ptr AbstractModelChecker::checkStateFormula(storm::logic::StateFormula const& stateFormula, CheckSettings const& checkSettings) { if (stateFormula.isBinaryBooleanStateFormula()) { - return this->checkBinaryBooleanStateFormula(stateFormula.asBinaryBooleanStateFormula()); + return this->checkBinaryBooleanStateFormula(stateFormula.asBinaryBooleanStateFormula(), checkSettings); } else if (stateFormula.isUnaryBooleanStateFormula()) { - return this->checkUnaryBooleanStateFormula(stateFormula.asUnaryBooleanStateFormula()); + return this->checkUnaryBooleanStateFormula(stateFormula.asUnaryBooleanStateFormula(), checkSettings); } else if (stateFormula.isBooleanLiteralFormula()) { - return this->checkBooleanLiteralFormula(stateFormula.asBooleanLiteralFormula()); + return this->checkBooleanLiteralFormula(stateFormula.asBooleanLiteralFormula(), checkSettings); } else if (stateFormula.isProbabilityOperatorFormula()) { - return this->checkProbabilityOperatorFormula(stateFormula.asProbabilityOperatorFormula()); + return this->checkProbabilityOperatorFormula(stateFormula.asProbabilityOperatorFormula(), checkSettings); } else if (stateFormula.isRewardOperatorFormula()) { - return this->checkRewardOperatorFormula(stateFormula.asRewardOperatorFormula()); + return this->checkRewardOperatorFormula(stateFormula.asRewardOperatorFormula(), checkSettings); } else if (stateFormula.isExpectedTimeOperatorFormula()) { - return this->checkExpectedTimeOperatorFormula(stateFormula.asExpectedTimeOperatorFormula()); + return this->checkExpectedTimeOperatorFormula(stateFormula.asExpectedTimeOperatorFormula(), checkSettings); } else if (stateFormula.isLongRunAverageOperatorFormula()) { - return this->checkLongRunAverageOperatorFormula(stateFormula.asLongRunAverageOperatorFormula()); + return this->checkLongRunAverageOperatorFormula(stateFormula.asLongRunAverageOperatorFormula(), checkSettings); } else if (stateFormula.isAtomicExpressionFormula()) { - return this->checkAtomicExpressionFormula(stateFormula.asAtomicExpressionFormula()); + return this->checkAtomicExpressionFormula(stateFormula.asAtomicExpressionFormula(), checkSettings); } else if (stateFormula.isAtomicLabelFormula()) { - return this->checkAtomicLabelFormula(stateFormula.asAtomicLabelFormula()); + return this->checkAtomicLabelFormula(stateFormula.asAtomicLabelFormula(), checkSettings); } else if (stateFormula.isBooleanLiteralFormula()) { - return this->checkBooleanLiteralFormula(stateFormula.asBooleanLiteralFormula()); + return this->checkBooleanLiteralFormula(stateFormula.asBooleanLiteralFormula(), checkSettings); } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid."); } - std::unique_ptr AbstractModelChecker::checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula) { + std::unique_ptr AbstractModelChecker::checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula, CheckSettings const& checkSettings) { std::stringstream stream; stream << stateFormula.getExpression(); - return this->checkAtomicLabelFormula(storm::logic::AtomicLabelFormula(stream.str())); + return this->checkAtomicLabelFormula(storm::logic::AtomicLabelFormula(stream.str()), checkSettings); } - std::unique_ptr AbstractModelChecker::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) { + std::unique_ptr AbstractModelChecker::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula, CheckSettings const& checkSettings) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << stateFormula << "."); } - std::unique_ptr AbstractModelChecker::checkBinaryBooleanStateFormula(storm::logic::BinaryBooleanStateFormula const& stateFormula) { + std::unique_ptr AbstractModelChecker::checkBinaryBooleanStateFormula(storm::logic::BinaryBooleanStateFormula const& stateFormula, CheckSettings const& checkSettings) { 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()); @@ -157,13 +157,15 @@ namespace storm { return leftResult; } - std::unique_ptr AbstractModelChecker::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) { + std::unique_ptr AbstractModelChecker::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula, CheckSettings const& checkSettings) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << stateFormula << "."); } - std::unique_ptr AbstractModelChecker::checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula) { + std::unique_ptr AbstractModelChecker::checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula, CheckSettings const& checkSettings) { 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()) { @@ -193,7 +195,7 @@ namespace storm { } } - std::unique_ptr AbstractModelChecker::checkRewardOperatorFormula(storm::logic::RewardOperatorFormula const& stateFormula) { + std::unique_ptr AbstractModelChecker::checkRewardOperatorFormula(storm::logic::RewardOperatorFormula const& stateFormula, CheckSettings const& checkSettings) { 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. @@ -225,7 +227,7 @@ namespace storm { } } - std::unique_ptr AbstractModelChecker::checkExpectedTimeOperatorFormula(storm::logic::ExpectedTimeOperatorFormula const& stateFormula) { + std::unique_ptr AbstractModelChecker::checkExpectedTimeOperatorFormula(storm::logic::ExpectedTimeOperatorFormula const& stateFormula, CheckSettings const& checkSettings) { 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. @@ -257,7 +259,7 @@ namespace storm { } } - std::unique_ptr AbstractModelChecker::checkLongRunAverageOperatorFormula(storm::logic::LongRunAverageOperatorFormula const& stateFormula) { + std::unique_ptr AbstractModelChecker::checkLongRunAverageOperatorFormula(storm::logic::LongRunAverageOperatorFormula const& stateFormula, CheckSettings const& checkSettings) { STORM_LOG_THROW(stateFormula.getSubformula().isStateFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); std::unique_ptr result; @@ -280,7 +282,7 @@ namespace storm { } } - std::unique_ptr AbstractModelChecker::checkUnaryBooleanStateFormula(storm::logic::UnaryBooleanStateFormula const& stateFormula) { + std::unique_ptr AbstractModelChecker::checkUnaryBooleanStateFormula(storm::logic::UnaryBooleanStateFormula const& stateFormula, CheckSettings const& checkSettings) { std::unique_ptr subResult = this->check(stateFormula.getSubformula()); STORM_LOG_THROW(subResult->isQualitative(), storm::exceptions::InternalTypeErrorException, "Expected qualitative result."); if (stateFormula.isNot()) { diff --git a/src/modelchecker/CheckSettings.cpp b/src/modelchecker/CheckSettings.cpp index 74913b076..b030dcac3 100644 --- a/src/modelchecker/CheckSettings.cpp +++ b/src/modelchecker/CheckSettings.cpp @@ -49,6 +49,9 @@ namespace storm { if (probabilityOperatorFormula.getBound() == storm::utility::zero() || probabilityOperatorFormula.getBound() == storm::utility::one()) { qualitative = true; } + if (!optimizationDirection) { + 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(); @@ -65,6 +68,9 @@ namespace storm { if (rewardOperatorFormula.getBound() == storm::utility::zero()) { qualitative = true; } + if (!optimizationDirection) { + optimizationDirection = rewardOperatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || rewardOperatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize; + } } } return CheckSettings(optimizationDirection, rewardModel, onlyInitialStatesRelevant, initialStatesBound, qualitative, produceStrategies);