From e3c4f5fa729ee61c0835b66f1d88e56081003f93 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 4 Feb 2016 17:02:31 +0100 Subject: [PATCH] more work on customizing checking process Former-commit-id: 93e5895f7717462793a6ba6de07263cc13651255 --- src/builder/ExplicitPrismModelBuilder.cpp | 4 + .../MILPMinimalLabelSetGenerator.h | 2 - src/modelchecker/AbstractModelChecker.cpp | 58 ++++---- src/modelchecker/AbstractModelChecker.h | 52 +++---- src/modelchecker/CheckSettings.cpp | 127 ----------------- src/modelchecker/CheckTask.cpp | 129 ++++++++++++++++++ .../{CheckSettings.h => CheckTask.h} | 51 +++---- 7 files changed, 215 insertions(+), 208 deletions(-) delete mode 100644 src/modelchecker/CheckSettings.cpp create mode 100644 src/modelchecker/CheckTask.cpp rename src/modelchecker/{CheckSettings.h => CheckTask.h} (73%) diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index ed0f43d3b..9e5474061 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -264,6 +264,10 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The program contains undefined constants that appear in some places other than update probabilities and reward value expressions, which is not admitted."); #endif } + + if (!std::is_same::value) { + doMagic(iasdfasdpfoy); + } // If the set of labels we are supposed to built is restricted, we need to remove the other labels from the program. if (options.labelsToBuild) { diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index bc5be2111..17825b23d 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -957,8 +957,6 @@ namespace storm { // (4.2) Construct constraint system. buildConstraintSystem(*solver, labeledMdp, psiStates, stateInformation, choiceInformation, variableInformation, probabilityThreshold, strictBound, includeSchedulerCuts); - solver->writeModelToFile("model.lp"); - // (4.3) Optimize the model. solver->optimize(); diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index e5e272d23..2487949b6 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -11,20 +11,20 @@ namespace storm { namespace modelchecker { - std::unique_ptr AbstractModelChecker::check(storm::logic::Formula const& formula, boost::optional> const& checkSettings) { + std::unique_ptr AbstractModelChecker::check(storm::logic::Formula const& formula, boost::optional> checkSettings) { STORM_LOG_THROW(this->canHandle(formula), storm::exceptions::InvalidArgumentException, "The model checker is not able to check the formula '" << formula << "'."); - CheckSettings settingsToUse = checkSettings ? checkSettings.get() : CheckSettings::fromToplevelFormula(formula); + CheckSettings newCheckSettings = checkSettings ? checkSettings.get() : CheckSettings::fromNestedFormula(formula); if (formula.isStateFormula()) { - return this->checkStateFormula(formula.asStateFormula(), settingsToUse); + return this->checkStateFormula(formula.asStateFormula(), newCheckSettings); } else if (formula.isPathFormula()) { - return this->computeProbabilities(formula.asPathFormula(), settingsToUse); + return this->computeProbabilities(formula.asPathFormula(), newCheckSettings); } else if (formula.isRewardPathFormula()) { - return this->computeRewards(formula.asRewardPathFormula(), settingsToUse); + return this->computeRewards(formula.asRewardPathFormula(), newCheckSettings); } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid."); } - std::unique_ptr AbstractModelChecker::computeProbabilities(storm::logic::PathFormula const& pathFormula, CheckSettings const& checkSettings) { + std::unique_ptr AbstractModelChecker::computeProbabilities(storm::logic::PathFormula const& pathFormula, boost::optional> checkSettings) { if (pathFormula.isBoundedUntilFormula()) { return this->computeBoundedUntilProbabilities(pathFormula.asBoundedUntilFormula(), checkSettings); } else if (pathFormula.isConditionalPathFormula()) { @@ -41,32 +41,32 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << pathFormula << "' is invalid."); } - std::unique_ptr AbstractModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, CheckSettings const& checkSettings) { + 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::computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, CheckSettings const& checkSettings) { + 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::computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, CheckSettings const& checkSettings) { + std::unique_ptr AbstractModelChecker::computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, boost::optional> checkSettings) { storm::logic::UntilFormula newFormula(storm::logic::Formula::getTrueFormula(), pathFormula.getSubformula().asSharedPointer()); return this->computeUntilProbabilities(newFormula, checkSettings); } - std::unique_ptr AbstractModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, CheckSettings const& checkSettings) { + 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::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, CheckSettings const& checkSettings) { + 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::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, CheckSettings const& checkSettings) { + 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::computeRewards(storm::logic::RewardPathFormula const& rewardPathFormula, CheckSettings const& checkSettings) { + std::unique_ptr AbstractModelChecker::computeRewards(storm::logic::RewardPathFormula const& rewardPathFormula, boost::optional> checkSettings) { if (rewardPathFormula.isCumulativeRewardFormula()) { return this->computeCumulativeRewards(rewardPathFormula.asCumulativeRewardFormula(), checkSettings); } else if (rewardPathFormula.isInstantaneousRewardFormula()) { @@ -79,31 +79,31 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardPathFormula << "' is invalid."); } - std::unique_ptr AbstractModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, CheckSettings const& checkSettings) { + 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::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, CheckSettings const& checkSettings) { + 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::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, CheckSettings const& checkSettings) { + 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::computeLongRunAverageRewards(storm::logic::LongRunAverageRewardFormula const& rewardPathFormula, CheckSettings const& checkSettings) { + 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::computeLongRunAverageProbabilities(storm::logic::StateFormula const& eventuallyFormula, CheckSettings const& checkSettings) { + 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::computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, CheckSettings const& checkSettings) { + 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::checkStateFormula(storm::logic::StateFormula const& stateFormula, CheckSettings const& checkSettings) { + std::unique_ptr AbstractModelChecker::checkStateFormula(storm::logic::StateFormula const& stateFormula, boost::optional> checkSettings) { if (stateFormula.isBinaryBooleanStateFormula()) { return this->checkBinaryBooleanStateFormula(stateFormula.asBinaryBooleanStateFormula(), checkSettings); } else if (stateFormula.isUnaryBooleanStateFormula()) { @@ -128,17 +128,17 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid."); } - std::unique_ptr AbstractModelChecker::checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula, CheckSettings const& checkSettings) { + std::unique_ptr AbstractModelChecker::checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula, boost::optional> checkSettings) { std::stringstream stream; stream << stateFormula.getExpression(); return this->checkAtomicLabelFormula(storm::logic::AtomicLabelFormula(stream.str()), checkSettings); } - std::unique_ptr AbstractModelChecker::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula, CheckSettings const& checkSettings) { + 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::checkBinaryBooleanStateFormula(storm::logic::BinaryBooleanStateFormula const& stateFormula, CheckSettings const& checkSettings) { + std::unique_ptr AbstractModelChecker::checkBinaryBooleanStateFormula(storm::logic::BinaryBooleanStateFormula const& stateFormula, boost::optional> 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,11 +157,11 @@ namespace storm { return leftResult; } - std::unique_ptr AbstractModelChecker::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula, CheckSettings const& checkSettings) { + 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::checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula, CheckSettings const& checkSettings) { + std::unique_ptr AbstractModelChecker::checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula, boost::optional> checkSettings) { STORM_LOG_THROW(stateFormula.getSubformula().isPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); CheckSettings newCheckSettings = @@ -195,7 +195,7 @@ namespace storm { } } - std::unique_ptr AbstractModelChecker::checkRewardOperatorFormula(storm::logic::RewardOperatorFormula const& stateFormula, CheckSettings const& checkSettings) { + std::unique_ptr AbstractModelChecker::checkRewardOperatorFormula(storm::logic::RewardOperatorFormula const& stateFormula, boost::optional> 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. @@ -227,7 +227,7 @@ namespace storm { } } - std::unique_ptr AbstractModelChecker::checkExpectedTimeOperatorFormula(storm::logic::ExpectedTimeOperatorFormula const& stateFormula, CheckSettings const& checkSettings) { + std::unique_ptr AbstractModelChecker::checkExpectedTimeOperatorFormula(storm::logic::ExpectedTimeOperatorFormula const& stateFormula, boost::optional> 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. @@ -259,7 +259,7 @@ namespace storm { } } - std::unique_ptr AbstractModelChecker::checkLongRunAverageOperatorFormula(storm::logic::LongRunAverageOperatorFormula const& stateFormula, CheckSettings const& checkSettings) { + std::unique_ptr AbstractModelChecker::checkLongRunAverageOperatorFormula(storm::logic::LongRunAverageOperatorFormula const& stateFormula, boost::optional> checkSettings) { STORM_LOG_THROW(stateFormula.getSubformula().isStateFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); std::unique_ptr result; @@ -282,7 +282,7 @@ namespace storm { } } - std::unique_ptr AbstractModelChecker::checkUnaryBooleanStateFormula(storm::logic::UnaryBooleanStateFormula const& stateFormula, CheckSettings const& checkSettings) { + std::unique_ptr AbstractModelChecker::checkUnaryBooleanStateFormula(storm::logic::UnaryBooleanStateFormula const& stateFormula, boost::optional> 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/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h index 8adb9adcc..7acbac752 100644 --- a/src/modelchecker/AbstractModelChecker.h +++ b/src/modelchecker/AbstractModelChecker.h @@ -3,7 +3,7 @@ #include -#include "src/modelchecker/CheckSettings.h" +#include "src/modelchecker/CheckTask.h" #include "src/logic/Formulas.h" #include "src/solver/OptimizationDirection.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(storm::logic::Formula const& formula, boost::optional> const& checkSettings = boost::none); + virtual std::unique_ptr check(CheckTask<> storm::logic::Formula const& formula, boost::optional> checkSettings = boost::none); // The methods to compute probabilities for path formulas. - virtual std::unique_ptr computeProbabilities(storm::logic::PathFormula const& pathFormula, CheckSettings const& checkSettings); - virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, CheckSettings const& checkSettings); - virtual std::unique_ptr computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, CheckSettings const& checkSettings); - virtual std::unique_ptr computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, CheckSettings const& checkSettings); - virtual std::unique_ptr computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, CheckSettings const& checkSettings); - virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, CheckSettings const& checkSettings); - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, CheckSettings const& checkSettings); + 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); // The methods to compute the rewards for path formulas. - virtual std::unique_ptr computeRewards(storm::logic::RewardPathFormula const& rewardPathFormula, CheckSettings const& checkSettings); - virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, CheckSettings const& checkSettings); - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, CheckSettings const& checkSettings); - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, CheckSettings const& checkSettings); - virtual std::unique_ptr computeLongRunAverageRewards(storm::logic::LongRunAverageRewardFormula const& rewardPathFormula, CheckSettings const& checkSettings); + 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); // The methods to compute the long-run average and expected time. - virtual std::unique_ptr computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, CheckSettings const& checkSettings); - virtual std::unique_ptr computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, CheckSettings const& checkSettings); + 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); // The methods to check state formulas. - virtual std::unique_ptr checkStateFormula(storm::logic::StateFormula const& stateFormula, CheckSettings const& checkSettings); - virtual std::unique_ptr checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula, CheckSettings const& checkSettings); - virtual std::unique_ptr checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula, CheckSettings const& checkSettings); - virtual std::unique_ptr checkBinaryBooleanStateFormula(storm::logic::BinaryBooleanStateFormula const& stateFormula, CheckSettings const& checkSettings); - virtual std::unique_ptr checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula, CheckSettings const& checkSettings); - virtual std::unique_ptr checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula, CheckSettings const& checkSettings); - virtual std::unique_ptr checkRewardOperatorFormula(storm::logic::RewardOperatorFormula const& stateFormula, CheckSettings const& checkSettings); - virtual std::unique_ptr checkExpectedTimeOperatorFormula(storm::logic::ExpectedTimeOperatorFormula const& stateFormula, CheckSettings const& checkSettings); - virtual std::unique_ptr checkLongRunAverageOperatorFormula(storm::logic::LongRunAverageOperatorFormula const& stateFormula, CheckSettings const& checkSettings); - virtual std::unique_ptr checkUnaryBooleanStateFormula(storm::logic::UnaryBooleanStateFormula const& stateFormula, CheckSettings const& checkSettings); + 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); }; } } diff --git a/src/modelchecker/CheckSettings.cpp b/src/modelchecker/CheckSettings.cpp deleted file mode 100644 index b030dcac3..000000000 --- a/src/modelchecker/CheckSettings.cpp +++ /dev/null @@ -1,127 +0,0 @@ -#include "src/modelchecker/CheckSettings.h" - -#include "src/logic/Formulas.h" - -#include "src/utility/constants.h" - -namespace storm { - namespace modelchecker { - - template - CheckSettings::CheckSettings() : CheckSettings(boost::none, boost::none, false, boost::none, false, false) { - // Intentionally left empty. - } - - template - CheckSettings::CheckSettings(boost::optional const& optimizationDirection, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional> const& initialStatesBound, bool qualitative, bool produceStrategies) : optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), initialStatesBound(initialStatesBound), qualitative(qualitative), produceStrategies(produceStrategies) { - // Intentionally left empty. - } - - template - CheckSettings CheckSettings::fromToplevelFormula(storm::logic::Formula const& formula) { - return fromFormula(formula, true); - } - - template - CheckSettings CheckSettings::fromNestedFormula(storm::logic::Formula const& formula) { - return fromFormula(formula, false); - } - - template - CheckSettings CheckSettings::fromFormula(storm::logic::Formula const& formula, bool toplevel) { - boost::optional optimizationDirection; - boost::optional rewardModel; - boost::optional> initialStatesBound; - bool qualitative = false; - bool onlyInitialStatesRelevant = !toplevel; - bool produceStrategies = false; - - if (formula.isProbabilityOperatorFormula()) { - storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula(); - if (probabilityOperatorFormula.hasOptimalityType()) { - optimizationDirection = probabilityOperatorFormula.getOptimalityType(); - } - - if (probabilityOperatorFormula.hasBound()) { - if (onlyInitialStatesRelevant) { - initialStatesBound = std::make_pair(probabilityOperatorFormula.getComparisonType(), static_cast(probabilityOperatorFormula.getBound())); - } - 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(); - rewardModel = rewardOperatorFormula.getOptionalRewardModelName(); - - if (rewardOperatorFormula.hasOptimalityType()) { - optimizationDirection = rewardOperatorFormula.getOptimalityType(); - } - - if (rewardOperatorFormula.hasBound()) { - if (onlyInitialStatesRelevant) { - initialStatesBound = std::make_pair(rewardOperatorFormula.getComparisonType(), static_cast(rewardOperatorFormula.getBound())); - } - 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); - } - - template - bool CheckSettings::isOptimizationDirectionSet() const { - return static_cast(optimizationDirection); - } - - template - storm::OptimizationDirection const& CheckSettings::getOptimizationDirection() const { - return optimizationDirection.get(); - } - - template - bool CheckSettings::isRewardModelSet() const { - return static_cast(rewardModel); - } - - template - std::string const& CheckSettings::getRewardModel() const { - return rewardModel.get(); - } - - template - bool CheckSettings::isOnlyInitialStatesRelevantSet() const { - return onlyInitialStatesRelevant; - } - - template - bool CheckSettings::isInitialStatesBoundSet() const { - return static_cast(initialStatesBound); - } - - template - std::pair const& CheckSettings::getInitialStatesBound() const { - return initialStatesBound.get(); - } - - template - bool CheckSettings::isQualitativeSet() const { - return qualitative; - } - - template - bool CheckSettings::isProduceStrategiesSet() const { - return produceStrategies; - } - - template class CheckSettings; - - } -} \ No newline at end of file diff --git a/src/modelchecker/CheckTask.cpp b/src/modelchecker/CheckTask.cpp new file mode 100644 index 000000000..d88939823 --- /dev/null +++ b/src/modelchecker/CheckTask.cpp @@ -0,0 +1,129 @@ +#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/CheckSettings.h b/src/modelchecker/CheckTask.h similarity index 73% rename from src/modelchecker/CheckSettings.h rename to src/modelchecker/CheckTask.h index 2703cc119..f41ee6e40 100644 --- a/src/modelchecker/CheckSettings.h +++ b/src/modelchecker/CheckTask.h @@ -1,5 +1,5 @@ -#ifndef STORM_MODELCHECKER_CHECKSETTINGS_H_ -#define STORM_MODELCHECKER_CHECKSETTINGS_H_ +#ifndef STORM_MODELCHECKER_CHECKTASK_H_ +#define STORM_MODELCHECKER_CHECKTASK_H_ #include @@ -16,27 +16,34 @@ namespace storm { /* * This class is used to customize the checking process of a formula. */ - template - class CheckSettings { + template + class CheckTask { public: /*! - * Creates a settings object with the default options. + * Creates an empty task object with the default options. */ - CheckSettings(); + CheckTask(); /*! - * Creates a settings object for the given top-level formula. - * - * @param formula The formula for which to create the settings. + * Creates a task object with the default options for the given formula. */ - static CheckSettings fromToplevelFormula(storm::logic::Formula const& formula); + CheckTask(FormulaType const& formula); /*! - * Creates a settings object for the given formula that is nested within another formula. - * - * @param formula The formula for which to create the settings. + * Converts the check task object to one with the given new formula type. + */ + template + CheckTask convert(); + + /*! + * Retrieves whether this task is associated with a formula. */ - static CheckSettings fromNestedFormula(storm::logic::Formula const& formula); + bool hasFormula() const; + + /*! + * Retrieves the formula from this task. + */ + FormulaType const& getFormula() const; /*! * Retrieves whether an optimization direction was set. @@ -86,8 +93,9 @@ namespace storm { private: /*! - * Creates a settings object with the given options. + * Creates a task object with the given options. * + * @param formula The formula to attach to the task. * @param optimizationDirection If set, the probabilities will be minimized/maximized. * @param rewardModelName If given, the checking has to be done wrt. to this reward model. * @param onlyInitialStatesRelevant If set to true, the model checker may decide to only compute the values @@ -99,15 +107,10 @@ 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. */ - CheckSettings(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& initialStatesBound, bool qualitative, bool produceStrategies); - /*! - * Creates a settings object for the given formula. - * - * @param formula The formula for which to create the settings. - * @param toplevel Indicates whether this formula is the top-level formula. - */ - static CheckSettings fromFormula(storm::logic::Formula const& formula, bool toplevel); + // The formula that is to be checked. + boost::optional> formula; // If set, the probabilities will be minimized/maximized. boost::optional optimizationDirection; @@ -132,4 +135,4 @@ namespace storm { } } -#endif /* STORM_MODELCHECKER_CHECKSETTINGS_H_ */ \ No newline at end of file +#endif /* STORM_MODELCHECKER_CHECKTASK_H_ */ \ No newline at end of file